| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Jinja/J/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 74 kB |
|
Quelle Equivalence.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Jinja/J/Equivalence.thy Author: Tobias Nipkow Copyright 2003 Technische Universitaet Muenchen *) section ‹Equivalence of Big Step and Small Step Semantics› theory Equivalence imports BigStep SmallStep WWellForm begin subsection‹Small steps simulate big step› subsubsection "Cast" lemma CastReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨Cast C e,s⟩ →* ⟨Cast C e',s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CastRed[OF step(2)]]) qed (*>*) lemma CastRedsNull: "P ⊨ ⟨e,s⟩ →* ⟨null,s'⟩ ==> P ⊨ ⟨Cast C e,s⟩ →* ⟨null,s'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastNull])(*>*) lemma CastRedsAddr: "[ P ⊨ ⟨e,s⟩ →* ⟨addr a,s'⟩; hp s' a = Some(D,fs); P ⊨ D ⪯* C ] ==> P ⊨ ⟨Cast C e,s⟩ →* ⟨addr a,s'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCast])(*>*) lemma CastRedsFail: "[ P ⊨ ⟨e,s⟩ →* ⟨addr a,s'⟩; hp s' a = Some(D,fs); ¬ P ⊨ D ⪯* C ] ==> P ⊨ ⟨Cast C e,s⟩ →* ⟨THROW ClassCast,s'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastFail])(*>*) lemma CastRedsThrow: "[ P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ] ==> P ⊨ ⟨Cast C e,s⟩ →* ⟨throw a,s'⟩" (*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CastThrow])(*>*) subsubsection "LAss" lemma LAssReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨ V:=e,s⟩ →* ⟨ V:=e',s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) LAssRed[OF step(2)]]) qed (*>*) lemma LAssRedsVal: "[ P ⊨ ⟨e,s⟩ →* ⟨Val v,(h',l')⟩ ] ==> P ⊨ ⟨ V:=e,s⟩ →* ⟨unit,(h',l'(V↦v))⟩" (*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ RedLAss])(*>*) lemma LAssRedsThrow: "[ P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ] ==> P ⊨ ⟨ V:=e,s⟩ →* ⟨throw a,s'⟩" (*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.LAssThrow])(*>*) subsubsection "BinOp" lemma BinOp1Reds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨ e «bop¬ e2, s⟩ →* ⟨e' «bop¬ e2, s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) BinOpRed1[OF step(2)]]) qed (*>*) lemma BinOp2Reds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨(Val v) «bop¬ e, s⟩ →* ⟨(Val v) «bop¬ e', s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by 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⟩ →* ⟨Val v1,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨Val v2,s2⟩" and op: "binop(bop,v1,v2) = Some v" shows "P ⊨ ⟨e1 «bop¬ e2, s0⟩ →* ⟨Val v,s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v1 «bop¬ e2, s1)" let ?y' = "(Val v1 «bop¬ Val v2, s2)" have "(?x, ?y) ∈ (red P)*" by(rule BinOp1Reds[OF e1_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule BinOp2Reds[OF e2_steps]) also have "(?y', ?z) ∈ (red P)" by(rule RedBinOp[OF op]) ultimately show ?thesis by simp qed (*>*) lemma BinOpRedsThrow1: "P ⊨ ⟨e,s⟩ →* ⟨throw e',s'⟩ ==> P ⊨ ⟨e «bop¬ e2, s⟩ →* ⟨throw e', s'⟩" (*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*) lemma BinOpRedsThrow2: assumes e1_steps: "P ⊨ ⟨e1,s0⟩ →* ⟨Val v1,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨throw e,s2⟩" shows "P ⊨ ⟨e1 «bop¬ e2, s0⟩ →* ⟨throw e,s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v1 «bop¬ e2, s1)" let ?y' = "(Val v1 «bop¬ throw e, s2)" have "(?x, ?y) ∈ (red P)*" by(rule BinOp1Reds[OF e1_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule BinOp2Reds[OF e2_steps]) also have "(?y', ?z) ∈ (red P)" by(rule red_reds.BinOpThrow2) ultimately show ?thesis by simp qed (*>*) subsubsection "FAcc" lemma FAccReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨e∙F{D}, s⟩ →* ⟨e'∙F{D}, s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) FAccRed[OF step(2)]]) qed (*>*) lemma FAccRedsVal: "[P ⊨ ⟨e,s⟩ →* ⟨addr a,s'⟩; hp s' a = Some(C,fs); fs(F,D) = Some v ] ==> P ⊨ ⟨e∙F{D},s⟩ →* ⟨Val v,s'⟩" (*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAcc])(*>*) lemma FAccRedsNull: "P ⊨ ⟨e,s⟩ →* ⟨null,s'⟩ ==> P ⊨ ⟨e∙F{D},s⟩ →* ⟨THROW NullPointer,s'⟩" (*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccNull])(*>*) lemma FAccRedsThrow: "P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ==> P ⊨ ⟨e∙F{D},s⟩ →* ⟨throw a,s'⟩" (*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ red_reds.FAccThrow])(*>*) subsubsection "FAss" lemma FAssReds1: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨e∙F{D}:=e2, s⟩ →* ⟨e'∙F{D}:=e2, s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) FAssRed1[OF step(2)]]) qed (*>*) lemma FAssReds2: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨Val v∙F{D}:=e, s⟩ →* ⟨Val v∙F{D}:=e', s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by 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⟩ →* ⟨addr a,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨Val v,(h2,l2)⟩" and hC: "Some(C,fs) = h2 a" shows "P ⊨ ⟨e1∙F{D}:=e2, s0⟩ →* ⟨unit, (h2(a↦(C,fs((F,D)↦v))),l2)⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(addr a∙F{D}:=e2, s1)" let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2))" have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps]) also have "(?y', ?z) ∈ (red P)" using RedFAss hC by simp ultimately show ?thesis by simp qed (*>*) lemma FAssRedsNull: assumes e1_steps: "P ⊨ ⟨e1,s0⟩ →* ⟨null,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨Val v,s2⟩" shows "P ⊨ ⟨e1∙F{D}:=e2, s0⟩ →* ⟨THROW NullPointer, s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(null∙F{D}:=e2, s1)" let ?y' = "(null∙F{D}:=Val v::expr,s2)" have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps]) also have "(?y', ?z) ∈ (red P)" by(rule RedFAssNull) ultimately show ?thesis by simp qed (*>*) lemma FAssRedsThrow1: "P ⊨ ⟨e,s⟩ →* ⟨throw e',s'⟩ ==> P ⊨ ⟨e∙F{D}:=e2, s⟩ →* ⟨throw e', s'⟩" (*<*)by(rule FAssReds1[THEN rtrancl_into_rtrancl, OF _ red_reds.FAssThrow1])(*>*) lemma FAssRedsThrow2: assumes e1_steps: "P ⊨ ⟨e1,s0⟩ →* ⟨Val v,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨throw e,s2⟩" shows "P ⊨ ⟨e1∙F{D}:=e2,s0⟩ →* ⟨throw e,s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v∙F{D}:=e2,s1)" let ?y' = "(Val v∙F{D}:=throw e,s2)" have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps]) also have "(?y', ?z) ∈ (red P)" by(rule red_reds.FAssThrow2) ultimately show ?thesis by simp qed (*>*) subsubsection";;" lemma SeqReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨e;;e2, s⟩ →* ⟨e';;e2, s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) SeqRed[OF step(2)]]) qed (*>*) lemma SeqRedsThrow: "P ⊨ ⟨e,s⟩ →* ⟨throw e',s'⟩ ==> P ⊨ ⟨e;;e2, s⟩ →* ⟨throw e', s'⟩" (*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*) lemma SeqReds2: assumes e1_steps: "P ⊨ ⟨e1,s0⟩ →* ⟨Val v1,s1⟩" and e2_steps: "P ⊨ ⟨e2,s1⟩ →* ⟨e2',s2⟩" shows "P ⊨ ⟨e1;;e2, s0⟩ →* ⟨e2',s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v1;; e2,s1)" have "(?x, ?y) ∈ (red P)*" by(rule SeqReds[OF e1_steps]) also have "(?y, ?z) ∈ (red P)*" by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF e2_steps]) ultimately show ?thesis by simp qed (*>*) subsubsection"If" lemma CondReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨if (e) e1 else e2,s⟩ →* ⟨if (e') e1 else e2,s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CondRed[OF step(2)]]) qed (*>*) lemma CondRedsThrow: "P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ==> P ⊨ ⟨if (e) e1 else e2, s⟩ →* ⟨throw a,s'⟩" (*<*)by(rule CondReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CondThrow])(*>*) lemma CondReds2T: assumes e_steps: "P ⊨ ⟨e,s0⟩ →* ⟨true,s1⟩" and e1_steps: "P ⊨ ⟨e1, s1⟩ →* ⟨e',s2⟩" shows "P ⊨ ⟨if (e) e1 else e2, s0⟩ →* ⟨e',s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(if (true) e1 else e2,s1)" have "(?x, ?y) ∈ (red P)*" by(rule CondReds[OF e_steps]) also have "(?y, ?z) ∈ (red P)*" by(rule RedCondT[THEN converse_rtrancl_into_rtrancl, OF e1_steps]) ultimately show ?thesis by simp qed (*>*) lemma CondReds2F: assumes e_steps: "P ⊨ ⟨e,s0⟩ →* ⟨false,s1⟩" and e2_steps: "P ⊨ ⟨e2, s1⟩ →* ⟨e',s2⟩" shows "P ⊨ ⟨if (e) e1 else e2, s0⟩ →* ⟨e',s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(if (false) e1 else e2,s1)" have "(?x, ?y) ∈ (red P)*" by(rule CondReds[OF e_steps]) also have "(?y, ?z) ∈ (red P)*" by(rule RedCondF[THEN converse_rtrancl_into_rtrancl, OF e2_steps]) ultimately show ?thesis by simp qed (*>*) subsubsection "While" lemma WhileFReds: assumes b_steps: "P ⊨ ⟨b,s⟩ →* ⟨false,s'⟩" shows "P ⊨ ⟨while (b) c,s⟩ →* ⟨unit,s'⟩" (*<*) by(rule RedWhile[THEN converse_rtrancl_into_rtrancl, OF CondReds[THEN rtrancl_into_rtrancl, OF b_steps RedCondF]]) (*>*) lemma WhileRedsThrow: assumes b_steps: "P ⊨ ⟨b,s⟩ →* ⟨throw e,s'⟩" shows "P ⊨ ⟨while (b) c,s⟩ →* ⟨throw e,s'⟩" (*<*) by(rule RedWhile[THEN converse_rtrancl_into_rtrancl, OF CondReds[THEN rtrancl_into_rtrancl, OF b_steps red_reds.CondThrow]]) (*>*) lemma WhileTReds: assumes b_steps: "P ⊨ ⟨b,s0⟩ →* ⟨true,s1⟩" and c_steps: "P ⊨ ⟨c,s1⟩ →* ⟨Val v1,s2⟩" and while_steps: "P ⊨ ⟨while (b) c,s2⟩ →* ⟨e,s3⟩" shows "P ⊨ ⟨while (b) c,s0⟩ →* ⟨e,s3⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(if (b) (c;; while (b) c) else unit,s0)" let ?y = "(if (true) (c;; while (b) c) else unit,s1)" let ?b' = "(c;; while (b) c,s1)" let ?y' = "(Val v1;; while (b) c,s2)" have "(?a, ?b) ∈ (red P)*" using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp also have "(?b, ?y) ∈ (red P)*" by(rule CondReds[OF b_steps]) also have "(?y, ?b') ∈ (red P)*" using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp also have "(?b', ?y') ∈ (red P)*" by(rule SeqReds[OF c_steps]) also have "(?y', ?c) ∈ (red P)*" by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF while_steps]) ultimately show ?thesis by simp qed (*>*) lemma WhileTRedsThrow: assumes b_steps: "P ⊨ ⟨b,s0⟩ →* ⟨true,s1⟩" and c_steps: "P ⊨ ⟨c,s1⟩ →* ⟨throw e,s2⟩" shows "P ⊨ ⟨while (b) c,s0⟩ →* ⟨throw e,s2⟩" (*<*)(is "(?a, ?c) \<in> (red P)\<^sup>*") proof - let ?b = "(if (b) (c;; while (b) c) else unit,s0)" let ?y = "(if (true) (c;; while (b) c) else unit,s1)" let ?b' = "(c;; while (b) c,s1)" let ?y' = "(throw e;; while (b) c,s2)" have "(?a, ?b) ∈ (red P)*" using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp also have "(?b, ?y) ∈ (red P)*" by(rule CondReds[OF b_steps]) also have "(?y, ?b') ∈ (red P)*" using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp also have "(?b', ?y') ∈ (red P)*" by(rule SeqReds[OF c_steps]) also have "(?y', ?c) ∈ (red P)" by(rule red_reds.SeqThrow) ultimately show ?thesis by simp qed (*>*) subsubsection"Throw" lemma ThrowReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨throw e,s⟩ →* ⟨throw e',s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ThrowRed[OF step(2)]]) qed (*>*) lemma ThrowRedsNull: "P ⊨ ⟨e,s⟩ →* ⟨null,s'⟩ ==> P ⊨ ⟨throw e,s⟩ →* ⟨THROW NullPointer,s'⟩" (*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ RedThrowNull])(*>*) lemma ThrowRedsThrow: "P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ==> P ⊨ ⟨throw e,s⟩ →* ⟨throw a,s'⟩" (*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ red_reds.ThrowThrow])(*>*) subsubsection "InitBlock" lemma InitBlockReds_aux: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> ∀h l h' l' v. s = (h,l(V↦v)) ⟶ s' = (h',l') ⟶ P ⊨ ⟨{V:T := Val v; e},(h,l)⟩ →* ⟨{V:T := Val(the(l' V)); e'},(h',l'(V:=(l V)))⟩" (*<*) proof(induct rule: converse_rtrancl_induct2) case refl then show ?case by(fastforce simp: fun_upd_same simp del:fun_upd_apply) next case (step e0 s0 e1 s1) obtain h1 l1 where s1[simp]: "s1 = (h1, l1)" by(cases s1) simp { fix h0 l0 h2 l2 v0 assume [simp]: "s0 = (h0, l0(V ↦ v0))" and s'[simp]: "s' = (h2, l2)" then have "V ∈ dom l1" using step(1) by(auto dest!: red_lcl_incr) then obtain v1 where l1V[simp]: "l1 V = ⌊v1⌋" by blast let ?a = "({V:T; V:=Val v0;; e0},(h0, l0))" let ?b = "({V:T; V:=Val v1;; e1},(h1, l1(V := l0 V)))" let ?c = "({V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l0 V)))" let ?l = "l1(V := l0 V)" and ?v = v1 have e0_steps: "P ⊨ ⟨e0,(h0, l0(V ↦ v0))⟩ → ⟨e1,(h1, l1)⟩" using step(1) by simp have lv: "∧l v. l1 = l(V ↦ v) ⟶ P ⊨ ⟨{V:T; V:=Val v;; e1},(h1, l)⟩ →* ⟨{V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l V))⟩" using step(3) s' s1 by blast moreover have "l1 = ?l(V ↦ ?v)" by(rule ext) (simp add:fun_upd_def) ultimately have "(?b, ?c) ∈ (red P)*" using lv[of ?l ?v] by simp then have "(?a, ?c) ∈ (red P)*" by(rule InitBlockRed[THEN converse_rtrancl_into_rtrancl, OF e0_steps l1V]) } then show ?case by blast qed (*>*) lemma InitBlockReds: "P ⊨ ⟨e, (h,l(V↦v))⟩ →* ⟨e', (h',l')⟩ ==> P ⊨ ⟨{V:T := Val v; e}, (h,l)⟩ →* ⟨{V:T := Val(the(l' V)); e'}, (h',l'(V:=(l V)))⟩" (*<*)by(blast dest:InitBlockReds_aux)(*>*) lemma InitBlockRedsFinal: "[ P ⊨ ⟨e,(h,l(V↦v))⟩ →* ⟨e',(h',l')⟩; final e' ] ==> P ⊨ ⟨{V:T := Val v; e},(h,l)⟩ →* ⟨e',(h', l'(V := l V))⟩" (*<*) by(fast elim!:InitBlockReds[THEN rtrancl_into_rtrancl] finalE intro:RedInitBlock InitBlockThrow) (*>*) subsubsection "Block" lemma BlockRedsFinal: assumes reds: "P ⊨ ⟨e0,s0⟩ →* ⟨e2,(h2,l2)⟩" and fin: "final e2" shows "∧h0 l0. s0 = (h0,l0(V:=None)) ==> P ⊨ ⟨{V:T; e0},(h0,l0)⟩ →* ⟨e2,(h2,l2(V:=l0 (*<*) using reds proof (induct rule:converse_rtrancl_induct2) case refl thus ?case by(fastforce intro:finalE[OF fin] RedBlock BlockThrow simp del:fun_upd_apply) next case (step e0 s0 e1 s1) have red: "P ⊨ ⟨e0,s0⟩ → ⟨e1,s1⟩" and reds: "P ⊨ ⟨e1,s1⟩ →* ⟨e2,(h2,l2)⟩" and IH: "∧h l. s1 = (h,l(V := None)) ==> P ⊨ ⟨{V:T; e1},(h,l)⟩ →* ⟨e2,(h2, l2(V := l V))⟩" and s0: "s0 = (h0, l0(V := None))" by fact+ obtain h1 l1 where s1: "s1 = (h1,l1)" by fastforce show ?case proof cases assume "assigned V e0" then obtain v e where e0: "e0 = V := Val v;; e" by (unfold assigned_def)blast from red e0 s0 have e1: "e1 = unit;;e" and s1: "s1 = (h0, l0(V ↦ v))" by auto from e1 fin have "e1 ≠ e2" by (auto simp:final_def) then obtain e' s' where red1: "P ⊨ ⟨e1,s1⟩ → ⟨e',s'⟩" and reds': "P ⊨ ⟨e',s'⟩ →* ⟨e2,(h2,l2)⟩" using converse_rtranclE2[OF reds] by blast from red1 e1 have es': "e' = e" "s' = s1" by auto show ?case using e0 s1 es' reds' by(fastforce 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)⟩ → ⟨{V:T; e1},(h1, l1(V := l0 V))⟩" using s0 s1 red by(simp add: BlockRedNone[OF _ _ unass]) moreover have "P ⊨ ⟨{V:T; e1},(h1, l1(V := l0 V))⟩ →* ⟨e2,(h2, l2(V := l0 V))⟩" using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem) ultimately show ?case by(rule converse_rtrancl_into_rtrancl) next fix v assume Some: "l1 V = Some v" hence "P ⊨ ⟨{V:T;e0},(h0,l0)⟩ → ⟨{V:T := Val v; e1},(h1,l1(V := l0 V))⟩" using s0 s1 red by(simp add: BlockRedSome[OF _ _ unass]) moreover have "P ⊨ ⟨{V:T := Val v; e1},(h1,l1(V:= l0 V))⟩ →* ⟨e2,(h2,l2(V:=l0 V))⟩" using InitBlockRedsFinal[OF _ fin,of _ _ "l1(V:=l0 V)" V] Some reds s1 by(simp add:fun_upd_idem) ultimately show ?case by(rule converse_rtrancl_into_rtrancl) qed qed qed (*>*) subsubsection "try-catch" lemma TryReds: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨try e catch(C V) e2,s⟩ →* ⟨try e' catch(C V) e2,s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) TryRed[OF step(2)]]) qed (*>*) lemma TryRedsVal: "P ⊨ ⟨e,s⟩ →* ⟨Val v,s'⟩ ==> P ⊨ ⟨try e catch(C V) e2,s⟩ →* ⟨Val v,s'⟩" (*<*)by(rule TryReds[THEN rtrancl_into_rtrancl, OF _ RedTry])(*>*) lemma TryCatchRedsFinal: assumes e1_steps: "P ⊨ ⟨e1,s0⟩ →* ⟨Throw a,(h1,l1)⟩" and h1a: "h1 a = Some(D,fs)" and sub: "P ⊨ D ⪯* C" and e2_steps: "P ⊨ ⟨e2, (h1, l1(V ↦ Addr a))⟩ →* ⟨e2', (h2,l2)⟩" and final: "final e2'" shows "P ⊨ ⟨try e1 catch(C V) e2, s0⟩ →* ⟨e2', (h2, (l2::locals)(V := l1 V))⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(try Throw a catch(C V) e2,(h1, l1))" let ?b = "({V:Class C; V:=addr a;; e2},(h1, l1))" have bz: "(?b, ?z) ∈ (red P)*" by(rule InitBlockRedsFinal[OF e2_steps final]) have hp: "hp (h1, l1) a = ⌊(D, fs)⌋" using h1a by simp have "(?x, ?y) ∈ (red P)*" by(rule TryReds[OF e1_steps]) also have "(?y, ?z) ∈ (red P)*" by(rule RedTryCatch[THEN converse_rtrancl_into_rtrancl, OF hp sub bz]) ultimately show ?thesis by simp qed (*>*) lemma TryRedsFail: "[ P ⊨ ⟨e1,s⟩ →* ⟨Throw a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯* C ] ==> P ⊨ ⟨try e1 catch(C V) e2,s⟩ →* ⟨Throw a,(h,l)⟩" (*<*)by(fastforce intro!: TryReds[THEN rtrancl_into_rtrancl, OF _ RedTryFail])(*>*) subsubsection "List" lemma ListReds1: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨e#es,s⟩ [→]* ⟨e' # es,s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ListRed1[OF step(2)]]) qed (*>*) lemma ListReds2: "P ⊨ ⟨es,s⟩ [→]* ⟨es',s'⟩ ==> P ⊨ ⟨Val v # es,s⟩ [→]* ⟨Val v # es',s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) ListRed2[OF step(2)]]) qed (*>*) lemma ListRedsVal: "[ P ⊨ ⟨e,s0⟩ →* ⟨Val v,s1⟩; P ⊨ ⟨es,s1⟩ [→]* ⟨es',s2⟩ ] ==> P ⊨ ⟨e#es,s0⟩ [→]* ⟨Val v # es',s2⟩" (*<*)by(rule rtrancl_trans[OF ListReds1 ListReds2])(*>*) subsubsection"Call" text‹First a few lemmas on what happens to free variables during redction.› lemma assumes wf: "wwf_J_prog P" shows Red_fv: "P ⊨ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ==> fv e' ⊆ fv e" and "P ⊨ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ==> fvs es' ⊆ fvs es" (*<*) proof (induct rule:red_reds_inducts) case (RedCall h l a C fs M Ts T pns body D vs) hence "fv body ⊆ {this} ∪ set pns" using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def) with RedCall.hyps show ?case by fastforce qed auto (*>*) lemma Red_dom_lcl: "P ⊨ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fv e" and "P ⊨ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fvs es" (*<*) proof (induct rule:red_reds_inducts) case RedLAss thus ?case by(force split:if_splits) next case CallParams thus ?case by(force split:if_splits) next case BlockRedNone thus ?case by clarsimp (fastforce split:if_splits) next case BlockRedSome thus ?case by clarsimp (fastforce split:if_splits) next case InitBlockRed thus ?case by clarsimp (fastforce split:if_splits) qed auto (*>*) lemma Reds_dom_lcl: assumes wf: "wwf_J_prog P" shows "P ⊨ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fv e" (*<*) proof(induct rule: converse_rtrancl_induct_red) case 1 then show ?case by blast next case 2 then show ?case using wf by(blast dest: Red_fv Red_dom_lcl) qed (*>*) text‹Now a few lemmas on the behaviour of blocks during reduction.› (* If you want to avoid the premise "distinct" further down \<dots> consts upd_vals :: "locals \<Rightarrow> vname list \<Rightarrow> val list \<Rightarrow> val list" primrec "upd_vals l [] vs = []" "upd_vals l (V#Vs) vs = (if V \<in> set Vs then hd vs else the(l V)) # upd_vals l Vs (tl vs)" lemma [simp]: "\<And>vs. length(upd_vals l Vs vs) = length Vs" by(induct Vs, auto) *) 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) declare fun_upd_apply[simp del] map_upds_twist[simp del] (*>*) lemma blocksReds: "∧l. [ length Vs = length Ts; length vs = length Ts; distinct Vs; P ⊨ ⟨e, (h,l(Vs [↦] vs))⟩ →* ⟨e', (h',l')⟩ ] ==> P ⊨ ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ →* ⟨blocks(Vs,Ts,map (the ∘ l') Vs,e'), (h',over (*<*) 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)⟩ →* ⟨e, (h,l)⟩" (*<*) proof(induct Vs Ts vs e rule:blocks_induct) case 1 show ?case using "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))⟩ →* ⟨e', (h',l')⟩" and fin: "final e'" and l'': "l'' = override_on l' l (set Vs)" shows "P ⊨ ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ →* ⟨e', (h',l'')⟩" (*<*) proof - let ?bv = "blocks(Vs,Ts,map (the o l') Vs,e')" have "P ⊨ ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ →* ⟨?bv, (h',l'')⟩" using l'' by simp (rule blocksReds[OF wf reds]) also have "P ⊨ ⟨?bv, (h',l'')⟩ →* ⟨e', (h',l'')⟩" using wf by(fastforce intro:blocksFinal fin) finally show ?thesis . qed (*>*) text‹An now the actual method call reduction lemmas.› lemma CallRedsObj: "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨e∙M(es),s⟩ →* ⟨e'∙M(es),s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by blast next case step show ?case by(rule rtrancl_into_rtrancl[OF step(3) CallObj[OF step(2)]]) qed (*>*) lemma CallRedsParams: "P ⊨ ⟨es,s⟩ [→]* ⟨es',s'⟩ ==> P ⊨ ⟨(Val v)∙M(es),s⟩ →* ⟨(Val v)∙M(es'),s'⟩" (*<*) proof(induct rule: rtrancl_induct2) case refl show ?case by 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⟩ →* ⟨addr a,s1⟩" "P ⊨ ⟨es,s1⟩ [→]* ⟨map Val vs,(h2,l2)⟩" "h2 a = Some(C,fs)" "P ⊨ C sees M:Ts→T = (pns,body) in D" "size vs = size pns" and l2': "l2' = [this ↦ Addr a, pns[↦]vs]" and body: "P ⊨ ⟨body,(h2,l2')⟩ →* ⟨ef,(h3,l3)⟩" and "final ef" shows "P ⊨ ⟨e∙M(es), s0⟩ →* ⟨ef,(h3,l2)⟩" (*<*) 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))⟩ →* ⟨ef,(h3,l2++l3)⟩" 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⟩ →* ⟨(addr a)∙M(es),s1⟩" by(rule CallRedsObj)(rule assms(2)) also have "P ⊨ ⟨(addr a)∙M(es),s1⟩ →* ⟨(addr a)∙M(map Val vs),(h2,l2)⟩" by(rule CallRedsParams)(rule assms(3)) also have "P ⊨ ⟨(addr a)∙M(map Val vs), (h2,l2)⟩ → ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2)⟩" 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) →* ⟨ef,(h3,override_on (l2++l3) l2 ({this} ∪ set pns))⟩" by(rule blocksRedsFinal, insert assms wf body', simp_all) finally show ?thesis using eql2 by simp qed (*>*) lemma CallRedsThrowParams: assumes e_steps: "P ⊨ ⟨e,s0⟩ →* ⟨Val v,s1⟩" and es_steps: "P ⊨ ⟨es,s1⟩ [→]* ⟨map Val vs1 @ throw a # es2,s2⟩" shows "P ⊨ ⟨e∙M(es),s0⟩ →* ⟨throw a,s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(Val v∙M(es),s1)" let ?y' = "(Val v∙M(map Val vs1 @ throw a # es2),s2)" have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps]) also have "(?y', ?z) ∈ (red P)*" using CallThrowParams by fast ultimately show ?thesis by simp qed (*>*) lemma CallRedsThrowObj: "P ⊨ ⟨e,s0⟩ →* ⟨throw a,s1⟩ ==> P ⊨ ⟨e∙M(es),s0⟩ →* ⟨throw a,s1⟩" (*<*)by(rule CallRedsObj[THEN rtrancl_into_rtrancl, OF _ CallThrowObj])(*>*) lemma CallRedsNull: assumes e_steps: "P ⊨ ⟨e,s0⟩ →* ⟨null,s1⟩" and es_steps: "P ⊨ ⟨es,s1⟩ [→]* ⟨map Val vs,s2⟩" shows "P ⊨ ⟨e∙M(es),s0⟩ →* ⟨THROW NullPointer,s2⟩" (*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*") proof - let ?y = "(null∙M(es),s1)" let ?y' = "(null∙M(map Val vs),s2)" have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps]) also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps]) also have "(?y', ?z) ∈ (red P)" by(rule RedCallNull) ultimately show ?thesis by simp qed (*>*) subsubsection "The main Theorem" lemma assumes wwf: "wwf_J_prog P" shows big_by_small: "P ⊨ ⟨e,s⟩ ==> ⟨e',s'⟩ ==> P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩" and bigs_by_smalls: "P ⊨ ⟨es,s⟩ [==>] ⟨es',s'⟩ ==> P ⊨ ⟨es,s⟩ [→]* ⟨es',s'⟩" (*<*) proof (induct rule: eval_evals.inducts) case New thus ?case by (auto simp:RedNew) next case NewFail thus ?case by (auto simp:RedNewFail) next case Cast thus ?case by(fastforce intro:CastRedsAddr) next case CastNull thus ?case by(simp add:CastRedsNull) next case CastFail thus ?case by(fastforce intro!:CastRedsFail) next case CastThrow thus ?case by(auto dest!:eval_final simp:CastRedsThrow) next case Val thus ?case by simp next case BinOp thus ?case by(auto simp:BinOpRedsVal) next case BinOpThrow1 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow1) next case BinOpThrow2 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow2) next case Var thus ?case by (auto simp:RedVar) next case LAss thus ?case by(auto simp: LAssRedsVal) next case LAssThrow thus ?case by(auto dest!:eval_final simp: LAssRedsThrow) next case FAcc thus ?case by(auto intro:FAccRedsVal) next case FAccNull thus ?case by(simp add:FAccRedsNull) next case FAccThrow thus ?case by(auto dest!:eval_final simp:FAccRedsThrow) next case FAss thus ?case by(auto simp:FAssRedsVal) next case FAssNull thus ?case by(auto simp:FAssRedsNull) next case FAssThrow1 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow1) next case FAssThrow2 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow2) next case CallObjThrow thus ?case by(auto dest!:eval_final simp:CallRedsThrowObj) next case CallNull thus ?case by(simp add:CallRedsNull) next case CallParamsThrow thus ?case by(auto dest!:evals_final simp:CallRedsThrowParams) next case (Call e s0 a s1 ps vs h2 l2 C fs M Ts T pns body D l2' e' h3 l3) have IHe: "P ⊨ ⟨e,s0⟩ →* ⟨addr a,s1⟩" and IHes: "P ⊨ ⟨ps,s1⟩ [→]* ⟨map Val vs,(h2,l2)⟩" and h2a: "h2 a = Some(C,fs)" and "method": "P ⊨ C sees M:Ts→T = (pns,body) in D" and same_length: "length vs = length pns" and l2': "l2' = [this ↦ Addr a, pns[↦]vs]" and eval_body: "P ⊨ ⟨body,(h2, l2')⟩ ==> ⟨e',(h3, l3)⟩" and IHbody: "P ⊨ ⟨body,(h2,l2')⟩ →* ⟨e',(h3,l3)⟩" by fact+ show "P ⊨ ⟨e∙M(ps),s0⟩ →* ⟨e',(h3, l2)⟩" using "method" same_length l2' h2a IHbody eval_final[OF eval_body] by(fastforce intro:CallRedsFinal[OF wwf IHe IHes]) next case Block thus ?case by(auto simp: BlockRedsFinal dest:eval_final) next case Seq thus ?case by(auto simp:SeqReds2) next case SeqThrow thus ?case by(auto dest!:eval_final simp: SeqRedsThrow) next case CondT thus ?case by(auto simp:CondReds2T) next case CondF thus ?case by(auto simp:CondReds2F) next case CondThrow thus ?case by(auto dest!:eval_final simp:CondRedsThrow) next case WhileF thus ?case by(auto simp:WhileFReds) next case WhileT thus ?case by(auto simp: WhileTReds) next case WhileCondThrow thus ?case by(auto dest!:eval_final simp: WhileRedsThrow) next case WhileBodyThrow thus ?case by(auto dest!:eval_final simp: WhileTRedsThrow) next case Throw thus ?case by(auto simp:ThrowReds) next case ThrowNull thus ?case by(auto simp:ThrowRedsNull) next case ThrowThrow thus ?case by(auto dest!:eval_final simp:ThrowRedsThrow) next case Try thus ?case by(simp add:TryRedsVal) next case TryCatch thus ?case by(fast intro!: TryCatchRedsFinal dest!:eval_final) next case TryThrow thus ?case by(fastforce intro!:TryRedsFail) next case Nil thus ?case by simp next case Cons thus ?case by(fastforce intro!:Cons_eq_appendI[OF refl refl] ListRedsVal) next case ConsThrow thus ?case by(fastforce elim: ListReds1) qed (*>*) subsection‹Big steps simulates small step› text‹This direction was carried out by Norbert Schirmer and Daniel .› text ‹The big step equivalent of ‹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 ==> ∃ l''. P ⊨ ⟨e,(h,l(ps[↦]vs))⟩ ==> ⟨e',(h',l'')⟩" (*<*) 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)⟩ ==> ⟨e',(h', l')⟩" by fact with Ts vs have "P ⊨ ⟨{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l)⟩ ==> ⟨e',(h', l')⟩" by simp then obtain l''' where eval_ps': "P ⊨ ⟨blocks (ps', Ts', vs', e),(h, l(p↦v))⟩ ==> ⟨e',(h', l''')⟩" 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'))⟩ ==> ⟨e',(h', l'')⟩" using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto from hyp show "∃l''. P ⊨ ⟨e,(h, l(p # ps'[↦]vs))⟩ ==> ⟨e',(h', l'')⟩" using Ts vs by auto qed (*>*) (* FIXME exercise: show precise relationship between l' and l'': lemma blocksEval: "\<And> Ts vs l l'. \<lbrakk>length ps = length Ts; length ps = length vs; P\<turnstile> \<langle>blocks(ps,Ts,vs,e),(h,l)\<rangle> \<Rightarrow> \<langle>e',(h',l')\<ra \<Longrightarrow> \<exists> l''. P \<turnstile> \<langle>e,(h,l(ps[\<mapsto>]vs))\<rangle> \<Righta proof (induct ps) case Nil then show ?case by simp next case (Cons p ps') have length_eqs: "length (p # ps') = length Ts" "length (p # ps') = length vs" . 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 \<turnstile> \<langle>blocks (p # ps', Ts, vs, e),(h,l)\<rangle> \<Rightarrow> \<langle>e',(h with Ts vs have "P \<turnstile> \<langle>{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l)\<rangle> \<Rightarrow> by simp then obtain l''' where eval_ps': "P \<turnstile> \<langle>blocks (ps', Ts', vs', e),(h, l(p\<mapsto>v))\<rangle> \<Righta and l''': "l'=l'''(p:=l p)" by (cases) (auto elim: eval_cases) then obtain l'' where hyp: "P \<turnstile> \<langle>e,(h, l(p\<mapsto>v)(ps'[\<mapsto>]vs'))\<rangle> \<Rightarrow> \<lan l'': "l''' = l''(l(p\<mapsto>v)|set ps')" using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto have "l' = l''(l|set (p # ps'))" proof - have "(l''(l(p\<mapsto>v)|set ps'))(p := l p) = l''(l|insert p (set ps'))" by (induct ps') (auto intro: ext simp add: fun_upd_def override_on_def) with l''' l'' show ?thesis by simp qed with hyp show "\<exists>l''. P \<turnstile> \<langle>e,(h, l(p # ps'[\<mapsto>]vs))\<rangle> \<Rightarrow> \<la l' = l''(l|set (p # ps'))" using Ts vs by auto qed *) lemma assumes wf: "wwf_J_prog P" shows eval_restrict_lcl: "P ⊨ ⟨e,(h,l)⟩ ==> ⟨e',(h',l')⟩ ==> (∧W. fv e ⊆ W ==> P ⊨ ⟨e,(h,l|`W)⟩ ==> ⟨e',(h',l'|` and "P ⊨ ⟨es,(h,l)⟩ [==>] ⟨es',(h',l')⟩ ==> (∧W. fvs es ⊆ W ==> P ⊨ ⟨es,(h,l|`W)⟩ [==>] (*<*) proof(induct rule:eval_evals_inducts) case (Block e0 h0 l0 V e1 h1 l1 T) have IH: "∧W. fv e0 ⊆ W ==> P ⊨ ⟨e0,(h0,l0(V:=None)|`W)⟩ ==> ⟨e1,(h1,l1|`W)⟩" 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))⟩ ==> ⟨e1,(h1, l1|`insert V W)⟩" 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 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 v h l l' V) have IH: "∧W. fv e ⊆ W ==> P ⊨ ⟨e,(h0,l0|`W)⟩ ==> ⟨Val v,(h,l|`W)⟩" 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 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 CallObjThrow thus ?case by simp (blast intro: eval_evals.intros) next case CallNull thus ?case by simp (blast intro: eval_evals.CallNull) next case CallParamsThrow thus ?case by simp (blast intro: eval_evals.CallParamsThrow) next case (Call e h0 l0 a h1 l1 ps vs h2 l2 C fs M Ts T pns body D l2' e' h3 l3) have IHe: "∧W. fv e ⊆ W ==> P ⊨ ⟨e,(h0,l0|`W)⟩ ==> ⟨addr a,(h1,l1|`W)⟩" and IHps: "∧W. fvs ps ⊆ W ==> P ⊨ ⟨ps,(h1,l1|`W)⟩ [==>] ⟨map Val vs,(h2,l2|`W)⟩" and IHbd: "∧W. fv body ⊆ W ==> P ⊨ ⟨body,(h2,l2'|`W)⟩ ==> ⟨e',(h3,l3|`W)⟩" and h2a: "h2 a = Some (C, fs)" and "method": "P ⊨ C sees M: 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 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 a h1 l1 D fs C e2 V e2' h2 l2) have IH1: "∧W. fv e1 ⊆ W ==> P ⊨ ⟨e1,(h0,l0|`W)⟩ ==> ⟨Throw a,(h1,l1|`W)⟩" and IH2: "∧W. fv e2 ⊆ W ==> P ⊨ ⟨e2,(h1,l1(V↦Addr a)|`W)⟩ ==> ⟨e2',(h2,l2|`W)⟩" 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))⟩ ==> ⟨e2',(h2,l2|`insert V W)⟩" using IH2[OF fv2] fun_upd_restrict[of l1 W] (*FIXME just l|W instead of l|(W-V) in simp rule?? 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) qed (*>*) lemma eval_notfree_unchanged: "P ⊨ ⟨e,(h,l)⟩ ==> ⟨e',(h',l')⟩ ==> (∧V. V ∉ fv e ==> l' V = l V)" and "P ⊨ ⟨es,(h,l)⟩ [==>] ⟨es',(h',l')⟩ ==> (∧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 qed simp_all (*>*) lemma eval_closed_lcl_unchanged: "[ P ⊨ ⟨e,(h,l)⟩ ==> ⟨e',(h',l')⟩; 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 (*>*) (* 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] (*>*) (* FIXME exercise 1: define a big step semantics where the body of a procedure can access not juts this and pns but all of the enclosing l. What exactly is fed in? What exactly is returned at the end? Notion: "dynamic binding" excercise 2: the semantics of exercise 1 is closer to the small step semantics. Reformulate equivalence proof by modifying call lemmas. *) text ‹The key lemma:› lemma assumes wf: "wwf_J_prog P" shows extend_1_eval: "P ⊨ ⟨e,s⟩ → ⟨e'',s''⟩ ==> (∧s' e'. P ⊨ ⟨e'',s''⟩ ==> ⟨e',s'⟩ ==> P ⊨ ⟨e,s⟩ ==> ⟨e',s'⟩)" and extend_1_evals: "P ⊨ ⟨es,t⟩ [→] ⟨es'',t''⟩ ==> (∧t' es'. P ⊨ ⟨es'',t''⟩ [==>] ⟨es',t'⟩ ==> P ⊨ ⟨es,t⟩ [==>] (*<*) proof (induct rule: red_reds.inducts) case (RedCall s a C fs M Ts T pns body D vs s' e') have "P ⊨ ⟨addr a,s⟩ ==> ⟨addr a,s⟩" by (rule eval_evals.intros) moreover have finals: "finals(map Val vs)" by simp obtain h2 l2 where s: "s = (h2,l2)" by (cases s) with finals have "P ⊨ ⟨map Val vs,s⟩ [==>] ⟨map Val vs,(h2,l2)⟩" by (iprover intro: eval_finalsId) moreover from s have "h2 a = Some (C, fs)" using RedCall by simp moreover have "method": "P ⊨ C sees M: 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 where s': "s' = (h3,l3)" by (cases s') have eval_blocks: "P ⊨ ⟨blocks (this # pns, Class D # Ts, Addr a # vs, body),s⟩ ==> ⟨e',s'⟩" by fact hence id: "l3 = l2" using fv s s' same_len1 same_len by(fastforce elim: eval_closed_lcl_unchanged) from eval_blocks obtain l3' where "P ⊨ ⟨body,(h2,l2')⟩ ==> ⟨e',(h3,l3')⟩" proof - from same_len1 have "length(this#pns) = length(Class D#Ts)" by simp moreover from same_len1 same_len have "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),(h2,l2)⟩ ==>⟨e',(h3,l3)⟩" using s s' by simp ultimately obtain l'' where "P ⊨ ⟨body,(h2,l2(this # pns[↦]Addr a # vs))⟩==>⟨e',(h3, l'')⟩" by (blast dest:blocksEval) from eval_restrict_lcl[OF wf this fv] this_distinct same_len1 same_len have "P ⊨ ⟨body,(h2,[this # pns[↦]Addr a # vs])⟩ ==> ⟨e',(h3, l''|`(set(this#pns)))⟩" 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),s⟩ ==> ⟨e',(h3,l2)⟩" by (rule Call) with s' id show ?case by simp next case RedNew thus ?case by (iprover elim: eval_cases intro: eval_evals.intros) next case RedNewFail thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (CastRed e s e'' s'' C s' e') thus ?case by(cases s, cases s') (erule eval_cases, auto intro: eval_evals.intros) next case RedCastNull thus ?case by (iprover elim: eval_cases intro: eval_evals.intros) next case (RedCast s a D fs C s'' e'') thus ?case by (cases s) (auto elim: eval_cases intro: eval_evals.intros) next case (RedCastFail s a D fs C s'' e'') thus ?case by (cases s) (auto elim!: eval_cases intro: eval_evals.intros) next case (BinOpRed1 e s e' s' bop e2 s'' e') thus ?case by (cases s'')(erule eval_cases,auto intro: eval_evals.intros) next case BinOpRed2 thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId) next case RedBinOp thus ?case by (iprover elim: eval_cases intro: eval_evals.intros) next case (RedVar s V v s' e') thus ?case by (cases s)(fastforce elim: eval_cases intro: eval_evals.intros) next case (LAssRed e s e' s' V s'') thus ?case by (cases s'')(erule eval_cases,auto intro: eval_evals.intros) next case RedLAss thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (FAccRed e s e' s' F D s'') thus ?case by (cases s'')(erule eval_cases,auto intro: eval_evals.intros) next case (RedFAcc s a C fs F D v s' e') thus ?case by (cases s)(fastforce elim: eval_cases intro: eval_evals.intros) next case RedFAccNull thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros) next case (FAssRed1 e s e' s'' F D e2 s' e') thus ?case by (cases s')(erule eval_cases, auto intro: eval_evals.intros) next case (FAssRed2 e s e' s'' v F D s' e') thus ?case by (cases s) (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId) 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 CallObj thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros) next case CallParams thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId) next case RedCallNull thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros eval_finalsId) next case InitBlockRed thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId simp add: map_upd_triv fun_upd_same) next case (RedInitBlock V T v u s s' e') have "P ⊨ ⟨Val u,s⟩ ==> ⟨e',s'⟩" by fact then obtain s': "s'=s" and e': "e'=Val u" by cases simp obtain h l where s: "s=(h,l)" by (cases s) have "P ⊨ ⟨{V:T :=Val v; Val u},(h,l)⟩ ==> ⟨Val u,(h, (l(V↦v))(V:=l V))⟩" by (fastforce intro!: eval_evals.intros) thus "P ⊨ ⟨{V:T := Val v; Val u},s⟩ ==> ⟨e',s'⟩" using s s' e' 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 s' e') have "P ⊨ ⟨Val v,s⟩ ==> ⟨e',s'⟩" by fact then obtain s': "s'=s" and e': "e'=Val v" by cases simp obtain h l where s: "s=(h,l)" by (cases s) have "P ⊨ ⟨Val v,(h,l(V:=None))⟩ ==> ⟨Val v,(h,l(V:=None))⟩" by (rule eval_evals.intros) hence "P ⊨ ⟨{V:T;Val v},(h,l)⟩ ==> ⟨Val v,(h,(l(V:=None))(V:=l V))⟩" by (rule eval_evals.Block) thus "P ⊨ ⟨{V:T; Val v},s⟩ ==> ⟨e',s'⟩" using s s' e' by simp next case SeqRed thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) 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) 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 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case RedThrowNull thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (TryRed e s e' s' C V e2 s'' e') thus ?case by (cases s, cases s'', auto elim!: eval_cases intro: eval_evals.intros) next case RedTry 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 s' e') 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) next case ListRed2 thus ?case by (fastforce elim!: evals_cases eval_cases intro: eval_evals.intros eval_finalId) next case CastThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case BinOpThrow1 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case BinOpThrow2 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case LAssThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case FAccThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case FAssThrow1 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 CallThrowObj thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case (CallThrowParams es vs e es' v M s s' e') have "P ⊨ ⟨Val v,s⟩ ==> ⟨Val v,s⟩" by (rule eval_evals.intros) moreover have es: "es = map Val vs @ throw e # es'" by fact have eval_e: "P ⊨ ⟨throw e,s⟩ ==> ⟨e',s'⟩" by fact then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final) with list_eval_Throw [OF eval_e] es have "P ⊨ ⟨es,s⟩ [==>] ⟨map Val vs @ Throw xa # es',s'⟩" by simp ultimately have "P ⊨ ⟨Val v∙M(es),s⟩ ==> ⟨Throw xa,s'⟩" by (rule eval_evals.CallParamsThrow) thus ?case using e' by simp next case (InitBlockThrow V T v a s s' e') have "P ⊨ ⟨Throw a,s⟩ ==> ⟨e',s'⟩" by fact then obtain s': "s' = s" and e': "e' = Throw a" by cases (auto elim!:eval_cases) obtain h l where s: "s = (h,l)" by (cases s) have "P ⊨ ⟨{V:T :=Val v; Throw a},(h,l)⟩ ==> ⟨Throw a, (h, (l(V↦v))(V:=l V))⟩" by(fastforce intro:eval_evals.intros) thus "P ⊨ ⟨{V:T := Val v; Throw a},s⟩ ==> ⟨e',s'⟩" using s s' e' by simp next case (BlockThrow V T a s s' e') have "P ⊨ ⟨Throw a, s⟩ ==> ⟨e',s'⟩" by fact then obtain s': "s' = s" and e': "e' = Throw a" by cases (auto elim!:eval_cases) obtain h l where s: "s=(h,l)" by (cases s) have "P ⊨ ⟨Throw a, (h,l(V:=None))⟩ ==> ⟨Throw a, (h,l(V:=None))⟩" by (simp add:eval_evals.intros eval_finalId) hence "P⊨⟨{V:T;Throw a},(h,l)⟩==>⟨Throw a, (h,(l(V:=None))(V:=l V))⟩" by (rule eval_evals.Block) thus "P ⊨ ⟨{V:T; Throw a},s⟩ ==> ⟨e',s'⟩" using s s' e' by simp next case SeqThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case CondThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) next case ThrowThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros) qed (*>*) (*<*) (* ... und wieder anschalten: *) declare split_paired_All [simp] split_paired_Ex [simp] (*>*) text ‹Its extension to ‹→*›:› lemma extend_eval: assumes wf: "wwf_J_prog P" and reds: "P ⊨ ⟨e,s⟩ →* ⟨e'',s''⟩" and eval_rest: "P ⊨ ⟨e'',s''⟩ ==> ⟨e',s'⟩" shows "P ⊨ ⟨e,s⟩ ==> ⟨e',s'⟩" (*<*) using reds eval_rest proof (induct rule: converse_rtrancl_induct2) case refl then show ?case by simp next case step show ?case using step extend_1_eval[OF wf step.hyps(1)] by simp qed (*>*) lemma extend_evals: assumes wf: "wwf_J_prog P" and reds: "P ⊨ ⟨es,s⟩ [→]* ⟨es'',s''⟩" and eval_rest: "P ⊨ ⟨es'',s''⟩ [==>] ⟨es',s'⟩" shows "P ⊨ ⟨es,s⟩ [==>] ⟨es',s'⟩" (*<*) using reds eval_rest proof (induct rule: converse_rtrancl_induct2) case refl then show ?case by simp next case step show ?case using step extend_1_evals[OF wf step.hyps(1)] by simp qed (*>*) text ‹Finally, small step semantics can be simulated by big step semantics: › theorem assumes wf: "wwf_J_prog P" shows small_by_big: "[P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩; final e'] ==> P ⊨ ⟨e,s⟩ ==> ⟨e',s'⟩" and "[P ⊨ ⟨es,s⟩ [→]* ⟨es',s'⟩; finals es'] ==> P ⊨ ⟨es,s⟩ [==>] ⟨es',s'⟩" (*<*) proof - note wf moreover assume "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩" moreover assume "final e'" then have "P ⊨ ⟨e',s'⟩ ==> ⟨e',s'⟩" by (rule eval_finalId) ultimately show "P ⊨ ⟨e,s⟩==>⟨e',s'⟩" by (rule extend_eval) next note wf moreover assume "P ⊨ ⟨es,s⟩ [→]* ⟨es',s'⟩" moreover assume "finals es'" then have "P ⊨ ⟨es',s'⟩ [==>] ⟨es',s'⟩" by (rule eval_finalsId) 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 ==> P ⊨ ⟨e,s⟩ ==> ⟨e',s'⟩ = (P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ∧ final e')" (*<*)by(blast dest: big_by_small eval_final small_by_big)(*>*) end
¤ Dauer der Verarbeitung: 0.64 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09