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 then show ?thesis using RedNew[OF New.hyps(2-4)] by auto next case False then show ?thesis using New.hyps(1) NewInitDoneReds[OF _ New.hyps(2-4)] by auto qed next case NewFail show ?case proof(cases b) case True then show ?thesis using RedNewFail[OF NewFail.hyps(2)] NewFail.hyps(3) by fastforce next case False then show ?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 then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInit.hyps(1) NewInit.prems by(clarsimp simp: bconf_def initPD_def) then have s': "(h',l',sh') = (h,l,sh)" using NewInit.hyps(2) init_ProcessingE by clarsimp then show ?thesis using RedNew[OF NewInit.hyps(4-6)] True by auto next case False then have 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) then show ?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 then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInitOOM.hyps(1) NewInitOOM.prems by(clarsimp simp: bconf_def initPD_def) then have s': "(h',l',sh') = (h,l,sh)" using NewInitOOM.hyps(2) init_ProcessingE by clarsimp then show ?thesis using RedNewFail[OF NewInitOOM.hyps(4)] True r_into_rtrancl NewInitOOM.hyps(5) by auto next case False then have 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) then show ?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 then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋" using NewInitThrow.hyps(1) NewInitThrow.prems by(clarsimp simp: bconf_def initPD_def) then show ?thesis using NewInitThrow.hyps(2) init_ProcessingE by blast next case False then have init: "P ⊨⟨INIT C ([C],False) ← unit,(h, l, sh),b⟩→* ⟨throw a,s',False⟩" using NewInitThrow.hyps(3) by(auto simp: bconf_def) then show ?thesis using NewInitThrow NewInitThrowReds[of "(h,l,sh)" C P a s'] False by auto qed next case Cast then show ?case by(fastforce intro:CastRedsAddr) next case CastNull then show ?case by(fastforce intro: CastRedsNull) next case CastFail thus ?case by(fastforce intro!:CastRedsFail) next case CastThrow thus ?case by(fastforce dest!:eval_final intro:CastRedsThrow) next case Val then show ?case using 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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v2,s2,False⟩" using BinOp.hyps(4)[OF iconf2'] by auto then show ?thesis using BinOpRedsVal[OF b1 b2 BinOp.hyps(5)] by fast next case (Some a) then obtain 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]) then have 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 then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf binop BinOp.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v2,s2,False⟩" using BinOp.hyps(4)[OF iconf2'] by auto then show ?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 then have "iconf (shp s0) e1" and "P,shp s0⊨b (e1,b) √" using BinOpThrow1.prems by auto then have b1: "P ⊨⟨e1,s0,b⟩→* ⟨throw e,s1,False⟩" using BinOpThrow1.hyps(2) by auto then have "P ⊨⟨e1«bop¬ e2,s0,b⟩→* ⟨throw e,s1,False⟩" using BinOpThrow1 None by(auto dest!:eval_final simp: BinOpRedsThrow1[OF b1]) then show ?thesis by fast next case (Some a) then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨throw e,s2,False⟩" using BinOpThrow2.hyps(4)[OF iconf2'] by auto then show ?thesis using BinOpRedsThrow2[OF b1 b2] by fast next case (Some a) then obtain 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]) then have 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 then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf binop BinOpThrow2.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨throw e,s2,False⟩" using BinOpThrow2.hyps(4)[OF iconf2'] by auto then show ?thesis using BinOpRedsThrow2[OF b1 b2] by fast qed next case Var thus ?case by(auto dest:RedVar simp: bconf_def) next case LAss thus ?case by(auto dest: LAssRedsVal) next case LAssThrow thus ?case by(auto dest!:eval_final dest: LAssRedsThrow) next case FAcc thus ?case by(fastforce intro:FAccRedsVal) next case FAccNull thus ?case by(auto dest:FAccRedsNull) next case FAccThrow thus ?case by(auto dest!:eval_final dest:FAccRedsThrow) next case FAccNone then show ?case by(fastforce intro: FAccRedsNone) next case FAccStatic then show ?case by(fastforce intro: FAccRedsStatic) next case SFAcc show ?case proof(cases b) case True then show ?thesis using RedSFAcc SFAcc.hyps by auto next case False then show ?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 then obtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋" using SFAccInit.hyps(2) SFAccInit.prems by(clarsimp simp: bconf_def initPD_def) then have s': "(h',l',sh') = (h,l,sh)" using SFAccInit.hyps(3) init_ProcessingE by clarsimp then show ?thesis using RedSFAcc SFAccInit.hyps True by auto next case False then have 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) then show ?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 then obtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋" using SFAccInitThrow.hyps(2) SFAccInitThrow.prems(2) by(clarsimp simp: bconf_def initPD_def) then show ?thesis using SFAccInitThrow.hyps(3) init_ProcessingE by blast next case False then have init: "P ⊨⟨INIT D ([D],False) ← unit,(h, l, sh),b⟩→* ⟨throw a,s',False⟩" using SFAccInitThrow.hyps(4) by(auto simp: bconf_def) then show ?thesis using SFAccInitThrow SFAccInitThrowReds False by auto qed next case SFAccNone then show ?case by(fastforce intro: SFAccRedsNone) next case SFAccNonStatic then show ?case by(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 then have 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 then have 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]) then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAss by auto have "P,shp s1⊨b (e2,False) √" by(simp add: bconf_def) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAss.hyps(4)[OF iconf2'] by auto then show ?thesis using FAssRedsVal[OF b1 b2 FAss.hyps(6) FAss.hyps(5)[THEN sym]] FAss.hyps(7,8) by fast next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAss.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAss.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,s2,False⟩" using FAssNull.hyps(4)[OF iconf2'] by auto then show ?thesis using FAssRedsNull[OF b1 b2] by fast next case (Some a') then obtain 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]) then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssNull by auto have bconf2: "P,shp s0⊨b (e2,b) √" using FAssNull.prems Some by simp then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssNull.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,s2,False⟩" using FAssNull.hyps(4)[OF iconf2'] by auto then show ?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 then have "iconf (shp s0) e1" and "P,shp s0⊨b (e1,b) √" using FAssThrow1.prems by auto then have b1: "P ⊨⟨e1,s0,b⟩→* ⟨throw e',s1,False⟩" using FAssThrow1.hyps(2) by auto then have "P ⊨⟨e1∙F{D} := e2,s0,b⟩→* ⟨throw e',s1,False⟩" using FAssThrow1 None by(auto dest!:eval_final simp: FAssRedsThrow1[OF b1]) then show ?thesis by fast next case (Some a) then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨throw e',s2,False⟩" using FAssThrow2.hyps(4)[OF iconf2'] by auto then show ?thesis using FAssRedsThrow2[OF b1 b2] by fast next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssThrow2.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨throw e',s2,False⟩" using FAssThrow2.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAssNone.hyps(4)[OF iconf2'] by auto then show ?thesis using FAssRedsNone[OF b1 b2 FAssNone.hyps(5,6)] by fast next case (Some a') then obtain 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]) then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssNone by auto have bconf2: "P,shp s0⊨b (e2,b) √" using FAssNone.prems Some by simp then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssNone.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAssNone.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAssStatic.hyps(4)[OF iconf2'] by auto then show ?thesis using FAssRedsStatic[OF b1 b2 FAssStatic.hyps(5,6)] by fast next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssStatic.prems] by simp then have b2: "P ⊨⟨e2,s1,b1⟩→* ⟨Val v,(h2, l2, sh2),False⟩" using FAssStatic.hyps(4)[OF iconf2'] by auto then show ?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 then have bconf: "P,shp s0⊨b (e2,b) √" using SFAss.prems(2) by simp then have 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) then obtain 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'') then have iconf: "iconf (shp s0) e2" by simp show ?case proof(cases "val_of e2") case None then have bconf: "P,shp s0⊨b (e2,b) √" using SFAssInit.prems(2) by simp then have reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInit.hyps(2)[OF iconf bconf] by auto then have 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) then show ?thesis using SFAssInit SFAssInitReds[OF reds SFAssInit.hyps(3) _ init] by auto next case (Some v2) show ?thesis proof(cases b) case False then have bconf: "P,shp s0⊨b (e2,b) √" by(simp add: bconf_def) then have reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInit.hyps(2)[OF iconf bconf] by auto then have 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) then show ?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 then have vs: "v2 = v ∧ s0 = (h1, l1, sh1)" using eval_final_same[OF SFAssInit.hyps(1)] by simp then obtain 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) then have s': "(h',l',sh') = (h1, l1, sh1)" using SFAssInit.hyps(5) init_ProcessingE by clarsimp then show ?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') then have iconf: "iconf (shp s0) e2" by simp show ?case proof(cases "val_of e2") case None then have bconf: "P,shp s0⊨b (e2,b) √" using SFAssInitThrow.prems(2) by simp then have reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto then have init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SFAssInitThrow.hyps(6) by(auto simp: bconf_def) then show ?thesis using SFAssInitThrow SFAssInitThrowReds[OF reds _ _ init] by auto next case (Some v2) show ?thesis proof(cases b) case False then have bconf: "P,shp s0⊨b (e2,b) √" by(simp add: bconf_def) then have reds: "P ⊨⟨e2,s0,b⟩→* ⟨Val v,(h1, l1, sh1),False⟩" using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto then have init: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SFAssInitThrow.hyps(6) by(auto simp: bconf_def) then show ?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 then have vs: "v2 = v ∧ s0 = (h1, l1, sh1)" using eval_final_same[OF SFAssInitThrow.hyps(1)] by simp then obtain 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) then show ?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 then have bconf: "P,shp s0⊨b (e2,b) √" using SFAssThrow.prems(2) None by simp then have 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) then show ?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 then have iconf: "iconf (shp s0) e2" using SFAssNone by simp then have bconf: "P,shp s0⊨b (e2,b) √" using SFAssNone.prems(2) None by simp then have 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) then obtain 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 then have iconf: "iconf (shp s0) e2" using SFAssNonStatic by simp then have bconf: "P,shp s0⊨b (e2,b) √" using SFAssNonStatic.prems(2) None by simp then have 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) then obtain 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 then have "iconf (shp s0) e" and "P,shp s0⊨b (e,b) √" using CallObjThrow.prems by auto then have b1: "P ⊨⟨e,s0,b⟩→* ⟨throw e',s1,False⟩" using CallObjThrow.hyps(2) by auto then have "P ⊨⟨e∙M(ps),s0,b⟩→* ⟨throw e',s1,False⟩" using CallObjThrow None by(auto dest!:eval_final simp: CallRedsThrowObj[OF b1]) then show ?thesis by fast next case (Some a) then show ?thesis using eval_final_same[OF CallObjThrow.hyps(1)] val_of_spec[OF Some] by auto qed next case (CallNull e s0 s1 ps vs s2 M) show ?case proof(cases "val_of e") case None then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,s2,False⟩" using CallNull.hyps(4)[OF iconf2'] by auto then show ?thesis using CallRedsNull[OF b1 b2] by fast next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (ps,b1) √" using Red_preserves_bconf[OF wwf fass CallNull.prems] by simp then have b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,s2,False⟩" using CallNull.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨es,s1,False⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩" using CallParamsThrow.hyps(4)[OF iconf2'] by auto then show ?thesis using CallRedsThrowParams[OF b1 b2] by fast next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (es,b1) √" using Red_preserves_bconf[OF wwf fass CallParamsThrow.prems] by simp then have b2: "P ⊨⟨es,s1,b1⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩" using CallParamsThrow.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallNone.hyps(4)[OF iconf2'] by auto then show ?thesis using CallRedsNone[OF b1 b2 _ CallNone.hyps(6)] CallNone.hyps(5) by fastforce next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (ps,b1) √" using Red_preserves_bconf[OF wwf fass CallNone.prems] by simp then have b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallNone.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallStatic.hyps(4)[OF iconf2'] by auto then show ?thesis using CallRedsStatic[OF b1 b2 _ CallStatic.hyps(6)] CallStatic.hyps(5) by fastforce next case (Some a') then obtain 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]) then have 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 then have "P,shp s1⊨b (ps,b1) √" using Red_preserves_bconf[OF wwf call CallStatic.prems] by simp then have b2: "P ⊨⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩" using CallStatic.hyps(4)[OF iconf2'] by auto then show ?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 then have 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 then have 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]) then have iconf2: "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] None Call by auto have "P,shp s1⊨b (ps,False) √" by(simp add: bconfs_def) then have 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) then have 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') then obtain 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]) then have 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 then have "P,shp s1⊨b (ps,b1) √" using Red_preserves_bconf[OF wwf call Call.prems] by simp then have 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) then have 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 then have 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 then have 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') then have "es = map Val vs'" by(rule map_vals_of_spec) then show ?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 then have 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 then have b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩" using SCallNone.hyps(2)[OF iconf] by auto then show ?thesis using SCallRedsNone[OF b1 SCallNone.hyps(3)] SCallNone.hyps(1) by simp next case (Some vs') then have ps: "ps = map Val vs'" by(rule map_vals_of_spec) then have s0: "s0 = s2" using SCallNone.hyps(1) evals_finals_same by blast then show ?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 then have 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 then have b1: "P ⊨⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩" using SCallNonStatic.hyps(2)[OF iconf] by auto then show ?thesis using SCallRedsNonStatic[OF b1 SCallNonStatic.hyps(3)] SCallNonStatic.hyps(1) by simp next case (Some vs') then have ps: "ps = map Val vs'" by(rule map_vals_of_spec) then have s0: "s0 = s2" using SCallNonStatic.hyps(1) evals_finals_same by blast then show ?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 then have 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 then have 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) then have b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SCallInitThrow.hyps(7) by auto then show ?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]) then have 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) then show ?thesis using init_ProcessingE[OF _ SCallInitThrow.hyps(6)] by blast next case False then have 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) then have b2: "P ⊨⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩→* ⟨throw a,s',False⟩" using SCallInitThrow.hyps(7) by auto then show ?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 then have 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 then have 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) then have 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) then have 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') then have ps: "ps = map Val vs'" by(rule map_vals_of_spec) then have 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 then have 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) then have 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) then have b3: "P ⊨⟨body,(h2, l2', sh2),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using SCallInit.hyps(11)[OF iconf3] by simp then have b3': "P ⊨⟨body,(h1, l2', sh1),False⟩→* ⟨e',(h3, l3, sh3),False⟩" using s' by simp then show ?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 then have 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) then have 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) then have 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 then have 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 then have 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) then have 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') then have ps: "ps = map Val vs'" by(rule map_vals_of_spec) then have vs: "vs = vs' ∧ s0 = (h2, l2, sh2)" using evals_finals_same[OF _ SCall.hyps(1)] map_Val_eq by auto then have 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) then have 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) then have 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 ?case using BlockRedsFinal[OF b' fin] by simp next case (Seq e0 s0 v s1 e1 e2 s2) then have 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 then have bconf: "P,shp s0⊨b (e0,b) √" using Seq.prems(2) None by simp then have "P ⊨⟨e0,s0,b⟩→* ⟨Val v,s1,False⟩" using iconf Seq.hyps(2) by auto then show ?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) then have eval: "P ⊨⟨e0,(h,l,sh)⟩==>⟨Val v,(h',l',sh')⟩" using Seq.hyps(1) by simp then have s1': "Val v = unit ∧ h' = h ∧ l' = l(V' ↦ v') ∧ sh' = sh" using lass_val_of_eval[OF Some eval] p e0 by simp then have "P ⊨⟨e0,s0,b⟩→⟨Val v,s1,b⟩" using e0 s0 s1 by(auto intro: RedLAss) then show ?thesis by auto qed next case (Some a) then have "e0 = Val v" and "s0 = s1" using Seq.hyps(1) eval_cases(3) val_of_spec by blast+ then show ?thesis using Seq by auto qed then obtain 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']) then have 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]) then have 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]) then show ?case using 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 ?case using SeqThrow notVal by(auto dest!:eval_final dest: SeqRedsThrow) next case (CondT e s0 s1 e1 e' s2 e2) then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e1,s1,False⟩→* ⟨e',s2,False⟩" using CondT.hyps(4)[OF iconf2'] by auto then show ?case using CondReds2T[OF b1 b2] by fast next case (CondF e s0 s1 e2 e' s2 e1) then have 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 then have 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]) then have 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) then have b2: "P ⊨⟨e2,s1,False⟩→* ⟨e',s2,False⟩" using CondF.hyps(4)[OF iconf2'] by auto then show ?case using CondReds2F[OF b1 b2] by fast next case CondThrow thus ?case by(auto dest!:eval_final dest:CondRedsThrow) next case (WhileF e s0 s1 c) then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto then have bconf: "P,shp s0⊨b (e,b) √" using WhileF.prems(2) by(simp add: bconf_def) then have b': "P ⊨⟨e,s0,b⟩→* ⟨false,s1,False⟩" using WhileF.hyps(2) iconf by auto thus ?case using WhileFReds[OF b'] by fast next case (WhileT e s0 s1 c v1 s2 e3 s3) then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto then have bconf: "P,shp s0⊨b (e,b) √" using WhileT.prems(2) by(simp add: bconf_def) then have 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) then have 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) then have b3: "P ⊨⟨while (e) c,s2,False⟩→* ⟨e3,s3,False⟩" using WhileT.hyps(6) iconf3 by auto show ?case using 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) then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto then have bconf: "P,shp s0⊨b (e,b) √" using WhileBodyThrow.prems(2) by(simp add: bconf_def) then have 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) then have b2: "P ⊨⟨c,s1,False⟩→* ⟨throw e',s2,False⟩" using WhileBodyThrow.hyps(4) iconf2 by auto show ?case using WhileTRedsThrow[OF b1 b2] by fast next case Throw thus ?case by (meson ThrowReds iconf.simps(17) bconf_Throw) next case ThrowNull thus ?case by (meson ThrowRedsNull iconf.simps(17) bconf_Throw) next case ThrowThrow thus ?case by (meson ThrowRedsThrow iconf.simps(17) bconf_Throw) next case Try thus ?case by (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) then have 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) then have b2: "P ⊨⟨e2,(h1, l1(V ↦ Addr a), sh1),False⟩→* ⟨e2',(h2, l2, sh2),False⟩" using TryCatch.hyps(6) iconf by auto thus ?case using TryCatchRedsFinal[OF b1] TryCatch.hyps(3-5) by (meson eval_final) next case TryThrow thus ?case by (meson TryRedsFail iconf.simps(18) bconf_Try) next case Nil thus ?case by(auto simp: bconfs_def) next case (Cons e s0 v s1 es es' s2) show ?case proof(cases "val_of e") case None then have 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 then have 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]) then have 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) then have 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) then obtain 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]) then have 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 then have "P,shp s1⊨b (es,b1) √" using Reds_preserves_bconf[OF wwf cons Cons.prems] by simp then have 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 then have 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 then have 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]) then show ?thesis by fast next case (Some a) then show ?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') then have "¬sub_RI e" by simp then show ?case using 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') then have 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 ?case by(rule InitNoneReds[OF InitNone.hyps(1) init]) next case (InitDone sh C sfs C' Cs e h l e' s') then have "iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)" using InitDone.hyps(1) proof(cases Cs) case Nil then have "C = C'" "¬sub_RI e" using InitDone.prems(1) by simp+ then show ?thesis using Nil InitDone.hyps(1) by(simp add: initPD_def) qed(auto) then have init: "P ⊨⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩→* ⟨e',s',False⟩" using InitDone by(simp add: bconf_def) show ?case by(rule InitDoneReds[OF InitDone.hyps(1) init]) next case (InitProcessing sh C sfs C' Cs e h l e' s') then have "iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)" using InitProcessing.hyps(1) proof(cases Cs) case Nil then have "C = C'" "¬sub_RI e" using InitProcessing.prems(1) by simp+ then show ?thesis using Nil InitProcessing.hyps(1) by(simp add: initPD_def) qed(auto) then have init: "P ⊨⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩→* ⟨e',s',False⟩" using InitProcessing by(simp add: bconf_def) show ?case by(rule InitProcessingReds[OF InitProcessing.hyps(1) init]) next case InitError thus ?case by(fastforce intro: InitErrorReds simp: bconf_def) next case InitObject thus ?case by(fastforce intro: InitObjectReds simp: bconf_def) next case InitNonObject thus ?case by(fastforce intro: InitNonObjectReds simp: bconf_def) next case InitRInit thus ?case by(fastforce intro: RedsInitRInit simp: bconf_def) next case (RInit e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1) then have 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 then have 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 then have 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) then have b2: "P ⊨⟨INIT C' (Cs,True) ← e',(h',l',sh''),False⟩→* ⟨e1,s1,False⟩" using RInit.hyps(7)[OF iconf2] by auto then show ?thesis using RedsRInit[OF b1 RInit.hyps(3-5) b2] by fast next case (Some a') then obtain 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) then have 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) then have b2: "P ⊨⟨INIT C' (Cs,True) ← e',(h', l', sh''),b1⟩→* ⟨e1,s1,False⟩" using RInit.hyps(7)[OF iconf2] by auto then show ?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 then obtain 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 then have 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 then have 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) then have 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) then obtain 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) then have 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) then have 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 then obtain a' where a': "throw a = Throw a'" by auto show ?case proof(cases "val_of e") case None then have 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 then have 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) then show ?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 Wasserrab (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) moreover from eval_false have "P ⊨⟨while (b) c,s⟩==>⟨unit,s1⟩" by - (rule WhileF, simp) ultimately show ?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 then show ?case by fastforce next case (Cons p ps') have length_eqs: "length (p # ps') = length Ts" "length (p # ps') = length vs" by fact+ then obtain 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 then obtain 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) then obtain 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 ?case by fastforce next case Seq thus ?case by simp (blast intro:eval_evals.Seq) next case New thus ?case by(simp add:eval_evals.intros) next case NewFail thus ?case by(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 then have "P ⊨⟨INIT C ([C],False) ← unit,(h, l |` W, sh)⟩==>⟨Val v',(h', l' |` W, sh')⟩" by (simp add: NewInit.hyps(3)) thus ?case using 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 then have "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 ?case by(simp add:eval_evals.intros) next case Cast thus ?case by simp (blast intro:eval_evals.Cast) next case CastNull thus ?case by simp (blast intro:eval_evals.CastNull) next case CastFail thus ?case by simp (blast intro:eval_evals.CastFail) next case CastThrow thus ?case by(simp add:eval_evals.intros) next case Val thus ?case by(simp add:eval_evals.intros) next case BinOp thus ?case by simp (blast intro:eval_evals.BinOp) next case BinOpThrow1 thus ?case by simp (blast intro:eval_evals.BinOpThrow1) next case BinOpThrow2 thus ?case by simp (blast intro:eval_evals.BinOpThrow2) next case Var thus ?case by(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 ?case by simp next case LAssThrow thus ?case by(fastforce intro: eval_evals.LAssThrow) next case FAcc thus ?case by simp (blast intro: eval_evals.FAcc) next case FAccNull thus ?case by(fastforce intro: eval_evals.FAccNull) next case FAccThrow thus ?case by(fastforce intro: eval_evals.FAccThrow) next case FAccNone thus ?case by(metis eval_evals.FAccNone fv.simps(7)) next case FAccStatic thus ?case by(metis eval_evals.FAccStatic fv.simps(7)) next case SFAcc thus ?case by simp (blast intro: eval_evals.SFAcc) next case SFAccInit thus ?case by simp (blast intro: eval_evals.SFAccInit) next case SFAccInitThrow thus ?case by simp (blast intro: eval_evals.SFAccInitThrow) next case SFAccNone thus ?case by simp (blast intro: eval_evals.SFAccNone) next case SFAccNonStatic thus ?case by simp (blast intro: eval_evals.SFAccNonStatic) next case FAss thus ?case by simp (blast intro: eval_evals.FAss) next case FAssNull thus ?case by simp (blast intro: eval_evals.FAssNull) next case FAssThrow1 thus ?case by simp (blast intro: eval_evals.FAssThrow1) next case FAssThrow2 thus ?case by simp (blast intro: eval_evals.FAssThrow2) next case FAssNone thus ?case by simp (blast intro: eval_evals.FAssNone) next case FAssStatic thus ?case by simp (blast intro: eval_evals.FAssStatic) next case SFAss thus ?case by simp (blast intro: eval_evals.SFAss) next case SFAssInit thus ?case by simp (blast intro: eval_evals.SFAssInit) next case SFAssInitThrow thus ?case by simp (blast intro: eval_evals.SFAssInitThrow) next case SFAssThrow thus ?case by simp (blast intro: eval_evals.SFAssThrow) next case SFAssNone thus ?case by simp (blast intro: eval_evals.SFAssNone) next case SFAssNonStatic thus ?case by simp (blast intro: eval_evals.SFAssNonStatic) next case CallObjThrow thus ?case by simp (blast intro: eval_evals.intros) next case CallNull thus ?case by 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)⟩" using local.CallNone(4) local.CallNone(7) by auto then show ?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 then show ?case using SCallNone.hyps(3) eval_evals.SCallNone by auto next case SCallNonStatic thus ?case by (metis eval_evals.SCallNonStatic fv.simps(12)) next case SCallParamsThrow thus ?case by simp (blast intro: eval_evals.SCallParamsThrow) next case SCallInitThrow thus ?case by simp (blast intro: eval_evals.SCallInitThrow) next case SCallInit thus ?case by 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 ?case by simp (blast intro: eval_evals.SeqThrow) next case CondT thus ?case by simp (blast intro: eval_evals.CondT) next case CondF thus ?case by simp (blast intro: eval_evals.CondF) next case CondThrow thus ?case by simp (blast intro: eval_evals.CondThrow) next case WhileF thus ?case by simp (blast intro: eval_evals.WhileF) next case WhileT thus ?case by simp (blast intro: eval_evals.WhileT) next case WhileCondThrow thus ?case by simp (blast intro: eval_evals.WhileCondThrow) next case WhileBodyThrow thus ?case by simp (blast intro: eval_evals.WhileBodyThrow) next case Throw thus ?case by simp (blast intro: eval_evals.Throw) next case ThrowNull thus ?case by simp (blast intro: eval_evals.ThrowNull) next case ThrowThrow thus ?case by simp (blast intro: eval_evals.ThrowThrow) next case Try thus ?case by 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 ?case by fastforce next case TryThrow thus ?case by simp (blast intro: eval_evals.TryThrow) next case Nil thus ?case by (simp add: eval_evals.Nil) next case Cons thus ?case by simp (blast intro: eval_evals.Cons) next case ConsThrow thus ?case by simp (blast intro: eval_evals.ConsThrow) next case InitFinal thus ?case by (simp add: eval_evals.InitFinal) next case InitNone thus ?case by(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 ?case by (simp add: eval_evals.InitProcessing) next case InitError thus ?case using eval_evals.InitError by auto next case InitObject thus ?case by(simp add: eval_evals.InitObject) next case InitNonObject thus ?case by(simp add: eval_evals.InitNonObject) next case InitRInit thus ?case by(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 then have 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)) then show ?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 then have f2: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨throw a,(h', l' |` W, sh')⟩" using RInitInitFail.hyps(2) by blast then have f2': "fv (throw a) ⊆ W" using eval_final[OF f2] by auto then have 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)) then show ?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 then have f2: "P ⊨⟨e,(h, l |` W, sh)⟩==>⟨throw a,(h', l' |` W, sh')⟩" using RInitFailFinal.hyps(2) by blast then have f2': "fv (throw a) ⊆ W" using eval_final[OF f2] by auto then show ?case using 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 ?case by(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 then have "fv e ∪ fv (RI (D,throw a) ; Cs ← unit) ⊆ fv (RI (C,e) ; D#Cs ← unit)" by auto then show ?case using 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 ?case by 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 moreover from eval_e e' have "P ⊨⟨throw x # es,s⟩ [==>] ⟨Throw a # es,s'⟩" by (iprover intro: ConsThrow) ultimately show ?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) moreover from es have "P ⊨⟨es,s⟩ [==>] ⟨map Val vs' @ e' # es',s'⟩" by (rule Cons.hyps) ultimately show "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 (*>*)
\<comment> ‹ 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' s1 assume 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 then show ?thesis using estep Seq by simp next fix et assume e'': "P ⊨⟨e'',s''⟩==>⟨throw et,s'⟩" and e': "e' = throw et" have "P ⊨⟨e,s⟩==>⟨throw et,s'⟩" using e'' IH by simp then show ?thesis using eval_evals.SeqThrow e' by simp qed
\<comment> ‹ 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 then show ?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 then show ?thesis using riD rinit_throwE by blast qed(simp)
\<comment> ‹ 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 then show ?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 then show ?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 = []" then show ?thesis using RInitFailFinal IH by auto qed
\<comment> ‹ 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'⟩" then have "final e'" using eval_final by simp then show "P ⊨⟨RI (C,e) ; Cs ← e0,s⟩==>⟨e',s'⟩" proof(rule finalE) fix v assume "e' = Val v" then show ?thesis using rinit_Val_ext[OF _ IH] ri'' by simp next fix a assume "e' = throw a" then show ?thesis using rinit_throw_ext[OF _ IH] ri'' by simp qed qed
\<comment> ‹ @{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) then show ?case by(fastforce simp: initPD_def dest: eval_final_same) next case (InitDone sh C sfs C' Cs e h l e' s') then have "final e'" using eval_final by simp then show ?case proof(rule finalE) fix v assume e': "e' = Val v" then show ?thesis using InitDone initPD_def proof(cases Cs) qed(auto) next fix a assume e': "e' = throw a" then show ?thesis using InitDone initPD_def proof(cases Cs) qed(auto) qed next case (InitProcessing sh C sfs C' Cs e h l e' s') then have "final e'" using eval_final by simp then show ?case proof(rule finalE) fix v assume e': "e' = Val v" then show ?thesis using InitProcessing initPD_def proof(cases Cs) qed(auto) next fix a assume e': "e' = throw a" then show ?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 then show ?thesis using InitError by simp next case (Cons C2 list) then have "final e'" using InitError eval_final by simp then show ?thesis proof(rule finalE) fix v assume e': "e' = Val v" then show ?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 then show ?thesis using InitError.hyps(2) e' by(auto dest!: rinit_throwE) qed next fix a assume e': "e' = throw a" then show ?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 then show ?thesis using InitRInit by simp next case (Cons C' list) then show ?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) then have final: "final e1" using eval_final by simp then show ?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" then show ?thesis using RInit Cons by clarsimp (metis last.simps last_appendR list.distinct(1)) next fix a assume e': "e1 = throw a" then show ?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) then have final: "final e1" using eval_final by simp then show ?case proof(rule finalE) fix v assume e': "e1 = Val v" then show ?thesis using RInitInitFail by clarsimp (meson exp.distinct(101) rinit_throwE) next fix a' assume e': "e1 = Throw a'" then have "iconf (sh'(C ↦ (sfs, Error))) a" using RInitInitFail.hyps(1) eval_final by fastforce then show ?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])
\<comment> ‹ 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 then show ?case by(auto simp: Seq[OF eval_evals.InitFinal[OF Val[where v=Unit]]]) next case (InitNone sh) then show ?case using seq_ext[OF eval_evals.InitNone[where sh=sh and e=unit, OF InitNone.hyps(1)]] by fastforce next case (InitDone sh) then show ?case using seq_ext[OF eval_evals.InitDone[where sh=sh and e=unit, OF InitDone.hyps(1)]] by fastforce next case (InitProcessing sh) then show ?case using seq_ext[OF eval_evals.InitProcessing[where sh=sh and e=unit, OF InitProcessing.hyps(1)]] by fastforce next case (InitError sh) then show ?case using seq_ext[OF eval_evals.InitError[where sh=sh and e=unit, OF InitError.hyps(1)]] by fastforce next case (InitObject sh) then show ?case using seq_ext[OF eval_evals.InitObject[where sh=sh and e=unit, OF InitObject.hyps(1)]] by fastforce next case (InitNonObject sh) then show ?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') then show ?case using seq_ext[OF eval_evals.InitRInit[where e=unit]] by fastforce next case RInit then show ?case using seq_ext[OF eval_evals.RInit[where e=unit, OF RInit.hyps(1)]] by fastforce next case RInitInitFail then show ?case using seq_ext[OF eval_evals.RInitInitFail[where e=unit, OF RInitInitFail.hyps(1)]] by fastforce next case RInitFailFinal then show ?case using 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) then have 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) then show ?case proof(cases i) case Done then show ?thesis using RedNew shC e' s' New by simp next case Processing then have shC': "∄sfs. sh C = Some(sfs,Done)" and shP: "sh C = Some(sfs,Processing)" using shC by simp+ then have 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]) then show ?thesis using e' s' by simp qed(auto) next case (RedNewFail h C l sh) then have 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) then show ?case proof(cases i) case Done then show ?thesis using RedNewFail shC e' s' NewFail by simp next case Processing then have shC': "∄sfs. sh C = Some(sfs,Done)" and shP: "sh C = Some(sfs,Processing)" using shC by simp+ then have 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]) then show ?thesis using e' s' by simp qed(auto) next case (NewInitRed sh C h l) then have seq: "P ⊨⟨(INIT C ([C],False) ← unit);; new C,(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 C ([C],False) ← unit,(h, l, sh)⟩==>⟨Val v,s1⟩" and new: "P ⊨⟨new C,s1⟩==>⟨e',s'⟩" obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1) then obtain 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" then show ?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" then show ?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" then have i: "i = Processing" using iDP shC s1 by simp then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shC by blast then show ?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" then have i: "i = Processing" using iDP shC s1 by simp then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shC by blast then show ?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'⟩" then have i: "i = Processing" using iDP shC s1 by simp then show ?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') then obtain sfs i where shC: "sh' C = ⌊(sfs, i)⌋" and iDP: "i = Error" using init_throw_PD[OF init] by auto then show ?thesis by (simp add: NewInitRed.hyps NewInitThrow e' init) qed next case CastRed then show ?case by(fastforce elim!: eval_cases intro: eval_evals.intros intro!: CastFail) next case RedCastNull then show ?case by simp (iprover elim: eval_cases intro: eval_evals.intros) next case RedCast then show ?case by (auto elim: eval_cases intro: eval_evals.intros) next case RedCastFail then show ?case by (auto elim!: eval_cases intro: eval_evals.intros) next case BinOpRed1 then show ?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 then show ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case RedFAccNull then show ?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) then have 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) then show ?case proof(cases i) case Done then show ?thesis using RedSFAcc e' s' SFAcc by simp next case Processing then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)" using RedSFAcc 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∙sF{D},(h, l, sh)⟩==>⟨Val v,(h,l,sh)⟩" by(rule SFAccInit[OF RedSFAcc.hyps(1) shC' init shP RedSFAcc.hyps(3)]) then show ?thesis using e' s' by simp qed(auto) next case (SFAccInitRed C F t D sh h l) then have seq: "P ⊨⟨(INIT D ([D],False) ← unit);; C∙sF{D},(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 acc: "P ⊨⟨C∙sF{D},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(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⌋" then show ?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⌋" then have i: "i = Processing" using iDP shD s1 by simp then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shD by blast then show ?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'⟩" then have i: "i = Processing" using iDP shD s1 by simp then show ?thesis using init' init_ProcessingE s1 s1a shD by blast next assume "∀b t. ¬ P ⊨ C has F,b:t in D" then show ?thesis using SFAccInitRed.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 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') 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 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 then show ?case by(auto elim!: eval_cases intro: eval_evals.intros eval_finalId) next case RedFAssStatic then show ?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) then have bconf: "P,sh ⊨b (e,b) √" using SFAssRed by simp show ?case using SFAssRed.prems(2) SFAssRed bconf proof cases case 2 with SFAssRed bconf show ?thesis by(auto intro!: SFAssInit) next case 3 with 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) then show ?case proof(cases i) case Done then show ?thesis using RedSFAss e' s' SFAss Val by auto next case Processing then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)" using RedSFAss 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∙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]) then show ?thesis using e' s' by simp qed(auto) next case (SFAssInitRed C F t D sh v h l) then have seq: "P ⊨⟨(INIT D ([D],False) ← unit);; C∙sF{D} := Val v,(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 acc: "P ⊨⟨C∙sF{D} := Val v,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(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 then show ?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' assume e': "e' = unit" and s': "s' = (h', l', sh'(D ↦ (sfs(F ↦ va), i')))" and val: "P ⊨⟨Val v,s1⟩==>⟨Val va,(h1, l1, sh1)⟩" and field: "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)⟩==>⟨Val v',(h', l', sh')⟩" and shD': "sh' D = ⌊(sfs, i')⌋" 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) = (h', l', sh')" using init' init_ProcessingE s1 s1a shD by blast 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: "wwf_J_prog P" shows 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'⟩" and "[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 moreover assume "P ⊨⟨e,s,b⟩→* ⟨e',s',b'⟩" moreover assume "final e'" then have "P ⊨⟨e',s'⟩==>⟨e',s'⟩" by (simp add: eval_finalId) moreover assume "iconf (shp s) e" moreover assume "P,shp s ⊨b (e,b) √" ultimately show "P ⊨⟨e,s⟩==>⟨e',s'⟩" by (rule extend_eval) next assume fins: "finals es'" note wf moreover assume "P ⊨⟨es,s,b⟩ [→]* ⟨es',s',b'⟩" moreover have "P ⊨⟨es',s'⟩ [==>] ⟨es',s'⟩" using fins by (rule eval_finalsId) moreover assume "iconfs (shp s) es" moreover assume "P,shp s ⊨b (es,b) √" ultimately show "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.239 Sekunden
(vorverarbeitet am 2026-06-10)
¤
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.