(* Title: JinjaThreads/J/SmallTypeSafe.thy Author: Tobias Nipkow, Andreas Lochbihler *) section ‹Type Safety Proof› theory TypeSafe imports Progress DefAssPreservation begin subsection‹Basic preservation lemmas› text‹First two easy preservation lemmas.› theorem (in J_conf_read) shows red_preserves_hconf: "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; P,E,hp s ⊢ e : T; hconf (hp s) ⟧ ⟹ hconf (hp s')" and reds_preserves_hconf: "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es [:] Ts; hconf (hp s) ⟧ ⟹ hconf (hp s')" proof (induct arbitrary: T E and Ts E rule: red_reds.inducts) case RedNew thus ?case by(auto intro: hconf_heap_ops_mono) next case RedNewFail thus ?case by(auto intro: hconf_heap_ops_mono) next case RedNewArray thus ?case by(auto intro: hconf_heap_ops_mono) next case RedNewArrayFail thus ?case by(auto intro: hconf_heap_ops_mono) next case (RedAAss h a U n i v U' h' l) from ‹sint i < int n› ‹0 <=s i› have "nat (sint i) < n" by (simp add: word_sle_eq nat_less_iff) thus ?case using RedAAss by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def) next case RedFAss thus ?case by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def) next case RedCASSucceed thus ?case by(fastforce elim: hconf_heap_write_mono intro: addr_loc_type.intros simp add: conf_def) next case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s') hence "P,hp s ⊢ a∙M(vs) : T" by(fastforce simp add: external_WT'_iff dest: sees_method_fun) with RedCallExternal show ?case by(auto dest: external_call_hconf) qed auto theorem (in J_heap) red_preserves_lconf: "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; P,E,hp s ⊢ e:T; P,hp s ⊢ lcl s (:≤) E ⟧ ⟹ P,hp s' ⊢ lcl s' (:≤) E" and reds_preserves_lconf: "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es[:]Ts; P,hp s ⊢ lcl s (:≤) E ⟧ ⟹ P,hp s' ⊢ lcl s' (:≤) E" proof(induct arbitrary: T E and Ts E rule:red_reds.inducts) case RedNew thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedNewFail thus ?case by(auto intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedNewArray thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedNewArrayFail thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedLAss thus ?case by(fastforce elim: lconf_upd simp add: conf_def simp del: fun_upd_apply ) next case RedAAss thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedFAss thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case RedCASSucceed thus ?case by(fastforce intro:lconf_hext hext_heap_ops simp del: fun_upd_apply) next case (BlockRed e h x V vo ta e' h' x' T T' E) note red = ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩› note IH = ‹⋀T E. ⟦P,E,hp (h, x(V := vo)) ⊢ e : T; P,hp (h, x(V := vo)) ⊢ lcl (h, x(V := vo)) (:≤) E⟧ ⟹ P,hp (h', x') ⊢ lcl (h', x') (:≤) E› note wt = ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'› note lconf = ‹P,hp (h, x) ⊢ lcl (h, x) (:≤) E› from lconf_hext[OF lconf[simplified] red_hext_incr[OF red, simplified]] have "P,h' ⊢ x (:≤) E" . moreover from wt have "P,E(V↦T),h ⊢ e : T'" by(cases vo, auto) moreover from lconf wt have "P,h ⊢ x(V := vo) (:≤) E(V ↦ T)" by(cases vo)(simp add: lconf_def,auto intro: lconf_upd2 simp add: conf_def) ultimately have "P,h' ⊢ x' (:≤) E(V↦T)" by(auto intro: IH[simplified]) with ‹P,h' ⊢ x (:≤) E› show ?case by(auto simp add: lconf_def split: if_split_asm) next case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s') from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› have "hp s ⊴ h'" by(rule red_external_hext) with ‹s' = (h', lcl s)› ‹P,hp s ⊢ lcl s (:≤) E› show ?case by(auto intro: lconf_hext) qed auto text‹Combining conformance of heap and local variables:› definition (in J_heap_conf_base) sconf :: "env ⇒ ('addr, 'heap) Jstate ⇒ bool" ("_ ⊢ _ √" [51,51]50) where "E ⊢ s √ ≡ let (h,l) = s in hconf h ∧ P,h ⊢ l (:≤) E ∧ preallocated h" context J_conf_read begin lemma red_preserves_sconf: "⟦ extTA,P,t ⊢ ⟨e,s⟩ -tas→ ⟨e',s'⟩; P,E,hp s ⊢ e : T; E ⊢ s √ ⟧ ⟹ E ⊢ s' √" apply(auto dest: red_preserves_hconf red_preserves_lconf simp add:sconf_def) apply(fastforce dest: red_hext_incr intro: preallocated_hext) done lemma reds_preserves_sconf: "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; P,E,hp s ⊢ es [:] Ts; E ⊢ s √ ⟧ ⟹ E ⊢ s' √" apply(auto dest: reds_preserves_hconf reds_preserves_lconf simp add: sconf_def) apply(fastforce dest: reds_hext_incr intro: preallocated_hext) done end lemma (in J_heap_base) wt_external_call: "⟦ conf_extRet P h va T; P,E,h ⊢ e : T ⟧ ⟹ ∃T'. P,E,h ⊢ extRet2J e va : T' ∧ P ⊢ T' ≤ T" by(cases va)(auto simp add: conf_def) subsection "Subject reduction" theorem (in J_conf_read) assumes wf: "wf_J_prog P" shows subject_reduction: "⟦ extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩; E ⊢ s √; P,E,hp s ⊢ e:T; P,hp s ⊢ t √t ⟧ ⟹ ∃T'. P,E,hp s' ⊢ e':T' ∧ P ⊢ T' ≤ T" and subjects_reduction: "⟦ extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩; E ⊢ s √; P,E,hp s ⊢ es[:]Ts; P,hp s ⊢ t √t ⟧ ⟹ ∃Ts'. P,E,hp s' ⊢ es'[:]Ts' ∧ P ⊢ Ts' [≤] Ts" proof (induct arbitrary: T E and Ts E rule:red_reds.inducts) case RedNew thus ?case by(auto dest: allocate_SomeD) next case RedNewFail thus ?case unfolding sconf_def by(fastforce intro:typeof_OutOfMemory preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf]) next case NewArrayRed thus ?case by fastforce next case RedNewArray thus ?case by(auto dest: allocate_SomeD) next case RedNewArrayNegative thus ?case unfolding sconf_def by(fastforce intro: preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedNewArrayFail thus ?case unfolding sconf_def by(fastforce intro:typeof_OutOfMemory preallocated_heap_ops simp add: xcpt_subcls_Throwable[OF _ wf]) next case (CastRed e s ta e' s' C T E) have esse: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" and IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" and hconf: "E ⊢ s √" and wtc: "P,E,hp s ⊢ Cast C e : T" by fact+ thus ?case proof(clarsimp) fix T' assume wte: "P,E,hp s ⊢ e : T'" "is_type P C" from wte and hconf and IH and ‹P,hp s ⊢ t √t› have "∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T'" by simp then obtain U where wtee: "P,E,hp s' ⊢ e' : U" and UsTT: "P ⊢ U ≤ T'" by blast from wtee ‹is_type P C› have "P,E,hp s' ⊢ Cast C e' : C" by(rule WTrtCast) thus "∃T'. P,E,hp s' ⊢ Cast C e' : T' ∧ P ⊢ T' ≤ C" by blast qed next case RedCast thus ?case by(clarsimp simp add: is_refT_def) next case RedCastFail thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (InstanceOfRed e s ta e' s' U T E) have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" and hconf: "E ⊢ s √" and wtc: "P,E,hp s ⊢ e instanceof U : T" and tconf: "P,hp s ⊢ t √t" by fact+ from wtc obtain T' where "P,E,hp s ⊢ e : T'" by auto from IH[OF hconf this tconf] obtain T'' where "P,E,hp s' ⊢ e' : T''" by auto with wtc show ?case by auto next case RedInstanceOf thus ?case by(clarsimp) next case (BinOpRed1 e⇩_{1}s ta e⇩_{1}' s' bop e⇩_{2}T E) have red: "extTA,P,t ⊢ ⟨e⇩_{1}, s⟩ -ta→ ⟨e⇩_{1}', s'⟩" and IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩_{1}:T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e⇩_{1}' : U ∧ P ⊢ U ≤ T" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e⇩_{1}«bop» e⇩_{2}: T" and tconf: "P,hp s ⊢ t √t" by fact+ from wt obtain T1 T2 where wt1: "P,E,hp s ⊢ e⇩_{1}: T1" and wt2: "P,E,hp s ⊢ e⇩_{2}: T2" and wtbop: "P ⊢ T1«bop»T2 : T" by auto from IH[OF conf wt1 tconf] obtain T1' where wt1': "P,E,hp s' ⊢ e⇩_{1}' : T1'" and sub: "P ⊢ T1' ≤ T1" by blast from WTrt_binop_widen_mono[OF wtbop sub widen_refl] obtain T' where wtbop': "P ⊢ T1'«bop»T2 : T'" and sub': "P ⊢ T' ≤ T" by blast from wt1' WTrt_hext_mono[OF wt2 red_hext_incr[OF red]] wtbop' have "P,E,hp s' ⊢ e⇩_{1}' «bop» e⇩_{2}: T'" by(rule WTrtBinOp) with sub' show ?case by blast next case (BinOpRed2 e⇩_{2}s ta e⇩_{2}' s' v⇩_{1}bop T E) have red: "extTA,P,t ⊢ ⟨e⇩_{2},s⟩ -ta→ ⟨e⇩_{2}',s'⟩" by fact have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩_{2}:T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e⇩_{2}' : U ∧ P ⊢ U ≤ T" and tconf: "P,hp s ⊢ t √t" by fact+ have conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ (Val v⇩_{1}) «bop» e⇩_{2}: T" by fact+ from wt obtain T1 T2 where wt1: "P,E,hp s ⊢ Val v⇩_{1}: T1" and wt2: "P,E,hp s ⊢ e⇩_{2}: T2" and wtbop: "P ⊢ T1«bop»T2 : T" by auto from IH[OF conf wt2 tconf] obtain T2' where wt2': "P,E,hp s' ⊢ e⇩_{2}' : T2'" and sub: "P ⊢ T2' ≤ T2" by blast from WTrt_binop_widen_mono[OF wtbop widen_refl sub] obtain T' where wtbop': "P ⊢ T1«bop»T2' : T'" and sub': "P ⊢ T' ≤ T" by blast from WTrt_hext_mono[OF wt1 red_hext_incr[OF red]] wt2' wtbop' have "P,E,hp s' ⊢ Val v⇩_{1}«bop» e⇩_{2}' : T'" by(rule WTrtBinOp) with sub' show ?case by blast next case (RedBinOp bop v1 v2 v s) from ‹E ⊢ s √› have preh: "preallocated (hp s)" by(cases s)(simp add: sconf_def) from ‹P,E,hp s ⊢ Val v1 «bop» Val v2 : T› obtain T1 T2 where "typeof⇘hp s⇙ v1 = ⌊T1⌋" "typeof⇘hp s⇙ v2 = ⌊T2⌋" "P ⊢ T1«bop»T2 : T" by auto with wf preh have "P,hp s ⊢ v :≤ T" using ‹binop bop v1 v2 = ⌊Inl v⌋› by(rule binop_type) thus ?case by(auto simp add: conf_def) next case (RedBinOpFail bop v1 v2 a s) from ‹E ⊢ s √› have preh: "preallocated (hp s)" by(cases s)(simp add: sconf_def) from ‹P,E,hp s ⊢ Val v1 «bop» Val v2 : T› obtain T1 T2 where "typeof⇘hp s⇙ v1 = ⌊T1⌋" "typeof⇘hp s⇙ v2 = ⌊T2⌋" "P ⊢ T1«bop»T2 : T" by auto with wf preh have "P,hp s ⊢ Addr a :≤ Class Throwable" using ‹binop bop v1 v2 = ⌊Inr a⌋› by(rule binop_type) thus ?case by(auto simp add: conf_def) next case RedVar thus ?case by (fastforce simp:sconf_def lconf_def conf_def) next case LAssRed thus ?case by(blast intro:widen_trans) next case RedLAss thus ?case by fastforce next case (AAccRed1 a s ta a' s' i T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ a : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ a' : T' ∧ P ⊢ T' ≤ T" and assa: "extTA,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩" and wt: "P,E,hp s ⊢ a⌊i⌉ : T" and hconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have wti: "P,E,hp s ⊢ i : Integer" by auto from wti red_hext_incr[OF assa] have wti': "P,E,hp s' ⊢ i : Integer" by - (rule WTrt_hext_mono) { assume wta: "P,E,hp s ⊢ a : T⌊⌉" from IH[OF hconf wta tconf] obtain U where wta': "P,E,hp s' ⊢ a' : U" and UsubT: "P ⊢ U ≤ T⌊⌉" by fastforce with wta' wti' have ?case by(cases U, auto simp add: widen_Array) } moreover { assume wta: "P,E,hp s ⊢ a : NT" from IH[OF hconf wta tconf] have "P,E,hp s' ⊢ a' : NT" by fastforce from this wti' have ?case by(fastforce intro:WTrtAAccNT) } ultimately show ?case using wt by auto next case (AAccRed2 i s ta i' s' a T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ i : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ i' : T' ∧ P ⊢ T' ≤ T" and issi: "extTA,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩" and wt: "P,E,hp s ⊢ Val a⌊i⌉ : T" and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have wti: "P,E,hp s ⊢ i : Integer" by auto from wti IH sconf tconf have wti': "P,E,hp s' ⊢ i' : Integer" by blast from wt show ?case proof (rule WTrt_elim_cases) assume wta: "P,E,hp s ⊢ Val a : T⌊⌉" from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : T⌊⌉" by (rule WTrt_hext_mono) from wta' wti' show ?case by(fastforce) next assume wta: "P,E,hp s ⊢ Val a : NT" from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by (rule WTrt_hext_mono) from wta' wti' show ?case by(fastforce elim:WTrtAAccNT) qed next case RedAAccNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedAAccBounds thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (RedAAcc h a T n i v l T' E) from ‹E ⊢ (h, l) √› have "hconf h" by(clarsimp simp add: sconf_def) from ‹0 <=s i› ‹sint i < int n› have "nat (sint i) < n" by (simp add: word_sle_eq nat_less_iff) with ‹typeof_addr h a = ⌊Array_type T n⌋› have "P,h ⊢ a@ACell (nat (sint i)) : T" by(auto intro: addr_loc_type.intros) from heap_read_conf[OF ‹heap_read h a (ACell (nat (sint i))) v› this] ‹hconf h› have "P,h ⊢ v :≤ T" by simp thus ?case using RedAAcc by(auto simp add: conf_def) next case (AAssRed1 a s ta a' s' i e T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ a : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ a' : T' ∧ P ⊢ T' ≤ T" and assa: "extTA,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩" and wt: "P,E,hp s ⊢ a⌊i⌉ := e : T" and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have void: "T = Void" by blast from wt have wti: "P,E,hp s ⊢ i : Integer" by auto from wti red_hext_incr[OF assa] have wti': "P,E,hp s' ⊢ i : Integer" by - (rule WTrt_hext_mono) { assume wta: "P,E,hp s ⊢ a : NT" from IH[OF sconf wta tconf] have wta': "P,E,hp s' ⊢ a' : NT" by fastforce from wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by(auto) from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono) from wta' wti' wte' void have ?case by(fastforce elim: WTrtAAssNT) } moreover { fix U assume wta: "P,E,hp s ⊢ a : U⌊⌉" from IH[OF sconf wta tconf] obtain U' where wta': "P,E,hp s' ⊢ a' : U'" and UsubT: "P ⊢ U' ≤ U⌊⌉" by fastforce with wta' have ?case proof(cases U') case NT assume UNT: "U' = NT" from UNT wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by(auto) from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono) from wta' UNT wti' wte' void show ?thesis by(fastforce elim: WTrtAAssNT) next case (Array A) have UA: "U' = A⌊⌉" by fact with UA UsubT wt wta obtain V where wte: "P,E,hp s ⊢ e : V" by auto from wte red_hext_incr[OF assa] have wte': "P,E,hp s' ⊢ e : V" by - (rule WTrt_hext_mono) with wta' wte' UA wti' void show ?thesis by (fast elim:WTrtAAss) qed(simp_all add: widen_Array) } ultimately show ?case using wt by blast next case (AAssRed2 i s ta i' s' a e T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ i : T; P,hp s ⊢ t √t ⟧ ⟹ ∃T'. P,E,hp s' ⊢ i' : T' ∧ P ⊢ T' ≤ T" and issi: "extTA,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩" and wt: "P,E,hp s ⊢ Val a⌊i⌉ := e : T" and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have void: "T = Void" by blast from wt have wti: "P,E,hp s ⊢ i : Integer" by auto from IH[OF sconf wti tconf] have wti': "P,E,hp s' ⊢ i' : Integer" by fastforce from wt show ?case proof(rule WTrt_elim_cases) fix U T' assume wta: "P,E,hp s ⊢ Val a : U⌊⌉" and wte: "P,E,hp s ⊢ e : T'" from wte red_hext_incr[OF issi] have wte': "P,E,hp s' ⊢ e : T'" by - (rule WTrt_hext_mono) from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : U⌊⌉" by - (rule WTrt_hext_mono) from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss) next fix T' assume wta: "P,E,hp s ⊢ Val a : NT" and wte: "P,E,hp s ⊢ e : T'" from wte red_hext_incr[OF issi] have wte': "P,E,hp s' ⊢ e : T'" by - (rule WTrt_hext_mono) from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by - (rule WTrt_hext_mono) from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss) qed next case (AAssRed3 e s ta e' s' a i T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" and issi: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" and wt: "P,E,hp s ⊢ Val a⌊Val i⌉ := e : T" and sconf: "E ⊢ s √" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have void: "T = Void" by blast from wt have wti: "P,E,hp s ⊢ Val i : Integer" by auto from wti red_hext_incr[OF issi] have wti': "P,E,hp s' ⊢ Val i : Integer" by - (rule WTrt_hext_mono) from wt show ?case proof(rule WTrt_elim_cases) fix U T' assume wta: "P,E,hp s ⊢ Val a : U⌊⌉" and wte: "P,E,hp s ⊢ e : T'" from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : U⌊⌉" by - (rule WTrt_hext_mono) from IH[OF sconf wte tconf] obtain V where wte': "P,E,hp s' ⊢ e' : V" by fastforce from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss) next fix T' assume wta: "P,E,hp s ⊢ Val a : NT" and wte: "P,E,hp s ⊢ e : T'" from wta red_hext_incr[OF issi] have wta': "P,E,hp s' ⊢ Val a : NT" by - (rule WTrt_hext_mono) from IH[OF sconf wte tconf] obtain V where wte': "P,E,hp s' ⊢ e' : V" by fastforce from wta' wti' wte' void show ?case by (fastforce elim:WTrtAAss) qed next case RedAAssNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedAAssBounds thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedAAssStore thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedAAss thus ?case by(auto simp del:fun_upd_apply) next case (ALengthRed a s ta a' s' T E) note IH = ‹⋀T'. ⟦E ⊢ s √; P,E,hp s ⊢ a : T'; P,hp s ⊢ t √t⟧ ⟹ ∃T''. P,E,hp s' ⊢ a' : T'' ∧ P ⊢ T'' ≤ T'› from ‹P,E,hp s ⊢ a∙length : T› show ?case proof(rule WTrt_elim_cases) fix T' assume [simp]: "T = Integer" and wta: "P,E,hp s ⊢ a : T'⌊⌉" from wta ‹E ⊢ s √› IH ‹P,hp s ⊢ t √t› obtain T'' where wta': "P,E,hp s' ⊢ a' : T''" and sub: "P ⊢ T'' ≤ T'⌊⌉" by blast from sub have "P,E,hp s' ⊢ a'∙length : Integer" unfolding widen_Array proof(rule disjE) assume "T'' = NT" with wta' show ?thesis by(auto) next assume "∃V. T'' = V⌊⌉ ∧ P ⊢ V ≤ T'" then obtain V where "T'' = V⌊⌉" "P ⊢ V ≤ T'" by blast with wta' show ?thesis by -(rule WTrtALength, simp) qed thus ?thesis by(simp) next assume "P,E,hp s ⊢ a : NT" with ‹E ⊢ s √› IH ‹P,hp s ⊢ t √t› obtain T'' where wta': "P,E,hp s' ⊢ a' : T''" and sub: "P ⊢ T'' ≤ NT" by blast from sub have "T'' = NT" by auto with wta' show ?thesis by(auto) qed next case (RedALength h a T n l T' E) from ‹P,E,hp (h, l) ⊢ addr a∙length : T'› ‹typeof_addr h a = ⌊Array_type T n⌋› have [simp]: "T' = Integer" by(auto) thus ?case by(auto) next case RedALengthNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (FAccRed e s ta e' s' F D T E) have IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙F{D} : T" and tconf: "P,hp s ⊢ t √t" by fact+ ― ‹Now distinguish the two cases how wt can have arisen.› { fix T' C fm assume wte: "P,E,hp s ⊢ e : T'" and icto: "class_type_of' T' = ⌊C⌋" and has: "P ⊢ C has F:T (fm) in D" from IH[OF conf wte tconf] obtain U where wte': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'" by auto ― ‹Now distinguish what @{term U} can be.› with UsubC have ?case proof(cases "U = NT") case True thus ?thesis using wte' by(blast intro:WTrtFAccNT widen_refl) next case False with icto UsubC obtain C' where icto': "class_type_of' U = ⌊C'⌋" and C'subC: "P ⊢ C' ≼⇧^{*}C" by(rule widen_is_class_type_of) from has_field_mono[OF has C'subC] wte' icto' show ?thesis by(auto intro!:WTrtFAcc) qed } moreover { assume "P,E,hp s ⊢ e : NT" hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce hence ?case by(fastforce intro:WTrtFAccNT widen_refl) } ultimately show ?case using wt by blast next case RedFAcc thus ?case unfolding sconf_def by(fastforce dest: heap_read_conf intro: addr_loc_type.intros simp add: conf_def) next case RedFAccNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (FAssRed1 e s ta e' s' F D e⇩_{2}) have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙F{D}:=e⇩_{2}: T" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have void: "T = Void" by blast ― ‹We distinguish if @{term e} has type @{term NT} or a Class type› { assume "P,E,hp s ⊢ e : NT" hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce moreover obtain T⇩_{2}where "P,E,hp s ⊢ e⇩_{2}: T⇩_{2}" using wt by auto from this red_hext_incr[OF red] have "P,E,hp s' ⊢ e⇩_{2}: T⇩_{2}" by(rule WTrt_hext_mono) ultimately have ?case using void by(blast intro!:WTrtFAssNT) } moreover { fix T' C TF T⇩_{2}fm assume wt⇩_{1}: "P,E,hp s ⊢ e : T'" and icto: "class_type_of' T' = ⌊C⌋" and wt⇩_{2}: "P,E,hp s ⊢ e⇩_{2}: T⇩_{2}" and has: "P ⊢ C has F:TF (fm) in D" and sub: "P ⊢ T⇩_{2}≤ TF" obtain U where wt⇩_{1}': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'" using IH[OF conf wt⇩_{1}tconf] by blast have wt⇩_{2}': "P,E,hp s' ⊢ e⇩_{2}: T⇩_{2}" by(rule WTrt_hext_mono[OF wt⇩_{2}red_hext_incr[OF red]]) ― ‹Is @{term U} the null type or a class type?› have ?case proof(cases "U = NT") case True with wt⇩_{1}' wt⇩_{2}' void show ?thesis by(blast intro!:WTrtFAssNT) next case False with icto UsubC obtain C' where icto': "class_type_of' U = ⌊C'⌋" and "subclass": "P ⊢ C' ≼⇧^{*}C" by(rule widen_is_class_type_of) have "P ⊢ C' has F:TF (fm) in D" by(rule has_field_mono[OF has "subclass"]) with wt⇩_{1}' show ?thesis using wt⇩_{2}' sub void icto' by(blast intro:WTrtFAss) qed } ultimately show ?case using wt by blast next case (FAssRed2 e⇩_{2}s ta e⇩_{2}' s' v F D T E) have red: "extTA,P,t ⊢ ⟨e⇩_{2},s⟩ -ta→ ⟨e⇩_{2}',s'⟩" and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e⇩_{2}: T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e⇩_{2}' : U ∧ P ⊢ U ≤ T" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ Val v∙F{D}:=e⇩_{2}: T" and tconf: "P,hp s ⊢ t √t" by fact+ from wt have [simp]: "T = Void" by auto from wt show ?case proof (rule WTrt_elim_cases) fix U C TF T⇩_{2}fm assume wt⇩_{1}: "P,E,hp s ⊢ Val v : U" and icto: "class_type_of' U = ⌊C⌋" and has: "P ⊢ C has F:TF (fm) in D" and wt⇩_{2}: "P,E,hp s ⊢ e⇩_{2}: T⇩_{2}" and TsubTF: "P ⊢ T⇩_{2}≤ TF" have wt⇩_{1}': "P,E,hp s' ⊢ Val v : U" by(rule WTrt_hext_mono[OF wt⇩_{1}red_hext_incr[OF red]]) obtain T⇩_{2}' where wt⇩_{2}': "P,E,hp s' ⊢ e⇩_{2}' : T⇩_{2}'" and T'subT: "P ⊢ T⇩_{2}' ≤ T⇩_{2}" using IH[OF conf wt⇩_{2}tconf] by blast have "P,E,hp s' ⊢ Val v∙F{D}:=e⇩_{2}' : Void" by(rule WTrtFAss[OF wt⇩_{1}' icto has wt⇩_{2}' widen_trans[OF T'subT TsubTF]]) thus ?case by auto next fix T⇩_{2}assume null: "P,E,hp s ⊢ Val v : NT" and wt⇩_{2}: "P,E,hp s ⊢ e⇩_{2}: T⇩_{2}" from null have "v = Null" by simp moreover obtain T⇩_{2}' where "P,E,hp s' ⊢ e⇩_{2}' : T⇩_{2}' ∧ P ⊢ T⇩_{2}' ≤ T⇩_{2}" using IH[OF conf wt⇩_{2}tconf] by blast ultimately show ?thesis by(fastforce intro:WTrtFAssNT) qed next case RedFAss thus ?case by(auto simp del:fun_upd_apply) next case RedFAssNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (CASRed1 e s ta e' s' D F e2 e3) from CASRed1.prems(2) consider (NT) T2 T3 where "P,E,hp s ⊢ e : NT" "T = Boolean" "P,E,hp s ⊢ e2 : T2" "P,E,hp s ⊢ e3 : T3" | (RefT) U T' C fm T2 T3 where "P,E,hp s ⊢ e : U" "T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D" "P,E,hp s ⊢ e2 : T2" "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e3 : T3" "P ⊢ T3 ≤ T'" "volatile fm" by fastforce thus ?case proof cases case NT have "P,E,hp s' ⊢ e' : NT" using CASRed1.hyps(2)[OF CASRed1.prems(1) NT(1) CASRed1.prems(3)] by auto moreover from NT CASRed1.hyps(1)[THEN red_hext_incr] have "P,E,hp s' ⊢ e2 : T2" "P,E,hp s' ⊢ e3 : T3" by(auto intro: WTrt_hext_mono) ultimately show ?thesis using NT by(auto intro: WTrtCASNT) next case RefT from CASRed1.hyps(2)[OF CASRed1.prems(1) RefT(1) CASRed1.prems(3)] obtain U' where wt1: "P,E,hp s' ⊢ e' : U'" "P ⊢ U' ≤ U" by blast from RefT CASRed1.hyps(1)[THEN red_hext_incr] have wt2: "P,E,hp s' ⊢ e2 : T2" and wt3: "P,E,hp s' ⊢ e3 : T3" by(auto intro: WTrt_hext_mono) show ?thesis proof(cases "U' = NT") case True with RefT wt1 wt2 wt3 show ?thesis by(auto intro: WTrtCASNT) next case False with RefT(3) wt1 obtain C' where icto': "class_type_of' U' = ⌊C'⌋" and "subclass": "P ⊢ C' ≼⇧^{*}C" by(blast intro: widen_is_class_type_of) have "P ⊢ C' has F:T' (fm) in D" by(rule has_field_mono[OF RefT(4) "subclass"]) with RefT wt1 wt2 wt3 icto' show ?thesis by(auto intro!: WTrtCAS) qed qed next case (CASRed2 e s ta e' s' v D F e3) consider (Null) "v = Null" | (Val) U C T' fm T2 T3 where "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D" "volatile fm" "P,E,hp s ⊢ e : T2" "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e3 : T3" "P ⊢ T3 ≤ T'" "T = Boolean" "typeof⇘hp s⇙ v = ⌊U⌋" using CASRed2.prems(2) by auto then show ?case proof cases case Null then show ?thesis using CASRed2 by(force dest: red_hext_incr intro: WTrt_hext_mono WTrtCASNT) next case Val from CASRed2.hyps(1) have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr) with Val(9) have "typeof⇘hp s'⇙ v = ⌊U⌋" by(rule type_of_hext_type_of) moreover from CASRed2.hyps(2)[OF CASRed2.prems(1) Val(4) CASRed2.prems(3)] Val(5) obtain T2' where "P,E,hp s' ⊢ e' : T2'" "P ⊢ T2' ≤ T'" by(auto intro: widen_trans) moreover from Val(6) hext have "P,E,hp s' ⊢ e3 : T3" by(rule WTrt_hext_mono) ultimately show ?thesis using Val by(auto intro: WTrtCAS) qed next case (CASRed3 e s ta e' s' v D F v') consider (Null) "v = Null" | (Val) U C T' fm T2 T3 where "T = Boolean" "class_type_of' U = ⌊C⌋" "P ⊢ C has F:T' (fm) in D" "volatile fm" "P ⊢ T2 ≤ T'" "P,E,hp s ⊢ e : T3" "P ⊢ T3 ≤ T'" "typeof⇘hp s⇙ v = ⌊U⌋" "typeof⇘hp s⇙ v' = ⌊T2⌋" using CASRed3.prems(2) by auto then show ?case proof cases case Null then show ?thesis using CASRed3 by(force dest: red_hext_incr intro: type_of_hext_type_of WTrtCASNT) next case Val from CASRed3.hyps(1) have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr) with Val(8,9) have "typeof⇘hp s'⇙ v = ⌊U⌋" "typeof⇘hp s'⇙ v' = ⌊T2⌋" by(blast intro: type_of_hext_type_of)+ moreover from CASRed3.hyps(2)[OF CASRed3.prems(1) Val(6) CASRed3.prems(3)] Val(7) obtain T3' where "P,E,hp s' ⊢ e' : T3'" "P ⊢ T3' ≤ T'" by(auto intro: widen_trans) ultimately show ?thesis using Val by(auto intro: WTrtCAS) qed next case CASNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (CallObj e s ta e' s' M es T E) have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" and IH: "⋀E T. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃U. P,E,hp s' ⊢ e' : U ∧ P ⊢ U ≤ T" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ e∙M(es) : T" and tconf: "P,hp s ⊢ t √t" by fact+ ― ‹We distinguish if @{term e} has type @{term NT} or a Class type› from wt show ?case proof(rule WTrt_elim_cases) fix T' C Ts meth D Us assume wte: "P,E,hp s ⊢ e : T'" and icto: "class_type_of' T' = ⌊C⌋" and "method": "P ⊢ C sees M:Ts→T = meth in D" and wtes: "P,E,hp s ⊢ es [:] Us" and subs: "P ⊢ Us [≤] Ts" obtain U where wte': "P,E,hp s' ⊢ e' : U" and UsubC: "P ⊢ U ≤ T'" using IH[OF conf wte tconf] by blast show ?thesis proof(cases "U = NT") case True moreover have "P,E,hp s' ⊢ es [:] Us" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) ultimately show ?thesis using wte' by(blast intro!:WTrtCallNT) next case False with icto UsubC obtain C' where icto': "class_type_of' U = ⌊C'⌋" and "subclass": "P ⊢ C' ≼⇧^{*}C" by(rule widen_is_class_type_of) obtain Ts' T' meth' D' where method': "P ⊢ C' sees M:Ts'→T' = meth' in D'" and subs': "P ⊢ Ts [≤] Ts'" and sub': "P ⊢ T' ≤ T" using Call_lemma[OF "method" "subclass" wf] by fast have wtes': "P,E,hp s' ⊢ es [:] Us" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) show ?thesis using wtes' wte' icto' subs method' subs' sub' by(blast intro:widens_trans) qed next fix Ts assume "P,E,hp s ⊢ e:NT" hence "P,E,hp s' ⊢ e' : NT" using IH[OF conf _ tconf] by fastforce moreover fix Ts assume wtes: "P,E,hp s ⊢ es [:] Ts" have "P,E,hp s' ⊢ es [:] Ts" by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]]) ultimately show ?thesis by(blast intro!:WTrtCallNT) qed next case (CallParams es s ta es' s' v M T E) have reds: "extTA,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩" and IH: "⋀Ts E. ⟦E ⊢ s √; P,E,hp s ⊢ es [:] Ts; P,hp s ⊢ t √t⟧ ⟹ ∃Ts'. P,E,hp s' ⊢ es' [:] Ts' ∧ P ⊢ Ts' [≤] Ts" and conf: "E ⊢ s √" and wt: "P,E,hp s ⊢ Val v∙M(es) : T" and tconf: "P,hp s ⊢ t √t" by fact+ from wt show ?case proof (rule WTrt_elim_cases) fix U C Ts meth D Us assume wte: "P,E,hp s ⊢ Val v : U" and icto: "class_type_of' U = ⌊C⌋" and "P ⊢ C sees M:Ts→T = meth in D" and wtes: "P,E,hp s ⊢ es [:] Us" and "P ⊢ Us [≤] Ts" moreover have "P,E,hp s' ⊢ Val v : U" by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]]) moreover obtain Us' where "P,E,hp s' ⊢ es' [:] Us'" "P ⊢ Us' [≤] Us" using IH[OF conf wtes tconf] by blast ultimately show ?thesis by(fastforce intro:WTrtCall widens_trans) next fix Us assume null: "P,E,hp s ⊢ Val v : NT" and wtes: "P,E,hp s ⊢ es [:] Us" from null have "v = Null" by simp moreover obtain Us' where "P,E,hp s' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us" using IH[OF conf wtes tconf] by blast ultimately show ?thesis by(fastforce intro:WTrtCallNT) qed next case (RedCall s a U M Ts T pns body D vs T' E) have hp: "typeof_addr (hp s) a = ⌊U⌋" and "method": "P ⊢ class_type_of U sees M: Ts→T = ⌊(pns,body)⌋ in D" and wt: "P,E,hp s ⊢ addr a∙M(map Val vs) : T'" by fact+ obtain Ts' where wtes: "P,E,hp s ⊢ map Val vs [:] Ts'" and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T" using wt "method" hp wf by(auto 4 3 dest: sees_method_fun) from wtes subs have length_vs: "length vs = length Ts" by(auto simp add: WTrts_conv_list_all2 dest!: list_all2_lengthD) have UsubD: "P ⊢ ty_of_htype U ≤ Class (class_type_of U)" by(cases U)(simp_all add: widen_array_object) from sees_wf_mdecl[OF wf "method"] obtain T'' where wtabody: "P,[this#pns [↦] Class D#Ts] ⊢ body :: T''" and T''subT: "P ⊢ T'' ≤ T" and length_pns: "length pns = length Ts" by(fastforce simp:wf_mdecl_def simp del:map_upds_twist) from wtabody have "P,Map.empty(this#pns [↦] Class D#Ts),hp s ⊢ body : T''" by(rule WT_implies_WTrt) hence "P,E(this#pns [↦] Class D#Ts),hp s ⊢ body : T''" by(rule WTrt_env_mono) simp hence "P,E,hp s ⊢ blocks (this#pns) (Class D#Ts) (Addr a#vs) body : T''" using wtes subs hp sees_method_decl_above[OF "method"] length_vs length_pns UsubD by(auto simp add:wt_blocks rel_list_all2_Cons2 intro: widen_trans) with T''subT T'isT show ?case by blast next case (RedCallExternal s a U M Ts T' D vs ta va h' ta' e' s') from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› have "hp s ⊴ h'" by(rule red_external_hext) with ‹P,E,hp s ⊢ addr a∙M(map Val vs) : T› have "P,E,h' ⊢ addr a∙M(map Val vs) : T" by(rule WTrt_hext_mono) moreover from ‹typeof_addr (hp s) a = ⌊U⌋› ‹P ⊢ class_type_of U sees M: Ts→T' = Native in D› ‹P,E,hp s ⊢ addr a∙M(map Val vs) : T› have "P,hp s ⊢ a∙M(vs) : T'" by(fastforce simp add: external_WT'_iff dest: sees_method_fun) ultimately show ?case using RedCallExternal by(auto 4 3 intro: red_external_conf_extRet[OF wf] intro!: wt_external_call simp add: sconf_def dest: sees_method_fun[where C="class_type_of U"]) next case RedCallNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (BlockRed e h x V vo ta e' h' x' T T' E) note IH = ‹⋀T E. ⟦E ⊢ (h, x(V := vo)) √; P,E,hp (h, x(V := vo)) ⊢ e : T; P,hp (h, x(V := vo)) ⊢ t √t⟧ ⟹ ∃T'. P,E,hp (h', x') ⊢ e' : T' ∧ P ⊢ T' ≤ T›[simplified] from ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'› have "P,E(V↦T),h ⊢ e : T'" by(cases vo, auto) moreover from ‹E ⊢ (h, x) √› ‹P,E,hp (h, x) ⊢ {V:T=vo; e} : T'› have "(E(V ↦ T)) ⊢ (h, x(V := vo)) √" by(cases vo)(simp add: lconf_def sconf_def,auto simp add: sconf_def conf_def intro: lconf_upd2) ultimately obtain T'' where wt': "P,E(V↦T),h' ⊢ e' : T''" "P ⊢ T'' ≤ T'" using ‹P,hp (h, x) ⊢ t √t› by(auto dest: IH) { fix v assume vo: "x' V = ⌊v⌋" from ‹(E(V ↦ T)) ⊢ (h, x(V := vo)) √› ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩› ‹P,E(V↦T),h ⊢ e : T'› have "P,h' ⊢ x' (:≤) (E(V ↦ T))" by(auto simp add: sconf_def dest: red_preserves_lconf) with vo have "∃T'. typeof⇘h'⇙ v = ⌊T'⌋ ∧ P ⊢ T' ≤ T" by(fastforce simp add: sconf_def lconf_def conf_def) then obtain T' where "typeof⇘h'⇙ v = ⌊T'⌋" "P ⊢ T' ≤ T" by blast hence ?case using wt' vo by(auto) } moreover { assume "x' V = None" with wt' have ?case by(auto) } ultimately show ?case by blast next case RedBlock thus ?case by auto next case (SynchronizedRed1 o' s ta o'' s' e T E) have red: "extTA,P,t ⊢ ⟨o',s⟩ -ta→ ⟨o'',s'⟩" by fact have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ o' : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ o'' : T' ∧ P ⊢ T' ≤ T" by fact have conf: "E ⊢ s √" by fact have wt: "P,E,hp s ⊢ sync(o') e : T" by fact+ thus ?case proof(rule WTrt_elim_cases) fix To assume wto: "P,E,hp s ⊢ o' : To" and refT: "is_refT To" and wte: "P,E,hp s ⊢ e : T" from IH[OF conf wto ‹P,hp s ⊢ t √t›] obtain To' where "P,E,hp s' ⊢ o'' : To'" and sub: "P ⊢ To' ≤ To" by auto moreover have "P,E,hp s' ⊢ e : T" by(rule WTrt_hext_mono[OF wte red_hext_incr[OF red]]) moreover have "is_refT To'" using refT sub by(auto intro: widen_refT) ultimately show ?thesis by(auto) qed next case SynchronizedNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case LockSynchronized thus ?case by(auto) next case (SynchronizedRed2 e s ta e' s' a T E) have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" by fact have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact have conf: "E ⊢ s √" by fact have wt: "P,E,hp s ⊢ insync(a) e : T" by fact thus ?case proof(rule WTrt_elim_cases) fix Ta assume "P,E,hp s ⊢ e : T" and hpa: "typeof_addr (hp s) a = ⌊Ta⌋" from ‹P,E,hp s ⊢ e : T› conf ‹P,hp s ⊢ t √t› obtain T' where "P,E,hp s' ⊢ e' : T'" "P ⊢ T' ≤ T" by(blast dest: IH) moreover from red have hext: "hp s ⊴ hp s'" by(auto dest: red_hext_incr) with hpa have "P,E,hp s' ⊢ addr a : ty_of_htype Ta" by(auto intro: typeof_addr_hext_mono) ultimately show ?thesis by auto qed next case UnlockSynchronized thus ?case by(auto) next case SeqRed thus ?case apply(auto) apply(drule WTrt_hext_mono[OF _ red_hext_incr], assumption) by auto next case (CondRed b s ta b' s' e1 e2 T E) have red: "extTA,P,t ⊢ ⟨b,s⟩ -ta→ ⟨b',s'⟩" by fact have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ b : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ b' : T' ∧ P ⊢ T' ≤ T" by fact have conf: "E ⊢ s √" by fact have wt: "P,E,hp s ⊢ if (b) e1 else e2 : T" by fact thus ?case proof(rule WTrt_elim_cases) fix T1 T2 assume wtb: "P,E,hp s ⊢ b : Boolean" and wte1: "P,E,hp s ⊢ e1 : T1" and wte2: "P,E,hp s ⊢ e2 : T2" and lub: "P ⊢ lub(T1, T2) = T" from IH[OF conf wtb ‹P,hp s ⊢ t √t›] have "P,E,hp s' ⊢ b' : Boolean" by(auto) moreover have "P,E,hp s' ⊢ e1 : T1" by(rule WTrt_hext_mono[OF wte1 red_hext_incr[OF red]]) moreover have "P,E,hp s' ⊢ e2 : T2" by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]]) ultimately show ?thesis using lub by auto qed next case (ThrowRed e s ta e' s' T E) have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact have conf: "E ⊢ s √" by fact have wt: "P,E,hp s ⊢ throw e : T" by fact then obtain T' where wte: "P,E,hp s ⊢ e : T'" and nobject: "P ⊢ T' ≤ Class Throwable" by auto from IH[OF conf wte ‹P,hp s ⊢ t √t›] obtain T'' where wte': "P,E,hp s' ⊢ e' : T''" and PT'T'': "P ⊢ T'' ≤ T'" by blast from nobject PT'T'' have "P ⊢ T'' ≤ Class Throwable" by(auto simp add: widen_Class)(erule notE, rule rtranclp_trans) hence "P,E,hp s' ⊢ throw e' : T" using wte' PT'T'' by -(erule WTrtThrow) thus ?case by(auto) next case RedThrowNull thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case (TryRed e s ta e' s' C V e2 T E) have red: "extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩" by fact have IH: "⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T" by fact have conf: "E ⊢ s √" by fact have wt: "P,E,hp s ⊢ try e catch(C V) e2 : T" by fact thus ?case proof(rule WTrt_elim_cases) fix T1 assume wte: "P,E,hp s ⊢ e : T1" and wte2: "P,E(V ↦ Class C),hp s ⊢ e2 : T" and sub: "P ⊢ T1 ≤ T" from IH[OF conf wte ‹P,hp s ⊢ t √t›] obtain T1' where "P,E,hp s' ⊢ e' : T1'" and "P ⊢ T1' ≤ T1" by(auto) moreover have "P,E(V ↦ Class C),hp s' ⊢ e2 : T" by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]]) ultimately show ?thesis using sub by(auto elim: widen_trans) qed next case RedTryFail thus ?case unfolding sconf_def by(fastforce simp add: xcpt_subcls_Throwable[OF _ wf]) next case RedSeq thus ?case by auto next case RedCondT thus ?case by(auto dest: is_lub_upper) next case RedCondF thus ?case by(auto dest: is_lub_upper) next case RedWhile thus ?case by(fastforce) next case RedTry thus ?case by auto next case RedTryCatch thus ?case by(fastforce) next case (ListRed1 e s ta e' s' es Ts E) note IH = ‹⋀T E. ⟦E ⊢ s √; P,E,hp s ⊢ e : T; P,hp s ⊢ t √t⟧ ⟹ ∃T'. P,E,hp s' ⊢ e' : T' ∧ P ⊢ T' ≤ T› from ‹P,E,hp s ⊢ e # es [:] Ts› obtain T Ts' where "Ts = T # Ts'" "P,E,hp s ⊢ e : T" "P,E,hp s ⊢ es [:] Ts'" by auto with IH[of E T] ‹E ⊢ s √› WTrts_hext_mono[OF ‹P,E,hp s ⊢ es [:] Ts'› red_hext_incr[OF ‹extTA,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›]] show ?case using ‹P,hp s ⊢ t √t› by(auto simp add: list_all2_Cons2 intro: widens_refl) next case ListRed2 thus ?case by(fastforce dest: hext_typeof_mono[OF reds_hext_incr]) qed(fastforce)+ end