Quelle  Equivalence.thy

(*  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¬ e₂, s⟩ →* ⟨e' «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) 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₁_steps: "P ⊨ ⟨e₁,s₀⟩ →* ⟨Val v₁,s₁⟩"
  and e₂_steps: "P ⊨ ⟨e₂,s₁⟩ →* ⟨Val v₂,s₂⟩"
  and op: "binop(bop,v₁,v₂) = Some v"
shows "P ⊨ ⟨e₁ «bop¬ e₂, s₀⟩ →* ⟨Val v,s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(Val v₁ «bop¬ e₂, s₁)"
  let ?y' = "(Val v₁ «bop¬ Val v₂, s₂)"
  have "(?x, ?y) ∈ (red P)^*" by(rule BinOp1Reds[OF e₁_steps])
  also have "(?y, ?y') ∈ (red P)^*" by(rule BinOp2Reds[OF e₂_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₂, s⟩ →* ⟨throw e', s'⟩"
(*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*)

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

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

lemma FAssRedsThrow2:
assumes e₁_steps: "P ⊨ ⟨e₁,s₀⟩ →* ⟨Val v,s₁⟩"
  and e₂_steps: "P ⊨ ⟨e₂,s₁⟩ →* ⟨throw e,s₂⟩"
shows "P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ →* ⟨throw e,s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(Val v∙F{D}:=e₂,s₁)"
  let ?y' = "(Val v∙F{D}:=throw e,s₂)"
  have "(?x, ?y) ∈ (red P)^*" by(rule FAssReds1[OF e₁_steps])
  also have "(?y, ?y') ∈ (red P)^*" by(rule FAssReds2[OF e₂_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₂, s⟩ →* ⟨e';;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) SeqRed[OF step(2)]])
qed
(*>*)

lemma SeqRedsThrow:
  "P ⊨ ⟨e,s⟩ →* ⟨throw e',s'⟩ ==> P ⊨ ⟨e;;e₂, s⟩ →* ⟨throw e', s'⟩"
(*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*)

lemma SeqReds2:
assumes e₁_steps: "P ⊨ ⟨e₁,s₀⟩ →* ⟨Val v₁,s₁⟩"
  and   e₂_steps: "P ⊨ ⟨e₂,s₁⟩ →* ⟨e₂',s₂⟩"
shows "P ⊨ ⟨e₁;;e₂, s₀⟩ →* ⟨e₂',s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(Val v₁;; e₂,s₁)"
  have "(?x, ?y) ∈ (red P)^*" by(rule SeqReds[OF e₁_steps])
  also have "(?y, ?z) ∈ (red P)^*"
    by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF e₂_steps])
  ultimately show ?thesis by simp
qed
(*>*)


subsubsection"If"

lemma CondReds:
  "P ⊨ ⟨e,s⟩ →* ⟨e',s'⟩ ==> P ⊨ ⟨if (e) e₁ else e₂,s⟩ →* ⟨if (e') e₁ else 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) CondRed[OF step(2)]])
qed
(*>*)

lemma CondRedsThrow:
  "P ⊨ ⟨e,s⟩ →* ⟨throw a,s'⟩ ==> P ⊨ ⟨if (e) e₁ else e₂, s⟩ →* ⟨throw a,s'⟩"
(*<*)by(rule CondReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CondThrow])(*>*)

lemma CondReds2T:
assumes e_steps: "P ⊨ ⟨e,s₀⟩ →* ⟨true,s₁⟩"
  and   e₁_steps: "P ⊨ ⟨e₁, s₁⟩ →* ⟨e',s₂⟩"
shows "P ⊨ ⟨if (e) e₁ else e₂, s₀⟩ →* ⟨e',s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(if (true) e₁ else e₂,s₁)"
  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₁_steps])
  ultimately show ?thesis by simp
qed
(*>*)

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

lemma TryRedsVal:
  "P ⊨ ⟨e,s⟩ →* ⟨Val v,s'⟩ ==> P ⊨ ⟨try e catch(C V) e₂,s⟩ →* ⟨Val v,s'⟩"
(*<*)by(rule TryReds[THEN rtrancl_into_rtrancl, OF _ RedTry])(*>*)

lemma TryCatchRedsFinal:
assumes e₁_steps: "P ⊨ ⟨e₁,s₀⟩ →* ⟨Throw a,(h₁,l₁)⟩"
  and h₁a: "h₁ a = Some(D,fs)" and sub: "P ⊨ D ⪯^* C"
  and e₂_steps: "P ⊨ ⟨e₂, (h₁, l₁(V ↦ Addr a))⟩ →* ⟨e₂', (h₂,l₂)⟩"
  and final: "final e₂'"
