section‹ Equivalence of Big Step and Small Step Semantics ›
theory Equivalence imports TypeSafe WWellForm begin
subsection‹Small steps simulate big step›
subsubsection"Init"
text"The reduction of initialization expressions doesn't touch or use their on-hold expressions (the subexpression to the right of @{text ←}) until the initialization operation completes. This function is used to prove this and related properties. It is then used for general reduction of initialization expressions separately from their on-hold expressions by using the on-hold expression @{term unit}, then putting the real on-hold expression back in at the end."
fun init_switch :: "'a exp ==> 'a exp ==> 'a exp"where "init_switch (INIT C (Cs,b) ← ei) e = (INIT C (Cs,b) ← e)" | "init_switch (RI(C,e');Cs ← ei) e = (RI(C,e');Cs ← e)" | "init_switch e' e = e'"
fun INIT_class :: "'a exp ==> cname option"where "INIT_class (INIT C (Cs,b) ← e) = (if C = last (C#Cs) then Some C else None)" | "INIT_class (RI(C,e0);Cs ← e) = Some (last (C#Cs))" | "INIT_class _ = None"
lemma init_red_sync: "[ P ⊨⟨e0,s0,b0⟩→⟨e1,s1,b1⟩; init_exp_of e0 = ⌊e⌋; e1≠ e ] ==> (∧e'. P ⊨⟨init_switch e0 e',s0,b0⟩→⟨init_switch e1 e',s1,b1⟩)" proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)
lemma init_red_sync_end: "[ P ⊨⟨e0,s0,b0⟩→⟨e1,s1,b1⟩; init_exp_of e0 = ⌊e⌋; e1 = e; throw_of e = None ] ==> (∧e'. ¬sub_RI e' ==> P ⊨⟨init_switch e0 e',s0,b0⟩→⟨e',s1,icheck P (the(INIT_class e0)) e'⟩)" proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)
lemma init_reds_sync_unit': "[ P ⊨⟨e0,s0,b0⟩→* ⟨Val v',s1,b1⟩; init_exp_of e0 = ⌊unit⌋; INIT_class e0 = ⌊C⌋] ==> (∧e'. ¬sub_RI e' ==> P ⊨⟨init_switch e0 e',s0,b0⟩→* ⟨e',s1,icheck P (the(INIT_class e0)) e'⟩)" proof(induct rule:converse_rtrancl_induct3) case refl thenshow ?caseby simp next case (step e0 s0 b0 e1 s1 b1) have"(init_exp_of e1 = ⌊unit⌋∧ (INIT_class e0 = ⌊C⌋⟶ INIT_class e1 = ⌊C⌋)) ∨ (e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit) ∨ (∃a. e1 = throw a)" using init_red_init[OF step.prems(1) step.hyps(1)] by simp thenshow ?case proof(rule disjE) assume assm: "init_exp_of e1 = ⌊unit⌋∧ (INIT_class e0 = ⌊C⌋⟶ INIT_class e1 = ⌊C⌋)" thenhave red: "P ⊨⟨init_switch e0 e',s0,b0⟩→⟨init_switch e1 e',s1,b1⟩" using init_red_sync[OF step.hyps(1) step.prems(1)] by simp have reds: "P ⊨⟨init_switch e1 e',s1,b1⟩→* ⟨e',s1,icheck P (the (INIT_class e0)) e'⟩" using step.hyps(3)[OF _ _ step.prems(3)] assm step.prems(2) by simp show ?thesis by(rule converse_rtrancl_into_rtrancl[OF red reds]) next assume"(e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit) ∨ (∃a. e1 = throw a)" thenshow ?thesis proof(rule disjE) assume assm: "e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit"thenhave e1: "e1 = unit"by simp have sb: "s1 = s1""b1 = b1"using reds_final_same[OF step.hyps(2)] assm by(simp_all add: final_def) thenhave step': "P ⊨⟨init_switch e0 e',s0,b0⟩→⟨e',s1,icheck P (the (INIT_class e0)) e'⟩" using init_red_sync_end[OF step.hyps(1) step.prems(1) e1 _ step.prems(3)] by auto thenhave"P ⊨⟨init_switch e0 e',s0,b0⟩→* ⟨e',s1,icheck P (the (INIT_class e0)) e'⟩" using r_into_rtrancl by auto thenshow ?thesis using step assm sb by simp next assume"∃a. e1 = throw a"thenobtain a where"e1 = throw a"by clarsimp thenhave tof: "throw_of e1 = ⌊a⌋"by simp thenshow ?thesis using reds_throw[OF step.hyps(2) tof] by simp qed qed qed
lemma init_reds_sync_unit_throw': "[ P ⊨⟨e0,s0,b0⟩→* ⟨throw a,s1,b1⟩; init_exp_of e0 = ⌊unit⌋] ==> (∧e'. P ⊨⟨init_switch e0 e',s0,b0⟩→* ⟨throw a,s1,b1⟩)" proof(induct rule:converse_rtrancl_induct3) case refl thenshow ?caseby simp next case (step e0 s0 b0 e1 s1 b1) have"init_exp_of e1 = ⌊unit⌋∧ (∀C. INIT_class e0 = ⌊C⌋⟶ INIT_class e1 = ⌊C⌋) ∨ e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit ∨ (∃a. e1 = throw a)" using init_red_init[OF step.prems(1) step.hyps(1)] by auto thenshow ?case proof(rule disjE) assume assm: "init_exp_of e1 = ⌊unit⌋∧ (∀C. INIT_class e0 = ⌊C⌋⟶ INIT_class e1 = ⌊C⌋)" thenhave"P ⊨⟨init_switch e0 e',s0,b0⟩→⟨init_switch e1 e',s1,b1⟩" using step init_red_sync[OF step.hyps(1) step.prems] by simp thenshow ?thesis using step assm by (meson converse_rtrancl_into_rtrancl) next assume"e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit ∨ (∃a. e1 = throw a)" thenshow ?thesis proof(rule disjE) assume"e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit" thenshow ?thesis using step using final_def reds_final_same by blast next assume assm: "∃a. e1 = throw a" thenhave"P ⊨⟨init_switch e0 e',s0,b0⟩→⟨e1,s1,b1⟩" using init_red_sync[OF step.hyps(1) step.prems] by clarsimp thenshow ?thesis using step by simp qed qed qed
lemma init_reds_sync_unit: assumes"P ⊨⟨e0,s0,b0⟩→* ⟨Val v',s1,b1⟩"and"init_exp_of e0 = ⌊unit⌋"and"INIT_class e0= ⌊C⌋" and"¬sub_RI e'" shows"P ⊨⟨init_switch e0 e',s0,b0⟩→* ⟨e',s1,icheck P (the(INIT_class e0)) e'⟩" using init_reds_sync_unit'[OF assms] by clarsimp
lemma init_reds_sync_unit_throw: assumes"P ⊨⟨e0,s0,b0⟩→* ⟨throw a,s1,b1⟩"and"init_exp_of e0 = ⌊unit⌋" shows"P ⊨⟨init_switch e0 e',s0,b0⟩→* ⟨throw a,s1,b1⟩" using init_reds_sync_unit_throw'[OF assms] by clarsimp
―‹ init reds lemmas ›
lemma InitSeqReds: assumes"P ⊨⟨INIT C ([C],b) ← unit,s0,b0⟩→* ⟨Val v',s1,b1⟩" and"P ⊨⟨e,s1,icheck P C e⟩→* ⟨e2,s2,b2⟩"and"¬sub_RI e" shows"P ⊨⟨INIT C ([C],b) ← e,s0,b0⟩→* ⟨e2,s2,b2⟩" using assms proof - have"P ⊨⟨init_switch (INIT C ([C],b) ← unit) e,s0,b0⟩→* ⟨e,s1,icheck P C e⟩" using init_reds_sync_unit[OF assms(1) _ _ assms(3)] by simp thenshow ?thesis using assms(2) by simp qed
lemma InitSeqThrowReds: assumes"P ⊨⟨INIT C ([C],b) ← unit,s0,b0⟩→* ⟨throw a,s1,b1⟩" shows"P ⊨⟨INIT C ([C],b) ← e,s0,b0⟩→* ⟨throw a,s1,b1⟩" using assms proof - have"P ⊨⟨init_switch (INIT C ([C],b) ← unit) e,s0,b0⟩→* ⟨throw a,s1,b1⟩" using init_reds_sync_unit_throw[OF assms(1)] by simp thenshow ?thesis by simp qed
lemma InitNoneReds: "[ sh C = None; P ⊨⟨INIT C' (C # Cs,False) ← e,(h, l, sh(C ↦ (sblank P C, Prepared))),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule InitNoneRed[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma InitDoneReds: "[ sh C = Some(sfs,Done); P ⊨⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule RedInitDone[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma InitProcessingReds: "[ sh C = Some(sfs,Processing); P ⊨⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule RedInitProcessing[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma InitErrorReds: "[ sh C = Some(sfs,Error); P ⊨⟨RI (C,THROW NoClassDefFoundError);Cs ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule RedInitError[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma InitObjectReds: "[ sh C = Some(sfs,Prepared); C = Object; sh' = sh(C ↦ (sfs,Processing)); P ⊨⟨INIT C' (C#Cs,True) ← e,(h,l,sh'),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule InitObjectRed[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma InitNonObjectReds: "[ sh C = Some(sfs,Prepared); C ≠ Object; class P C = Some (D,r); sh' = sh(C ↦ (sfs,Processing)); P ⊨⟨INIT C' (D#C#Cs,False) ← e,(h,l,sh'),b⟩→* ⟨e',s',b'⟩] \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule InitNonObjectSuperRed[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma RedsInitRInit: "P ⊨⟨RI (C,C∙sclinit([]));Cs ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩ \<Longrightarrow> P ⊨⟨INIT C' (C#Cs,True) ← e,(h,l,sh),b⟩→* ⟨e',s',b'⟩" (*<*)by(rule RedInitRInit[THEN converse_rtrancl_into_rtrancl])(*>*)
lemma RInitReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩ \<Longrightarrow> P ⊨⟨RI (C,e);Cs ← e0, s, b⟩→* ⟨RI (C,e');Cs ← e0, s', b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) RInitRed[OF step(2)]]) qed (*>*)
lemma RedsRInit: "[ P ⊨⟨e0,s0,b0⟩→* ⟨Val v,(h1,l1,sh1),b1⟩; sh1 C = Some (sfs, i); sh2 = sh1(C ↦ (sfs,Done)); C' = last(C#Cs); P ⊨⟨INIT C' (Cs,True) ← e,(h1,l1,sh2),b1⟩→* ⟨e',s',b'⟩] ==> P ⊨⟨RI (C, e0);Cs ← e,s0,b0⟩→* ⟨e',s',b'⟩" (*<*) by(rule rtrancl_trans[OF RInitReds
RedRInit[THEN converse_rtrancl_into_rtrancl]]) (*>*)
lemma RInitInitThrowReds: "[ P ⊨⟨e,s,b⟩→* ⟨Throw a,(h',l',sh'),b'⟩; sh' C = Some (sfs, i); sh'' = sh'(C ↦ (sfs,Error)); P ⊨⟨RI (D,Throw a);Cs ← e0, (h',l',sh''),b'⟩→* ⟨e1,s1,b1⟩] ==> P ⊨⟨RI (C, e);D#Cs ← e0,s,b⟩→* ⟨e1,s1,b1⟩" (*<*) by(rule rtrancl_trans[OF RInitReds
RInitInitThrow[THEN converse_rtrancl_into_rtrancl]]) (*>*)
lemma RInitThrowReds: "[ P ⊨⟨e,s,b⟩→* ⟨Throw a, (h',l',sh'),b'⟩; sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error)) ] ==> P ⊨⟨RI (C,e);Nil ← e0,s,b⟩→* ⟨Throw a, (h',l',sh''),b'⟩" (*<*)by(rule RInitReds[THEN rtrancl_into_rtrancl, OF _ RInitThrow])(*>*)
subsubsection"New"
lemma NewInitDoneReds: "[ sh C = Some (sfs, Done); new_Addr h = Some a; P ⊨ C has_fields FDTs; h' = h(a↦blank P C) ] ==> P ⊨⟨new C,(h,l,sh),False⟩→* ⟨addr a,(h',l,sh),False⟩" (*<*) by(rule NewInitDoneRed[THEN converse_rtrancl_into_rtrancl,
OF _ RedNew[THEN r_into_rtrancl]]) (*>*)
lemma NewInitDoneReds2: "[ sh C = Some (sfs, Done); new_Addr h = None; is_class P C ] ==> P ⊨⟨new C,(h,l,sh),False⟩→* ⟨THROW OutOfMemory, (h,l,sh), False⟩" (*<*) by(rule NewInitDoneRed[THEN converse_rtrancl_into_rtrancl,
OF _ RedNewFail[THEN r_into_rtrancl]]) (*>*)
lemma NewInitReds: assumes nDone: "∄sfs. shp s C = Some (sfs, Done)" and INIT_steps: "P ⊨⟨INIT C ([C],False) ← unit,s,False⟩→* ⟨Val v',(h',l',sh'),b'⟩" and Addr: "new_Addr h' = Some a"and has: "P ⊨ C has_fields FDTs" and h'': "h'' = h'(a↦blank P C)"and cls_C: "is_class P C" shows"P ⊨⟨new C,s,False⟩→* ⟨addr a,(h'',l',sh'),False⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(INIT C ([C],False) ← new C,s,False)" let ?b' = "(new C,(h', l', sh'),icheck P C (new C::expr))" have b'c: "(?b', ?c) ∈ (red P)*" using RedNew[OF Addr has h'', THEN r_into_rtrancl] by simp obtain h l sh where [simp]: "s = (h, l, sh)"by(cases s) simp have"(?a, ?b) ∈ (red P)*" using NewInitRed[OF _ cls_C] nDone by fastforce alsohave"(?b, ?c) ∈ (red P)*" by(rule InitSeqReds[OF INIT_steps b'c]) simp ultimatelyshow ?thesis by simp qed (*>*)
lemma NewInitOOMReds: assumes nDone: "∄sfs. shp s C = Some (sfs, Done)" and INIT_steps: "P ⊨⟨INIT C ([C],False) ← unit,s,False⟩→* ⟨Val v',(h',l',sh'),b'⟩" and Addr: "new_Addr h' = None"and cls_C: "is_class P C" shows"P ⊨⟨new C,s,False⟩→* ⟨THROW OutOfMemory,(h',l',sh'),False⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(INIT C ([C],False) ← new C,s,False)" let ?b' = "(new C,(h', l', sh'),icheck P C (new C::expr))" have b'c: "(?b', ?c) ∈ (red P)*" using RedNewFail[OF Addr cls_C, THEN r_into_rtrancl] by simp obtain h l sh where [simp]: "s = (h, l, sh)"by(cases s) simp have"(?a, ?b) ∈ (red P)*" using NewInitRed[OF _ cls_C] nDone by fastforce alsohave"(?b, ?c) ∈ (red P)*" by(rule InitSeqReds[OF INIT_steps b'c]) simp ultimatelyshow ?thesis by simp qed (*>*)
lemma NewInitThrowReds: assumes nDone: "∄sfs. shp s C = Some (sfs, Done)" and cls_C: "is_class P C" and INIT_steps: "P ⊨⟨INIT C ([C],False) ← unit,s,False⟩→* ⟨throw a,s',b'⟩" shows"P ⊨⟨new C,s,False⟩→* ⟨throw a,s',b'⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(INIT C ([C],False) ← new C,s,False)" obtain h l sh where [simp]: "s = (h, l, sh)"by(cases s) simp have"(?a, ?b) ∈ (red P)*" using NewInitRed[OF _ cls_C] nDone by fastforce alsohave"(?b, ?c) ∈ (red P)*" using InitSeqThrowReds[OF INIT_steps] by simp ultimatelyshow ?thesis by simp qed (*>*)
subsubsection"Cast"
lemma CastReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨Cast C e,s,b⟩→* ⟨Cast C e',s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CastRed[OF step(2)]]) qed (*>*)
lemma CastRedsNull: "P ⊨⟨e,s,b⟩→* ⟨null,s',b'⟩==> P ⊨⟨Cast C e,s,b⟩→* ⟨null,s',b'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastNull])(*>*)
lemma CastRedsAddr: "[ P ⊨⟨e,s,b⟩→* ⟨addr a,s',b'⟩; hp s' a = Some(D,fs); P ⊨ D ⪯* C ]==> P ⊨⟨Cast C e,s,b⟩→* ⟨addr a,s',b'⟩" (*<*)by(cases s', simp) (rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCast])(*>*)
lemma CastRedsFail: "[ P ⊨⟨e,s,b⟩→* ⟨addr a,s',b'⟩; hp s' a = Some(D,fs); ¬ P ⊨ D ⪯* C ]==> P ⊨⟨Cast C e,s,b⟩→* ⟨THROW ClassCast,s',b'⟩" (*<*)by(cases s', simp) (rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastFail])(*>*)
lemma CastRedsThrow: "[ P ⊨⟨e,s,b⟩→* ⟨throw a,s',b'⟩]==> P ⊨⟨Cast C e,s,b⟩→* ⟨throw a,s',b'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CastThrow])(*>*)
subsubsection"LAss"
lemma LAssReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨ V:=e,s,b⟩→* ⟨ V:=e',s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) LAssRed[OF step(2)]]) qed (*>*)
lemma LAssRedsVal: "[ P ⊨⟨e,s,b⟩→* ⟨Val v,(h',l',sh'),b'⟩]==> P ⊨⟨ V:=e,s,b⟩→* ⟨unit,(h',l'(V↦v),sh'),b'⟩" (*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ RedLAss])(*>*)
lemma LAssRedsThrow: "[ P ⊨⟨e,s,b⟩→* ⟨throw a,s',b'⟩]==> P ⊨⟨ V:=e,s,b⟩→* ⟨throw a,s',b'⟩" (*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.LAssThrow])(*>*)
subsubsection"BinOp"
lemma BinOp1Reds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨ e «bop¬ e2, s,b⟩→* ⟨e' «bop¬ e2, s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) BinOpRed1[OF step(2)]]) qed (*>*)
lemma BinOp2Reds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨(Val v) «bop¬ e, s,b⟩→* ⟨(Val v) «bop¬ e', s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) BinOpRed2[OF step(2)]]) qed (*>*)
lemma BinOpRedsVal: assumes e1_steps: "P ⊨⟨e1,s0,b0⟩→* ⟨Val v1,s1,b1⟩" and e2_steps: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v2,s2,b2⟩" and op: "binop(bop,v1,v2) = Some v" shows"P ⊨⟨e1«bop¬ e2, s0,b0⟩→* ⟨Val v,s2,b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v1«bop¬ e2, s1,b1)" let ?y' = "(Val v1«bop¬ Val v2, s2,b2)" have"(?x, ?y) ∈ (red P)*"by(rule BinOp1Reds[OF e1_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule BinOp2Reds[OF e2_steps]) alsohave"(?y', ?z) ∈ (red P)"by(rule RedBinOp[OF op]) ultimatelyshow ?thesis by simp qed (*>*)
lemma BinOpRedsThrow1: "P ⊨⟨e,s,b⟩→* ⟨throw e',s',b'⟩==> P ⊨⟨e «bop¬ e2, s,b⟩→* ⟨throw e', s',b'⟩" (*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*)
lemma FAccReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨e∙F{D}, s,b⟩→* ⟨e'∙F{D}, s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) FAccRed[OF step(2)]]) qed (*>*)
lemma FAccRedsVal: "[ P ⊨⟨e,s,b⟩→* ⟨addr a,s',b'⟩; hp s' a = Some(C,fs); fs(F,D) = Some v; P ⊨ C has F,NonStatic:t in D ] ==> P ⊨⟨e∙F{D},s,b⟩→* ⟨Val v,s',b'⟩" (*<*)by(cases s',simp) (rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAcc])(*>*)
lemma FAccRedsNull: "P ⊨⟨e,s,b⟩→* ⟨null,s',b'⟩==> P ⊨⟨e∙F{D},s,b⟩→* ⟨THROW NullPointer,s',b'⟩" (*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccNull])(*>*)
lemma FAccRedsNone: "[ P ⊨⟨e,s,b⟩→* ⟨addr a,s',b'⟩; hp s' a = Some(C,fs); ¬(∃b t. P ⊨ C has F,b:t in D) ] ==> P ⊨⟨e∙F{D},s,b⟩→* ⟨THROW NoSuchFieldError,s',b'⟩" (*<*)by(cases s',simp) (auto intro: FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccNone])(*>*)
lemma FAccRedsStatic: "[ P ⊨⟨e,s,b⟩→* ⟨addr a,s',b'⟩; hp s' a = Some(C,fs); P ⊨ C has F,Static:t in D ] ==> P ⊨⟨e∙F{D},s,b⟩→* ⟨THROW IncompatibleClassChangeError,s',b'⟩" (*<*)by(cases s',simp) (rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccStatic])(*>*)
lemma FAccRedsThrow: "P ⊨⟨e,s,b⟩→* ⟨throw a,s',b'⟩==> P ⊨⟨e∙F{D},s,b⟩→* ⟨throw a,s',b'⟩" (*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ red_reds.FAccThrow])(*>*)
subsubsection"SFAcc"
lemma SFAccReds: "[ P ⊨ C has F,Static:t in D; shp s D = Some(sfs,Done); sfs F = Some v ] ==> P ⊨⟨C∙sF{D},s,True⟩→* ⟨Val v,s,False⟩" (*<*)by(cases s,simp) (rule RedSFAcc[THEN r_into_rtrancl])(*>*)
lemma SFAccRedsNone: "¬(∃b t. P ⊨ C has F,b:t in D) ==> P ⊨⟨C∙sF{D},s,b⟩→* ⟨THROW NoSuchFieldError,s,False⟩" (*<*)by(cases s,simp) (auto intro: RedSFAccNone[THEN r_into_rtrancl])(*>*)
lemma SFAccRedsNonStatic: "P ⊨ C has F,NonStatic:t in D ==> P ⊨⟨C∙sF{D},s,b⟩→* ⟨THROW IncompatibleClassChangeError,s,False⟩" (*<*)by(cases s,simp) (rule RedSFAccNonStatic[THEN r_into_rtrancl])(*>*)
lemma SFAccInitDoneReds: assumes cF: "P ⊨ C has F,Static:t in D" and shp: "shp s D = Some (sfs,Done)"and sfs: "sfs F = Some v" shows"P ⊨⟨C∙sF{D}, s, b⟩→* ⟨Val v, s, False⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - obtain h l sh where [simp]: "s = (h, l, sh)"by(cases s) simp show ?thesis proof(cases b) case True thenshow ?thesis using assms by simp (rule RedSFAcc[THEN r_into_rtrancl]) next case False let ?b = "(C∙sF{D},s,True)" have"(?a, ?b) ∈ (red P)*" using False SFAccInitDoneRed[where sh="shp s", OF cF shp] by fastforce alsohave"(?b, ?c) ∈ (red P)*"by(rule SFAccReds[OF assms]) ultimatelyshow ?thesis by simp qed qed (*>*)
lemma SFAccInitReds: assumes cF: "P ⊨ C has F,Static:t in D" and nDone: "∄sfs. shp s D = Some (sfs,Done)" and INIT_steps: "P ⊨⟨INIT D ([D],False) ← unit,s,False⟩→* ⟨Val v',s',b'⟩" and shp': "shp s' D = Some (sfs,i)"and sfs: "sfs F = Some v" shows"P ⊨⟨C∙sF{D},s,False⟩→* ⟨Val v,s',False⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(INIT D ([D],False) ← C∙sF{D},s,False)" let ?b' = "(C∙sF{D},s',icheck P D (C∙sF{D}::expr))" obtain h l sh where [simp]: "s = (h, l, sh)"by(cases s) simp obtain h' l' sh' where [simp]: "s' = (h', l', sh')"by(cases s') simp have icheck: "icheck P D (C∙sF{D}) = True"using cF by fastforce thenhave b'c: "(?b', ?c) ∈ (red P)*" using RedSFAcc[THEN r_into_rtrancl, OF cF] shp' sfs by simp have"(?a, ?b) ∈ (red P)"using SFAccInitRed[OF cF] nDone by simp alsohave"(?b, ?c) ∈ (red P)*" by(rule InitSeqReds[OF INIT_steps b'c]) simp ultimatelyshow ?thesis by simp qed (*>*)
lemma SFAccInitThrowReds: "[ P ⊨ C has F,Static:t in D; ∄sfs. shp s D = Some (sfs,Done); P ⊨⟨INIT D ([D],False) ← unit,s,False⟩→* ⟨throw a,s',b'⟩] ==> P ⊨⟨C∙sF{D},s,False⟩→* ⟨throw a,s',b'⟩" (*<*) by(cases s, simp)
(auto elim: converse_rtrancl_into_rtrancl[OF SFAccInitRed InitSeqThrowReds]) (*>*)
subsubsection"FAss"
lemma FAssReds1: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨e∙F{D}:=e2, s,b⟩→* ⟨e'∙F{D}:=e2, s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) FAssRed1[OF step(2)]]) qed (*>*)
lemma FAssReds2: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨Val v∙F{D}:=e, s,b⟩→* ⟨Val v∙F{D}:=e', s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) FAssRed2[OF step(2)]]) qed (*>*)
lemma FAssRedsVal: assumes e1_steps: "P ⊨⟨e1,s0,b0⟩→* ⟨addr a,s1,b1⟩" and e2_steps: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2,l2,sh2),b2⟩" and cF: "P ⊨ C has F,NonStatic:t in D"and hC: "Some(C,fs) = h2 a" shows"P ⊨⟨e1∙F{D}:=e2, s0, b0⟩→* ⟨unit, (h2(a↦(C,fs((F,D)↦v))),l2,sh2),b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙F{D}:=e2, s1, b1)" let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)" have"(?x, ?y) ∈ (red P)*"by(rule FAssReds1[OF e1_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule FAssReds2[OF e2_steps]) alsohave"(?y', ?z) ∈ (red P)"using RedFAss[OF cF] hC by simp ultimatelyshow ?thesis by simp qed (*>*)
lemma FAssRedsNone: assumes e1_steps: "P ⊨⟨e1,s0,b0⟩→* ⟨addr a,s1,b1⟩" and e2_steps: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2,l2,sh2),b2⟩" and hC: "h2 a = Some(C,fs)"and ncF: "¬(∃b t. P ⊨ C has F,b:t in D)" shows"P ⊨⟨e1∙F{D}:=e2, s0, b0⟩→* ⟨THROW NoSuchFieldError, (h2,l2,sh2), b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙F{D}:=e2, s1, b1)" let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)" have"(?x, ?y) ∈ (red P)*"by(rule FAssReds1[OF e1_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule FAssReds2[OF e2_steps]) alsohave"(?y', ?z) ∈ (red P)" using RedFAssNone[OF _ ncF] hC by simp ultimatelyshow ?thesis by simp qed (*>*)
lemma FAssRedsStatic: assumes e1_steps: "P ⊨⟨e1,s0,b0⟩→* ⟨addr a,s1,b1⟩" and e2_steps: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2,l2,sh2),b2⟩" and hC: "h2 a = Some(C,fs)"and cF_Static: "P ⊨ C has F,Static:t in D" shows"P ⊨⟨e1∙F{D}:=e2, s0, b0⟩→* ⟨THROW IncompatibleClassChangeError, (h2,l2,sh2), b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙F{D}:=e2, s1, b1)" let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)" have"(?x, ?y) ∈ (red P)*"by(rule FAssReds1[OF e1_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule FAssReds2[OF e2_steps]) alsohave"(?y', ?z) ∈ (red P)" using RedFAssStatic[OF _ cF_Static] hC by simp ultimatelyshow ?thesis by simp qed (*>*)
subsubsection"SFAss"
lemma SFAssReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨C∙sF{D}:=e,s,b⟩→* ⟨C∙sF{D}:=e',s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) SFAssRed[OF step(2)]]) qed (*>*)
lemma SFAssRedsVal: assumes e2_steps: "P ⊨⟨e2,s0,b0⟩→* ⟨Val v,(h2,l2,sh2),b2⟩" and cF: "P ⊨ C has F,Static:t in D" and shD: "sh2 D = ⌊(sfs,Done)⌋" shows"P ⊨⟨C∙sF{D}:=e2, s0, b0⟩→* ⟨unit, (h2,l2,sh2(D↦(sfs(F↦v), Done))),False⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(C∙sF{D}:=Val v::expr, (h2,l2,sh2), b2)" have"(?a, ?b) ∈ (red P)*"by(rule SFAssReds[OF e2_steps]) alsohave"(?b, ?c) ∈ (red P)*"proof(cases b2) case True thenshow ?thesis using RedSFAss[THEN r_into_rtrancl, OF cF] shD by simp next case False let ?b' = "(C∙sF{D}:=Val v::expr, (h2,l2,sh2), True)" have"(?b, ?b') ∈ (red P)*" using False SFAssInitDoneRed[THEN converse_rtrancl_into_rtrancl, OF cF] shD by simp alsohave"(?b', ?c) ∈ (red P)*" using RedSFAss[THEN r_into_rtrancl, OF cF] shD by simp ultimatelyshow ?thesis by simp qed ultimatelyshow ?thesis by simp qed (*>*)
lemma SFAssRedsThrow: "[ P ⊨⟨e2,s0,b0⟩→* ⟨throw e,s2,b2⟩] ==> P ⊨⟨C∙sF{D}:=e2,s0,b0⟩→* ⟨throw e,s2,b2⟩" (*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SFAssThrow])(*>*)
lemma SFAssRedsNone: "[ P ⊨⟨e2,s0,b0⟩→* ⟨Val v,(h2,l2,sh2),b2⟩; ¬(∃b t. P ⊨ C has F,b:t in D) ]==> P ⊨⟨C∙sF{D}:=e2,s0,b0⟩→* ⟨THROW NoSuchFieldError, (h2,l2,sh2),False⟩" (*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNone])(*>*)
lemma SFAssRedsNonStatic: "[ P ⊨⟨e2,s0,b0⟩→* ⟨Val v,(h2,l2,sh2),b2⟩; P ⊨ C has F,NonStatic:t in D ]==> P ⊨⟨C∙sF{D}:=e2,s0,b0⟩→* ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2),False⟩" (*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNonStatic])(*>*)
lemma SFAssInitReds: assumes e2_steps: "P ⊨⟨e2,s0,b0⟩→* ⟨Val v,(h2,l2,sh2),False⟩" and cF: "P ⊨ C has F,Static:t in D" and nDone: "∄sfs. sh2 D = Some (sfs, Done)" and INIT_steps: "P ⊨⟨INIT D ([D],False) ← unit,(h2,l2,sh2),False⟩→* ⟨Val v',(h',l',sh'),b'⟩" and sh'D: "sh' D = Some(sfs,i)" and sfs': "sfs' = sfs(F↦v)"and sh'': "sh'' = sh'(D↦(sfs',i))" shows"P ⊨⟨C∙sF{D}:=e2,s0,b0⟩→* ⟨unit,(h',l',sh''),False⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(C∙sF{D} := Val v::expr,(h2, l2, sh2),False)" let ?y' = "(INIT D ([D],False) ← C∙sF{D} := Val v::expr,(h2, l2, sh2),False)" let ?y'' = "(C∙sF{D} := Val v::expr,(h', l', sh'),icheck P D (C∙sF{D} := Val v::expr))" have icheck: "icheck P D (C∙sF{D} := Val v::expr)"using cF by fastforce thenhave y''z: "(?y'',?z) ∈ (red P)" using RedSFAss[OF cF _ sfs' sh''] sh'D by simp have"(?x, ?y) ∈ (red P)*"by(rule SFAssReds[OF e2_steps]) alsohave"(?y, ?y') ∈ (red P)*" using SFAssInitRed[THEN converse_rtrancl_into_rtrancl, OF cF] nDone by simp alsohave"(?y', ?z) ∈ (red P)*" using InitSeqReds[OF INIT_steps y''z[THEN r_into_rtrancl]] by simp ultimatelyshow ?thesis by simp qed (*>*)
lemma SFAssInitThrowReds: assumes e2_steps: "P ⊨⟨e2,s0,b0⟩→* ⟨Val v,(h2,l2,sh2),False⟩" and cF: "P ⊨ C has F,Static:t in D" and nDone: "∄sfs. sh2 D = Some (sfs, Done)" and INIT_steps: "P ⊨⟨INIT D ([D],False) ← unit,(h2,l2,sh2),False⟩→* ⟨throw a,s',b'⟩" shows"P ⊨⟨C∙sF{D}:=e2,s0,b0⟩→* ⟨throw a,s',b'⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(C∙sF{D} := Val v::expr,(h2, l2, sh2),False)" let ?y' = "(INIT D ([D],False) ← C∙sF{D} := Val v::expr,(h2, l2, sh2),False)" have"(?x, ?y) ∈ (red P)*"by(rule SFAssReds[OF e2_steps]) alsohave"(?y, ?y') ∈ (red P)*" using SFAssInitRed[THEN converse_rtrancl_into_rtrancl, OF cF] nDone by simp alsohave"(?y', ?z) ∈ (red P)*" using InitSeqThrowReds[OF INIT_steps] by simp ultimatelyshow ?thesis by simp qed (*>*)
subsubsection";;"
lemma SeqReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨e;;e2, s,b⟩→* ⟨e';;e2, s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) SeqRed[OF step(2)]]) qed (*>*)
lemma SeqRedsThrow: "P ⊨⟨e,s,b⟩→* ⟨throw e',s',b'⟩==> P ⊨⟨e;;e2, s,b⟩→* ⟨throw e', s',b'⟩" (*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*)
lemma WhileTReds: assumes b_steps: "P ⊨⟨b,s0,b0⟩→* ⟨true,s1,b1⟩" and c_steps: "P ⊨⟨c,s1,b1⟩→* ⟨Val v1,s2,b2⟩" and while_steps: "P ⊨⟨while (b) c,s2,b2⟩→* ⟨e,s3,b3⟩" shows"P ⊨⟨while (b) c,s0,b0⟩→* ⟨e,s3,b3⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(if (b) (c;; while (b) c) else unit,s0,b0)" let ?y = "(if (true) (c;; while (b) c) else unit,s1,b1)" let ?b' = "(c;; while (b) c,s1,b1)" let ?y' = "(Val v1;; while (b) c,s2,b2)" have"(?a, ?b) ∈ (red P)*" using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp alsohave"(?b, ?y) ∈ (red P)*"by(rule CondReds[OF b_steps]) alsohave"(?y, ?b') ∈ (red P)*" using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp alsohave"(?b', ?y') ∈ (red P)*"by(rule SeqReds[OF c_steps]) alsohave"(?y', ?c) ∈ (red P)*" by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF while_steps]) ultimatelyshow ?thesis by simp qed (*>*)
lemma WhileTRedsThrow: assumes b_steps: "P ⊨⟨b,s0,b0⟩→* ⟨true,s1,b1⟩" and c_steps: "P ⊨⟨c,s1,b1⟩→* ⟨throw e,s2,b2⟩" shows"P ⊨⟨while (b) c,s0,b0⟩→* ⟨throw e,s2,b2⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(if (b) (c;; while (b) c) else unit,s0,b0)" let ?y = "(if (true) (c;; while (b) c) else unit,s1,b1)" let ?b' = "(c;; while (b) c,s1,b1)" let ?y' = "(throw e;; while (b) c,s2,b2)" have"(?a, ?b) ∈ (red P)*" using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp alsohave"(?b, ?y) ∈ (red P)*"by(rule CondReds[OF b_steps]) alsohave"(?y, ?b') ∈ (red P)*" using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp alsohave"(?b', ?y') ∈ (red P)*"by(rule SeqReds[OF c_steps]) alsohave"(?y', ?c) ∈ (red P)"by(rule red_reds.SeqThrow) ultimatelyshow ?thesis by simp qed (*>*)
subsubsection"Throw"
lemma ThrowReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨throw e,s,b⟩→* ⟨throw e',s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ThrowRed[OF step(2)]]) qed (*>*)
lemma ThrowRedsNull: "P ⊨⟨e,s,b⟩→* ⟨null,s',b'⟩==> P ⊨⟨throw e,s,b⟩→* ⟨THROW NullPointer,s',b'⟩" (*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ RedThrowNull])(*>*)
lemma ThrowRedsThrow: "P ⊨⟨e,s,b⟩→* ⟨throw a,s',b'⟩==> P ⊨⟨throw e,s,b⟩→* ⟨throw a,s',b'⟩" (*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ red_reds.ThrowThrow])(*>*)
subsubsection"InitBlock"
lemma InitBlockReds_aux: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> ∀h l sh h' l' sh' v. s = (h,l(V↦v),sh) ⟶ s' = (h',l',sh') ⟶ P ⊨⟨{V:T := Val v; e},(h,l,sh),b⟩→* ⟨{V:T := Val(the(l' V)); e'},(h',l'(V:=(l V)),sh'),b'⟩" (*<*) proof(induct rule: converse_rtrancl_induct3) case refl thenshow ?case by(fastforce simp: fun_upd_same simp del:fun_upd_apply) next case (step e0 s0 b0 e1 s1 b1) obtain h1 l1 sh1 where s1[simp]: "s1 = (h1, l1, sh1)"by(cases s1) simp
{ fix h0 l0 sh0 h2 l2 sh2 v0 assume [simp]: "s0 = (h0, l0(V ↦ v0), sh0)"and s'[simp]: "s' = (h2, l2, sh2)" thenhave"V ∈ dom l1"using step(1) by(auto dest!: red_lcl_incr) thenobtain v1 where l1V[simp]: "l1 V = ⌊v1⌋"by blast
let ?a = "({V:T; V:=Val v0;; e0},(h0, l0, sh0),b0)" let ?b = "({V:T; V:=Val v1;; e1},(h1, l1(V := l0 V), sh1),b1)" let ?c = "({V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l0 V), sh2),b')" let ?l = "l1(V := l0 V)"and ?v = v1
have e0_steps: "P ⊨⟨e0,(h0, l0(V ↦ v0), sh0),b0⟩→⟨e1,(h1, l1, sh1),b1⟩" using step(1) by simp
have lv: "∧l v. l1 = l(V ↦ v) ⟶ P ⊨⟨{V:T; V:=Val v;; e1},(h1, l, sh1),b1⟩→* ⟨{V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l V), sh2),b'⟩" using step(3) s' s1 by blast moreoverhave"l1 = ?l(V ↦ ?v)"by(rule ext) (simp add:fun_upd_def) ultimatelyhave"(?b, ?c) ∈ (red P)*"using lv[of ?l ?v] by simp thenhave"(?a, ?c) ∈ (red P)*" by(rule InitBlockRed[THEN converse_rtrancl_into_rtrancl, OF e0_steps l1V])
} thenshow ?caseby blast qed (*>*)
lemma InitBlockRedsFinal: "[ P ⊨⟨e,(h,l(V↦v),sh),b⟩→* ⟨e',(h',l',sh'),b'⟩; final e' ]==> P ⊨⟨{V:T := Val v; e},(h,l,sh),b⟩→* ⟨e',(h', l'(V := l V),sh'),b'⟩" (*<*) by(fast elim!:InitBlockReds[THEN rtrancl_into_rtrancl] finalE
intro:RedInitBlock InitBlockThrow) (*>*)
lemma BlockRedsFinal: assumes reds: "P ⊨⟨e0,s0,b0⟩→* ⟨e2,(h2,l2,sh2),b2⟩"and fin: "final e2" shows"∧h0 l0 sh0. s0 = (h0,l0(V:=None),sh0) ==> P ⊨⟨{V:T; e0},(h0,l0,sh0),b0⟩→* ⟨e2,(h2,l2(V:=l0 V),sh2),b2⟩" (*<*) using reds proof (induct rule:converse_rtrancl_induct3) case refl thus ?case by(fastforce intro:finalE[OF fin] RedBlock BlockThrow
simp del:fun_upd_apply) next case (step e0 s0 b0 e1 s1 b1) have red: "P ⊨⟨e0,s0,b0⟩→⟨e1,s1,b1⟩" and reds: "P ⊨⟨e1,s1,b1⟩→* ⟨e2,(h2,l2,sh2),b2⟩" and IH: "∧h l sh. s1 = (h,l(V := None),sh) ==> P ⊨⟨{V:T; e1},(h,l,sh),b1⟩→* ⟨e2,(h2, l2(V := l V),sh2),b2⟩" and s0: "s0 = (h0, l0(V := None),sh0)"by fact+ obtain h1 l1 sh1where s1: "s1 = (h1,l1,sh1)" using prod_cases3 by blast show ?case proof cases assume"assigned V e0" thenobtain v e where e0: "e0 = V := Val v;; e" by (unfold assigned_def)blast from red e0 s0have e1: "e1 = unit;;e"and s1: "s1 = (h0, l0(V ↦ v),sh0)"and b1: "b1 = b0" by auto from e1 fin have"e1≠ e2"by (auto simp:final_def) thenobtain e' s' b' where red1: "P ⊨⟨e1,s1,b1⟩→⟨e',s',b'⟩" and reds': "P ⊨⟨e',s',b'⟩→* ⟨e2,(h2,l2,sh2),b2⟩" using converse_rtranclE3[OF reds] by blast from red1 e1 b1have es': "e' = e""s' = s1""b' = b0"by auto show ?caseusing e0 s1 es' reds' by(auto intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply) next assume unass: "¬ assigned V e0" show ?thesis proof (cases "l1 V") assume None: "l1 V = None" hence"P ⊨⟨{V:T; e0},(h0,l0,sh0),b0⟩→⟨{V:T; e1},(h1, l1(V := l0 V),sh1),b1⟩" using s0 s1 red by(simp add: BlockRedNone[OF _ _ unass]) moreover have"P ⊨⟨{V:T; e1},(h1, l1(V := l0 V),sh1),b1⟩→* ⟨e2,(h2, l2(V := l0 V),sh2),b2⟩" using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem) ultimatelyshow ?caseby(rule converse_rtrancl_into_rtrancl) next fix v assume Some: "l1 V = Some v" hence"P ⊨⟨{V:T;e0},(h0,l0,sh0),b0⟩→⟨{V:T := Val v; e1},(h1,l1(V := l0 V),sh1),b1⟩" using s0 s1 red by(simp add: BlockRedSome[OF _ _ unass]) moreover have"P ⊨⟨{V:T := Val v; e1},(h1,l1(V:= l0 V),sh1),b1⟩→* ⟨e2,(h2,l2(V:=l0 V),sh2),b2⟩" using InitBlockRedsFinal[OF _ fin,of _ _ "l1(V:=l0 V)" V]
Some reds s1by(simp add:fun_upd_idem) ultimatelyshow ?caseby(rule converse_rtrancl_into_rtrancl) qed qed qed (*>*)
subsubsection"try-catch"
lemma TryReds: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨try e catch(C V) e2,s,b⟩→* ⟨try e' catch(C V) e2,s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) TryRed[OF step(2)]]) qed (*>*)
lemma TryRedsVal: "P ⊨⟨e,s,b⟩→* ⟨Val v,s',b'⟩==> P ⊨⟨try e catch(C V) e2,s,b⟩→* ⟨Val v,s',b'⟩" (*<*)by(rule TryReds[THEN rtrancl_into_rtrancl, OF _ RedTry])(*>*)
lemma TryCatchRedsFinal: assumes e1_steps: "P ⊨⟨e1,s0,b0⟩→* ⟨Throw a,(h1,l1,sh1),b1⟩" and h1a: "h1 a = Some(D,fs)"and sub: "P ⊨ D ⪯* C" and e2_steps: "P ⊨⟨e2, (h1, l1(V ↦ Addr a),sh1),b1⟩→* ⟨e2', (h2,l2,sh2), b2⟩" and final: "final e2'" shows"P ⊨⟨try e1 catch(C V) e2, s0, b0⟩→* ⟨e2', (h2, (l2::locals)(V := l1 V),sh2),b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(try Throw a catch(C V) e2,(h1, l1, sh1),b1)" let ?b = "({V:Class C; V:=addr a;; e2},(h1, l1, sh1),b1)" have bz: "(?b, ?z) ∈ (red P)*" by(rule InitBlockRedsFinal[OF e2_steps final]) have hp: "hp (h1, l1, sh1) a = ⌊(D, fs)⌋"using h1a by simp have"(?x, ?y) ∈ (red P)*"by(rule TryReds[OF e1_steps]) alsohave"(?y, ?z) ∈ (red P)*" by(rule RedTryCatch[THEN converse_rtrancl_into_rtrancl, OF hp sub bz]) ultimatelyshow ?thesis by simp qed (*>*)
lemma TryRedsFail: "[ P ⊨⟨e1,s,b⟩→* ⟨Throw a,(h,l,sh),b'⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯* C ] ==> P ⊨⟨try e1 catch(C V) e2,s,b⟩→* ⟨Throw a,(h,l,sh),b'⟩" (*<*)by(fastforce intro!: TryReds[THEN rtrancl_into_rtrancl, OF _ RedTryFail])(*>*)
subsubsection"List"
lemma ListReds1: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨e#es,s,b⟩ [→]* ⟨e' # es,s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ListRed1[OF step(2)]]) qed (*>*)
lemma ListReds2: "P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩==> P ⊨⟨Val v # es,s,b⟩ [→]* ⟨Val v # es',s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ListRed2[OF step(2)]]) qed (*>*)
lemma ListRedsVal: "[ P ⊨⟨e,s0,b0⟩→* ⟨Val v,s1,b1⟩; P ⊨⟨es,s1,b1⟩ [→]* ⟨es',s2,b2⟩] ==> P ⊨⟨e#es,s0,b0⟩ [→]* ⟨Val v # es',s2,b2⟩" (*<*)by(rule rtrancl_trans[OF ListReds1 ListReds2])(*>*)
subsubsection"Call"
text‹ First a few lemmas on what happens to free variables during redction. ›
lemmaassumes wf: "wwf_J_prog P" shows Red_fv: "P ⊨⟨e,(h,l,sh),b⟩→⟨e',(h',l',sh'),b'⟩==> fv e' ⊆ fv e" and"P ⊨⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩==> fvs es' ⊆ fvs es" (*<*) proof (induct rule:red_reds_inducts) case (RedCall h a C fs M Ts T pns body D vs l sh b) hence"fv body ⊆ {this} ∪ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def) with RedCall.hyps show ?caseby fastforce next case (RedSCall C M Ts T pns body D vs) hence"fv body ⊆ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def) with RedSCall.hyps show ?caseby fastforce qed auto (*>*)
lemma Red_dom_lcl: "P ⊨⟨e,(h,l,sh),b⟩→⟨e',(h',l',sh'),b'⟩==> dom l' ⊆ dom l ∪ fv e"and "P ⊨⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩==> dom l' ⊆ dom l ∪ fvs es" (*<*) proof (induct rule:red_reds_inducts) case RedLAss thus ?caseby(force split:if_splits) next case CallParams thus ?caseby(force split:if_splits) next case BlockRedNone thus ?caseby clarsimp (fastforce split:if_splits) next case BlockRedSome thus ?caseby clarsimp (fastforce split:if_splits) next case InitBlockRed thus ?caseby clarsimp (fastforce split:if_splits) qed auto (*>*)
lemma Reds_dom_lcl: assumes wf: "wwf_J_prog P" shows"P ⊨⟨e,(h,l,sh),b⟩→* ⟨e',(h',l',sh'),b'⟩==> dom l' ⊆ dom l ∪ fv e" (*<*) proof(induct rule: converse_rtrancl_induct_red) case1thenshow ?caseby blast next case2thenshow ?caseusing wf by(blast dest: Red_fv Red_dom_lcl) qed (*>*)
text‹ Now a few lemmas on the behaviour of blocks during reduction. ›
lemma override_on_upd_lemma: "(override_on f (g(a↦b)) A)(a := g a) = override_on f g (insert a A)" (*<*)by(rule ext) (simp add:override_on_def)
lemma blocksReds: "∧l. [ length Vs = length Ts; length vs = length Ts; distinct Vs; P ⊨⟨e, (h,l(Vs [↦] vs),sh),b⟩→* ⟨e', (h',l',sh'),b'⟩] ==> P ⊨⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩→* ⟨blocks(Vs,Ts,map (the ∘ l') Vs,e'), (h',override_on l' l (set Vs),sh'),b'⟩" (*<*) proof(induct Vs Ts vs e rule:blocks_induct) case (1 V Vs T Ts v vs e) show ?case using InitBlockReds[OF "1.hyps"[of "l(V↦v)"]] "1.prems" by(auto simp:override_on_upd_lemma) qed auto (*>*)
lemma blocksFinal: "∧l. [ length Vs = length Ts; length vs = length Ts; final e ]==> P ⊨⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩→* ⟨e, (h,l,sh),b⟩" (*<*) proof(induct Vs Ts vs e rule:blocks_induct) case1 show ?caseusing"1.prems" InitBlockReds[OF "1.hyps"] by(fastforce elim!:finalE elim: rtrancl_into_rtrancl[OF _ RedInitBlock]
rtrancl_into_rtrancl[OF _ InitBlockThrow]) qed auto (*>*)
lemma blocksRedsFinal: assumes wf: "length Vs = length Ts""length vs = length Ts""distinct Vs" and reds: "P ⊨⟨e, (h,l(Vs [↦] vs),sh),b⟩→* ⟨e', (h',l',sh'),b'⟩" and fin: "final e'"and l'': "l'' = override_on l' l (set Vs)" shows"P ⊨⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩→* ⟨e', (h',l'',sh'),b'⟩" (*<*) proof - let ?bv = "blocks(Vs,Ts,map (the o l') Vs,e')" have"P ⊨⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩→* ⟨?bv, (h',l'',sh'),b'⟩" using l'' by simp (rule blocksReds[OF wf reds]) alsohave"P ⊨⟨?bv, (h',l'',sh'),b'⟩→* ⟨e', (h',l'',sh'),b'⟩" using wf by(fastforce intro:blocksFinal fin) finallyshow ?thesis . qed (*>*)
text‹ An now the actual method call reduction lemmas. ›
lemma CallRedsObj: "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩==> P ⊨⟨e∙M(es),s,b⟩→* ⟨e'∙M(es),s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CallObj[OF step(2)]]) qed (*>*)
lemma CallRedsParams: "P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩==> P ⊨⟨(Val v)∙M(es),s,b⟩→* ⟨(Val v)∙M(es'),s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CallParams[OF step(2)]]) qed (*>*)
lemma CallRedsFinal: assumes wwf: "wwf_J_prog P" and"P ⊨⟨e,s0,b0⟩→* ⟨addr a,s1,b1⟩" "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩" "h2 a = Some(C,fs)""P ⊨ C sees M,NonStatic:Ts→T = (pns,body) in D" "size vs = size pns" and l2': "l2' = [this ↦ Addr a, pns[↦]vs]" and body: "P ⊨⟨body,(h2,l2',sh2),b2⟩→* ⟨ef,(h3,l3,sh3),b3⟩" and"final ef" shows"P ⊨⟨e∙M(es), s0,b0⟩→* ⟨ef,(h3,l2,sh3),b3⟩" (*<*) proof - have wf: "size Ts = size pns ∧ distinct pns ∧ this ∉ set pns" and wt: "fv body ⊆ {this} ∪ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ from body[THEN Red_lcl_add, of l2] have body': "P ⊨⟨body,(h2,l2(this↦ Addr a, pns[↦]vs),sh2),b2⟩→* ⟨ef,(h3,l2++l3,sh3),b3⟩" by (simp add:l2') have"dom l3⊆ {this} ∪ set pns" using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force hence eql2: "override_on (l2++l3) l2 ({this} ∪ set pns) = l2" by(fastforce simp add:map_add_def override_on_def fun_eq_iff) have"P ⊨⟨e∙M(es),s0,b0⟩→* ⟨(addr a)∙M(es),s1,b1⟩"by(rule CallRedsObj)(rule assms(2)) alsohave"P ⊨⟨(addr a)∙M(es),s1,b1⟩→* ⟨(addr a)∙M(map Val vs),(h2,l2,sh2),b2⟩" by(rule CallRedsParams)(rule assms(3)) alsohave"P ⊨⟨(addr a)∙M(map Val vs), (h2,l2,sh2),b2⟩→ ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2,sh2),b2⟩" by(rule RedCall)(auto simp: assms wf, rule assms(5)) also (rtrancl_into_rtrancl) have"P ⊨⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2,sh2),b2⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 ({this} ∪ set pns),sh3),b3⟩" by(rule blocksRedsFinal, insert assms wf body', simp_all) finallyshow ?thesis using eql2by simp qed (*>*)
lemma CallRedsThrowParams: assumes e_steps: "P ⊨⟨e,s0,b0⟩→* ⟨Val v,s1,b1⟩" and es_steps: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs1 @ throw a # es2,s2,b2⟩" shows"P ⊨⟨e∙M(es),s0,b0⟩→* ⟨throw a,s2,b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v∙M(es),s1,b1)" let ?y' = "(Val v∙M(map Val vs1 @ throw a # es2),s2,b2)" have"(?x, ?y) ∈ (red P)*"by(rule CallRedsObj[OF e_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule CallRedsParams[OF es_steps]) alsohave"(?y', ?z) ∈ (red P)*"using CallThrowParams by fast ultimatelyshow ?thesis by simp qed (*>*)
lemma CallRedsThrowObj: "P ⊨⟨e,s0,b0⟩→* ⟨throw a,s1,b1⟩==> P ⊨⟨e∙M(es),s0,b0⟩→* ⟨throw a,s1,b1⟩" (*<*)by(rule CallRedsObj[THEN rtrancl_into_rtrancl, OF _ CallThrowObj])(*>*)
lemma CallRedsNull: assumes e_steps: "P ⊨⟨e,s0,b0⟩→* ⟨null,s1,b1⟩" and es_steps: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩" shows"P ⊨⟨e∙M(es),s0,b0⟩→* ⟨THROW NullPointer,s2,b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(null∙M(es),s1,b1)" let ?y' = "(null∙M(map Val vs),s2,b2)" have"(?x, ?y) ∈ (red P)*"by(rule CallRedsObj[OF e_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule CallRedsParams[OF es_steps]) alsohave"(?y', ?z) ∈ (red P)"by(rule RedCallNull) ultimatelyshow ?thesis by simp qed (*>*)
lemma CallRedsNone: assumes e_steps: "P ⊨⟨e,s,b⟩→* ⟨addr a,s1,b1⟩" and es_steps: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩" and hp2a: "hp s2 a = Some(C,fs)" and ncM: "¬(∃b Ts T m D. P ⊨ C sees M,b:Ts→T = m in D)" shows"P ⊨⟨e∙M(es),s,b⟩→* ⟨THROW NoSuchMethodError,s2,b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙M(es),s1,b1)" let ?y' = "(addr a∙M(map Val vs),s2,b2)" have"(?x, ?y) ∈ (red P)*"by(rule CallRedsObj[OF e_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule CallRedsParams[OF es_steps]) alsohave"(?y', ?z) ∈ (red P)"using RedCallNone[OF _ ncM] hp2a by(cases s2) simp ultimatelyshow ?thesis by simp qed (*>*)
lemma CallRedsStatic: assumes e_steps: "P ⊨⟨e,s,b⟩→* ⟨addr a,s1,b1⟩" and es_steps: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩" and hp2a: "hp s2 a = Some(C,fs)" and cM_Static: "P ⊨ C sees M,Static:Ts→T = m in D" shows"P ⊨⟨e∙M(es),s,b⟩→* ⟨THROW IncompatibleClassChangeError,s2,b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙M(es),s1,b1)" let ?y' = "(addr a∙M(map Val vs),s2,b2)" have"(?x, ?y) ∈ (red P)*"by(rule CallRedsObj[OF e_steps]) alsohave"(?y, ?y') ∈ (red P)*"by(rule CallRedsParams[OF es_steps]) alsohave"(?y', ?z) ∈ (red P)"using RedCallStatic[OF _ cM_Static] hp2a by(cases s2) simp ultimatelyshow ?thesis by simp qed (*>*)
subsection‹SCall›
lemma SCallRedsParams: "P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩==> P ⊨⟨C∙sM(es),s,b⟩→* ⟨C∙sM(es'),s',b'⟩" (*<*) proof(induct rule: rtrancl_induct3) case refl show ?caseby blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) SCallParams[OF step(2)]]) qed (*>*)
lemma SCallRedsFinal: assumes wwf: "wwf_J_prog P" and"P ⊨⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩" "P ⊨ C sees M,Static:Ts→T = (pns,body) in D" "sh2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh2 D = ⌊(sfs, Processing)⌋)" "size vs = size pns" and l2': "l2' = [pns[↦]vs]" and body: "P ⊨⟨body,(h2,l2',sh2),False⟩→* ⟨ef,(h3,l3,sh3),b3⟩" and"final ef" shows"P ⊨⟨C∙sM(es), s0,b0⟩→* ⟨ef,(h3,l2,sh3),b3⟩" (*<*) proof - have wf: "size Ts = size pns ∧ distinct pns" and wt: "fv body ⊆ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ from body[THEN Red_lcl_add, of l2] have body': "P ⊨⟨body,(h2,l2(pns[↦]vs),sh2),False⟩→* ⟨ef,(h3,l2++l3,sh3),b3⟩" by (simp add:l2') have"dom l3⊆ set pns" using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force hence eql2: "override_on (l2++l3) l2 (set pns) = l2" by(fastforce simp add:map_add_def override_on_def fun_eq_iff) have b2T: "P ⊨⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩→* ⟨C∙sM(map Val vs), (h2,l2,sh2),True⟩" proof(cases b2) case True thenshow ?thesis by simp next case False thenshow ?thesis using assms(3,4) by(auto elim: SCallInitDoneRed) qed have"P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨C∙sM(map Val vs),(h2,l2,sh2),b2⟩" by(rule SCallRedsParams)(rule assms(2)) alsohave"P ⊨⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩→* ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩" by(auto intro!: rtrancl_into_rtrancl[OF b2T] RedSCall assms(3) simp: assms wf) also (rtrancl_trans) have"P ⊨⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩" by(rule blocksRedsFinal, insert assms wf body', simp_all) finallyshow ?thesis using eql2by simp qed (*>*)
lemma SCallRedsThrowParams: "[ P ⊨⟨es,s0,b0⟩ [→]* ⟨map Val vs1 @ throw a # es2,s2,b2⟩] ==> P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨throw a,s2,b2⟩" (*<*) by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ SCallThrowParams])
simp (*>*)
lemma SCallRedsNone: "[ P ⊨⟨es,s,b⟩ [→]* ⟨map Val vs,s2,False⟩; ¬(∃b Ts T m D. P ⊨ C sees M,b:Ts→T = m in D) ] ==> P ⊨⟨C∙sM(es),s,b⟩→* ⟨THROW NoSuchMethodError,s2,False⟩" (*<*) by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ RedSCallNone])
simp (*>*)
lemma SCallRedsNonStatic: "[ P ⊨⟨es,s,b⟩ [→]* ⟨map Val vs,s2,False⟩; P ⊨ C sees M,NonStatic:Ts→T = m in D ] ==> P ⊨⟨C∙sM(es),s,b⟩→* ⟨THROW IncompatibleClassChangeError,s2,False⟩" (*<*) by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ RedSCallNonStatic])
simp (*>*)
lemma SCallInitThrowReds: assumes wwf: "wwf_J_prog P" and"P ⊨⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h1,l1,sh1),False⟩" "P ⊨ C sees M,Static:Ts→T = (pns,body) in D" "∄sfs. sh1 D = Some(sfs,Done)" "M ≠ clinit" and"P ⊨⟨INIT D ([D],False) ← unit,(h1,l1,sh1),False⟩→* ⟨throw a,(h2,l2,sh2),b2⟩" shows"P ⊨⟨C∙sM(es), s0,b0⟩→* ⟨throw a,(h2,l2,sh2),b2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(C∙sM(map Val vs),(h1,l1,sh1),False)" let ?y' = "(INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False)" have"(?x, ?y) ∈ (red P)*"by(rule SCallRedsParams[OF assms(2)]) alsohave"(?y, ?y') ∈ (red P)*" using SCallInitRed[OF assms(3)] assms(4-5) by auto alsohave"(?y', ?z) ∈ (red P)*"by(rule InitSeqThrowReds[OF assms(6)]) finallyshow ?thesis by simp qed (*>*)
lemma SCallInitReds: assumes wwf: "wwf_J_prog P" and"P ⊨⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h1,l1,sh1),False⟩" "P ⊨ C sees M,Static:Ts→T = (pns,body) in D" "∄sfs. sh1 D = Some(sfs,Done)" "M ≠ clinit" and"P ⊨⟨INIT D ([D],False) ← unit,(h1,l1,sh1),False⟩→* ⟨Val v',(h2,l2,sh2),b2⟩" and"size vs = size pns" and l2': "l2' = [pns[↦]vs]" and body: "P ⊨⟨body,(h2,l2',sh2),False⟩→* ⟨ef,(h3,l3,sh3),b3⟩" and"final ef" shows"P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨ef,(h3,l2,sh3),b3⟩" (*<*) proof - have wf: "size Ts = size pns ∧ distinct pns" and wt: "fv body ⊆ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ from body[THEN Red_lcl_add, of l2] have body': "P ⊨⟨body,(h2,l2(pns[↦]vs),sh2),False⟩→* ⟨ef,(h3,l2++l3,sh3),b3⟩" by (simp add:l2') have"dom l3⊆ set pns" using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force hence eql2: "override_on (l2++l3) l2 (set pns) = l2" by(fastforce simp add:map_add_def override_on_def fun_eq_iff) have"icheck P D (C∙sM(map Val vs)::'a exp)"using assms(3) by auto thenhave"P ⊨⟨C∙sM(map Val vs),(h2, l2, sh2),icheck P D (C∙sM(map Val vs))⟩ →⟨blocks(pns, Ts, vs, body), (h2, l2, sh2), False⟩" by (metis (full_types) assms(3) assms(7) local.wf red_reds.RedSCall) alsohave"P ⊨⟨blocks(pns, Ts, vs, body), (h2, l2, sh2), False⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩" by(rule blocksRedsFinal, insert assms wf body', simp_all) finallyhave trueReds: "P ⊨⟨C∙sM(map Val vs),(h2, l2, sh2),icheck P D (C∙sM(map Val vs))⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩"by simp have"P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨C∙sM(map Val vs),(h1,l1,sh1),False⟩" by(rule SCallRedsParams)(rule assms(2)) alsohave"P ⊨⟨C∙sM(map Val vs),(h1,l1,sh1),False⟩→⟨INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False⟩" using SCallInitRed[OF assms(3)] assms(4-5) by auto also (rtrancl_into_rtrancl) have"P ⊨⟨INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩" using InitSeqReds[OF assms(6) trueReds] assms(5) by simp finallyshow ?thesis using eql2by simp qed (*>*)
lemma SCallInitProcessingReds: assumes wwf: "wwf_J_prog P" and"P ⊨⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩" "P ⊨ C sees M,Static:Ts→T = (pns,body) in D" "sh2 D = Some(sfs,Processing)" and"size vs = size pns" and l2': "l2' = [pns[↦]vs]" and body: "P ⊨⟨body,(h2,l2',sh2),False⟩→* ⟨ef,(h3,l3,sh3),b3⟩" and"final ef" shows"P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨ef,(h3,l2,sh3),b3⟩" (*<*) proof - have wf: "size Ts = size pns ∧ distinct pns" and wt: "fv body ⊆ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ from body[THEN Red_lcl_add, of l2] have body': "P ⊨⟨body,(h2,l2(pns[↦]vs),sh2),False⟩→* ⟨ef,(h3,l2++l3,sh3),b3⟩" by (simp add:l2') have"dom l3⊆ set pns" using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force hence eql2: "override_on (l2++l3) l2 (set pns) = l2" by(fastforce simp add:map_add_def override_on_def fun_eq_iff) have b2T: "P ⊨⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩→* ⟨C∙sM(map Val vs), (h2,l2,sh2),True⟩" proof(cases b2) case True thenshow ?thesis by simp next case False show ?thesis proof(cases "M = clinit") case True thenshow ?thesis using False assms(3) red_reds.SCallInitDoneRed assms(4) by (simp add: r_into_rtrancl) next case nclinit: False have icheck: "icheck P D (C∙sM(map Val vs))"using assms(3) by auto have"P ⊨⟨C∙sM(map Val vs),(h2, l2, sh2),b2⟩ →⟨INIT D ([D],False) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩" using SCallInitRed[OF assms(3)] assms(4) False nclinit by simp alsohave"P ⊨⟨INIT D ([D],False) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩ →⟨INIT D (Nil,True) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩" using RedInitProcessing assms(4) by simp alsohave"P ⊨⟨INIT D (Nil,True) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩ →⟨C∙sM(map Val vs),(h2, l2, sh2),True⟩" using RedInit[of "C∙sM(map Val vs)" D _ _ _ P] icheck nclinit by (metis (full_types) nsub_RI_Vals sub_RI.simps(12)) finallyshow ?thesis by simp qed qed have"P ⊨⟨C∙sM(es),s0,b0⟩→* ⟨C∙sM(map Val vs),(h2,l2,sh2),b2⟩" by(rule SCallRedsParams)(rule assms(2)) alsohave"P ⊨⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩→* ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩" by(auto intro!: rtrancl_into_rtrancl[OF b2T] RedSCall assms(3) simp: assms wf) also (rtrancl_trans) have"P ⊨⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩ →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩" by(rule blocksRedsFinal, insert assms wf body', simp_all) finallyshow ?thesis using eql2by simp qed (*>*)
(***********************************)
subsubsection"The main Theorem"
lemmaassumes wwf: "wwf_J_prog P" shows big_by_small: "P ⊨⟨e,s⟩==>⟨e',s'⟩ ==> (∧b. iconf (shp s) e ==> P,shp s ⊨b (e,b) √==> P ⊨⟨e,s,b⟩→* ⟨e',s',False⟩)" and bigs_by_smalls: "P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩ ==> (∧b. iconfs (shp s) es ==> P,shp s ⊨b (es,b) √==> P ⊨⟨es,s,b⟩ [→]* ⟨es',s',False⟩)" (*<*) proof (induct rule: eval_evals.inducts) case New show ?case proof(cases b) case True thenshow ?thesis using RedNew[OF New.hyps(2-4)] by auto next case False thenshow ?thesis using New.hyps(1) NewInitDoneReds[OF _ New.hyps(2-4)] by auto qed next case NewFail show ?case proof(cases b) case True thenshow ?thesis using RedNewFail[OF NewFail.hyps(2)] NewFail.hyps(3) by fastforce next case False thenshow ?thesis using NewInitDoneReds2[OF _ NewFail.hyps(2)] NewFail by fastforce qed next case (NewInit sh C h l v' h' l' sh' a FDTs h'') show ?case proof(cases b) case True thenobtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInit.hyps(1) NewInit.prems by(clarsimp simp: bconf_def initPD_def) thenhave s': "(h',l',sh') = (h,l,sh)"using NewInit.hyps(2) init_ProcessingE by clarsimp thenshow ?thesis using RedNew[OF NewInit.hyps(4-6)] True by auto next case False thenhave init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh),False⟩→* ⟨Val v',(h', l', sh'),False⟩" using NewInit.hyps(3) by(auto simp: bconf_def) thenshow ?thesis using NewInit NewInitReds[OF _ init NewInit.hyps(4-6)] False
has_fields_is_class[OF NewInit.hyps(5)] by auto qed next case (NewInitOOM sh C h l v' h' l' sh') show ?case proof(cases b) case True thenobtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInitOOM.hyps(1) NewInitOOM.prems by(clarsimp simp: bconf_def initPD_def) thenhave s': "(h',l',sh') = (h,l,sh)"using NewInitOOM.hyps(2) init_ProcessingE by clarsimp thenshow ?thesis using RedNewFail[OF NewInitOOM.hyps(4)] True r_into_rtrancl NewInitOOM.hyps(5) by auto next case False thenhave init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh),False⟩→* ⟨Val v',(h', l', sh'),False⟩" using NewInitOOM.hyps(3) by(auto simp: bconf_def) thenshow ?thesis using NewInitOOM.hyps(1) NewInitOOMReds[OF _ init NewInitOOM.hyps(4)] False
NewInitOOM.hyps(5) by auto qed next case (NewInitThrow sh C h l a s') show ?case proof(cases b) case True thenobtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInitThrow.hyps(1) NewInitThrow.prems by(clarsimp simp: bconf_def initPD_def) thenshow ?thesis using NewInitThrow.hyps(2) init_ProcessingE by blast next case False thenhave init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh),b⟩→* ⟨throw a,s',False⟩" using NewInitThrow.hyps(3) by(auto simp: bconf_def) thenshow ?thesis using NewInitThrow NewInitThrowReds[of "(h,l,sh)" C P a s'] False by auto qed next case Cast thenshow ?caseby(fastforce intro:CastRedsAddr) next case CastNull thenshow ?caseby(fastforce intro: CastRedsNull) next case CastFail thus ?caseby(fastforce intro!:CastRedsFail) next case CastThrow thus ?caseby(fastforce dest!:eval_final intro:CastRedsThrow) next case Val thenshow ?caseusing exI[of _ b] by(simp add: bconf_def) next case (BinOp e1 s0 v1 s1 e2 v2 s2 bop v) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None BinOp.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None BinOp.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v1,s1,False⟩"using iconf BinOp.hyps(2) by auto have binop: "P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨Val v1«bop¬ e2,s1,False⟩"by(rule BinOp1Reds[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf binop] None BinOp by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v2,s2,False⟩"using BinOp.hyps(4)[OF iconf2'] by auto thenshow ?thesis using BinOpRedsVal[OF b1 b2 BinOp.hyps(5)] by fast next case (Some a) thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v1,s1,b1⟩" by (metis (no_types, lifting) BinOp.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have binop: "P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨Val v1«bop¬ e2,s1,b1⟩"by(rule BinOp1Reds[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf binop] BinOp by auto have bconf2: "P,shp s0⊨b (e2,b) √"using BinOp.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf binop BinOp.prems] bysimp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v2,s2,False⟩"using BinOp.hyps(4)[OF iconf2'] by auto thenshow ?thesis using BinOpRedsVal[OF b1 b2 BinOp.hyps(5)] by fast qed next case (BinOpThrow1 e1 s0 e s1 bop e2) show ?case proof(cases "val_of e1") case None thenhave"iconf (shp s0) e1"and"P,shp s0⊨b (e1,b) √"using BinOpThrow1.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨throw e,s1,False⟩"using BinOpThrow1.hyps(2) by auto thenhave"P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨throw e,s1,False⟩" using BinOpThrow1 None by(auto dest!:eval_final simp: BinOpRedsThrow1[OF b1]) thenshow ?thesis by fast next case (Some a) thenshow ?thesis using eval_final_same[OF BinOpThrow1.hyps(1)] val_of_spec[OF Some] by auto qed next case (BinOpThrow2 e1 s0 v1 s1 e2 e s2 bop) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None BinOpThrow2.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None BinOpThrow2.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v1,s1,False⟩"using iconf BinOpThrow2.hyps(2) by auto have binop: "P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨Val v1«bop¬ e2,s1,False⟩"by(rule BinOp1Reds[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf binop] None BinOpThrow2 by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨throw e,s2,False⟩"using BinOpThrow2.hyps(4)[OF iconf2'] by auto thenshow ?thesis using BinOpRedsThrow2[OF b1 b2] by fast next case (Some a) thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v1,s1,b1⟩" by (metis (no_types, lifting) BinOpThrow2.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have binop: "P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨Val v1«bop¬ e2,s1,b1⟩"by(rule BinOp1Reds[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf binop] BinOpThrow2 by auto have bconf2: "P,shp s0⊨b (e2,b) √"using BinOpThrow2.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf binop BinOpThrow2.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨throw e,s2,False⟩"using BinOpThrow2.hyps(4)[OF iconf2'] by auto thenshow ?thesis using BinOpRedsThrow2[OF b1 b2] by fast qed next case Var thus ?caseby(auto dest:RedVar simp: bconf_def) next case LAss thus ?caseby(auto dest: LAssRedsVal) next case LAssThrow thus ?caseby(auto dest!:eval_final dest: LAssRedsThrow) next case FAcc thus ?caseby(fastforce intro:FAccRedsVal) next case FAccNull thus ?caseby(auto dest:FAccRedsNull) next case FAccThrow thus ?caseby(auto dest!:eval_final dest:FAccRedsThrow) next case FAccNone thenshow ?caseby(fastforce intro: FAccRedsNone) next case FAccStatic thenshow ?caseby(fastforce intro: FAccRedsStatic) next case SFAcc show ?case proof(cases b) case True thenshow ?thesis using RedSFAcc SFAcc.hyps by auto next case False thenshow ?thesis using SFAcc.hyps SFAccInitDoneReds[OF SFAcc.hyps(1)] by auto qed next case (SFAccInit C F t D sh h l v' h' l' sh' sfs i v) show ?case proof(cases b) case True thenobtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋" using SFAccInit.hyps(2) SFAccInit.prems by(clarsimp simp: bconf_def initPD_def) thenhave s': "(h',l',sh') = (h,l,sh)"using SFAccInit.hyps(3) init_ProcessingE by clarsimp thenshow ?thesis using RedSFAcc SFAccInit.hyps True by auto next case False thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh),False⟩→* ⟨Val v',(h', l', sh'),False⟩" using SFAccInit.hyps(4) by(auto simp: bconf_def) thenshow ?thesis using SFAccInit SFAccInitReds[OF _ _ init] False by auto qed next case (SFAccInitThrow C F t D sh h l a s') show ?case proof(cases b) case True thenobtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋" using SFAccInitThrow.hyps(2) SFAccInitThrow.prems(2) by(clarsimp simp: bconf_def initPD_def) thenshow ?thesis using SFAccInitThrow.hyps(3) init_ProcessingE by blast next case False thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh),b⟩→* ⟨throw a,s',False⟩" using SFAccInitThrow.hyps(4) by(auto simp: bconf_def) thenshow ?thesis using SFAccInitThrow SFAccInitThrowReds False by auto qed next case SFAccNone thenshow ?caseby(fastforce intro: SFAccRedsNone) next case SFAccNonStatic thenshow ?caseby(fastforce intro: SFAccRedsNonStatic) next case (FAss e1 s0 a s1 e2 v h2 l2 sh2 C fs F t D fs' h2') show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None FAss.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None FAss.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,False⟩"using iconf FAss.hyps(2) by auto have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,False⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] None FAss byauto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAss.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsVal[OF b1 b2 FAss.hyps(6) FAss.hyps(5)[THEN sym]] FAss.hyps(7,8) by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) FAss.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,b1⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] FAss by auto have bconf2: "P,shp s0⊨b (e2,b) √"using FAss.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf fass FAss.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAss.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsVal[OF b1 b2] FAss.hyps(5)[THEN sym] FAss.hyps(6-8) by fast qed next case (FAssNull e1 s0 s1 e2 v s2 F D) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using FAssNull.prems(1) by simp have bconf: "P,shp s0⊨b (e1,b) √"using FAssNull.prems(2) None by simp thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨null,s1,False⟩"using FAssNull.hyps(2)[OF iconf] by auto have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨null∙F{D} := e2,s1,False⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] None FAssNull by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,s2,False⟩"using FAssNull.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsNull[OF b1 b2] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨null,s1,b1⟩" by (metis (no_types, lifting) FAssNull.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨null∙F{D} := e2,s1,b1⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] FAssNull byauto have bconf2: "P,shp s0⊨b (e2,b) √"using FAssNull.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf fass FAssNull.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,s2,False⟩"using FAssNull.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsNull[OF b1 b2] by fast qed next case (FAssThrow1 e1 s0 e' s1 F D e2) show ?case proof(cases "val_of e1") case None thenhave"iconf (shp s0) e1"and"P,shp s0⊨b (e1,b) √"using FAssThrow1.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨throw e',s1,False⟩"using FAssThrow1.hyps(2) by auto thenhave"P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨throw e',s1,False⟩" using FAssThrow1 None by(auto dest!:eval_final simp: FAssRedsThrow1[OF b1]) thenshow ?thesis by fast next case (Some a) thenshow ?thesis using eval_final_same[OF FAssThrow1.hyps(1)] val_of_spec[OF Some] by auto qed next case (FAssThrow2 e1 s0 v s1 e2 e' s2 F D) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None FAssThrow2.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None FAssThrow2.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v,s1,False⟩"using iconf FAssThrow2.hyps(2) by auto have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨Val v∙F{D} := e2,s1,False⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] None FAssThrow2 by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨throw e',s2,False⟩"using FAssThrow2.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsThrow2[OF b1 b2] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨Val v,s1,b1⟩" by (metis (no_types, lifting) FAssThrow2.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨Val v∙F{D} := e2,s1,b1⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] FAssThrow2 by auto have bconf2: "P,shp s0⊨b (e2,b) √"using FAssThrow2.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf fass FAssThrow2.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨throw e',s2,False⟩"using FAssThrow2.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsThrow2[OF b1 b2] by fast qed next case (FAssNone e1 s0 a s1 e2 v h2 l2 sh2 C fs F D) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None FAssNone.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None FAssNone.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,False⟩"using iconf FAssNone.hyps(2) by auto have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,False⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] None FAssNone by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAssNone.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsNone[OF b1 b2 FAssNone.hyps(5,6)] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) FAssNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,b1⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] FAssNone byauto have bconf2: "P,shp s0⊨b (e2,b) √"using FAssNone.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf fass FAssNone.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAssNone.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsNone[OF b1 b2 FAssNone.hyps(5,6)] by fast qed next case (FAssStatic e1 s0 a s1 e2 v h2 l2 sh2 C fs F t D) show ?case proof(cases "val_of e1") case None thenhave iconf: "iconf (shp s0) e1"using None FAssStatic.prems by auto have bconf: "P,shp s0⊨b (e1,b) √"using None FAssStatic.prems by auto thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,False⟩"using iconf FAssStatic.hyps(2) by auto have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,False⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] None FAssStatic by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAssStatic.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsStatic[OF b1 b2 FAssStatic.hyps(5,6)] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e1,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) FAssStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨addr a∙F{D} := e2,s1,b1⟩"by(rule FAssReds1[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf fass] FAssStatic by auto have bconf2: "P,shp s0⊨b (e2,b) √"using FAssStatic.prems Some by simp thenhave"P,shp s1⊨b (e2,b1) √"using Red_preserves_bconf[OF wwf fass FAssStatic.prems] by simp thenhave b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using FAssStatic.hyps(4)[OF iconf2'] by auto thenshow ?thesis using FAssRedsStatic[OF b1 b2 FAssStatic.hyps(5,6)] by fast qed next case (SFAss e2 s0 v h1 l1 sh1 C F t D sfs sfs' sh1') show ?case proof(cases "val_of e2") case None thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAss.prems(2) by simp thenhave b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩"using SFAss by auto thus ?thesis using SFAssRedsVal[OF b1 SFAss.hyps(3,4)] SFAss.hyps(5,6) by fast next case (Some a) thenobtain b1 where b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),b1⟩" by (metis (no_types, lifting) SFAss.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) thus ?thesis using SFAssRedsVal[OF b1 SFAss.hyps(3,4)] SFAss.hyps(5,6) by fast qed next case (SFAssInit e2 s0 v h1 l1 sh1 C F t D v' h' l' sh' sfs i sfs' sh'') thenhave iconf: "iconf (shp s0) e2"by simp show ?case proof(cases "val_of e2") case None thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAssInit.prems(2) by simp thenhave reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInit.hyps(2)[OF iconf bconf] by auto thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨Val v',(h', l', sh'),False⟩" using SFAssInit.hyps(6) by(auto simp: bconf_def) thenshow ?thesis using SFAssInit SFAssInitReds[OF reds SFAssInit.hyps(3) _ init] by auto next case (Some v2) show ?thesis proof(cases b) case False thenhave bconf: "P,shp s0⊨b (e2,b) √"by(simp add: bconf_def) thenhave reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInit.hyps(2)[OF iconf bconf] by auto thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨Val v',(h', l', sh'),False⟩" using SFAssInit.hyps(6) by(auto simp: bconf_def) thenshow ?thesis using SFAssInit SFAssInitReds[OF reds SFAssInit.hyps(3) _ init] by auto next case True have e2: "e2 = Val v2"using val_of_spec[OF Some] by simp thenhave vs: "v2 = v ∧ s0 = (h1, l1, sh1)"using eval_final_same[OF SFAssInit.hyps(1)] by simp thenobtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋" using SFAssInit.hyps(3,4) SFAssInit.prems(2) Some True by(cases e2, auto simp: bconf_def initPD_def dest: sees_method_fun) thenhave s': "(h',l',sh') = (h1, l1, sh1)"using SFAssInit.hyps(5) init_ProcessingE byclarsimp thenshow ?thesis using SFAssInit.hyps(3,7-9) True e2 red_reds.RedSFAss vs by auto qed qed next case (SFAssInitThrow e2 s0 v h1 l1 sh1 C F t D a s') thenhave iconf: "iconf (shp s0) e2"by simp show ?case proof(cases "val_of e2") case None thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAssInitThrow.prems(2) by simp thenhave reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SFAssInitThrow.hyps(6) by(auto simp: bconf_def) thenshow ?thesis using SFAssInitThrow SFAssInitThrowReds[OF reds _ _ init] by auto next case (Some v2) show ?thesis proof(cases b) case False thenhave bconf: "P,shp s0⊨b (e2,b) √"by(simp add: bconf_def) thenhave reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SFAssInitThrow.hyps(6) by(auto simp: bconf_def) thenshow ?thesis using SFAssInitThrow SFAssInitThrowReds[OF reds _ _ init] by auto next case True obtain v2 where e2: "e2 = Val v2"using val_of_spec[OF Some] by simp thenhave vs: "v2 = v ∧ s0 = (h1, l1, sh1)" using eval_final_same[OF SFAssInitThrow.hyps(1)] by simp thenobtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋" using SFAssInitThrow.hyps(4) SFAssInitThrow.prems(2) Some True by(cases e2, auto simp: bconf_def initPD_def dest: sees_method_fun) thenshow ?thesis using SFAssInitThrow.hyps(5) init_ProcessingE by blast qed qed next case (SFAssThrow e2 s0 e' s2 C F D) show ?case proof(cases "val_of e2") case None thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAssThrow.prems(2) None by simp thenhave b1: "P ⊨⟨e2,s0,b⟩→* ⟨throw e',s2,False⟩"using SFAssThrow by auto thus ?thesis using SFAssRedsThrow[OF b1] by fast next case (Some a) thenshow ?thesis using eval_final_same[OF SFAssThrow.hyps(1)] val_of_spec[OF Some] by auto qed next case (SFAssNone e2 s0 v h2 l2 sh2 C F D) show ?case proof(cases "val_of e2") case None thenhave iconf: "iconf (shp s0) e2"using SFAssNone by simp thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAssNone.prems(2) None by simp thenhave b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using SFAssNone.hyps(2) iconf by auto thus ?thesis using SFAssRedsNone[OF b1 SFAssNone.hyps(3)] by fast next case (Some a) thenobtain b1 where b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h2, l2, sh2),b1⟩" by (metis (no_types, lifting) SFAssNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) thus ?thesis using SFAssRedsNone[OF b1 SFAssNone.hyps(3)] by fast qed next case (SFAssNonStatic e2 s0 v h2 l2 sh2 C F t D) show ?case proof(cases "val_of e2") case None thenhave iconf: "iconf (shp s0) e2"using SFAssNonStatic by simp thenhave bconf: "P,shp s0⊨b (e2,b) √"using SFAssNonStatic.prems(2) None by simp thenhave b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h2, l2, sh2),False⟩"using SFAssNonStatic.hyps(2) iconf by auto thus ?thesis using SFAssRedsNonStatic[OF b1 SFAssNonStatic.hyps(3)] by fast next case (Some a) thenobtain b' where b1: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h2, l2, sh2),b'⟩" by (metis (no_types, lifting) SFAssNonStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) thus ?thesis using SFAssRedsNonStatic[OF b1 SFAssNonStatic.hyps(3)] by fast qed next case (CallObjThrow e s0 e' s1 M ps) show ?case proof(cases "val_of e") case None thenhave"iconf (shp s0) e"and"P,shp s0⊨b (e,b) √"using CallObjThrow.prems by auto thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨throw e',s1,False⟩"using CallObjThrow.hyps(2) by auto thenhave"P ⊨⟨e∙M(ps),s0,b⟩→* ⟨throw e',s1,False⟩" using CallObjThrow None by(auto dest!:eval_final simp: CallRedsThrowObj[OF b1]) thenshow ?thesis by fast next case (Some a) thenshow ?thesis using eval_final_same[OF CallObjThrow.hyps(1)] val_of_spec[OF Some] byauto qed next case (CallNull e s0 s1 ps vs s2 M) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using CallNull.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using CallNull.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨null,s1,False⟩"using CallNull.hyps(2)[OF iconf] by auto have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨null∙M(ps),s1,False⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] None CallNull by auto have"P,shp s1⊨b (ps,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,s2,False⟩"using CallNull.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsNull[OF b1 b2] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨null,s1,b1⟩" by (metis (no_types, lifting) CallNull.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨null∙M(ps),s1,b1⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf fass] CallNull by auto have bconf2: "P,shp s0⊨b (ps,b) √"using CallNull.prems Some by simp thenhave"P,shp s1⊨b (ps,b1) √"using Red_preserves_bconf[OF wwf fass CallNull.prems] by simp thenhave b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,s2,False⟩"using CallNull.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsNull[OF b1 b2] by fast qed next case (CallParamsThrow e s0 v s1 es vs ex es' s2 M) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using CallParamsThrow.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using CallParamsThrow.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨Val v,s1,False⟩"using CallParamsThrow.hyps(2)[OF iconf] by auto have call: "P ⊨⟨e∙M(es),s0,b⟩→* ⟨Val v∙M(es),s1,False⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) es"using Red_preserves_iconf[OF wwf call] None CallParamsThrow by auto have"P,shp s1⊨b (es,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨es,s1,False⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩" using CallParamsThrow.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsThrowParams[OF b1 b2] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨Val v,s1,b1⟩" by (metis (no_types, lifting) CallParamsThrow.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e∙M(es),s0,b⟩→* ⟨Val v∙M(es),s1,b1⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) es"using Red_preserves_iconf[OF wwf fass] CallParamsThrow by auto have bconf2: "P,shp s0⊨b (es,b) √"using CallParamsThrow.prems Some by simp thenhave"P,shp s1⊨b (es,b1) √"using Red_preserves_bconf[OF wwf fass CallParamsThrow.prems] by simp thenhave b2: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩" using CallParamsThrow.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsThrowParams[OF b1 b2] by fast qed next case (CallNone e s0 a s1 ps vs h2 l2 sh2 C fs M) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using CallNone.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using CallNone.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,False⟩"using CallNone.hyps(2)[OF iconf] by auto have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,False⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] None CallNone by auto have"P,shp s1⊨b (ps,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallNone.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsNone[OF b1 b2 _ CallNone.hyps(6)] CallNone.hyps(5) by fastforce next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) CallNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fass: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,b1⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf fass] CallNone by auto have bconf2: "P,shp s0⊨b (ps,b) √"using CallNone.prems Some by simp thenhave"P,shp s1⊨b (ps,b1) √"using Red_preserves_bconf[OF wwf fass CallNone.prems] by simp thenhave b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallNone.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsNone[OF b1 b2 _ CallNone.hyps(6)] CallNone.hyps(5) by fastforce qed next case (CallStatic e s0 a s1 ps vs h2 l2 sh2 C fs M Ts T m D) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using CallStatic.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using CallStatic.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,False⟩"using CallStatic.hyps(2)[OF iconf] by auto have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,False⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] None CallStatic by auto have"P,shp s1⊨b (ps,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallStatic.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsStatic[OF b1 b2 _ CallStatic.hyps(6)] CallStatic.hyps(5) by fastforce next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) CallStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,b1⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] CallStatic by auto have bconf2: "P,shp s0⊨b (ps,b) √"using CallStatic.prems Some by simp thenhave"P,shp s1⊨b (ps,b1) √"using Red_preserves_bconf[OF wwf call CallStatic.prems] by simp thenhave b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallStatic.hyps(4)[OF iconf2'] by auto thenshow ?thesis using CallRedsStatic[OF b1 b2 _ CallStatic.hyps(6)] CallStatic.hyps(5) by fastforce qed next case (Call e s0 a s1 ps vs h2 l2 sh2 C fs M Ts T pns body D l2' e' h3 l3 sh3) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using Call.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using Call.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,False⟩"using Call.hyps(2)[OF iconf] by auto have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,False⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2: "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] None Call byauto have"P,shp s1⊨b (ps,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using Call.hyps(4)[OF iconf2] by simp have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf Call.hyps(6)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using Call.hyps(10)[OF iconf3] by simp show ?thesis by(rule CallRedsFinal[OF wwf b1 b2 Call.hyps(5-8) b3 eval_final[OF Call.hyps(9)]]) next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨addr a,s1,b1⟩" by (metis (no_types, lifting) Call.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have call: "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨addr a∙M(ps),s1,b1⟩"by(rule CallRedsObj[OF b1]) thenhave iconf2': "iconfs (shp s1) ps"using Red_preserves_iconf[OF wwf call] Call by auto have bconf2: "P,shp s0⊨b (ps,b) √"using Call.prems Some by simp thenhave"P,shp s1⊨b (ps,b1) √"using Red_preserves_bconf[OF wwf call Call.prems] by simp thenhave b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using Call.hyps(4)[OF iconf2'] by auto have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf Call.hyps(6)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using Call.hyps(10)[OF iconf3] by simp show ?thesis by(rule CallRedsFinal[OF wwf b1 b2 Call.hyps(5-8) b3 eval_final[OF Call.hyps(9)]]) qed next case (SCallParamsThrow es s0 vs ex es' s2 C M) show ?case proof(cases "map_vals_of es") case None thenhave iconf: "iconfs (shp s0) es"using SCallParamsThrow.prems(1) by simp have bconf: "P,shp s0⊨b (es,b) √"using SCallParamsThrow.prems(2) None by simp thenhave b1: "P ⊨⟨es,s0,b⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩" using SCallParamsThrow.hyps(2)[OF iconf] by simp show ?thesis using SCallRedsThrowParams[OF b1] by simp next case (Some vs') thenhave"es = map Val vs'"by(rule map_vals_of_spec) thenshow ?thesis using evals_finals_same[OF _ SCallParamsThrow.hyps(1)] map_Val_nthrow_neq by auto qed next case (SCallNone ps s0 vs s2 C M) show ?case proof(cases "map_vals_of ps") case None thenhave iconf: "iconfs (shp s0) ps"using SCallNone.prems(1) by simp have bconf: "P,shp s0⊨b (ps,b) √"using SCallNone.prems(2) None by simp thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩"using SCallNone.hyps(2)[OF iconf] by auto thenshow ?thesis using SCallRedsNone[OF b1 SCallNone.hyps(3)] SCallNone.hyps(1) by simp next case (Some vs') thenhave ps: "ps = map Val vs'"by(rule map_vals_of_spec) thenhave s0: "s0 = s2"using SCallNone.hyps(1) evals_finals_same by blast thenshow ?thesis using RedSCallNone[OF SCallNone.hyps(3)] ps by(cases s2, auto) qed next case (SCallNonStatic ps s0 vs s2 C M Ts T m D) show ?case proof(cases "map_vals_of ps") case None thenhave iconf: "iconfs (shp s0) ps"using SCallNonStatic.prems(1) by simp have bconf: "P,shp s0⊨b (ps,b) √"using SCallNonStatic.prems(2) None by simp thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩"using SCallNonStatic.hyps(2)[OF iconf] by auto thenshow ?thesis using SCallRedsNonStatic[OF b1 SCallNonStatic.hyps(3)] SCallNonStatic.hyps(1) by simp next case (Some vs') thenhave ps: "ps = map Val vs'"by(rule map_vals_of_spec) thenhave s0: "s0 = s2"using SCallNonStatic.hyps(1) evals_finals_same by blast thenshow ?thesis using RedSCallNonStatic[OF SCallNonStatic.hyps(3)] ps by(cases s2, auto) qed next case (SCallInitThrow ps s0 vs h1 l1 sh1 C M Ts T pns body D a s') show ?case proof(cases "map_vals_of ps") case None thenhave iconf: "iconfs (shp s0) ps"using SCallInitThrow.prems(1) by simp have bconf: "P,shp s0⊨b (ps,b) √"using SCallInitThrow.prems(2) None by simp thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩" using SCallInitThrow.hyps(2)[OF iconf] by auto have bconf2: "P,shp (h1, l1, sh1) ⊨b (INIT D ([D],False) ← unit,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SCallInitThrow.hyps(7) by auto thenshow ?thesis using SCallInitThrowReds[OF wwf b1 SCallInitThrow.hyps(3-5)] by(cases s', auto) next case (Some vs') have ps: "ps = map Val vs'"by(rule map_vals_of_spec[OF Some]) thenhave vs: "vs = vs' ∧ s0 = (h1, l1, sh1)" using evals_finals_same[OF _ SCallInitThrow.hyps(1)] map_Val_eq by auto show ?thesis proof(cases b) case True obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋" using SCallInitThrow.hyps(3,4) SCallInitThrow.prems(2) True Some vs by(auto simp: bconf_def initPD_def dest: sees_method_fun) thenshow ?thesis using init_ProcessingE[OF _ SCallInitThrow.hyps(6)] by blast next case False thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩"using ps vs by simp have bconf2: "P,shp (h1, l1, sh1) ⊨b (INIT D ([D],False) ← unit,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SCallInitThrow.hyps(7) by auto thenshow ?thesis using SCallInitThrowReds[OF wwf b1 SCallInitThrow.hyps(3-5)] by(cases s', auto) qed qed next case (SCallInit ps s0 vs h1 l1 sh1 C M Ts T pns body D v' h2 l2 sh2 l2' e' h3 l3 sh3) show ?case proof(cases "map_vals_of ps") case None thenhave iconf: "iconfs (shp s0) ps"using SCallInit.prems(1) by simp have bconf: "P,shp s0⊨b (ps,b) √"using SCallInit.prems(2) None by simp thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩" using SCallInit.hyps(2)[OF iconf] by auto have bconf2: "P,shp (h1, l1, sh1) ⊨b (INIT D ([D],False) ← unit,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨Val v',(h2, l2, sh2),False⟩" using SCallInit.hyps(7) by auto have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCallInit.hyps(11)[OF iconf3] by simp show ?thesis by(rule SCallInitReds[OF wwf b1 SCallInit.hyps(3-5) b2 SCallInit.hyps(8-9)
b3 eval_final[OF SCallInit.hyps(10)]]) next case (Some vs') thenhave ps: "ps = map Val vs'"by(rule map_vals_of_spec) thenhave vs: "vs = vs' ∧ s0 = (h1, l1, sh1)" using evals_finals_same[OF _ SCallInit.hyps(1)] map_Val_eq by auto show ?thesis proof(cases b) case True thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),b⟩"using ps vs by simp obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋" using SCallInit.hyps(3,4) SCallInit.prems(2) True Some vs by(auto simp: bconf_def initPD_def dest: sees_method_fun) thenhave s': "(h1, l1, sh1) = (h2, l2, sh2)"using init_ProcessingE[OF _ SCallInit.hyps(6)] by simp have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCallInit.hyps(11)[OF iconf3] by simp thenhave b3': "P ⊨⟨body,(h1, l2', sh1),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using s' by simp thenshow ?thesis using SCallInitProcessingReds[OF wwf b1 SCallInit.hyps(3) shC
SCallInit.hyps(8-9) b3' eval_final[OF SCallInit.hyps(10)]] s' by simp next case False thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩"using ps vs by simp have bconf2: "P,shp (h1, l1, sh1) ⊨b (INIT D ([D],False) ← unit,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨Val v',(h2, l2, sh2),False⟩" using SCallInit.hyps(7) by auto have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCallInit.hyps(11)[OF iconf3] by simp show ?thesis by(rule SCallInitReds[OF wwf b1 SCallInit.hyps(3-5) b2 SCallInit.hyps(8-9)
b3 eval_final[OF SCallInit.hyps(10)]]) qed qed next case (SCall ps s0 vs h2 l2 sh2 C M Ts T pns body D sfs l2' e' h3 l3 sh3) show ?case proof(cases "map_vals_of ps") case None thenhave iconf: "iconfs (shp s0) ps"using SCall.prems(1) by simp have bconf: "P,shp s0⊨b (ps,b) √"using SCall.prems(2) None by simp thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using SCall.hyps(2)[OF iconf] by auto have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCall.hyps(3)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCall.hyps(8)[OF iconf3] by simp show ?thesis by(rule SCallRedsFinal[OF wwf b1 SCall.hyps(3-6) b2 eval_final[OF SCall.hyps(7)]]) next case (Some vs') thenhave ps: "ps = map Val vs'"by(rule map_vals_of_spec) thenhave vs: "vs = vs' ∧ s0 = (h2, l2, sh2)" using evals_finals_same[OF _ SCall.hyps(1)] map_Val_eq by auto thenhave b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h2, l2, sh2),b⟩"using ps by simp have iconf3: "iconf (shp (h2, l2', sh2)) body" by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCall.hyps(3)]]) have"P,shp (h2, l2', sh2) ⊨b (body,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCall.hyps(8)[OF iconf3] by simp show ?thesis by(rule SCallRedsFinal[OF wwf b1 SCall.hyps(3-6) b2 eval_final[OF SCall.hyps(7)]]) qed next case (Block e0 h0 l0 V sh0 e1 h1 l1 sh1 T) have iconf: "iconf (shp (h0, l0(V := None), sh0)) e0" using Block.prems(1) by (auto simp: assigned_def) have bconf: "P,shp (h0, l0(V := None), sh0) ⊨b (e0,b) √"using Block.prems(2) by(auto simp: bconf_def) thenhave b': "P ⊨⟨e0,(h0, l0(V := None), sh0),b⟩→* ⟨e1,(h1, l1, sh1),False⟩" using Block.hyps(2)[OF iconf] by auto have fin: "final e1"using Block by(auto dest: eval_final) thus ?caseusing BlockRedsFinal[OF b' fin] by simp next case (Seq e0 s0 v s1 e1 e2 s2) thenhave iconf: "iconf (shp s0) e0"using Seq.prems(1) by(auto dest: val_of_spec lass_val_of_spec) have b1: "∃b1. P ⊨⟨e0,s0,b⟩→* ⟨Val v,s1,b1⟩" proof(cases "val_of e0") case None show ?thesis proof(cases "lass_val_of e0") case lNone:None thenhave bconf: "P,shp s0⊨b (e0,b) √"using Seq.prems(2) None by simp thenhave"P ⊨⟨e0,s0,b⟩→* ⟨Val v,s1,False⟩"using iconf Seq.hyps(2) by auto thenshow ?thesis by fast next case (Some p) obtain V' v' where p: "p = (V',v')"and e0: "e0 = V':=Val v'" using lass_val_of_spec[OF Some] by(cases p, auto) obtain h l sh h' l' sh' where s0: "s0 = (h,l,sh)"and s1: "s1 = (h',l',sh')"by(cases s0, cases s1) thenhave eval: "P ⊨⟨e0,(h,l,sh)⟩==>⟨Val v,(h',l',sh')⟩"using Seq.hyps(1) by simp thenhave s1': "Val v = unit ∧ h' = h ∧ l' = l(V' ↦ v') ∧ sh' = sh" using lass_val_of_eval[OF Some eval] p e0by simp thenhave"P ⊨⟨e0,s0,b⟩→⟨Val v,s1,b⟩"using e0 s0 s1by(auto intro: RedLAss) thenshow ?thesis by auto qed next case (Some a) thenhave"e0 = Val v"and"s0 = s1"using Seq.hyps(1) eval_cases(3) val_of_spec by blast+ thenshow ?thesis using Seq by auto qed thenobtain b1 where b1': "P ⊨⟨e0,s0,b⟩→* ⟨Val v,s1,b1⟩"by clarsimp have seq: "P ⊨⟨e0;;e1,s0,b⟩→* ⟨Val v;;e1,s1,b1⟩"by(rule SeqReds[OF b1']) thenhave iconf2: "iconf (shp s1) e1"using Red_preserves_iconf[OF wwf seq] Seq nsub_RI_iconf by auto have"P,shp s1⊨b (Val v;; e1,b1) √"by(rule Red_preserves_bconf[OF wwf seq Seq.prems]) thenhave bconf2: "P,shp s1⊨b (e1,b1) √"by simp have b2: "P ⊨⟨e1,s1,b1⟩→* ⟨e2,s2,False⟩"by(rule Seq.hyps(4)[OF iconf2 bconf2]) thenshow ?caseusing SeqReds2[OF b1' b2] by fast next case (SeqThrow e0 s0 a s1 e1 b) have notVal: "val_of e0 = None""lass_val_of e0 = None" using SeqThrow.hyps(1) eval_throw_nonVal eval_throw_nonLAss by auto thus ?caseusing SeqThrow notVal by(auto dest!:eval_final dest: SeqRedsThrow) next case (CondT e s0 s1 e1 e' s2 e2) thenhave iconf: "iconf (shp s0) e"using CondT.prems(1) by auto have bconf: "P,shp s0⊨b (e,b) √"using CondT.prems(2) by auto thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨true,s1,False⟩"using iconf CondT.hyps(2) by auto have cond: "P ⊨⟨if (e) e1 else e2,s0,b⟩→* ⟨if (true) e1 else e2,s1,False⟩"by(rule CondReds[OF b1]) thenhave iconf2': "iconf (shp s1) e1"using Red_preserves_iconf[OF wwf cond] CondT nsub_RI_iconf by auto have"P,shp s1⊨b (e1,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e1,s1,False⟩→* ⟨e',s2,False⟩"using CondT.hyps(4)[OF iconf2'] by auto thenshow ?caseusing CondReds2T[OF b1 b2] by fast next case (CondF e s0 s1 e2 e' s2 e1) thenhave iconf: "iconf (shp s0) e"using CondF.prems(1) by auto have bconf: "P,shp s0⊨b (e,b) √"using CondF.prems(2) by auto thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨false,s1,False⟩"using iconf CondF.hyps(2) by auto have cond: "P ⊨⟨if (e) e1 else e2,s0,b⟩→* ⟨if (false) e1 else e2,s1,False⟩"by(rule CondReds[OF b1]) thenhave iconf2': "iconf (shp s1) e2"using Red_preserves_iconf[OF wwf cond] CondF nsub_RI_iconf by auto have"P,shp s1⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,s1,False⟩→* ⟨e',s2,False⟩"using CondF.hyps(4)[OF iconf2'] by auto thenshow ?caseusing CondReds2F[OF b1 b2] by fast next case CondThrow thus ?caseby(auto dest!:eval_final dest:CondRedsThrow) next case (WhileF e s0 s1 c) thenhave iconf: "iconf (shp s0) e"using nsub_RI_iconf by auto thenhave bconf: "P,shp s0⊨b (e,b) √"using WhileF.prems(2) by(simp add: bconf_def) thenhave b': "P ⊨⟨e,s0,b⟩→* ⟨false,s1,False⟩"using WhileF.hyps(2) iconf by auto thus ?caseusing WhileFReds[OF b'] by fast next case (WhileT e s0 s1 c v1 s2 e3 s3) thenhave iconf: "iconf (shp s0) e"using nsub_RI_iconf by auto thenhave bconf: "P,shp s0⊨b (e,b) √"using WhileT.prems(2) by(simp add: bconf_def) thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨true,s1,False⟩"using WhileT.hyps(2) iconf by auto have iconf2: "iconf (shp s1) c"using WhileT.prems(1) nsub_RI_iconf by auto have bconf2: "P,shp s1⊨b (c,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨c,s1,False⟩→* ⟨Val v1,s2,False⟩"using WhileT.hyps(4) iconf2 by auto have iconf3: "iconf (shp s2) (while (e) c)"using WhileT.prems(1) by auto have"P,shp s2⊨b (while (e) c,False) √"by(simp add: bconf_def) thenhave b3: "P ⊨⟨while (e) c,s2,False⟩→* ⟨e3,s3,False⟩"using WhileT.hyps(6) iconf3 by auto show ?caseusing WhileTReds[OF b1 b2 b3] by fast next case WhileCondThrow thus ?case by (metis (no_types, lifting) WhileRedsThrow iconf.simps(16) bconf_While bconf_def nsub_RI_iconf) next case (WhileBodyThrow e s0 s1 c e' s2) thenhave iconf: "iconf (shp s0) e"using nsub_RI_iconf by auto thenhave bconf: "P,shp s0⊨b (e,b) √"using WhileBodyThrow.prems(2) by(simp add: bconf_def) thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨true,s1,False⟩"using WhileBodyThrow.hyps(2) iconf by auto have iconf2: "iconf (shp s1) c"using WhileBodyThrow.prems(1) nsub_RI_iconf by auto have bconf2: "P,shp s1⊨b (c,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨c,s1,False⟩→* ⟨throw e',s2,False⟩"using WhileBodyThrow.hyps(4) iconf2 by auto show ?caseusing WhileTRedsThrow[OF b1 b2] by fast next case Throw thus ?caseby (meson ThrowReds iconf.simps(17) bconf_Throw) next case ThrowNull thus ?caseby (meson ThrowRedsNull iconf.simps(17) bconf_Throw) next case ThrowThrow thus ?caseby (meson ThrowRedsThrow iconf.simps(17) bconf_Throw) next case Try thus ?caseby (meson TryRedsVal iconf.simps(18) bconf_Try) next case (TryCatch e1 s0 a h1 l1 sh1 D fs C e2 V e2' h2 l2 sh2) thenhave b1: "P ⊨⟨e1,s0,b⟩→* ⟨Throw a,(h1, l1, sh1),False⟩"by auto have Try: "P ⊨⟨try e1 catch(C V) e2,s0,b⟩→* ⟨try (Throw a) catch(C V) e2,(h1, l1, sh1),False⟩" by(rule TryReds[OF b1]) have iconf: "iconf sh1 e2"using Red_preserves_iconf[OF wwf Try] TryCatch nsub_RI_iconf by auto have bconf: "P,shp (h1, l1(V ↦ Addr a), sh1) ⊨b (e2,False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨e2,(h1, l1(V ↦ Addr a), sh1),False⟩→* ⟨e2',(h2, l2, sh2),False⟩" using TryCatch.hyps(6) iconf by auto thus ?caseusing TryCatchRedsFinal[OF b1] TryCatch.hyps(3-5) by (meson eval_final) next case TryThrow thus ?caseby (meson TryRedsFail iconf.simps(18) bconf_Try) next case Nil thus ?caseby(auto simp: bconfs_def) next case (Cons e s0 v s1 es es' s2) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using Cons.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using Cons.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨Val v,s1,False⟩"using Cons.hyps(2) iconf by auto have cons: "P ⊨⟨e # es,s0,b⟩ [→]* ⟨Val v # es,s1,False⟩"by(rule ListReds1[OF b1]) thenhave iconf2': "iconfs (shp s1) es"using Reds_preserves_iconf[OF wwf cons] None Cons by auto have"P,shp s1⊨b (es,False) √"by(simp add: bconfs_def) thenhave b2: "P ⊨⟨es,s1,False⟩ [→]* ⟨es',s2,False⟩"using Cons.hyps(4)[OF iconf2'] by auto show ?thesis using ListRedsVal[OF b1 b2] by auto next case (Some a) thenobtain b1 where b1: "P ⊨⟨e,s0,b⟩→* ⟨Val v,s1,b1⟩" by (metis (no_types, lifting) Cons.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have cons: "P ⊨⟨e # es,s0,b⟩ [→]* ⟨Val v # es,s1,b1⟩"by(rule ListReds1[OF b1]) thenhave iconf2': "iconfs (shp s1) es"using Reds_preserves_iconf[OF wwf cons] Cons by auto have bconf2: "P,shp s0⊨b (es,b) √"using Cons.prems Some by simp thenhave"P,shp s1⊨b (es,b1) √"using Reds_preserves_bconf[OF wwf cons Cons.prems] by simp thenhave b2: "P ⊨⟨es,s1,b1⟩ [→]* ⟨es',s2,False⟩"using Cons.hyps(4)[OF iconf2'] by auto show ?thesis using ListRedsVal[OF b1 b2] by auto qed next case (ConsThrow e s0 e' s1 es) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s0) e"using ConsThrow.prems(1) by simp have bconf: "P,shp s0⊨b (e,b) √"using ConsThrow.prems(2) None by simp thenhave b1: "P ⊨⟨e,s0,b⟩→* ⟨throw e',s1,False⟩"using ConsThrow.hyps(2) iconf by auto have cons: "P ⊨⟨e # es,s0,b⟩ [→]* ⟨throw e' # es,s1,False⟩"by(rule ListReds1[OF b1]) thenshow ?thesis by fast next case (Some a) thenshow ?thesis using eval_final_same[OF ConsThrow.hyps(1)] val_of_spec[OF Some] by auto qed next case (InitFinal e s e' s' C b') thenhave"¬sub_RI e"by simp thenshow ?caseusing InitFinal RedInit[of e C b' s b P] by (meson converse_rtrancl_into_rtrancl nsub_RI_iconf red_preserves_bconf RedInit) next case (InitNone sh C C' Cs e h l e' s') thenhave init: "P ⊨⟨INIT C' (C # Cs,False) ← e,(h, l, sh(C ↦ (sblank P C, Prepared))),b⟩→* ⟨e',s',False⟩" by(simp add: bconf_def) show ?caseby(rule InitNoneReds[OF InitNone.hyps(1) init]) next case (InitDone sh C sfs C' Cs e h l e' s') thenhave"iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)"using InitDone.hyps(1) proof(cases Cs) case Nil thenhave"C = C'""¬sub_RI e"using InitDone.prems(1) by simp+ thenshow ?thesis using Nil InitDone.hyps(1) by(simp add: initPD_def) qed(auto) thenhave init: "P ⊨⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩→* ⟨e',s',False⟩" using InitDone by(simp add: bconf_def) show ?caseby(rule InitDoneReds[OF InitDone.hyps(1) init]) next case (InitProcessing sh C sfs C' Cs e h l e' s') thenhave"iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)"using InitProcessing.hyps(1) proof(cases Cs) case Nil thenhave"C = C'""¬sub_RI e"using InitProcessing.prems(1) by simp+ thenshow ?thesis using Nil InitProcessing.hyps(1) by(simp add: initPD_def) qed(auto) thenhave init: "P ⊨⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩→* ⟨e',s',False⟩" using InitProcessing by(simp add: bconf_def) show ?caseby(rule InitProcessingReds[OF InitProcessing.hyps(1) init]) next case InitError thus ?caseby(fastforce intro: InitErrorReds simp: bconf_def) next case InitObject thus ?caseby(fastforce intro: InitObjectReds simp: bconf_def) next case InitNonObject thus ?caseby(fastforce intro: InitNonObjectReds simp: bconf_def) next case InitRInit thus ?caseby(fastforce intro: RedsInitRInit simp: bconf_def) next case (RInit e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1) thenhave iconf2: "iconf (shp (h', l', sh'')) (INIT C' (Cs,True) ← e')" by(auto simp: initPD_def fun_upd_same list_nonempty_induct) show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s) e"using RInit.prems(1) by simp have bconf: "P,shp s ⊨b (e,b) √"using RInit.prems(2) None by simp thenhave b1: "P ⊨⟨e,s,b⟩→* ⟨Val v,(h',l',sh'),False⟩"using RInit.hyps(2)[OF iconf] by auto have"P,shp (h', l', sh'') ⊨b (INIT C' (Cs,True) ← e',False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT C' (Cs,True) ← e',(h',l',sh''),False⟩→* ⟨e1,s1,False⟩" using RInit.hyps(7)[OF iconf2] by auto thenshow ?thesis using RedsRInit[OF b1 RInit.hyps(3-5) b2] by fast next case (Some a') thenobtain b1 where b1: "P ⊨⟨e,s,b⟩→* ⟨Val v,(h',l',sh'),b1⟩" by (metis (no_types, lifting) RInit.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fin: "final e"by(simp add: val_of_spec[OF Some]) have"¬b"using RInit.prems(2) Some by(simp add: bconf_def) thenhave nb1: "¬b1"using reds_final_same[OF b1 fin] by simp have"P,shp (h', l', sh'') ⊨b (INIT C' (Cs,True) ← e',b1) √"using nb1 by(simp add: bconf_def) thenhave b2: "P ⊨⟨INIT C' (Cs,True) ← e',(h', l', sh''),b1⟩→* ⟨e1,s1,False⟩" using RInit.hyps(7)[OF iconf2] by auto thenshow ?thesis using RedsRInit[OF b1 RInit.hyps(3-5) b2] by fast qed next case (RInitInitFail e s a h' l' sh' C sfs i sh'' D Cs e' e1 s1) have fin: "final (throw a)"using eval_final[OF RInitInitFail.hyps(1)] by simp thenobtain a' where a': "throw a = Throw a'"by auto have iconf2: "iconf (shp (h', l', sh'')) (RI (D,Throw a') ; Cs ← e')" using RInitInitFail.prems(1) by auto show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s) e"using RInitInitFail.prems(1) by simp have bconf: "P,shp s ⊨b (e,b) √"using RInitInitFail.prems(2) None by simp thenhave b1: "P ⊨⟨e,s,b⟩→* ⟨Throw a',(h',l',sh'),False⟩" using RInitInitFail.hyps(2)[OF iconf] a' by auto have"P,shp (h', l', sh'') ⊨b (RI (D,Throw a') ; Cs ← e',False) √"by(simp add: bconf_def) thenhave b2: "P ⊨⟨RI (D,Throw a') ; Cs ← e',(h',l',sh''),False⟩→* ⟨e1,s1,False⟩" using RInitInitFail.hyps(6) iconf2 a' by auto show ?thesis using RInitInitThrowReds[OF b1 RInitInitFail.hyps(3-4) b2] by fast next case (Some a1) thenobtain b1 where b1: "P ⊨⟨e,s,b⟩→* ⟨Throw a',(h',l',sh'),b1⟩"using a' by (metis (no_types, lifting) RInitInitFail.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec) have fin: "final e"by(simp add: val_of_spec[OF Some]) have"¬b"using RInitInitFail.prems(2) Some by(simp add: bconf_def) thenhave nb1: "¬b1"using reds_final_same[OF b1 fin] by simp have"P,shp (h', l', sh'') ⊨b (RI (D,Throw a') ; Cs ← e',b1) √"using nb1 by(simp add: bconf_def) thenhave b2: "P ⊨⟨RI (D,Throw a') ; Cs ← e',(h', l', sh''),b1⟩→* ⟨e1,s1,False⟩" using RInitInitFail.hyps(6) iconf2 a' by auto show ?thesis using RInitInitThrowReds[OF b1 RInitInitFail.hyps(3-4) b2] by fast qed next case (RInitFailFinal e s a h' l' sh' C sfs i sh'' e') have fin: "final (throw a)"using eval_final[OF RInitFailFinal.hyps(1)] by simp thenobtain a' where a': "throw a = Throw a'"by auto show ?case proof(cases "val_of e") case None thenhave iconf: "iconf (shp s) e"using RInitFailFinal.prems(1) by simp have bconf: "P,shp s ⊨b (e,b) √"using RInitFailFinal.prems(2) None by simp thenhave b1: "P ⊨⟨e,s,b⟩→* ⟨Throw a',(h',l',sh'),False⟩" using RInitFailFinal.hyps(2)[OF iconf] a' by auto show ?thesis using RInitThrowReds[OF b1 RInitFailFinal.hyps(3-4)] a' by fast next case (Some a1) thenshow ?thesis using eval_final_same[OF RInitFailFinal.hyps(1)] val_of_spec[OF Some] by auto qed qed (*>*)
subsection‹Big steps simulates small step›
text‹ This direction was carried out by Norbert Schirmer and Daniel
(and modified to include statics and DCI by Susannah Mansky). ›
text‹ The big step equivalent of @{text RedWhile}: ›
lemma unfold_while: "P ⊨⟨while(b) c,s⟩==>⟨e',s'⟩ = P ⊨⟨if(b) (c;;while(b) c) else (unit),s⟩==>⟨e',s'⟩" (*<*) proof assume"P ⊨⟨while (b) c,s⟩==>⟨e',s'⟩" thus"P ⊨⟨if (b) (c;; while (b) c) else unit,s⟩==>⟨e',s'⟩" by cases (fastforce intro: eval_evals.intros)+ next assume"P ⊨⟨if (b) (c;; while (b) c) else unit,s⟩==>⟨e',s'⟩" thus"P ⊨⟨while (b) c,s⟩==>⟨e',s'⟩" proof (cases) fix a assume e': "e' = throw a" assume"P ⊨⟨b,s⟩==>⟨throw a,s'⟩" hence"P ⊨⟨while(b) c,s⟩==>⟨throw a,s'⟩"by (rule WhileCondThrow) with e' show ?thesis by simp next fix s1 assume eval_false: "P ⊨⟨b,s⟩==>⟨false,s1⟩" and eval_unit: "P ⊨⟨unit,s1⟩==>⟨e',s'⟩" with eval_unit have"s' = s1""e' = unit"by (auto elim: eval_cases) moreoverfrom eval_false have"P ⊨⟨while (b) c,s⟩==>⟨unit,s1⟩" by - (rule WhileF, simp) ultimatelyshow ?thesis by simp next fix s1 assume eval_true: "P ⊨⟨b,s⟩==>⟨true,s1⟩" and eval_rest: "P ⊨⟨c;; while (b) c,s1⟩==>⟨e',s'⟩" from eval_rest show ?thesis proof (cases) fix s2 v1 assume"P ⊨⟨c,s1⟩==>⟨Val v1,s2⟩""P ⊨⟨while (b) c,s2⟩==>⟨e',s'⟩" with eval_true show"P ⊨⟨while(b) c,s⟩==>⟨e',s'⟩"by (rule WhileT) next fix a assume"P ⊨⟨c,s1⟩==>⟨throw a,s'⟩""e' = throw a" with eval_true show"P ⊨⟨while(b) c,s⟩==>⟨e',s'⟩" by (iprover intro: WhileBodyThrow) qed qed qed (*>*)
lemma blocksEval: "∧Ts vs l l'. [size ps = size Ts; size ps = size vs; P ⊨⟨blocks(ps,Ts,vs,e),(h,l,sh)⟩==>⟨e',(h',l',sh')⟩] ==>∃ l''. P ⊨⟨e,(h,l(ps[↦]vs),sh)⟩==>⟨e',(h',l'',sh')⟩" (*<*) proof (induct ps) case Nil thenshow ?caseby fastforce next case (Cons p ps') have length_eqs: "length (p # ps') = length Ts" "length (p # ps') = length vs"by fact+ thenobtain T Ts' where Ts: "Ts = T#Ts'"by (cases "Ts") simp obtain v vs' where vs: "vs = v#vs'"using length_eqs by (cases "vs") simp have"P ⊨⟨blocks (p # ps', Ts, vs, e),(h,l,sh)⟩==>⟨e',(h', l',sh')⟩"by fact with Ts vs have"P ⊨⟨{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l,sh)⟩==>⟨e',(h', l',sh')⟩" by simp thenobtain l''' where
eval_ps': "P ⊨⟨blocks (ps', Ts', vs', e),(h, l(p↦v), sh)⟩==>⟨e',(h', l''', sh')⟩" and l''': "l'=l'''(p:=l p)" by (auto elim!: eval_cases) thenobtain l'' where
hyp: "P ⊨⟨e,(h, l(p↦v, ps'[↦]vs'), sh)⟩==>⟨e',(h', l'', sh')⟩" using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto from hyp show"∃l''. P ⊨⟨e,(h, l(p # ps'[↦]vs), sh)⟩==>⟨e',(h', l'', sh')⟩" using Ts vs by auto qed (*>*)
lemma assumes wf: "wwf_J_prog P" shows eval_restrict_lcl: "P ⊨⟨e,(h,l,sh)⟩==>⟨e',(h',l',sh')⟩==> (∧W. fv e ⊆ W ==> P ⊨⟨e,(h,l|`W,sh)⟩==>⟨e',(h',l'|`W,sh')⟩)" and"P ⊨⟨es,(h,l,sh)⟩ [==>] ⟨es',(h',l',sh')⟩==> (∧W. fvs es ⊆ W ==> P ⊨⟨es,(h,l|`W,sh)⟩ [==>] ⟨es',(h',l'|`W,sh')⟩)" (*<*) proof(induct rule:eval_evals_inducts) case (Block e0 h0 l0 V sh0 e1 h1 l1 sh1 T) have IH: "∧W. fv e0⊆ W ==> P ⊨⟨e0,(h0,l0(V:=None)|`W,sh0)⟩==>⟨e1,(h1,l1|`W,sh1)⟩"by fact have"fv({V:T; e0}) ⊆ W"by fact+ hence"fv e0 - {V} ⊆ W"by simp_all hence"fv e0⊆ insert V W"by fast from IH[OF this] have"P ⊨⟨e0,(h0, (l0|`W)(V := None), sh0)⟩==>⟨e1,(h1, l1|`insert V W, sh1)⟩" by fastforce from eval_evals.Block[OF this] show ?caseby fastforce next case Seq thus ?caseby simp (blast intro:eval_evals.Seq) next case New thus ?caseby(simp add:eval_evals.intros) next case NewFail thus ?caseby(simp add:eval_evals.intros) next case (NewInit sh C h l v' h' l' sh' a h'') have"fv(INIT C ([C],False) ← unit) ⊆ W"by simp thenhave"P ⊨⟨INIT C ([C],False) ← unit,(h, l |` W, sh)⟩==>⟨Val v',(h', l' |` W, sh')⟩" by (simp add: NewInit.hyps(3)) thus ?caseusing NewInit.hyps(1,4-6) eval_evals.NewInit by blast next case (NewInitOOM sh C h l v' h' l' sh') have"fv(INIT C ([C],False) ← unit) ⊆ W"by simp thenhave"P ⊨⟨INIT C ([C],False) ← unit,(h, l |` W, sh)⟩==>⟨Val v',(h', l' |` W, sh')⟩" by (simp add: NewInitOOM.hyps(3)) thus ?case using NewInitOOM.hyps(1,4,5) eval_evals.NewInitOOM by auto next case NewInitThrow thus ?caseby(simp add:eval_evals.intros) next case Cast thus ?caseby simp (blast intro:eval_evals.Cast) next case CastNull thus ?caseby simp (blast intro:eval_evals.CastNull) next case CastFail thus ?caseby simp (blast intro:eval_evals.CastFail) next case CastThrow thus ?caseby(simp add:eval_evals.intros) next case Val thus ?caseby(simp add:eval_evals.intros) next case BinOp thus ?caseby simp (blast intro:eval_evals.BinOp) next case BinOpThrow1 thus ?caseby simp (blast intro:eval_evals.BinOpThrow1) next case BinOpThrow2 thus ?caseby simp (blast intro:eval_evals.BinOpThrow2) next case Var thus ?caseby(simp add:eval_evals.intros) next case (LAss e h0 l0 sh0 v h l sh l' V) have IH: "∧W. fv e ⊆ W ==> P ⊨⟨e,(h0,l0|`W,sh0)⟩==>⟨Val v,(h,l|`W,sh)⟩" and [simp]: "l' = l(V ↦ v)"by fact+ have"fv (V:=e) ⊆ W"by fact hence fv: "fv e ⊆ W"and VinW: "V ∈ W"by auto from eval_evals.LAss[OF IH[OF fv] refl, of V] VinW show ?caseby simp next case LAssThrow thus ?caseby(fastforce intro: eval_evals.LAssThrow) next case FAcc thus ?caseby simp (blast intro: eval_evals.FAcc) next case FAccNull thus ?caseby(fastforce intro: eval_evals.FAccNull) next case FAccThrow thus ?caseby(fastforce intro: eval_evals.FAccThrow) next case FAccNone thus ?caseby(metis eval_evals.FAccNone fv.simps(7)) next case FAccStatic thus ?caseby(metis eval_evals.FAccStatic fv.simps(7)) next case SFAcc thus ?caseby simp (blast intro: eval_evals.SFAcc) next case SFAccInit thus ?caseby simp (blast intro: eval_evals.SFAccInit) next case SFAccInitThrow thus ?caseby simp (blast intro: eval_evals.SFAccInitThrow) next case SFAccNone thus ?caseby simp (blast intro: eval_evals.SFAccNone) next case SFAccNonStatic thus ?caseby simp (blast intro: eval_evals.SFAccNonStatic) next case FAss thus ?caseby simp (blast intro: eval_evals.FAss) next case FAssNull thus ?caseby simp (blast intro: eval_evals.FAssNull) next case FAssThrow1 thus ?caseby simp (blast intro: eval_evals.FAssThrow1) next case FAssThrow2 thus ?caseby simp (blast intro: eval_evals.FAssThrow2) next case FAssNone thus ?caseby simp (blast intro: eval_evals.FAssNone) next case FAssStatic thus ?caseby simp (blast intro: eval_evals.FAssStatic) next case SFAss thus ?caseby simp (blast intro: eval_evals.SFAss) next case SFAssInit thus ?caseby simp (blast intro: eval_evals.SFAssInit) next case SFAssInitThrow thus ?caseby simp (blast intro: eval_evals.SFAssInitThrow) next case SFAssThrow thus ?caseby simp (blast intro: eval_evals.SFAssThrow) next case SFAssNone thus ?caseby simp (blast intro: eval_evals.SFAssNone) next case SFAssNonStatic thus ?caseby simp (blast intro: eval_evals.SFAssNonStatic) next case CallObjThrow thus ?caseby simp (blast intro: eval_evals.intros) next case CallNull thus ?caseby simp (blast intro: eval_evals.CallNull) next case (CallNone e h l sh a h' l' sh' ps vs h2 l2 sh2 C fs M) have f1: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨addr a,(h', l' |` W, sh')⟩" by (metis (no_types) fv.simps(11) le_sup_iff local.CallNone(2) local.CallNone(7)) have"P ⊨⟨ps,(h', l' |` W, sh')⟩ [==>] ⟨map Val vs, (h2, l2 |` W, sh2)⟩" usinglocal.CallNone(4) local.CallNone(7) by auto thenshow ?case using f1 eval_evals.CallNone local.CallNone(5) local.CallNone(6) by auto next case CallStatic thus ?case by (metis (no_types, lifting) eval_evals.CallStatic fv.simps(11) le_sup_iff) next case CallParamsThrow thus ?case by simp (blast intro: eval_evals.CallParamsThrow) next case (Call e h0 l0 sh0 a h1 l1 sh1 ps vs h2 l2 sh2 C fs M Ts T pns body
D l2' e' h3 l3 sh3) have IHe: "∧W. fv e ⊆ W ==> P ⊨⟨e,(h0,l0|`W,sh0)⟩==>⟨addr a,(h1,l1|`W,sh1)⟩" and IHps: "∧W. fvs ps ⊆ W ==> P ⊨⟨ps,(h1,l1|`W,sh1)⟩ [==>] ⟨map Val vs,(h2,l2|`W,sh2)⟩" and IHbd: "∧W. fv body ⊆ W ==> P ⊨⟨body,(h2,l2'|`W,sh2)⟩==>⟨e',(h3,l3|`W,sh3)⟩" and h2a: "h2 a = Some (C, fs)" and"method": "P ⊨ C sees M,NonStatic: Ts→T = (pns, body) in D" and same_len: "size vs = size pns" and l2': "l2' = [this ↦ Addr a, pns [↦] vs]"by fact+ have"fv (e∙M(ps)) ⊆ W"by fact hence fve: "fv e ⊆ W"and fvps: "fvs(ps) ⊆ W"by auto have wfmethod: "size Ts = size pns ∧ this ∉ set pns"and
fvbd: "fv body ⊆ {this} ∪ set pns" using"method" wf by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ show ?case using IHbd[OF fvbd] l2' same_len wfmethod h2a
eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ "method" same_len l2'] by (simp add:subset_insertI) next case (SCallNone ps h l sh vs h' l' sh' C M) have"P ⊨⟨ps,(h, l |` W, sh)⟩ [==>] ⟨map Val vs,(h', l' |` W, sh')⟩" using SCallNone.hyps(2) SCallNone.prems by auto thenshow ?caseusing SCallNone.hyps(3) eval_evals.SCallNone by auto next case SCallNonStatic thus ?caseby (metis eval_evals.SCallNonStatic fv.simps(12)) next case SCallParamsThrow thus ?case by simp (blast intro: eval_evals.SCallParamsThrow) next case SCallInitThrow thus ?caseby simp (blast intro: eval_evals.SCallInitThrow) next case SCallInit thus ?caseby simp (blast intro: eval_evals.SCallInit) next case (SCall ps h0 l0 sh0 vs h2 l2 sh2 C M Ts T pns body D sfs l2' e' h3 l3 sh3) have IHps: "∧W. fvs ps ⊆ W ==> P ⊨⟨ps,(h0,l0|`W,sh0)⟩ [==>] ⟨map Val vs,(h2,l2|`W,sh2)⟩" and IHbd: "∧W. fv body ⊆ W ==> P ⊨⟨body,(h2,l2'|`W,sh2)⟩==>⟨e',(h3,l3|`W,sh3)⟩" and sh2D: "sh2 D = Some (sfs, Done) ∨ M = clinit ∧ sh2 D = ⌊(sfs, Processing)⌋" and"method": "P ⊨ C sees M,Static: Ts→T = (pns, body) in D" and same_len: "size vs = size pns" and l2': "l2' = [pns [↦] vs]"by fact+ have"fv (C∙sM(ps)) ⊆ W"by fact hence fvps: "fvs(ps) ⊆ W"by auto have wfmethod: "size Ts = size pns"and fvbd: "fv body ⊆ set pns" using"method" wf by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ show ?case using IHbd[OF fvbd] l2' same_len wfmethod sh2D
eval_evals.SCall[OF IHps[OF fvps] "method" _ same_len l2'] by (simp add:subset_insertI) next case SeqThrow thus ?caseby simp (blast intro: eval_evals.SeqThrow) next case CondT thus ?caseby simp (blast intro: eval_evals.CondT) next case CondF thus ?caseby simp (blast intro: eval_evals.CondF) next case CondThrow thus ?caseby simp (blast intro: eval_evals.CondThrow) next case WhileF thus ?caseby simp (blast intro: eval_evals.WhileF) next case WhileT thus ?caseby simp (blast intro: eval_evals.WhileT) next case WhileCondThrow thus ?caseby simp (blast intro: eval_evals.WhileCondThrow) next case WhileBodyThrow thus ?caseby simp (blast intro: eval_evals.WhileBodyThrow) next case Throw thus ?caseby simp (blast intro: eval_evals.Throw) next case ThrowNull thus ?caseby simp (blast intro: eval_evals.ThrowNull) next case ThrowThrow thus ?caseby simp (blast intro: eval_evals.ThrowThrow) next case Try thus ?caseby simp (blast intro: eval_evals.Try) next case (TryCatch e1 h0 l0 sh0 a h1 l1 sh1 D fs C e2 V e2' h2 l2 sh2) have IH1: "∧W. fv e1⊆ W ==> P ⊨⟨e1,(h0,l0|`W,sh0)⟩==>⟨Throw a,(h1,l1|`W,sh1)⟩" and IH2: "∧W. fv e2⊆ W ==> P ⊨⟨e2,(h1,l1(V↦Addr a)|`W,sh1)⟩==>⟨e2',(h2,l2|`W,sh2)⟩" and lookup: "h1 a = Some(D, fs)"and subtype: "P ⊨ D ⪯* C"by fact+ have"fv (try e1 catch(C V) e2) ⊆ W"by fact hence fv1: "fv e1⊆ W"and fv2: "fv e2⊆ insert V W"by auto have IH2': "P ⊨⟨e2,(h1,(l1|`W)(V ↦ Addr a),sh1)⟩==>⟨e2',(h2,l2|`insert V W,sh2)⟩" using IH2[OF fv2] fun_upd_restrict[of l1 W] (*FIXME just l|W instead of l|(W-V) in simp rule??*) by simp with eval_evals.TryCatch[OF IH1[OF fv1] _ subtype IH2'] lookup show ?caseby fastforce next case TryThrow thus ?caseby simp (blast intro: eval_evals.TryThrow) next case Nil thus ?caseby (simp add: eval_evals.Nil) next case Cons thus ?caseby simp (blast intro: eval_evals.Cons) next case ConsThrow thus ?caseby simp (blast intro: eval_evals.ConsThrow) next case InitFinal thus ?caseby (simp add: eval_evals.InitFinal) next case InitNone thus ?caseby(blast intro: eval_evals.InitNone) next case InitDone thus ?case by (simp add: InitDone.hyps(2) InitDone.prems eval_evals.InitDone) next case InitProcessing thus ?caseby (simp add: eval_evals.InitProcessing) next case InitError thus ?caseusing eval_evals.InitError by auto next case InitObject thus ?caseby(simp add: eval_evals.InitObject) next case InitNonObject thus ?caseby(simp add: eval_evals.InitNonObject) next case InitRInit thus ?caseby(simp add: eval_evals.InitRInit) next case (RInit e h l sh v h' l' sh' C sfs i sh'' C' Cs e' e1 h1 l1 sh1) have f1: "fv e ⊆ W ∧ fv (INIT C' (Cs,True) ← e') ⊆ W" using RInit.prems by auto thenhave f2: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨Val v,(h', l' |` W, sh')⟩" using RInit.hyps(2) by blast have"P ⊨⟨INIT C' (Cs,True) ← e', (h', l' |` W, sh'')⟩==>⟨e1,(h1, l1 |` W, sh1)⟩" using f1 by (meson RInit.hyps(7)) thenshow ?case using f2 RInit.hyps(3) RInit.hyps(4) RInit.hyps(5) eval_evals.RInit by blast next case (RInitInitFail e h l sh a h' l' sh' C sfs i sh'' D Cs e' e1 h1 l1 sh1) have f1: "fv e ⊆ W""fv e' ⊆ W" using RInitInitFail.prems by auto thenhave f2: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨throw a,(h', l' |` W, sh')⟩" using RInitInitFail.hyps(2) by blast thenhave f2': "fv (throw a) ⊆ W" using eval_final[OF f2] by auto thenhave f1': "fv (RI (D,throw a);Cs ← e') ⊆ W" using f1 by auto have"P ⊨⟨RI (D,throw a);Cs ← e', (h', l' |` W, sh'')⟩==>⟨e1,(h1, l1 |` W, sh1)⟩" using f1' by (meson RInitInitFail.hyps(6)) thenshow ?case using f2 by (simp add: RInitInitFail.hyps(3,4) eval_evals.RInitInitFail) next case (RInitFailFinal e h l sh a h' l' sh' sh'' C) have f1: "fv e ⊆ W" using RInitFailFinal.prems by auto thenhave f2: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨throw a,(h', l' |` W, sh')⟩" using RInitFailFinal.hyps(2) by blast thenhave f2': "fv (throw a) ⊆ W" using eval_final[OF f2] by auto thenshow ?caseusing f2 RInitFailFinal.hyps(3,4) eval_evals.RInitFailFinal by blast qed (*>*)
lemma eval_notfree_unchanged: "P ⊨⟨e,(h,l,sh)⟩==>⟨e',(h',l',sh')⟩==> (∧V. V ∉ fv e ==> l' V = l V)" and"P ⊨⟨es,(h,l,sh)⟩ [==>] ⟨es',(h',l',sh')⟩==> (∧V. V ∉ fvs es ==> l' V = l V)" (*<*) proof(induct rule:eval_evals_inducts) case LAss thus ?caseby(simp add:fun_upd_apply) next case Block thus ?case by (simp only:fun_upd_apply split:if_splits) fastforce next case TryCatch thus ?case by (simp only:fun_upd_apply split:if_splits) fastforce next case (RInitInitFail e h l sh a h' l' sh' C sfs i sh'' D Cs e1 h1 l1 sh1) have"fv (throw a) = {}" using RInitInitFail.hyps(1) eval_final final_fv by blast thenhave"fv e ∪ fv (RI (D,throw a) ; Cs ← unit) ⊆ fv (RI (C,e) ; D#Cs ← unit)" by auto thenshow ?caseusing RInitInitFail.hyps(2,6) RInitInitFail.prems by fastforce qed simp_all (*>*)
lemma eval_closed_lcl_unchanged: "[ P ⊨⟨e,(h,l,sh)⟩==>⟨e',(h',l',sh')⟩; fv e = {} ]==> l' = l" (*<*)by(fastforce dest:eval_notfree_unchanged simp add:fun_eq_iff [where 'b="val option"])(*>*)
lemma list_eval_Throw: assumes eval_e: "P ⊨⟨throw x,s⟩==>⟨e',s'⟩" shows"P ⊨⟨map Val vs @ throw x # es',s⟩ [==>] ⟨map Val vs @ e' # es',s'⟩" (*<*) proof - from eval_e obtain a where e': "e' = Throw a" by (cases) (auto dest!: eval_final)
{ fix es have"∧vs. es = map Val vs @ throw x # es' ==> P ⊨⟨es,s⟩[==>]⟨map Val vs @ e' # es',s'⟩" proof (induct es type: list) case Nil thus ?caseby simp next case (Cons e es vs) have e_es: "e # es = map Val vs @ throw x # es'"by fact show"P ⊨⟨e # es,s⟩ [==>] ⟨map Val vs @ e' # es',s'⟩" proof (cases vs) case Nil with e_es obtain"e=throw x""es=es'"by simp moreoverfrom eval_e e' have"P ⊨⟨throw x # es,s⟩ [==>] ⟨Throw a # es,s'⟩" by (iprover intro: ConsThrow) ultimatelyshow ?thesis using Nil e' by simp next case (Cons v vs') have vs: "vs = v # vs'"by fact with e_es obtain
e: "e=Val v"and es:"es= map Val vs' @ throw x # es'" by simp from e have"P ⊨⟨e,s⟩==>⟨Val v,s⟩" by (iprover intro: eval_evals.Val) moreoverfrom es have"P ⊨⟨es,s⟩ [==>] ⟨map Val vs' @ e' # es',s'⟩" by (rule Cons.hyps) ultimatelyshow "P ⊨⟨e#es,s⟩ [==>] ⟨map Val vs @ e' # es',s'⟩" using vs by (auto intro: eval_evals.Cons) qed qed
} thus ?thesis by simp qed (*>*)
―‹ separate evaluation of first subexp of a sequence › lemma seq_ext: assumes IH: "∧e' s'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩" and seq: "P ⊨⟨e'' ;; e0,s''⟩==>⟨e',s'⟩" shows"P ⊨⟨e ;; e0,s⟩==>⟨e',s'⟩" proof(rule eval_cases(14)[OF seq]) ―‹ Seq › fix v' s1assume e'': "P ⊨⟨e'',s''⟩==>⟨Val v',s1⟩"and estep: "P ⊨⟨e0,s1⟩==>⟨e',s'⟩" have"P ⊨⟨e,s⟩==>⟨Val v',s1⟩"using e'' IH by simp thenshow ?thesis using estep Seq by simp next fix etassume e'': "P ⊨⟨e'',s''⟩==>⟨throw et,s'⟩"and e': "e' = throw et" have"P ⊨⟨e,s⟩==>⟨throw et,s'⟩"using e'' IH by simp thenshow ?thesis using eval_evals.SeqThrow e' by simp qed
―‹ separate evaluation of @{text RI} subexp, val case › lemma rinit_Val_ext: assumes ri: "P ⊨⟨RI (C,e'') ; Cs ← e0,s''⟩==>⟨Val v',s1⟩" and IH: "∧e' s'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩" shows"P ⊨⟨RI (C,e) ; Cs ← e0,s⟩==>⟨Val v',s1⟩" proof(rule eval_cases(20)[OF ri]) ―‹ RI › fix v'' h' l' sh' sfs i assume e''step: "P ⊨⟨e'',s''⟩==>⟨Val v'',(h', l', sh')⟩" and shC: "sh' C = ⌊(sfs, i)⌋" and init: "P ⊨⟨INIT (if Cs = [] then C else last Cs) (Cs,True) ← e0,(h', l', sh'(C ↦ (sfs, Done)))⟩==> ⟨Val v',s1⟩" have"P ⊨⟨e,s⟩==>⟨Val v'',(h', l', sh')⟩"using IH[OF e''step] by simp thenshow ?thesis using RInit init shC by auto next fix a h' l' sh' sfs i D Cs' assume e''step: "P ⊨⟨e'',s''⟩==>⟨throw a,(h', l', sh')⟩" and riD: "P ⊨⟨RI (D,throw a) ; Cs' ← e0,(h', l', sh'(C ↦ (sfs, Error)))⟩==>⟨Val v',s1⟩" have"P ⊨⟨e,s⟩==>⟨throw a,(h', l', sh')⟩"using IH[OF e''step] by simp thenshow ?thesis using riD rinit_throwE by blast qed(simp)
―‹ separate evaluation of @{text RI} subexp, throw case › lemma rinit_throw_ext: assumes ri: "P ⊨⟨RI (C,e'') ; Cs ← e0,s''⟩==>⟨throw et,s'⟩" and IH: "∧e' s'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩" shows"P ⊨⟨RI (C,e) ; Cs ← e0,s⟩==>⟨throw et,s'⟩" proof(rule eval_cases(20)[OF ri]) ―‹ RI › fix v h' l' sh' sfs i assume e''step: "P ⊨⟨e'',s''⟩==>⟨Val v,(h', l', sh')⟩" and shC: "sh' C = ⌊(sfs, i)⌋" and init: "P ⊨⟨INIT (if Cs = [] then C else last Cs) (Cs,True) ← e0,(h', l', sh'(C ↦ (sfs, Done)))⟩==> ⟨throw et,s'⟩" have"P ⊨⟨e,s⟩==>⟨Val v,(h', l', sh')⟩"using IH[OF e''step] by simp thenshow ?thesis using RInit init shC by auto next fix a h' l' sh' sfs i D Cs' assume e''step: "P ⊨⟨e'',s''⟩==>⟨throw a,(h', l', sh')⟩" and shC: "sh' C = ⌊(sfs, i)⌋" and riD: "P ⊨⟨RI (D,throw a) ; Cs' ← e0,(h', l', sh'(C ↦ (sfs, Error)))⟩==>⟨throw et,s'⟩" and cons: "Cs = D # Cs'" have estep': "P ⊨⟨e,s⟩==>⟨throw a,(h', l', sh')⟩"using IH[OF e''step] by simp thenshow ?thesis using RInitInitFail cons riD shC by simp next fix a h' l' sh' sfs i assume"throw et = throw a" and"s' = (h', l', sh'(C ↦ (sfs, Error)))" and"P ⊨⟨e'',s''⟩==>⟨throw a,(h', l', sh')⟩" and"sh' C = ⌊(sfs, i)⌋" and"Cs = []" thenshow ?thesis using RInitFailFinal IH by auto qed
―‹ separate evaluation of @{text RI} subexp › lemma rinit_ext: assumes IH: "∧e' s'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩" shows"∧e' s'. P ⊨⟨RI (C,e'') ; Cs ← e0,s''⟩==>⟨e',s'⟩ ==> P ⊨⟨RI (C,e) ; Cs ← e0,s⟩==>⟨e',s'⟩" proof - fix e' s' assume ri'': "P ⊨⟨RI (C,e'') ; Cs ← e0,s''⟩==>⟨e',s'⟩" thenhave"final e'"using eval_final by simp thenshow"P ⊨⟨RI (C,e) ; Cs ← e0,s⟩==>⟨e',s'⟩" proof(rule finalE) fix v assume"e' = Val v"thenshow ?thesis using rinit_Val_ext[OF _ IH] ri'' by simp next fix a assume"e' = throw a"thenshow ?thesis using rinit_throw_ext[OF _ IH] ri'' by simp qed qed
―‹ @{text INIT} and @{text RI} return either @{text Val} with @{text Done} or
@{text Processing} flag or @{text Throw} with @{text Error} flag › lemma shows eval_init_return: "P ⊨⟨e,s⟩==>⟨e',s'⟩ ==> iconf (shp s) e ==> (∃Cs b. e = INIT C' (Cs,b) ← unit) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs@[C'] ← unit) ∨ (∃e0. e = RI(C',e0);Nil ← unit) ==> (val_of e' = Some v ⟶ (∃sfs i. shp s' C' = ⌊(sfs,i)⌋∧ (i = Done ∨ i = Processing))) ∧ (throw_of e' = Some a ⟶ (∃sfs i. shp s' C' = ⌊(sfs,Error)⌋))" and"P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩==> True" proof(induct rule: eval_evals.inducts) case (InitFinal e s e' s' C b) thenshow ?case by(fastforce simp: initPD_def dest: eval_final_same) next case (InitDone sh C sfs C' Cs e h l e' s') thenhave"final e'"using eval_final by simp thenshow ?case proof(rule finalE) fix v assume e': "e' = Val v"thenshow ?thesis using InitDone initPD_def proof(cases Cs) qed(auto) next fix a assume e': "e' = throw a"thenshow ?thesis using InitDone initPD_def proof(cases Cs) qed(auto) qed next case (InitProcessing sh C sfs C' Cs e h l e' s') thenhave"final e'"using eval_final by simp thenshow ?case proof(rule finalE) fix v assume e': "e' = Val v"thenshow ?thesis using InitProcessing initPD_def proof(cases Cs) qed(auto) next fix a assume e': "e' = throw a"thenshow ?thesis using InitProcessing initPD_def proof(cases Cs) qed(auto) qed next case (InitError sh C sfs Cs e h l e' s' C') show ?case proof(cases Cs) case Nil thenshow ?thesis using InitError by simp next case (Cons C2 list) thenhave"final e'"using InitError eval_final by simp thenshow ?thesis proof(rule finalE) fix v assume e': "e' = Val v"thenshow ?thesis using InitError proof - obtain ccss :: "char list list"and bb :: bool where "INIT C' (C # Cs,False) ← e = INIT C' (ccss,bb) ← unit" using InitError.prems(2) by blast thenshow ?thesis using InitError.hyps(2) e' by(auto dest!: rinit_throwE) qed next fix a assume e': "e' = throw a" thenshow ?thesis using Cons InitError cons_to_append[of list] by clarsimp qed qed next case (InitRInit C Cs h l sh e' s' C') show ?case proof(cases Cs) case Nil thenshow ?thesis using InitRInit by simp next case (Cons C' list) thenshow ?thesis using InitRInit Cons cons_to_append[of list] by clarsimp qed next case (RInit e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1) thenhave final: "final e1"using eval_final by simp thenshow ?case proof(cases Cs) case Nil show ?thesis using final proof(rule finalE) fix v assume e': "e1 = Val v"show ?thesis using RInit Nil by(auto simp: fun_upd_same initPD_def) next fix a assume e': "e1 = throw a"show ?thesis using RInit Nil by(auto simp: fun_upd_same initPD_def) qed next case (Cons a list) show ?thesis proof(rule finalE[OF final]) fix v assume e': "e1 = Val v"thenshow ?thesis using RInit Cons by clarsimp (metis last.simps last_appendR list.distinct(1)) next fix a assume e': "e1 = throw a"thenshow ?thesis using RInit Cons by clarsimp (metis last.simps last_appendR list.distinct(1)) qed qed next case (RInitInitFail e s a h' l' sh' C sfs i sh'' D Cs e' e1 s1) thenhave final: "final e1"using eval_final by simp thenshow ?case proof(rule finalE) fix v assume e': "e1 = Val v"thenshow ?thesis using RInitInitFail by clarsimp (meson exp.distinct(101) rinit_throwE) next fix a' assume e': "e1 = Throw a'" thenhave"iconf (sh'(C ↦ (sfs, Error))) a" using RInitInitFail.hyps(1) eval_final by fastforce thenshow ?thesis using RInitInitFail e' by clarsimp (meson Cons_eq_append_conv list.inject) qed qed(auto simp: fun_upd_same)
lemma init_Val_PD: "P ⊨⟨INIT C' (Cs,b) ← unit,s⟩==>⟨Val v,s'⟩ ==> iconf (shp s) (INIT C' (Cs,b) ← unit) ==>∃sfs i. shp s' C' = ⌊(sfs,i)⌋∧ (i = Done ∨ i = Processing)" by(drule_tac v = v in eval_init_return, simp+)
lemma init_throw_PD: "P ⊨⟨INIT C' (Cs,b) ← unit,s⟩==>⟨throw a,s'⟩ ==> iconf (shp s) (INIT C' (Cs,b) ← unit) ==>∃sfs i. shp s' C' = ⌊(sfs,Error)⌋" by(drule_tac a = a in eval_init_return, simp+)
lemma rinit_Val_PD: "P ⊨⟨RI(C,e0);Cs ← unit,s⟩==>⟨Val v,s'⟩ ==> iconf (shp s) (RI(C,e0);Cs ← unit) ==> last(C#Cs) = C' ==>∃sfs i. shp s' C' = ⌊(sfs,i)⌋∧ (i = Done ∨ i = Processing)" by(auto dest!: eval_init_return [where C'=C']
append_butlast_last_id[THEN sym])
lemma rinit_throw_PD: "P ⊨⟨RI(C,e0);Cs ← unit,s⟩==>⟨throw a,s'⟩ ==> iconf (shp s) (RI(C,e0);Cs ← unit) ==> last(C#Cs) = C' ==>∃sfs i. shp s' C' = ⌊(sfs,Error)⌋" by(auto dest!: eval_init_return [where C'=C']
append_butlast_last_id[THEN sym])
―‹ combining the above to get evaluation of @{text INIT} in a sequence ›
(* Hiermit kann man die ganze pair-Splitterei in den automatischen Taktiken
abschalten. Wieder anschalten siehe nach dem Beweis. *) (*<*) declare split_paired_All [simp del] split_paired_Ex [simp del] (*>*)
lemma eval_init_seq': "P ⊨⟨e,s⟩==>⟨e',s'⟩ ==> (∃C Cs b ei. e = INIT C (Cs,b) ← ei) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs ← ei) ==> (∃C Cs b ei. e = INIT C (Cs,b) ← ei∧ P ⊨⟨(INIT C (Cs,b) ← unit);; ei,s⟩==>⟨e',s'⟩) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs ← ei∧ P ⊨⟨(RI(C,e0);Cs ← unit);; ei,s⟩==>⟨e',s'⟩)" and"P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩==> True" proof(induct rule: eval_evals.inducts) case InitFinal thenshow ?caseby(auto simp: Seq[OF eval_evals.InitFinal[OF Val[where v=Unit]]]) next case (InitNone sh) thenshow ?case using seq_ext[OF eval_evals.InitNone[where sh=sh and e=unit, OF InitNone.hyps(1)]] by fastforce next case (InitDone sh) thenshow ?case using seq_ext[OF eval_evals.InitDone[where sh=sh and e=unit, OF InitDone.hyps(1)]] by fastforce next case (InitProcessing sh) thenshow ?case using seq_ext[OF eval_evals.InitProcessing[where sh=sh and e=unit, OF InitProcessing.hyps(1)]] by fastforce next case (InitError sh) thenshow ?case using seq_ext[OF eval_evals.InitError[where sh=sh and e=unit, OF InitError.hyps(1)]] by fastforce next case (InitObject sh) thenshow ?case using seq_ext[OF eval_evals.InitObject[where sh=sh and e=unit, OF InitObject.hyps(1)]] by fastforce next case (InitNonObject sh) thenshow ?case using seq_ext[OF eval_evals.InitNonObject[where sh=sh and e=unit, OF InitNonObject.hyps(1)]] by fastforce next case (InitRInit C Cs e h l sh e' s' C') thenshow ?case using seq_ext[OF eval_evals.InitRInit[where e=unit]] by fastforce next case RInit thenshow ?case using seq_ext[OF eval_evals.RInit[where e=unit, OF RInit.hyps(1)]] by fastforce next case RInitInitFail thenshow ?case using seq_ext[OF eval_evals.RInitInitFail[where e=unit, OF RInitInitFail.hyps(1)]] by fastforce next case RInitFailFinal thenshow ?caseusing eval_evals.RInitFailFinal eval_evals.SeqThrow by auto qed(auto)
lemma eval_init_seq: "P ⊨⟨INIT C (Cs,b) ← e,(h, l, sh)⟩==>⟨e',s'⟩ ==> P ⊨⟨(INIT C (Cs,b) ← unit);; e,(h, l, sh)⟩==>⟨e',s'⟩" by(auto dest: eval_init_seq')
text‹ The key lemma: › lemma assumes wf: "wwf_J_prog P" shows extend_1_eval: "P ⊨⟨e,s,b⟩→⟨e'',s'',b''⟩==> P,shp s ⊨b (e,b) √ ==> (∧s' e'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩)" and extend_1_evals: "P ⊨⟨es,s,b⟩ [→] ⟨es'',s'',b''⟩==> P,shp s ⊨b (es,b) √ ==> (∧s' es'. P ⊨⟨es'',s''⟩ [==>] ⟨es',s'⟩==> P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩)" proof (induct rule: red_reds.inducts) case (RedNew h a C FDTs h' l sh) thenhave e':"e' = addr a"and s':"s' = (h(a ↦ blank P C), l, sh)" using eval_cases(3) by fastforce+ obtain sfs i where shC: "sh C = ⌊(sfs, i)⌋"and"i = Done ∨ i = Processing" using RedNew by (clarsimp simp: bconf_def initPD_def) thenshow ?case proof(cases i) caseDonethenshow ?thesis using RedNew shC e' s' New by simp next case Processing thenhave shC': "∄sfs. sh C = Some(sfs,Done)"and shP: "sh C = Some(sfs,Processing)" using shC by simp+ thenhave init: "P ⊨⟨INIT C ([C],False) ← unit,(h,l,sh)⟩==>⟨unit,(h,l,sh)⟩" by(simp add: InitFinal InitProcessing Val) have"P ⊨⟨new C,(h, l, sh)⟩==>⟨addr a,(h(a ↦ blank P C),l,sh)⟩" using RedNew shC' by(auto intro: NewInit[OF _ init]) thenshow ?thesis using e' s' by simp qed(auto) next case (RedNewFail h C l sh) thenhave e':"e' = THROW OutOfMemory"and s':"s' = (h, l, sh)" using eval_final_same final_def by fastforce+ obtain sfs i where shC: "sh C = ⌊(sfs, i)⌋"and"i = Done ∨ i = Processing" using RedNewFail by (clarsimp simp: bconf_def initPD_def) thenshow ?case proof(cases i) caseDonethenshow ?thesis using RedNewFail shC e' s' NewFail by simp next case Processing thenhave shC': "∄sfs. sh C = Some(sfs,Done)"and shP: "sh C = Some(sfs,Processing)" using shC by simp+ thenhave init: "P ⊨⟨INIT C ([C],False) ← unit,(h,l,sh)⟩==>⟨unit,(h,l,sh)⟩" by(simp add: InitFinal InitProcessing Val) have"P ⊨⟨new C,(h, l, sh)⟩==>⟨THROW OutOfMemory,(h,l,sh)⟩" using RedNewFail shC' by(auto intro: NewInitOOM[OF _ init]) thenshow ?thesis using e' s' by simp qed(auto) next case (NewInitRed sh C h l) thenhave seq: "P ⊨⟨(INIT C ([C],False) ← unit);; new C,(h, l, sh)⟩==>⟨e',s'⟩" using eval_init_seq by simp thenshow ?case proof(rule eval_cases(14)) ―‹ Seq › fix v s1assume init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh)⟩==>⟨Val v,s1⟩" and new: "P ⊨⟨new C,s1⟩==>⟨e',s'⟩" obtain h1 l1 sh1where s1: "s1 = (h1,l1,sh1)"by(cases s1) thenobtain sfs i where shC: "sh1 C = ⌊(sfs, i)⌋"and iDP: "i = Done ∨ i = Processing" using init_Val_PD[OF init] by auto show ?thesis proof(rule eval_cases(1)[OF new]) ―‹ New › fix sha ha a FDTs la assume s1a: "s1 = (ha, la, sha)"and e': "e' = addr a" and s': "s' = (ha(a ↦ blank P C), la, sha)" and addr: "new_Addr ha = ⌊a⌋"and fields: "P ⊨ C has_fields FDTs" thenshow ?thesis using NewInit[OF _ _ addr fields] NewInitRed.hyps init by simp next fix sha ha la assume"s1 = (ha, la, sha)"and"e' = THROW OutOfMemory" and"s' = (ha, la, sha)"and"new_Addr ha = None" thenshow ?thesis using NewInitOOM NewInitRed.hyps init by simp next fix sha ha la v' h' l' sh' a FDTs assume s1a: "s1 = (ha, la, sha)"and e': "e' = addr a" and s': "s' = (h'(a ↦ blank P C), l', sh')" and shaC: "∀sfs. sha C ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩==>⟨Val v',(h', l', sh')⟩" and addr: "new_Addr h' = ⌊a⌋"and fields: "P ⊨ C has_fields FDTs" thenhave i: "i = Processing"using iDP shC s1by simp thenhave"(h', l', sh') = (ha, la, sha)"using init' init_ProcessingE s1 s1a shC by blast thenshow ?thesis using NewInit NewInitRed.hyps s1a addr fields init shaC e' s' by auto next fix sha ha la v' h' l' sh' assume s1a: "s1 = (ha, la, sha)"and e': "e' = THROW OutOfMemory" and s': "s' = (h', l', sh')"and"∀sfs. sha C ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩==>⟨Val v',(h', l', sh')⟩" and addr: "new_Addr h' = None" thenhave i: "i = Processing"using iDP shC s1by simp thenhave"(h', l', sh') = (ha, la, sha)"using init' init_ProcessingE s1 s1a shC by blast thenshow ?thesis using NewInitOOM NewInitRed.hyps e' addr s' s1a init by auto next fix sha ha la a assume s1a: "s1 = (ha, la, sha)" and"∀sfs. sha C ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩==>⟨throw a,s'⟩" thenhave i: "i = Processing"using iDP shC s1by simp thenshow ?thesis using init' init_ProcessingE s1 s1a shC by blast qed next fix e assume e': "e' = throw e" and init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh)⟩==>⟨throw e,s'⟩" obtain h' l' sh' where s': "s' = (h',l',sh')"by(cases s') thenobtain sfs i where shC: "sh' C = ⌊(sfs, i)⌋"and iDP: "i = Error" using init_throw_PD[OF init] by auto thenshow ?thesis by (simp add: NewInitRed.hyps NewInitThrow e' init) qed next case CastRed thenshow ?case by(fastforce elim!: eval_cases intro: eval_evals.intros intro!: CastFail) next case RedCastNull thenshow ?case by simp (iprover elim: eval_cases intro: eval_evals.intros) next case RedCast thenshow ?case by (auto elim: eval_cases intro: eval_evals.intros) next case RedCastFail thenshow ?case by (auto elim!: eval_cases intro: eval_evals.intros) next case BinOpRed1 thenshow ?case by(fastforce elim!: eval_cases intro: eval_evals.intros simp: val_no_step) next case BinOpRed2 thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId) next case RedBinOp thus ?case by simp (iprover elim: eval_cases intro: eval_evals.intros) next case RedVar thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case LAssRed thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case RedLAss thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case FAccRed thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case RedFAcc thenshow ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case RedFAccNull thenshow ?case by (fastforce elim!: eval_cases intro: eval_evals.intros) next case RedFAccNone thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case RedFAccStatic thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case (RedSFAcc C F t D sh sfs i v h l) thenhave e':"e' = Val v"and s':"s' = (h, l, sh)" using eval_cases(3) by fastforce+ have"i = Done ∨ i = Processing"using RedSFAcc by (clarsimp simp: bconf_def initPD_def) thenshow ?case proof(cases i) caseDonethenshow ?thesis using RedSFAcc e' s' SFAcc by simp next case Processing thenhave shC': "∄sfs. sh D = Some(sfs,Done)"and shP: "sh D = Some(sfs,Processing)" using RedSFAcc by simp+ thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h,l,sh)⟩==>⟨unit,(h,l,sh)⟩" by(simp add: InitFinal InitProcessing Val) have"P ⊨⟨C∙sF{D},(h, l, sh)⟩==>⟨Val v,(h,l,sh)⟩" by(rule SFAccInit[OF RedSFAcc.hyps(1) shC' init shP RedSFAcc.hyps(3)]) thenshow ?thesis using e' s' by simp qed(auto) next case (SFAccInitRed C F t D sh h l) thenhave seq: "P ⊨⟨(INIT D ([D],False) ← unit);; C∙sF{D},(h, l, sh)⟩==>⟨e',s'⟩" using eval_init_seq by simp thenshow ?case proof(rule eval_cases(14)) ―‹ Seq › fix v s1assume init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨Val v,s1⟩" and acc: "P ⊨⟨C∙sF{D},s1⟩==>⟨e',s'⟩" obtain h1 l1 sh1where s1: "s1 = (h1,l1,sh1)"by(cases s1) thenobtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋"and iDP: "i = Done ∨ i = Processing" using init_Val_PD[OF init] by auto show ?thesis proof(rule eval_cases(8)[OF acc]) ―‹ SFAcc › fix t sha sfs v ha la assume"s1 = (ha, la, sha)"and"e' = Val v" and"s' = (ha, la, sha)"and"P ⊨ C has F,Static:t in D" and"sha D = ⌊(sfs, Done)⌋"and"sfs F = ⌊v⌋" thenshow ?thesis using SFAccInit SFAccInitRed.hyps(2) init by auto next fix t sha ha la v' h' l' sh' sfs i' v assume s1a: "s1 = (ha, la, sha)"and e': "e' = Val v" and s': "s' = (h', l', sh')"and field: "P ⊨ C has F,Static:t in D" and"∀sfs. sha D ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT D ([D],False) ← unit,(ha, la, sha)⟩==>⟨Val v',(h', l', sh')⟩" and shD': "sh' D = ⌊(sfs, i')⌋"and sfsF: "sfs F = ⌊v⌋" thenhave i: "i = Processing"using iDP shD s1by simp thenhave"(h', l', sh') = (ha, la, sha)"using init' init_ProcessingE s1 s1a shD by blast thenshow ?thesis using SFAccInit SFAccInitRed.hyps(2) e' s' field init s1a sfsF shD' by auto next fix t sha ha la a assume s1a: "s1 = (ha, la, sha)"and"e' = throw a" and"P ⊨ C has F,Static:t in D"and"∀sfs. sha D ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT D ([D],False) ← unit,(ha, la, sha)⟩==>⟨throw a,s'⟩" thenhave i: "i = Processing"using iDP shD s1by simp thenshow ?thesis using init' init_ProcessingE s1 s1a shD by blast next assume"∀b t. ¬ P ⊨ C has F,b:t in D" thenshow ?thesis using SFAccInitRed.hyps(1) by blast next fix t assume field: "P ⊨ C has F,NonStatic:t in D" thenshow ?thesis using has_field_fun[OF SFAccInitRed.hyps(1) field] by simp qed next fix e assume e': "e' = throw e" and init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨throw e,s'⟩" obtain h' l' sh' where s': "s' = (h',l',sh')"by(cases s') thenobtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋"and iDP: "i = Error" using init_throw_PD[OF init] by auto thenshow ?thesis using SFAccInitRed.hyps(1) SFAccInitRed.hyps(2) SFAccInitThrow e' init by auto qed next case RedSFAccNone thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case RedSFAccNonStatic thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case (FAssRed1 e s b e1 s1 b1 F D e2) obtain h' l' sh' where"s'=(h',l',sh')"by(cases s') with FAssRed1 show ?case by(fastforce elim!: eval_cases(9)[where e1=e1] intro: eval_evals.intros simp: val_no_step
intro!: FAss FAssNull FAssNone FAssStatic FAssThrow2) next case FAssRed2 obtain h' l' sh' where"s'=(h',l',sh')"by(cases s') with FAssRed2 show ?case by(auto elim!: eval_cases intro: eval_evals.intros
intro!: FAss FAssNull FAssNone FAssStatic FAssThrow2 Val) next case RedFAss thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros) next case RedFAssNull thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros) next case RedFAssNone thenshow ?case by(auto elim!: eval_cases intro: eval_evals.intros eval_finalId) next case RedFAssStatic thenshow ?case by(auto elim!: eval_cases intro: eval_evals.intros eval_finalId) next case (SFAssRed e s b e'' s'' b'' C F D) obtain h l sh where [simp]: "s = (h,l,sh)"by(cases s) obtain h' l' sh' where [simp]: "s'=(h',l',sh')"by(cases s') have"val_of e = None"using val_no_step SFAssRed.hyps(1) by(meson option.exhaust) thenhave bconf: "P,sh ⊨b (e,b) √"using SFAssRed by simp show ?caseusing SFAssRed.prems(2) SFAssRed bconf proof cases case2with SFAssRed bconf show ?thesis by(auto intro!: SFAssInit) next case3with SFAssRed bconf show ?thesis by(auto intro!: SFAssInitThrow) qed(auto intro: eval_evals.intros intro!: SFAss SFAssInit SFAssNone SFAssNonStatic) next case (RedSFAss C F t D sh sfs i sfs' v sh' h l) let ?sfs' = "sfs(F ↦ v)" have e':"e' = unit"and s':"s' = (h, l, sh(D ↦ (?sfs', i)))" using RedSFAss eval_cases(3) by fastforce+ have"i = Done ∨ i = Processing"using RedSFAss by(clarsimp simp: bconf_def initPD_def) thenshow ?case proof(cases i) caseDonethenshow ?thesis using RedSFAss e' s' SFAss Val by auto next case Processing thenhave shC': "∄sfs. sh D = Some(sfs,Done)"and shP: "sh D = Some(sfs,Processing)" using RedSFAss by simp+ thenhave init: "P ⊨⟨INIT D ([D],False) ← unit,(h,l,sh)⟩==>⟨unit,(h,l,sh)⟩" by(simp add: InitFinal InitProcessing Val) have"P ⊨⟨C∙sF{D} := Val v,(h, l, sh)⟩==>⟨unit,(h,l,sh(D ↦ (?sfs', i)))⟩" using Processing by(auto intro: SFAssInit[OF Val RedSFAss.hyps(1) shC' init shP]) thenshow ?thesis using e' s' by simp qed(auto) next case (SFAssInitRed C F t D sh v h l) thenhave seq: "P ⊨⟨(INIT D ([D],False) ← unit);; C∙sF{D} := Val v,(h, l, sh)⟩==>⟨e',s'⟩" using eval_init_seq by simp thenshow ?case proof(rule eval_cases(14)) ―‹ Seq › fix v' s1assume init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨Val v',s1⟩" and acc: "P ⊨⟨C∙sF{D} := Val v,s1⟩==>⟨e',s'⟩" obtain h1 l1 sh1where s1: "s1 = (h1,l1,sh1)"by(cases s1) thenobtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋"and iDP: "i = Done ∨ i = Processing" using init_Val_PD[OF init] by auto show ?thesis proof(rule eval_cases(10)[OF acc]) ―‹ SFAss › fix va h1 l1 sh1 t sfs assume e': "e' = unit"and s': "s' = (h1, l1, sh1(D ↦ (sfs(F ↦ va), Done)))" and val: "P ⊨⟨Val v,s1⟩==>⟨Val va,(h1, l1, sh1)⟩" and field: "P ⊨ C has F,Static:t in D"and shD': "sh1 D = ⌊(sfs, Done)⌋" have"v = va"and"s1 = (h1, l1, sh1)"using eval_final_same[OF val] by auto thenshow ?thesis using SFAssInit field SFAssInitRed.hyps(2) shD' e' s' init val by (metis eval_final eval_finalId) next fix va h1 l1 sh1 t v' h' l' sh' sfs i' assumee: "'=uit"s "s' = (h', l', sh'(D \mapsto> (sfs(F ↦))" and val: "P ⊨⟨1⟩==>Val va,(h1, sh" and field: "P ⊨ C has<ightarrow < (g,g') ∈succs and init': " ⟨ unit,(h1, sh==>∠ and shD': "sh' D = ⌊(sfs, i')⌋" have v: "v = vajava.lang.NullPointerException then have i: "i = Processing" using iDP shD s\> ∀ set(succs g) ⟶ P g g 🚫 P g'" have^>, l1, sh1) = (h', l', sh')java.lang.NullPointerException then show ?thesis using SFAssInit SFAssInitRed.hyps(2) e' s' field init v s1a shD' val by (metis eval_final eval_finalId) next fix va h1 l1 sh1 t a assume "e' = throw a" and val: "P ⊨⟨Val v,s1⟩==>⟨Val va,(h1, l1, sh1)⟩" and "P ⊨ C has F,Static:t in D" and nDone: "∀sfs. sh1 D ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1)⟩==>⟨throw a,s'⟩" have v: "v = va" and s1a: "s1 = (h1, l1, sh1)" using eval_final_same[OF val] by auto then have i: "i = Processing" using iDP shD s1 nDone by simp then have "(h1, l1, sh1) = s'" using init' init_ProcessingE s1 s1a shD by blast then show ?thesis using init' init_ProcessingE s1 s1a shD i by blast next fix e'' assume val:"P ⊨⟨Val v,s1⟩==>⟨throw e'',s'⟩" then show ?thesis using eval_final_same[OF val] by simp next assume "∀b t. ¬ P ⊨ C has F,b:t in D" then show ?thesis using SFAssInitRed.hyps(1) by blast next fix t assume field: "P ⊨ C has F,NonStatic:t in D" then show ?thesis using has_field_fun[OF SFAssInitRed.hyps(1) field] by simp qed next fix e assume e': "e' = throw e" and init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨throw e,s'⟩" obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s') then obtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋" and iDP: "i = Error" using init_throw_PD[OF init] by auto then show ?thesis using SFAssInitRed.hyps(1) SFAssInitRed.hyps(2) SFAssInitThrow Val by (metis e' init) qed next case (RedSFAssNone C F D v s b) then show ?case by(cases s) (auto elim!: eval_cases intro: eval_evals.intros eval_finalId) next case (RedSFAssNonStatic C F t D v s b) then show ?case by(cases s) (auto elim!: eval_cases intro: eval_evals.intros eval_finalId) next case CallObj note val_no_step[simp] from CallObj.prems(2) CallObj show ?case proof cases case 2 with CallObj show ?thesis by(fastforce intro!: CallParamsThrow) next case 3 with CallObj show ?thesis by(fastforce intro!: CallNull) next case 4 with CallObj show ?thesis by(fastforce intro!: CallNone) next case 5 with CallObj show ?thesis by(fastforce intro!: CallStatic) qed(fastforce intro!: CallObjThrow Call)+ next case (CallParams es s b es'' s'' b'' v M s') then obtain h' l' sh' where "s' = (h',l',sh')" by(cases s') with CallParams show ?case by(auto elim!: eval_cases intro!: CallNone eval_finalId CallStatic Val) (auto intro!: CallParamsThrow CallNull Call Val) next case (RedCall h a C fs M Ts T pns body D vs l sh b) have "P ⊨⟨addr a,(h,l,sh)⟩==>⟨addr a,(h,l,sh)⟩" by (rule eval_evals.intros) moreover have finals: "finals(map Val vs)" by simp with finals have "P ⊨⟨map Val vs,(h,l,sh)⟩ [==>] ⟨map Val vs,(h,l,sh)⟩" by (iprover intro: eval_finalsId) moreover have "h a = Some (C, fs)" using RedCall by simp moreover have "method": "P ⊨ C sees M,NonStatic: Ts→T = (pns, body) in D" by fact moreover have same_len1: "length Ts = length pns" and this_distinct: "this ∉ set pns" and fv: "fv (body) ⊆ {this} ∪ set pns" using "method" wf by (fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ have same_len: "length vs = length pns" by fact moreover obtain l2' where l2': "l2' = [this↦Addr a,pns[↦]vs]" by simp moreover obtain h3 l3 sh3 where s': "s' = (h3,l3,sh3)" by (cases s') have eval_blocks: "P ⊨⟨(blocks (this # pns, Class D # Ts, Addr a # vs, body)),(h,l,sh)⟩==>⟨e',s'⟩" by fact hence id: "l3 = l" using fv s' same_len1 same_len by(fastforce elim: eval_closed_lcl_unchanged) from eval_blocks obtain l3' where "P ⊨⟨body,(h,l2',sh)⟩==>⟨e',(h3,l3',sh3)⟩" proof - from same_len1 have "length(this#pns) = length(Class D#Ts)" by simp moreover from same_len1 same_len have same_len2: "length (this#pns) = length (Addr a#vs)" by simp moreover from eval_blocks have "P ⊨⟨blocks (this#pns,Class D#Ts,Addr a#vs,body),(h,l,sh)⟩ ==>⟨e',(h3,l3,sh3)⟩" using s' same_len1 same_len2 by simp ultimately obtain l'' where "P ⊨⟨body,(h,l(this # pns[↦]Addr a # vs),sh)⟩==>⟨e',(h3, l'',sh3)⟩" by (blast dest:blocksEval) from eval_restrict_lcl[OF wf this fv] this_distinct same_len1 same_len have "P ⊨⟨body,(h,[this # pns[↦]Addr a # vs],sh)⟩==> ⟨e',(h3, l''|`(set(this#pns)),sh3)⟩" using wf method by(simp add:subset_insert_iff insert_Diff_if) thus ?thesis by(fastforce intro!:that simp add: l2') qed ultimately have "P ⊨⟨(addr a)∙M(map Val vs),(h,l,sh)⟩==>⟨e',(h3,l,sh3)⟩" by (rule Call) with s' id show ?case by simp next case RedCallNull thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros eval_finalsId) next case (RedCallNone h a C fs M vs l sh b) then have tes: "THROW NoSuchMethodError = e' ∧ (h,l,sh) = s'" using eval_final_same by simp have "P ⊨⟨addr a,(h,l,sh)⟩==>⟨addr a,(h,l,sh)⟩" and "P ⊨⟨map Val vs,(h,l,sh)⟩ [==>] ⟨map Val vs,(h,l,sh)⟩" using eval_finalId eval_finalsId by auto then show ?case using RedCallNone CallNone tes by auto next case (RedCallStatic h a C fs M Ts T m D vs l sh b) then have tes: "THROW IncompatibleClassChangeError = e' ∧ (h,l,sh) = s'" using eval_final_same by simp have "P ⊨⟨addr a,(h,l,sh)⟩==>⟨addr a,(h,l,sh)⟩" and "P ⊨⟨map Val vs,(h,l,sh)⟩ [==>] ⟨map Val vs,(h,l,sh)⟩" using eval_finalId eval_finalsId by auto then show ?case using RedCallStatic CallStatic tes by fastforce next case (SCallParams es s b es'' s'' b' C M s') obtain h' l' sh' where s'[simp]: "s' = (h',l',sh')" by(cases s') obtain h l sh where s[simp]: "s = (h,l,sh)" by(cases s) have es: "map_vals_of es = None" using vals_no_step SCallParams.hyps(1) by (meson not_Some_eq) have bconf: "P,sh ⊨b (es,b) √" using s SCallParams.prems(1) by (simp add: bconf_SCall[OF es]) from SCallParams.prems(2) SCallParams bconf show ?case proof cases case 2 with SCallParams bconf show ?thesis by(auto intro!: SCallNone) next case 3 with SCallParams bconf show ?thesis by(auto intro!: SCallNonStatic) next case 4 with SCallParams bconf show ?thesis by(auto intro!: SCallInitThrow) next case 5 with SCallParams bconf show ?thesis by(auto intro!: SCallInit) qed(auto intro!: SCallParamsThrow SCall) next case (RedSCall C M Ts T pns body D vs s) then obtain h l sh where s:"s = (h,l,sh)" by(cases s) then obtain sfs i where shC: "sh D = ⌊(sfs, i)⌋" and "i = Done∨ i = Processing" using RedSCall by(auto simp: bconf_def initPD_def dest: sees_method_fun) have finals: "finals(map Val vs)" by simp with finals have mVs: "P ⊨⟨map Val vs,(h,l,sh)⟩ [==>] ⟨map Val vs,(h,l,sh)⟩" by (iprover intro: eval_finalsId) obtain sfs i where shC: "sh D = ⌊(sfs, i)⌋" using RedSCall s by(auto simp: bconf_def initPD_def dest: sees_method_fun) then have iDP: "i = Done∨ i = Processing" using RedSCall s by (auto simp: bconf_def initPD_def dest: sees_method_fun[OF RedSCall.hyps(1)]) have "method": "P ⊨ C sees M,Static: Ts→T = (pns, body) in D" by fact have same_len1: "length Ts = length pns" and fv: "fv (body) ⊆ set pns" using "method" wf by (fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+ have same_len: "length vs = length pns" by fact obtain l2' where l2': "l2' = [pns[↦]vs]" by simp obtain h3 l3 sh3 where s': "s' = (h3,l3,sh3)" by (cases s') have eval_blocks: "P ⊨⟨(blocks (pns, Ts, vs, body)),(h,l,sh)⟩==>⟨e',s'⟩" using RedSCall.prems(2) s by simp hence id: "l3 = l" using fv s' same_len1 same_len by(fastforce elim: eval_closed_lcl_unchanged) from eval_blocks obtain l3' where body: "P ⊨⟨body,(h,l2',sh)⟩==>⟨e',(h3,l3',sh3)⟩" proof - from eval_blocks have "P ⊨⟨blocks (pns,Ts,vs,body),(h,l,sh)⟩ ==>⟨e',(h3,l3,sh3)⟩" using s' same_len same_len1 by simp then obtain l'' where "P ⊨⟨body,(h,l(pns[↦]vs),sh)⟩==>⟨e',(h3, l'',sh3)⟩" by (blast dest:blocksEval[OF same_len1[THEN sym] same_len[THEN sym]]) from eval_restrict_lcl[OF wf this fv] same_len1 same_len have "P ⊨⟨body,(h,[pns[↦]vs],sh)⟩==>⟨e',(h3, l''|`(set(pns)),sh3)⟩" using wf method by(simp add:subset_insert_iff insert_Diff_if) thus ?thesis by(fastforce intro!:that simp add: l2') qed show ?case using iDP proof(cases i) case Done then have shC': "sh D = ⌊(sfs, Done)⌋∨ M = clinit ∧ sh D = ⌊(sfs, Processing)⌋" using shC by simp have "P ⊨⟨C∙sM(map Val vs),(h,l,sh)⟩==>⟨e',(h3,l,sh3)⟩" by (rule SCall[OF mVs method shC' same_len l2' body]) with s s' id show ?thesis by simp next case Processing then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)" using shC by simp+ then have init: "P ⊨⟨INIT D ([D],False) ← unit,(h,l,sh)⟩==>⟨unit,(h,l,sh)⟩" by(simp add: InitFinal InitProcessing Val) have "P ⊨⟨C∙sM(map Val vs),(h,l,sh)⟩==>⟨e',(h3,l,sh3)⟩" proof(cases "M = clinit") case False show ?thesis by(rule SCallInit[OF mVs method shC' False init same_len l2' body]) next case True then have shC': "sh D = ⌊(sfs, Done)⌋∨ M = clinit ∧ sh D = ⌊(sfs, Processing)⌋" using shC Processing by simp have "P ⊨⟨C∙sM(map Val vs),(h,l,sh)⟩==>⟨e',(h3,l,sh3)⟩" by (rule SCall[OF mVs method shC' same_len l2' body]) with s s' id show ?thesis by simp qed with s s' id show ?thesis by simp qed(auto) next case (SCallInitRed C M Ts T pns body D sh vs h l) then have seq: "P ⊨⟨(INIT D ([D],False) ← unit);; C∙sM(map Val vs),(h, l, sh)⟩==>⟨e',s'⟩" using eval_init_seq by simp then show ?case proof(rule eval_cases(14)) ―‹ Seq › fix v' s1 assume init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨Val v',s1⟩" and call: "P ⊨⟨C∙sM(map Val vs),s1⟩==>⟨e',s'⟩" obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1) then obtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋" and iDP: "i = Done∨ i = Processing" using init_Val_PD[OF init] by auto show ?thesis proof(rule eval_cases(12)[OF call]) ―‹ SCall › fix vsa ex es' assume "P ⊨⟨map Val vs,s1⟩ [==>] ⟨map Val vsa @ throw ex # es',s'⟩" then show ?thesis using evals_finals_same by (meson finals_def map_Val_nthrow_neq) next assume "∀b Ts T a ba x. ¬ P ⊨ C sees M, b : Ts→T = (a, ba) in x" then show ?thesis using SCallInitRed.hyps(1) by auto next fix Ts T m D assume "P ⊨ C sees M, NonStatic : Ts→T = m in D" then show ?thesis using sees_method_fun[OF SCallInitRed.hyps(1)] by blast next fix vsa h1 l1 sh1 Ts T pns body D' a assume "e' = throw a" and vals: "P ⊨⟨map Val vs,s1⟩ [==>] ⟨map Val vsa,(h1, l1, sh1)⟩" and method: "P ⊨ C sees M, Static : Ts→T = (pns, body) in D'" and nDone: "∀sfs. sh1 D' ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT D' ([D'],False) ← unit,(h1, l1, sh1)⟩==>⟨throw a,s'⟩" have vs: "vs = vsa" and s1a: "s1 = (h1, l1, sh1)" using evals_finals_same[OF _ vals] map_Val_eq by auto have D: "D = D'" using sees_method_fun[OF SCallInitRed.hyps(1) method] by simp then have i: "i = Processing" using iDP shD s1 s1a nDone by simp then show ?thesis using D init' init_ProcessingE s1 s1a shD by blast next fix vsa h1 l1 sh1 Ts T pns' body' D' v' h2 l2 sh2 h3 l3 sh3 assume s': "s' = (h3, l2, sh3)" and vals: "P ⊨⟨map Val vs,s1⟩ [==>] ⟨map Val vsa,(h1, l1, sh1)⟩" and method: "P ⊨ C sees M, Static : Ts→T = (pns', body') in D'" and nDone: "∀sfs. sh1 D' ≠⌊(sfs, Done)⌋" and init': "P ⊨⟨INIT D' ([D'],False) ← unit,(h1, l1, sh1)⟩==>⟨Val v',(h2, l2, sh2)⟩" and len: "length vsa = length pns'" and bstep: "P ⊨⟨body',(h2, [pns' [↦] vsa], sh2)⟩==>⟨e',(h3, l3, sh3)⟩" have vs: "vs = vsa" and s1a: "s1 = (h1, l1, sh1)" using evals_finals_same[OF _ vals] map_Val_eq by auto have D: "D = D'" and pns: "pns = pns'" and body: "body = body'" using sees_method_fun[OF SCallInitRed.hyps(1) method] by auto then have i: "i = Processing" using iDP shD s1 s1a nDone by simp then have s2: "(h2, l2, sh2) = s1" using D init' init_ProcessingE s1 s1a shD by blast then show ?thesis using eval_finalId SCallInit[OF eval_finalsId[of "map Val vs" P "(h,l,sh)"] SCallInitRed.hyps(1)] init init' len bstep nDone D pns body s' s1 s1a shD vals vs SCallInitRed.hyps(2-3) s2 by auto next fix vsa h2 l2 sh2 Ts T pns' body' D' sfs h3 l3 sh3 assume s': "s' = (h3, l2, sh3)" and vals: "P ⊨⟨map Val vs,s1⟩ [==>] ⟨map Val vsa,(h2, l2, sh2)⟩" and method: "P ⊨ C sees M, Static : Ts→T = (pns', body') in D'" and "sh2 D' = ⌊(sfs, Done)⌋∨ M = clinit ∧ sh2 D' = ⌊(sfs, Processing)⌋" and len: "length vsa = length pns'" and bstep: "P ⊨⟨body',(h2, [pns' [↦] vsa], sh2)⟩==>⟨e',(h3, l3, sh3)⟩" have vs: "vs = vsa" and s1a: "s1 = (h2, l2, sh2)" using evals_finals_same[OF _ vals] map_Val_eq by auto have D: "D = D'" and pns: "pns = pns'" and body: "body = body'" using sees_method_fun[OF SCallInitRed.hyps(1) method] by auto then show ?thesis using SCallInit[OF eval_finalsId[of "map Val vs" P "(h,l,sh)"] SCallInitRed.hyps(1)] bstep SCallInitRed.hyps(2-3) len s' s1a vals vs init by auto qed next fix e assume e': "e' = throw e" and init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh)⟩==>⟨throw e,s'⟩" obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s') then obtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋" and iDP: "i = Error" using init_throw_PD[OF init] by auto then show ?thesis using SCallInitRed.hyps(2-3) init e' SCallInitThrow[OF eval_finalsId[of "map Val vs" _] SCallInitRed.hyps(1)] by auto qed next case (RedSCallNone C M vs s b) then have tes: "THROW NoSuchMethodError = e' ∧ s = s'" using eval_final_same by simp have "P ⊨⟨map Val vs,s⟩ [==>] ⟨map Val vs,s⟩" using eval_finalsId by simp then show ?case using RedSCallNone eval_evals.SCallNone tes by auto next case (RedSCallNonStatic C M Ts T m D vs s b) then have tes: "THROW IncompatibleClassChangeError = e' ∧ s = s'" using eval_final_same by simp have "P ⊨⟨map Val vs,s⟩ [==>] ⟨map Val vs,s⟩" using eval_finalsId by simp then show ?case using RedSCallNonStatic eval_evals.SCallNonStatic tes by auto next case InitBlockRed thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId simp: assigned_def map_upd_triv fun_upd_same) next case (RedInitBlock V T v u s b) then have "P ⊨⟨Val u,s⟩==>⟨e',s'⟩" by simp then obtain s': "s'=s" and e': "e'=Val u" by cases simp obtain h l sh where s: "s=(h,l,sh)" by (cases s) have "P ⊨⟨{V:T :=Val v; Val u},(h,l,sh)⟩==>⟨Val u,(h, (l(V↦v))(V:=l V), sh)⟩" by (fastforce intro!: eval_evals.intros) then have "P ⊨⟨{V:T := Val v; Val u},s⟩==>⟨e',s'⟩" using s s' e' by simp then show ?case by simp next case BlockRedNone thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros simp add: fun_upd_same fun_upd_idem) next case BlockRedSome thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros simp add: fun_upd_same fun_upd_idem) next case (RedBlock V T v s b) then have "P ⊨⟨Val v,s⟩==>⟨e',s'⟩" by simp then obtain s': "s'=s" and e': "e'=Val v" by cases simp obtain h l sh where s: "s=(h,l,sh)" by (cases s) have "P ⊨⟨Val v,(h,l(V:=None),sh)⟩==>⟨Val v,(h,l(V:=None),sh)⟩" by (rule eval_evals.intros) hence "P ⊨⟨{V:T;Val v},(h,l,sh)⟩==>⟨Val v,(h,(l(V:=None))(V:=l V),sh)⟩" by (rule eval_evals.Block) then have "P ⊨⟨{V:T; Val v},s⟩==>⟨e',s'⟩" using s s' e' by simp then show ?case by simp next case (SeqRed e s b e1 s1 b1 e2) show ?case proof(cases "val_of e") case None show ?thesis proof(cases "lass_val_of e") case lNone:None then have bconf: "P,shp s ⊨b (e,b) √" using SeqRed.prems(1) None by simp then show ?thesis using SeqRed using seq_ext by fastforce next case (Some p) obtain V' v' where p: "p = (V',v')" and e: "e = V':=Val v'" using lass_val_of_spec[OF Some] by(cases p, auto) obtain h l sh h' l' sh' where s: "s = (h,l,sh)" and s1: "s1 = (h',l',sh')" by(cases s, cases s1) then have red: "P ⊨⟨e,(h,l,sh),b⟩→⟨e1,(h',l',sh'),b1⟩" using SeqRed.hyps(1) by simp then have s1': "e1 = unit ∧ h' = h ∧ l' = l(V' ↦ v') ∧ sh' = sh" using lass_val_of_red[OF Some red] p e by simp then have eval: "P ⊨⟨e,s⟩==>⟨e1,s1⟩" using e s s1 LAss Val by auto then show ?thesis by (metis SeqRed.prems(2) eval_final eval_final_same seq_ext) qed next case (Some a) then show ?thesis using SeqRed.hyps(1) val_no_step by blast qed next case RedSeq thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case CondRed thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros simp: val_no_step) next case RedCondT thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case RedCondF thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case RedWhile thus ?case by (auto simp add: unfold_while intro:eval_evals.intros elim:eval_cases) next case ThrowRed then show ?case by(fastforce elim: eval_cases simp: eval_evals.intros) next case RedThrowNull thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case TryRed thus ?case by(fastforce elim: eval_cases intro: eval_evals.intros) next case RedTryCatch thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (RedTryFail s a D fs C V e2 b) thus ?case by (cases s)(auto elim!: eval_cases intro: eval_evals.intros) next case ListRed1 thus ?case by (fastforce elim: evals_cases intro: eval_evals.intros simp: val_no_step) next case ListRed2 thus ?case by (fastforce elim!: evals_cases eval_cases intro: eval_evals.intros eval_finalId) next case (RedInit e1 C b s1 b') then show ?case using InitFinal by simp next case (InitNoneRed sh C C' Cs e h l b) show ?case using InitNone InitNoneRed.hyps InitNoneRed.prems(2) by auto next case (RedInitDone sh C sfs C' Cs e h l b) show ?case using InitDone RedInitDone.hyps RedInitDone.prems(2) by auto next case (RedInitProcessing sh C sfs C' Cs e h l b) show ?case using InitProcessing RedInitProcessing.hyps RedInitProcessing.prems(2) by auto next case (RedInitError sh C sfs C' Cs e h l b) show ?case using InitError RedInitError.hyps RedInitError.prems(2) by auto next case (InitObjectRed sh C sfs sh' C' Cs e h l b) show ?case using InitObject InitObjectRed by auto next case (InitNonObjectSuperRed sh C sfs D r sh' C' Cs e h l b) show ?case using InitNonObject InitNonObjectSuperRed by auto next case (RedInitRInit C' C Cs e h l sh b) show ?case using InitRInit RedInitRInit by auto next case (RInitRed e s b e'' s'' b'' C Cs e0) then have IH: "∧e' s'. P ⊨⟨e'',s''⟩==>⟨e',s'⟩==> P ⊨⟨e,s⟩==>⟨e',s'⟩" by simp show ?case using RInitRed rinit_ext[OF IH] by simp next case (RedRInit sh C sfs i sh' C' Cs v e h l b s' e') then have init: "P ⊨⟨(INIT C' (Cs,True) ← e), (h, l, sh(C ↦ (sfs, Done)))⟩==>⟨e',s'⟩" using RedRInit by simp then show ?case using RInit RedRInit.hyps(1) RedRInit.hyps(3) Val by fastforce next case BinOpThrow2 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case FAssThrow2 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case SFAssThrow then show ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (CallThrowParams es vs e es' v M s b) have val: "P ⊨⟨Val v,s⟩==>⟨Val v,s⟩" by (rule eval_evals.intros) have eval_e: "P ⊨⟨throw (e),s⟩==>⟨e',s'⟩" using CallThrowParams by simp then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final) with list_eval_Throw [OF eval_e] have vals: "P ⊨⟨es,s⟩ [==>] ⟨map Val vs @ Throw xa # es',s'⟩" using CallThrowParams.hyps(1) eval_e list_eval_Throw by blast then have "P ⊨⟨Val v∙M(es),s⟩==>⟨Throw xa,s'⟩" using eval_evals.CallParamsThrow[OF val vals] by simp thus ?case using e' by simp next case (SCallThrowParams es vs e es' C M s b) have eval_e: "P ⊨⟨throw (e),s⟩==>⟨e',s'⟩" using SCallThrowParams by simp then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final) then have "P ⊨⟨es,s⟩ [==>] ⟨map Val vs @ Throw xa # es',s'⟩" using SCallThrowParams.hyps(1) eval_e list_eval_Throw by blast then have "P ⊨⟨C∙sM(es),s⟩==>⟨Throw xa,s'⟩" by (rule eval_evals.SCallParamsThrow) thus ?case using e' by simp next case (BlockThrow V T a s b) then have "P ⊨⟨Throw a, s⟩==>⟨e',s'⟩" by simp then obtain s': "s' = s" and e': "e' = Throw a" by cases (auto elim!:eval_cases) obtain h l sh where s: "s=(h,l,sh)" by (cases s) have "P ⊨⟨Throw a, (h,l(V:=None),sh)⟩==>⟨Throw a, (h,l(V:=None),sh)⟩" by (simp add:eval_evals.intros eval_finalId) hence "P⊨⟨{V:T;Throw a},(h,l,sh)⟩==>⟨Throw a, (h,(l(V:=None))(V:=l V),sh)⟩" by (rule eval_evals.Block) then have "P ⊨⟨{V:T; Throw a},s⟩==>⟨e',s'⟩" using s s' e' by simp then show ?case by simp next case (InitBlockThrow V T v a s b) then have "P ⊨⟨Throw a,s⟩==>⟨e',s'⟩" by simp then obtain s': "s' = s" and e': "e' = Throw a" by cases (auto elim!:eval_cases) obtain h l sh where s: "s = (h,l,sh)" by (cases s) have "P ⊨⟨{V:T :=Val v; Throw a},(h,l,sh)⟩==>⟨Throw a, (h, (l(V↦v))(V:=l V),sh)⟩" by(fastforce intro:eval_evals.intros) then have "P ⊨⟨{V:T := Val v; Throw a},s⟩==>⟨e',s'⟩" using s s' e' by simp then show ?case by simp next case (RInitInitThrow sh C sfs i sh' a D Cs e h l b) have IH: "∧e' s'. P ⊨⟨RI (D,Throw a) ; Cs ← e,(h, l, sh(C ↦ (sfs, Error)))⟩==>⟨e',s'⟩==>
P ⊨⟨RI (C,Throw a) ; D # Cs ← e,(h, l, sh)⟩==>⟨e',s'⟩" using RInitInitFail[OF eval_finalId] RInitInitThrow by simp then show ?case using RInitInitThrow.hyps(2) RInitInitThrow.prems(2) by auto next case (RInitThrow sh C sfs i sh' a e h l b) then have e': "e' = Throw a" and s': "s' = (h,l,sh')" using eval_final_same final_def by fastforce+ show ?case using RInitFailFinal RInitThrow.hyps(1) RInitThrow.hyps(2) e' eval_finalId s' by auto qed(auto elim: eval_cases simp: eval_evals.intros) (*>*)
(*<*) (* ... und wieder anschalten: *) declare split_paired_All [simp] split_paired_Ex [simp] (*>*)
text ‹ Its extension to @{text"→*"}: ›
lemma extend_eval: assumes wf: "wwf_J_prog P" shows "[ P ⊨⟨e,s,b⟩→* ⟨e'',s'',b''⟩; P ⊨⟨e'',s''⟩==>⟨e',s'⟩;
iconf (shp s) e; P,shp s ⊨b (e::expr,b) √] ==> P ⊨⟨e,s⟩==>⟨e',s'⟩" (*<*) proof (induct rule: converse_rtrancl_induct3) case refl then show ?case by simp next case (step e1 s1 b1 e2 s2 b2) then have ic: "iconf (shp s2) e2" using Red_preserves_iconf local.wf by blast then have ec: "P,shp s2 ⊨b (e2,b2) √" using Red_preserves_bconf local.wf step.hyps(1) step.prems(2) step.prems(3) by blast show ?case using step ic ec extend_1_eval[OF wf step.hyps(1)] by simp qed (*>*)
lemma extend_evals: assumes wf: "wwf_J_prog P" shows "[ P ⊨⟨es,s,b⟩ [→]* ⟨es'',s'',b''⟩; P ⊨⟨es'',s''⟩ [==>] ⟨es',s'⟩;
iconfs (shp s) es; P,shp s ⊨b (es::expr list,b) √] ==> P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩" (*<*) proof (induct rule: converse_rtrancl_induct3) case refl then show ?case by simp next case (step es1 s1 b1 es2 s2 b2) then have ic: "iconfs (shp s2) es2" using Reds_preserves_iconf local.wf by blast then have ec: "P,shp s2 ⊨b (es2,b2) √" using Reds_preserves_bconf local.wf step.hyps(1) step.prems(2) step.prems(3) by blast show ?case using step ic ec extend_1_evals[OF wf step.hyps(1)] by simp qed (*>*)
text ‹ Finally, small step semantics can be simulated by big step semantics: \<close>
theorem assumes wf: " P"
small_by_big:
"[P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩; iconf (shp s) e; P,shp s ⊨b (e,b) √; final e'] ==> P ⊨⟨e,s⟩==>⟨e',s'⟩"
"[P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩; iconfs (shp s) es; P,shp s ⊨b (es,b) √; finals es'] ==> P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩"
(*<*) proof - note wf moreoverassume"P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩" moreoverassume"final e'" thenhave"P ⊨⟨e',s'⟩==>⟨e',s'⟩" by (simp add: eval_finalId) moreoverassume"iconf (shp s) e" moreoverassume"P,shp s ⊨b (e,b) √" ultimatelyshow"P ⊨⟨e,s⟩==>⟨e',s'⟩" by (rule extend_eval) next assume fins: "finals es'" note wf moreoverassume"P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩" moreoverhave"P ⊨⟨es',s'⟩ [==>] ⟨es',s'⟩"using fins by (rule eval_finalsId) moreoverassume"iconfs (shp s) es" moreoverassume"P,shp s ⊨b (es,b) √" ultimatelyshow"P ⊨⟨es,s⟩ [==>] ⟨es',s'⟩" by (rule extend_evals) qed (*>*)
subsection"Equivalence"
text‹ And now, the crowning achievement: ›
corollary big_iff_small: "[ wwf_J_prog P; iconf (shp s) e; P,shp s ⊨b (e::expr,b) √] ==> P ⊨⟨e,s⟩==>⟨e',s'⟩ = (P ⊨⟨e,s,b⟩→* ⟨e',s',False⟩∧ final e')" (*<*)by(blast dest: big_by_small eval_final small_by_big)(*>*)
corollary big_iff_small_WT: "wwf_J_prog P ==> P,E ⊨ e::T ==> P,shp s ⊨b (e,b) √==> P ⊨⟨e,s⟩==>⟨e',s'⟩ = (P ⊨⟨e,s,b⟩→* ⟨e',s',False⟩∧ final e')" (*<*)by(blast dest: big_iff_small WT_nsub_RI nsub_RI_iconf)(*>*)
subsection‹ Lifting type safety to @{text"==>"} ›
text‹\dots and now to the big step semantics, just for fun. ›
lemma eval_preserves_sconf: fixes s::state and s'::state assumes"wf_J_prog P"and"P ⊨⟨e,s⟩==>⟨e',s'⟩"and"iconf (shp s) e" and"P,E ⊨ e::T"and"P,E ⊨ s√" shows"P,E ⊨ s'√" (*<*) proof - have"P,shp s ⊨b (e,False) √"by(simp add: bconf_def) with assms show ?thesis by(blast intro:Red_preserves_sconf Red_preserves_iconf Red_preserves_bconf big_by_small
WT_implies_WTrt wf_prog_wwf_prog) qed (*>*)
lemma eval_preserves_type: fixes s::state assumes wf: "wf_J_prog P" and"P ⊨⟨e,s⟩==>⟨e',s'⟩"and"P,E ⊨ s√"and"iconf (shp s) e"and"P,E ⊨ e::T" shows"∃T'. P ⊨ T' ≤ T ∧ P,E,hp s',shp s' ⊨ e':T'" (*<*) proof - have"P,shp s ⊨b (e,False) √"by(simp add: bconf_def) with assms show ?thesis by(blast dest:big_by_small[OF wf_prog_wwf_prog[OF wf]]
WT_implies_WTrt Red_preserves_type[OF wf]) qed (*>*)
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.273 Sekunden
(vorverarbeitet am 2026-06-13)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.