# Theory Equivalence

```(*  Title:      Jinja/J/Equivalence.thy
Author:     Tobias Nipkow
*)

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])(*>*)

"⟦ 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» e⇩2, s⟩ →* ⟨e' «bop» e⇩2, 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 e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v⇩2,s⇩2⟩"
and op: "binop(bop,v⇩1,v⇩2) = Some v"
shows "P ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ →* ⟨Val v,s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1 «bop» e⇩2, s⇩1)"
let ?y' = "(Val v⇩1 «bop» Val v⇩2, s⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule BinOp1Reds[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule BinOp2Reds[OF e⇩2_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» e⇩2, s⟩ →* ⟨throw e', s'⟩"
(*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*)

lemma BinOpRedsThrow2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨throw e,s⇩2⟩"
shows "P ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ →* ⟨throw e,s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1 «bop» e⇩2, s⇩1)"
let ?y' = "(Val v⇩1 «bop» throw e, s⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule BinOp1Reds[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule BinOp2Reds[OF e⇩2_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}:=e⇩2, s⟩ →* ⟨e'∙F{D}:=e⇩2, 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 e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨addr a,s⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v,(h⇩2,l⇩2)⟩"
and hC: "Some(C,fs) = h⇩2 a"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0⟩ →* ⟨unit, (h⇩2(a↦(C,fs((F,D)↦v))),l⇩2)⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(addr a∙F{D}:=e⇩2, s⇩1)"
let ?y' = "(addr a∙F{D}:=Val v::expr,(h⇩2,l⇩2))"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_steps])
also have "(?y', ?z) ∈ (red P)" using RedFAss hC by simp
ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsNull:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨null,s⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v,s⇩2⟩"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0⟩ →* ⟨THROW NullPointer, s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(null∙F{D}:=e⇩2, s⇩1)"
let ?y' = "(null∙F{D}:=Val v::expr,s⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_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}:=e⇩2, s⟩ →* ⟨throw e', s'⟩"
(*<*)by(rule FAssReds1[THEN rtrancl_into_rtrancl, OF _ red_reds.FAssThrow1])(*>*)

lemma FAssRedsThrow2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v,s⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨throw e,s⇩2⟩"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ →* ⟨throw e,s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v∙F{D}:=e⇩2,s⇩1)"
let ?y' = "(Val v∙F{D}:=throw e,s⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_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;;e⇩2, s⟩ →* ⟨e';;e⇩2, 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;;e⇩2, s⟩ →* ⟨throw e', s'⟩"
(*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*)

lemma SeqReds2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩"
and   e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨e⇩2',s⇩2⟩"
shows "P ⊢ ⟨e⇩1;;e⇩2, s⇩0⟩ →* ⟨e⇩2',s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1;; e⇩2,s⇩1)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule SeqReds[OF e⇩1_steps])
also have "(?y, ?z) ∈ (red P)⇧*"
by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF e⇩2_steps])
ultimately show ?thesis by simp
qed
(*>*)

subsubsection"If"

lemma CondReds:
"P ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P ⊢ ⟨if (e) e⇩1 else e⇩2,s⟩ →* ⟨if (e') e⇩1 else e⇩2,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) e⇩1 else e⇩2, s⟩ →* ⟨throw a,s'⟩"
(*<*)by(rule CondReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CondThrow])(*>*)

lemma CondReds2T:
assumes e_steps: "P ⊢ ⟨e,s⇩0⟩ →* ⟨true,s⇩1⟩"
and   e⇩1_steps: "P ⊢ ⟨e⇩1, s⇩1⟩ →* ⟨e',s⇩2⟩"
shows "P ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ →* ⟨e',s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(if (true) e⇩1 else e⇩2,s⇩1)"
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 e⇩1_steps])
ultimately show ?thesis by simp
qed
(*>*)

lemma CondReds2F:
assumes e_steps: "P ⊢ ⟨e,s⇩0⟩ →* ⟨false,s⇩1⟩"
and   e⇩2_steps: "P ⊢ ⟨e⇩2, s⇩1⟩ →* ⟨e',s⇩2⟩"
shows "P ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ →* ⟨e',s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(if (false) e⇩1 else e⇩2,s⇩1)"
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 e⇩2_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,s⇩0⟩ →* ⟨true,s⇩1⟩"
and c_steps: "P ⊢ ⟨c,s⇩1⟩ →* ⟨Val v⇩1,s⇩2⟩"
and while_steps: "P ⊢ ⟨while (b) c,s⇩2⟩ →* ⟨e,s⇩3⟩"
shows "P ⊢ ⟨while (b) c,s⇩0⟩ →* ⟨e,s⇩3⟩"
(*<*)(is "(?a, ?c) ∈ (red P)⇧*")
proof -
let ?b = "(if (b) (c;; while (b) c) else unit,s⇩0)"
let ?y = "(if (true) (c;; while (b) c) else unit,s⇩1)"
let ?b' = "(c;; while (b) c,s⇩1)"
let ?y' = "(Val v⇩1;; while (b) c,s⇩2)"
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,s⇩0⟩ →* ⟨true,s⇩1⟩"
and c_steps: "P ⊢ ⟨c,s⇩1⟩ →* ⟨throw e,s⇩2⟩"
shows "P ⊢ ⟨while (b) c,s⇩0⟩ →* ⟨throw e,s⇩2⟩"
(*<*)(is "(?a, ?c) ∈ (red P)⇧*")
proof -
let ?b = "(if (b) (c;; while (b) c) else unit,s⇩0)"
let ?y = "(if (true) (c;; while (b) c) else unit,s⇩1)"
let ?b' = "(c;; while (b) c,s⇩1)"
let ?y' = "(throw e;; while (b) c,s⇩2)"
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 ⊢ ⟨e⇩0,s⇩0⟩ →* ⟨e⇩2,(h⇩2,l⇩2)⟩" and fin: "final e⇩2"
shows "⋀h⇩0 l⇩0. s⇩0 = (h⇩0,l⇩0(V:=None)) ⟹ P ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ →* ⟨e⇩2,(h⇩2,l⇩2(V:=l⇩0 V))⟩"
(*<*)
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 e⇩0 s⇩0 e⇩1 s⇩1)
have red: "P ⊢ ⟨e⇩0,s⇩0⟩ → ⟨e⇩1,s⇩1⟩"
and reds: "P ⊢ ⟨e⇩1,s⇩1⟩ →* ⟨e⇩2,(h⇩2,l⇩2)⟩"
and IH: "⋀h l. s⇩1 = (h,l(V := None))
⟹ P ⊢ ⟨{V:T; e⇩1},(h,l)⟩ →* ⟨e⇩2,(h⇩2, l⇩2(V := l V))⟩"
and s⇩0: "s⇩0 = (h⇩0, l⇩0(V := None))" by fact+
obtain h⇩1 l⇩1 where s⇩1: "s⇩1 = (h⇩1,l⇩1)" by fastforce
show ?case
proof cases
assume "assigned V e⇩0"
then obtain v e where e⇩0: "e⇩0 = V := Val v;; e"
by (unfold assigned_def)blast
from red e⇩0 s⇩0 have e⇩1: "e⇩1 = unit;;e" and s⇩1: "s⇩1 = (h⇩0, l⇩0(V ↦ v))"
by auto
from e⇩1 fin have "e⇩1 ≠ e⇩2" by (auto simp:final_def)
then obtain e' s' where red1: "P ⊢ ⟨e⇩1,s⇩1⟩ → ⟨e',s'⟩"
and reds': "P ⊢ ⟨e',s'⟩ →* ⟨e⇩2,(h⇩2,l⇩2)⟩"
using converse_rtranclE2[OF reds] by blast
from red1 e⇩1 have es': "e' = e" "s' = s⇩1" by auto
show ?case using e⇩0 s⇩1 es' reds'
by(fastforce intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply)
next
assume unass: "¬ assigned V e⇩0"
show ?thesis
proof (cases "l⇩1 V")
assume None: "l⇩1 V = None"
hence "P ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ → ⟨{V:T; e⇩1},(h⇩1, l⇩1(V := l⇩0 V))⟩"
using s⇩0 s⇩1 red by(simp add: BlockRedNone[OF _ _ unass])
moreover
have "P ⊢ ⟨{V:T; e⇩1},(h⇩1, l⇩1(V := l⇩0 V))⟩ →* ⟨e⇩2,(h⇩2, l⇩2(V := l⇩0 V))⟩"
using IH[of _ "l⇩1(V := l⇩0 V)"] s⇩1 None by(simp add:fun_upd_idem)
ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
next
fix v assume Some: "l⇩1 V = Some v"
hence "P ⊢ ⟨{V:T;e⇩0},(h⇩0,l⇩0)⟩ → ⟨{V:T := Val v; e⇩1},(h⇩1,l⇩1(V := l⇩0 V))⟩"
using s⇩0 s⇩1 red by(simp add: BlockRedSome[OF _ _ unass])
moreover
have "P ⊢ ⟨{V:T := Val v; e⇩1},(h⇩1,l⇩1(V:= l⇩0 V))⟩ →*
⟨e⇩2,(h⇩2,l⇩2(V:=l⇩0 V))⟩"
using InitBlockRedsFinal[OF _ fin,of _ _ "l⇩1(V:=l⇩0 V)" V]
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) e⇩2,s⟩ →* ⟨try e' catch(C V) e⇩2,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) e⇩2,s⟩ →* ⟨Val v,s'⟩"
(*<*)by(rule TryReds[THEN rtrancl_into_rtrancl, OF _ RedTry])(*>*)

lemma TryCatchRedsFinal:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Throw a,(h⇩1,l⇩1)⟩"
and h⇩1a: "h⇩1 a = Some(D,fs)" and sub: "P ⊢ D ≼⇧* C"
and e⇩2_steps: "P ⊢ ⟨e⇩2, (h⇩1, l⇩1(V ↦ Addr a))⟩ →* ⟨e⇩2', (h⇩2,l⇩2)⟩"
and final: "final e⇩2'"
shows "P ⊢ ⟨try e⇩1 catch(C V) e⇩2, s⇩0⟩ →* ⟨e⇩2', (h⇩2, (l⇩2::locals)(V := l⇩1 V))⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(try Throw a catch(C V) e⇩2,(h⇩1, l⇩1))"
let ?b = "({V:Class C; V:=addr a;; e⇩2},(h⇩1, l⇩1))"
have bz: "(?b, ?z) ∈ (red P)⇧*"
by(rule InitBlockRedsFinal[OF e⇩2_steps final])
have hp: "hp (h⇩1, l⇩1) a = ⌊(D, fs)⌋" using h⇩1a by simp
have "(?x, ?y) ∈ (red P)⇧*" by(rule TryReds[OF e⇩1_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 ⊢ ⟨e⇩1,s⟩ →* ⟨Throw a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢ ⟨try e⇩1 catch(C V) e⇩2,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,s⇩0⟩ →* ⟨Val v,s⇩1⟩; P ⊢ ⟨es,s⇩1⟩ [→]* ⟨es',s⇩2⟩ ⟧
⟹ P ⊢ ⟨e#es,s⇩0⟩ [→]* ⟨Val v # es',s⇩2⟩"
(*<*)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 …
consts upd_vals :: "locals ⇒ vname list ⇒ val list ⇒ val list"
primrec
"upd_vals l [] vs = []"
"upd_vals l (V#Vs) vs = (if V ∈ set Vs then hd vs else the(l V)) #
upd_vals l Vs (tl vs)"

lemma [simp]: "⋀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)"

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',override_on l' l (set Vs))⟩"
(*<*)
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,s⇩0⟩ →* ⟨addr a,s⇩1⟩"
"P ⊢ ⟨es,s⇩1⟩ [→]* ⟨map Val vs,(h⇩2,l⇩2)⟩"
"h⇩2 a = Some(C,fs)" "P ⊢ C sees M:Ts→T = (pns,body) in D"
"size vs = size pns"
and l⇩2': "l⇩2' = [this ↦ Addr a, pns[↦]vs]"
and body: "P ⊢ ⟨body,(h⇩2,l⇩2')⟩ →* ⟨ef,(h⇩3,l⇩3)⟩"
and "final ef"
shows "P ⊢ ⟨e∙M(es), s⇩0⟩ →* ⟨ef,(h⇩3,l⇩2)⟩"
(*<*)
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)+
have body': "P ⊢ ⟨body,(h⇩2,l⇩2(this↦ Addr a, pns[↦]vs))⟩ →* ⟨ef,(h⇩3,l⇩2++l⇩3)⟩"
have "dom l⇩3 ⊆ {this} ∪ set pns"
using Reds_dom_lcl[OF wwf body] wt l⇩2' set_take_subset by force
hence eql⇩2: "override_on (l⇩2++l⇩3) l⇩2 ({this} ∪ set pns) = l⇩2"
have "P ⊢ ⟨e∙M(es),s⇩0⟩ →* ⟨(addr a)∙M(es),s⇩1⟩" by(rule CallRedsObj)(rule assms(2))
also have "P ⊢ ⟨(addr a)∙M(es),s⇩1⟩ →*
by(rule CallRedsParams)(rule assms(3))
also have "P ⊢ ⟨(addr a)∙M(map Val vs), (h⇩2,l⇩2)⟩ →
⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h⇩2,l⇩2)⟩"
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), (h⇩2,l⇩2)⟩
→* ⟨ef,(h⇩3,override_on (l⇩2++l⇩3) l⇩2 ({this} ∪ set pns))⟩"
by(rule blocksRedsFinal, insert assms wf body', simp_all)
finally show ?thesis using eql⇩2 by simp
qed
(*>*)

lemma CallRedsThrowParams:
assumes e_steps: "P ⊢ ⟨e,s⇩0⟩ →* ⟨Val v,s⇩1⟩"
and es_steps: "P ⊢ ⟨es,s⇩1⟩ [→]* ⟨map Val vs⇩1 @ throw a # es⇩2,s⇩2⟩"
shows "P ⊢ ⟨e∙M(es),s⇩0⟩ →* ⟨throw a,s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v∙M(es),s⇩1)"
let ?y' = "(Val v∙M(map Val vs⇩1 @ throw a # es⇩2),s⇩2)"
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,s⇩1⟩ ⟹ P ⊢ ⟨e∙M(es),s0⟩ →* ⟨throw a,s⇩1⟩"
(*<*)by(rule CallRedsObj[THEN rtrancl_into_rtrancl, OF _ CallThrowObj])(*>*)

lemma CallRedsNull:
assumes e_steps: "P ⊢ ⟨e,s⇩0⟩ →* ⟨null,s⇩1⟩"
and es_steps: "P ⊢ ⟨es,s⇩1⟩ [→]* ⟨map Val vs,s⇩2⟩"
shows "P ⊢ ⟨e∙M(es),s⇩0⟩ →* ⟨THROW NullPointer,s⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(null∙M(es),s⇩1)"
let ?y' = "(null∙M(map Val vs),s⇩2)"
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 s⇩0 a s⇩1 ps vs h⇩2 l⇩2 C fs M Ts T pns body D l⇩2' e' h⇩3 l⇩3)
have IHe: "P ⊢ ⟨e,s⇩0⟩ →* ⟨addr a,s⇩1⟩"
and IHes: "P ⊢ ⟨ps,s⇩1⟩ [→]* ⟨map Val vs,(h⇩2,l⇩2)⟩"
and h⇩2a: "h⇩2 a = Some(C,fs)"
and "method": "P ⊢ C sees M:Ts→T = (pns,body) in D"
and same_length: "length vs = length pns"
and l⇩2': "l⇩2' = [this ↦ Addr a, pns[↦]vs]"
and eval_body: "P ⊢ ⟨body,(h⇩2, l⇩2')⟩ ⇒ ⟨e',(h⇩3, l⇩3)⟩"
and IHbody: "P ⊢ ⟨body,(h⇩2,l⇩2')⟩ →* ⟨e',(h⇩3,l⇩3)⟩" by fact+
show "P ⊢ ⟨e∙M(ps),s⇩0⟩ →* ⟨e',(h⇩3, l⇩2)⟩"
using "method" same_length l⇩2' h⇩2a 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
Wasserrab.›

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 s⇩1
assume eval_false: "P ⊢ ⟨b,s⟩ ⇒ ⟨false,s⇩1⟩"
and eval_unit: "P ⊢ ⟨unit,s⇩1⟩ ⇒ ⟨e',s'⟩"
with eval_unit have "s' = s⇩1" "e' = unit" by (auto elim: eval_cases)
moreover from eval_false have "P ⊢ ⟨while (b) c,s⟩ ⇒ ⟨unit,s⇩1⟩"
by - (rule WhileF, simp)
ultimately show ?thesis by simp
next
fix s⇩1
assume eval_true: "P ⊢ ⟨b,s⟩ ⇒ ⟨true,s⇩1⟩"
and eval_rest: "P ⊢ ⟨c;; while (b) c,s⇩1⟩⇒⟨e',s'⟩"
from eval_rest show ?thesis
proof (cases)
fix s⇩2 v⇩1
assume "P ⊢ ⟨c,s⇩1⟩ ⇒ ⟨Val v⇩1,s⇩2⟩" "P ⊢ ⟨while (b) c,s⇩2⟩ ⇒ ⟨e',s'⟩"
with eval_true show "P ⊢ ⟨while(b) c,s⟩ ⇒ ⟨e',s'⟩" by (rule WhileT)
next
fix a
assume "P ⊢ ⟨c,s⇩1⟩ ⇒ ⟨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)⟩ ⇒ ⟨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:
"⋀ Ts vs l l'. ⟦length ps = length Ts; length ps = length vs;
P⊢ ⟨blocks(ps,Ts,vs,e),(h,l)⟩ ⇒ ⟨e',(h',l')⟩ ⟧
⟹ ∃ l''. P ⊢ ⟨e,(h,l(ps[↦]vs))⟩ ⇒ ⟨e',(h',l'')⟩ ∧ l'=l''(l|set ps)"
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 ⊢ ⟨blocks (p # ps', Ts, vs, e),(h,l)⟩ ⇒ ⟨e',(h', l')⟩".
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 (cases) (auto elim: eval_cases)

then obtain l'' where
hyp: "P ⊢ ⟨e,(h, l(p↦v)(ps'[↦]vs'))⟩ ⇒ ⟨e',(h', l'')⟩" and
l'': "l''' = l''(l(p↦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↦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 "∃l''. P ⊢ ⟨e,(h, l(p # ps'[↦]vs))⟩ ⇒ ⟨e',(h', l'')⟩ ∧
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'|`W)⟩)"
and "P ⊢ ⟨es,(h,l)⟩ [⇒] ⟨es',(h',l')⟩ ⟹ (⋀W. fvs es ⊆ W ⟹ P ⊢ ⟨es,(h,l|`W)⟩ [⇒] ⟨es',(h',l'|`W)⟩)"
(*<*)
proof(induct rule:eval_evals_inducts)
case (Block e⇩0 h⇩0 l⇩0 V e⇩1 h⇩1 l⇩1 T)
have IH: "⋀W. fv e⇩0 ⊆ W ⟹ P ⊢ ⟨e⇩0,(h⇩0,l⇩0(V:=None)|`W)⟩ ⇒ ⟨e⇩1,(h⇩1,l⇩1|`W)⟩" by fact
have "fv({V:T; e⇩0}) ⊆ W" by fact+
hence "fv e⇩0 - {V} ⊆ W" by simp_all
hence "fv e⇩0 ⊆ insert V W" by fast
from IH[OF this]
have "P ⊢ ⟨e⇩0,(h⇩0, (l⇩0|`W)(V := None))⟩ ⇒ ⟨e⇩1,(h⇩1, l⇩1|`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 h⇩0 l⇩0 v h l l' V)
have IH: "⋀W. fv e ⊆ W ⟹ P ⊢ ⟨e,(h⇩0,l⇩0|`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 h⇩0 l⇩0 a h⇩1 l⇩1 ps vs h⇩2 l⇩2 C fs M Ts T pns body
D l⇩2' e' h⇩3 l⇩3)
have IHe: "⋀W. fv e ⊆ W ⟹ P ⊢ ⟨e,(h⇩0,l⇩0|`W)⟩ ⇒ ⟨addr a,(h⇩1,l⇩1|`W)⟩"
and IHps: "⋀W. fvs ps ⊆ W ⟹ P ⊢ ⟨ps,(h⇩1,l⇩1|`W)⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2|`W)⟩"
and IHbd: "⋀W. fv body ⊆ W ⟹ P ⊢ ⟨body,(h⇩2,l⇩2'|`W)⟩ ⇒ ⟨e',(h⇩3,l⇩3|`W)⟩"
and h⇩2a: "h⇩2 a = Some (C, fs)"
and "method": "P ⊢ C sees M: Ts→T = (pns, body) in D"
and same_len: "size vs = size pns"
and l⇩2': "l⇩2' = [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] l⇩2' same_len wfmethod h⇩2a
eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ "method" same_len l⇩2']
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 e⇩1 h⇩0 l⇩0 a h⇩1 l⇩1 D fs C e⇩2 V e⇩2' h⇩2 l⇩2)
have IH⇩1: "⋀W. fv e⇩1 ⊆ W ⟹ P ⊢ ⟨e⇩1,(h⇩0,l⇩0|`W)⟩ ⇒ ⟨Throw a,(h⇩1,l⇩1|`W)⟩"
and IH⇩2: "⋀W. fv e⇩2 ⊆ W ⟹ P ⊢ ⟨e⇩2,(h⇩1,l⇩1(V↦Addr a)|`W)⟩ ⇒ ⟨e⇩2',(h⇩2,l⇩2|`W)⟩"
and lookup: "h⇩1 a = Some(D, fs)" and subtype: "P ⊢ D ≼⇧* C" by fact+
have "fv (try e⇩1 catch(C V) e⇩2) ⊆ W" by fact
hence fv⇩1: "fv e⇩1 ⊆ W" and fv⇩2: "fv e⇩2 ⊆ insert V W" by auto
have IH⇩2': "P ⊢ ⟨e⇩2,(h⇩1,(l⇩1|`W)(V ↦ Addr a))⟩ ⇒ ⟨e⇩2',(h⇩2,l⇩2|`insert V W)⟩"
using IH⇩2[OF fv⇩2] fun_upd_restrict[of l⇩1 W] (*FIXME just l|W instead of l|(W-V) in simp rule??*) by simp
with eval_evals.TryCatch[OF IH⇩1[OF fv⇩1] _ subtype IH⇩2'] 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⟩ [⇒] ⟨es',t'⟩)"
(*<*)
proof (induct rule: red_reds.inducts)
case (RedCall s a C fs M Ts T pns body D vs s' e')
moreover
have finals: "finals(map Val vs)" by simp
obtain h⇩2 l⇩2 where s: "s = (h⇩2,l⇩2)" by (cases s)
with finals have "P ⊢ ⟨map Val vs,s⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩"
by (iprover intro: eval_finalsId)
moreover from s have "h⇩2 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_len⇩1: "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 l⇩2' where l⇩2': "l⇩2' = [this↦Addr a,pns[↦]vs]" by simp
moreover
obtain h⇩3 l⇩3 where s': "s' = (h⇩3,l⇩3)" by (cases s')
have eval_blocks:
"P ⊢ ⟨blocks (this # pns, Class D # Ts, Addr a # vs, body),s⟩ ⇒ ⟨e',s'⟩" by fact
hence id: "l⇩3 = l⇩2" using fv s s' same_len⇩1 same_len
by(fastforce elim: eval_closed_lcl_unchanged)
from eval_blocks obtain l⇩3' where "P ⊢ ⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3')⟩"
proof -
from same_len⇩1 have "length(this#pns) = length(Class D#Ts)" by simp
moreover from same_len⇩1 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),(h⇩2,l⇩2)⟩
⇒⟨e',(h⇩3,l⇩3)⟩" using s s' by simp
ultimately obtain l''
where "P ⊢ ⟨body,(h⇩2,l⇩2(this # pns[↦]Addr a # vs))⟩⇒⟨e',(h⇩3, l'')⟩"
by (blast dest:blocksEval)
from eval_restrict_lcl[OF wf this fv] this_distinct same_len⇩1 same_len
have "P ⊢ ⟨body,(h⇩2,[this # pns[↦]Addr a # vs])⟩ ⇒
⟨e',(h⇩3, l''|`(set(this#pns)))⟩"
thus ?thesis by(fastforce intro!:that simp add: l⇩2')
qed
ultimately
have "P ⊢ ⟨(addr a)∙M(map Val vs),s⟩ ⇒ ⟨e',(h⇩3,l⇩2)⟩" 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 e⇩2 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 e⇩2 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