shows "P ⊨ ⟨try e₁ catch(C V) e₂, s₀⟩ →* ⟨e₂', (h₂, (l₂::locals)(V := l₁ V))⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(try Throw a catch(C V) e₂,(h₁, l₁))"
  let ?b = "({V:Class C; V:=addr a;; e₂},(h₁, l₁))"
  have bz: "(?b, ?z) ∈ (red P)^*"
    by(rule InitBlockRedsFinal[OF e₂_steps final])
  have hp: "hp (h₁, l₁) a = ⌊(D, fs)⌋" using h₁a by simp
  have "(?x, ?y) ∈ (red P)^*" by(rule TryReds[OF e₁_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₁,s⟩ →* ⟨Throw a,(h,l)⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨try e₁ catch(C V) e₂,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₀⟩ →* ⟨Val v,s₁⟩; P ⊨ ⟨es,s₁⟩ [→]* ⟨es',s₂⟩ ]
  ==> P ⊨ ⟨e#es,s₀⟩ [→]* ⟨Val v # es',s₂⟩"
(*<*)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',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₀⟩ →* ⟨addr a,s₁⟩"
      "P ⊨ ⟨es,s₁⟩ [→]* ⟨map Val vs,(h₂,l₂)⟩"
      "h₂ a = Some(C,fs)" "P ⊨ C sees M:Ts→T = (pns,body) in D"
      "size vs = size pns"
and l₂': "l₂' = [this ↦ Addr a, pns[↦]vs]"
and body: "P ⊨ ⟨body,(h₂,l₂')⟩ →* ⟨ef,(h₃,l₃)⟩"
and "final ef"
shows "P ⊨ ⟨e∙M(es), s₀⟩ →* ⟨ef,(h₃,l₂)⟩"
(*<*)
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 l₂]
  have body': "P ⊨ ⟨body,(h₂,l₂(this↦ Addr a, pns[↦]vs))⟩ →* ⟨ef,(h₃,l₂++l₃)⟩"
    by (simp add:l₂')
  have "dom l₃ ⊆ {this} ∪ set pns"
    using Reds_dom_lcl[OF wwf body] wt l₂' set_take_subset by force
  hence eql₂: "override_on (l₂++l₃) l₂ ({this} ∪ set pns) = l₂"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have "P ⊨ ⟨e∙M(es),s₀⟩ →* ⟨(addr a)∙M(es),s₁⟩" by(rule CallRedsObj)(rule assms(2))
  also have "P ⊨ ⟨(addr a)∙M(es),s₁⟩ →*
                 ⟨(addr a)∙M(map Val vs),(h₂,l₂)⟩"
    by(rule CallRedsParams)(rule assms(3))
  also have "P ⊨ ⟨(addr a)∙M(map Val vs), (h₂,l₂)⟩ →
                 ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h₂,l₂)⟩"
    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₂,l₂)⟩
                 →* ⟨ef,(h₃,override_on (l₂++l₃) l₂ ({this} ∪ set pns))⟩"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally show ?thesis using eql₂ by simp
qed
(*>*)


lemma CallRedsThrowParams:
assumes e_steps: "P ⊨ ⟨e,s₀⟩ →* ⟨Val v,s₁⟩"
  and es_steps: "P ⊨ ⟨es,s₁⟩ [→]* ⟨map Val vs₁ @ throw a # es₂,s₂⟩"
shows "P ⊨ ⟨e∙M(es),s₀⟩ →* ⟨throw a,s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(Val v∙M(es),s₁)"
  let ?y' = "(Val v∙M(map Val vs₁ @ throw a # es₂),s₂)"
  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₁⟩ ==> P ⊨ ⟨e∙M(es),s0⟩ →* ⟨throw a,s₁⟩"
(*<*)by(rule CallRedsObj[THEN rtrancl_into_rtrancl, OF _ CallThrowObj])(*>*)


lemma CallRedsNull:
assumes e_steps: "P ⊨ ⟨e,s₀⟩ →* ⟨null,s₁⟩"
  and es_steps: "P ⊨ ⟨es,s₁⟩ [→]* ⟨map Val vs,s₂⟩"
shows "P ⊨ ⟨e∙M(es),s₀⟩ →* ⟨THROW NullPointer,s₂⟩"
(*<*)(is "(?x, ?z) \<in> (red P)\<^sup>*")
proof -
  let ?y = "(null∙M(es),s₁)"
  let ?y' = "(null∙M(map Val vs),s₂)"
  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₀ a s₁ ps vs h₂ l₂ C fs M Ts T pns body D l₂' e' h₃ l₃)
  have IHe: "P ⊨ ⟨e,s₀⟩ →* ⟨addr a,s₁⟩"
    and IHes: "P ⊨ ⟨ps,s₁⟩ [→]* ⟨map Val vs,(h₂,l₂)⟩"
    and h₂a: "h₂ 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₂': "l₂' = [this ↦ Addr a, pns[↦]vs]"
    and eval_body: "P ⊨ ⟨body,(h₂, l₂')⟩ ==> ⟨e',(h₃, l₃)⟩"
    and IHbody: "P ⊨ ⟨body,(h₂,l₂')⟩ →* ⟨e',(h₃,l₃)⟩" by fact+
  show "P ⊨ ⟨e∙M(ps),s₀⟩ →* ⟨e',(h₃, l₂)⟩"
    using "method" same_length l₂' h₂a 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 s₁
    assume eval_false: "P ⊨ ⟨b,s⟩ ==> ⟨false,s₁⟩"
    and eval_unit: "P ⊨ ⟨unit,s₁⟩ ==> ⟨e',s'⟩"
    with eval_unit have "s' = s₁" "e' = unit" by (auto elim: eval_cases)
    moreover from eval_false have "P ⊨ ⟨while (b) c,s⟩ ==> ⟨unit,s₁⟩"
      by - (rule WhileF, simp)
    ultimately show ?thesis by simp
  next
    fix s₁
    assume eval_true: "P ⊨ ⟨b,s⟩ ==> ⟨true,s₁⟩"
    and eval_rest: "P ⊨ ⟨c;; while (b) c,s₁⟩==>⟨e',s'⟩"
    from eval_rest show ?thesis
    proof (cases)
      fix s₂ v₁
      assume "P ⊨ ⟨c,s₁⟩ ==> ⟨Val v₁,s₂⟩" "P ⊨ ⟨while (b) c,s₂⟩ ==> ⟨e',s'⟩"
      with eval_true show "P ⊨ ⟨while(b) c,s⟩ ==> ⟨e',s'⟩" by (rule WhileT)
    next
      fix a
      assume "P ⊨ ⟨c,s₁⟩ ==> ⟨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:
  "\<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')\<rangle> \<rbrakk>
    \<Longrightarrow> \<exists> l''. P \<turnstile> \<langle>e,(h,l(ps[\<mapsto>]vs))\<rangle> \<Rightarrow> \<langle>e',(h',l'')\<rangle> \<and> 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 \<turnstile> \<langle>blocks (p # ps', Ts, vs, e),(h,l)\<rangle> \<Rightarrow> \<langle>e',(h', l')\<rangle>".
  with Ts vs 
  have "P \<turnstile> \<langle>{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l)\<rangle> \<Rightarrow> \<langle>e',(h', l')\<rangle>"
    by simp
  then obtain l''' where
    eval_ps': "P \<turnstile> \<langle>blocks (ps', Ts', vs', e),(h, l(p\<mapsto>v))\<rangle> \<Rightarrow> \<langle>e',(h', l''')\<rangle>"
    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> \<langle>e',(h', l'')\<rangle>" and
    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> \<langle>e',(h', l'')\<rangle> \<and>
        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₀ h₀ l₀ V e₁ h₁ l₁ T)
  have IH: "∧W. fv e₀ ⊆ W ==> P ⊨ ⟨e₀,(h₀,l₀(V:=None)|`W)⟩ ==> ⟨e<sub>1</sub>,(h<sub>1</sub>,l<sub>1</sub>|`W)⟩" by fact
  have "fv({V:T; e₀}) ⊆ W" by fact+
  hence "fv e₀ - {V} ⊆ W" by simp_all
  hence "fv e₀ ⊆ insert V W" by fast
  from IH[OF this]
  have "P ⊨ ⟨e₀,(h₀, (l₀|`W)(V := None))⟩ ==> ⟨e<sub>1</sub>,(h<sub>1</sub>, l<sub>1</sub>|`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₀ l₀ v h l l' V)
  have IH: "∧W. fv e ⊆ W ==> P ⊨ ⟨e,(h₀,l₀|`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₀ l₀ a h₁ l₁ ps vs h₂ l₂ C fs M Ts T pns body
      D l₂' e' h₃ l₃)
  have IHe: "∧W. fv e ⊆ W ==> P ⊨ ⟨e,(h₀,l₀|`W)⟩ ==> ⟨addr a,(h<sub>1</sub>,l<sub>1</sub>|`W)⟩"
   and IHps: "∧W. fvs ps ⊆ W ==> P ⊨ ⟨ps,(h₁,l₁|`W)⟩ [==>] ⟨map Val vs,(h<sub>2</sub>,l<sub>2</sub>|`W)⟩"
   and IHbd: "∧W. fv body ⊆ W ==> P ⊨ ⟨body,(h₂,l₂'|`W)⟩ ==> ⟨e',(h<sub>3</sub>,l<sub>3</sub>|`W)⟩"
   and h₂a: "h₂ 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₂': "l₂' = [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₂' same_len wfmethod h₂a
      eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ "method" same_len l₂']
    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 e₁ h₀ l₀ a h₁ l₁ D fs C e₂ V e₂' h₂ l₂)
  have IH₁: "∧W. fv e₁ ⊆ W ==> P ⊨ ⟨e₁,(h₀,l₀|`W)⟩ ==> ⟨Throw a,(h<sub>1</sub>,l<sub>1</sub>|`W)⟩"
   and IH₂: "∧W. fv e₂ ⊆ W ==> P ⊨ ⟨e₂,(h₁,l₁(V↦Addr a)|`W)⟩ ==> ⟨e<sub>2</sub>',(h<sub>2</sub>,l<sub>2</sub>|`W)⟩"
   and lookup: "h₁ a = Some(D, fs)" and subtype: "P ⊨ D ⪯^* C" by fact+
  have "fv (try e₁ catch(C V) e₂) ⊆ W" by fact
  hence fv₁: "fv e₁ ⊆ W" and fv₂: "fv e₂ ⊆ insert V W" by auto
  have IH₂': "P ⊨ ⟨e₂,(h₁,(l₁|`W)(V ↦ Addr a))⟩ ==> ⟨e<sub>2</sub>',(h<sub>2</sub>,l<sub>2</sub>|`insert V W)⟩"
    using IH₂[OF fv₂] fun_upd_restrict[of l₁ W] (*FIXME just l|W instead of l|(W-V) in simp rule??*) by simp
  with eval_evals.TryCatch[OF IH₁[OF fv₁] _ subtype IH₂'] 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')
  have "P ⊨ ⟨addr a,s⟩ ==> ⟨addr a,s⟩" by (rule eval_evals.intros)
  moreover
  have finals: "finals(map Val vs)" by simp
  obtain h₂ l₂ where s: "s = (h₂,l₂)" by (cases s)
  with finals have "P ⊨ ⟨map Val vs,s⟩ [==>] ⟨map Val vs,(h₂,l₂)⟩"
    by (iprover intro: eval_finalsId)
  moreover from s have "h₂ 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₁: "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₂' where l₂': "l₂' = [this↦Addr a,pns[↦]vs]" by simp
  moreover
  obtain h₃ l₃ where s': "s' = (h₃,l₃)" 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₃ = l₂" using fv s s' same_len₁ same_len
    by(fastforce elim: eval_closed_lcl_unchanged)
  from eval_blocks obtain l₃' where "P ⊨ ⟨body,(h₂,l₂')⟩ ==> ⟨e',(h₃,l₃')⟩"
  proof -
    from same_len₁ have "length(this#pns) = length(Class D#Ts)" by simp
    moreover from same_len₁ 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₂,l₂)⟩
              ==>⟨e',(h₃,l₃)⟩" using s s' by simp
    ultimately obtain l''
      where "P ⊨ ⟨body,(h₂,l₂(this # pns[↦]Addr a # vs))⟩==>⟨e',(h₃, l'')⟩"
      by (blast dest:blocksEval)
    from eval_restrict_lcl[OF wf this fv] this_distinct same_len₁ same_len
    have "P ⊨ ⟨body,(h₂,[this # pns[↦]Addr a # vs])⟩ ==>
               ⟨e',(h₃, l''|`(set(this#pns)))⟩"
      by(simp add:subset_insert_iff insert_Diff_if)
    thus ?thesis by(fastforce intro!:that simp add: l₂')
  qed
  ultimately
  have "P ⊨ ⟨(addr a)∙M(map Val vs),s⟩ ==> ⟨e',(h₃,l₂)⟩" 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₂ 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₂ 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 e₂ 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 e₂ 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