Theory Execute

(*  Title:       CoreC++
    Author:      Daniel Wasserrab, Stefan Berghofer
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Code generation for Semantics and Type System›

theory Execute
imports BigStep WellType
  "HOL-Library.AList_Mapping"
  "HOL-Library.Code_Target_Numeral"
begin

subsection‹General redefinitions›

inductive app :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "app [] ys ys"
| "app xs ys zs ⟹ app (x # xs) ys (x # zs)"

theorem app_eq1: "⋀ys zs. zs = xs @ ys ⟹ app xs ys zs"
  apply (induct xs)
   apply simp
   apply (rule app.intros)
  apply simp
  apply (iprover intro: app.intros)
  done

theorem app_eq2: "app xs ys zs ⟹ zs = xs @ ys"
  by (erule app.induct) simp_all

theorem app_eq: "app xs ys zs = (zs = xs @ ys)"
  apply (rule iffI)
   apply (erule app_eq2)
  apply (erule app_eq1)
  done

code_pred
  (modes:
    i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool, i ⇒ o ⇒ i ⇒ bool,
    o ⇒ i ⇒ i ⇒ bool, o ⇒ o ⇒ i ⇒ bool as reverse_app)
  app
.

declare rtranclp_rtrancl_eq[code del]

lemmas [code_pred_intro] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp

code_pred 
  (modes: 
   (i => o => bool) => i => i => bool,
   (i => o => bool) => i => o => bool)
  rtranclp
by(erule converse_rtranclpE) blast+

definition Set_project :: "('a × 'b) set => 'a => 'b set"
where "Set_project A a = {b. (a, b) ∈ A}"

lemma Set_project_set [code]:
  "Set_project (set xs) a = set (List.map_filter (λ(a', b). if a = a' then Some b else None) xs)"
by(auto simp add: Set_project_def map_filter_def intro: rev_image_eqI split: if_split_asm)


text‹Redefine map Val vs›

inductive map_val :: "expr list ⇒ val list ⇒ bool"
where
  Nil: "map_val [] []"
| Cons: "map_val xs ys ⟹ map_val (Val y # xs) (y # ys)"

code_pred 
  (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool)
  map_val
.

inductive map_val2 :: "expr list ⇒ val list ⇒ expr list ⇒ bool"
where
  Nil: "map_val2 [] [] []"
| Cons: "map_val2 xs ys zs ⟹ map_val2 (Val y # xs) (y # ys) zs"
| Throw: "map_val2 (throw e # xs) [] (throw e # xs)"

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ o ⇒ o ⇒ bool)
  map_val2
.

theorem map_val_conv: "(xs = map Val ys) = map_val xs ys"
(*<*)
proof -
  have "⋀ys. xs = map Val ys ⟹ map_val xs ys"
    apply (induct xs type:list)
     apply (case_tac ys)
      apply simp
      apply (rule map_val.Nil)
     apply simp
    apply (case_tac ys)
     apply simp
    apply simp

    apply (rule map_val.Cons)
    apply simp
    done
  moreover have "map_val xs ys ⟹ xs = map Val ys"
    by (erule map_val.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)

theorem map_val2_conv:
 "(xs = map Val ys @ throw e # zs) = map_val2 xs ys (throw e # zs)"
(*<*)
proof -
  have "⋀ys. xs = map Val ys @ throw e # zs ⟹ map_val2 xs ys (throw e # zs)"
    apply (induct xs type:list)
     apply (case_tac ys)
      apply simp
     apply simp
    apply simp
    apply (case_tac ys)
     apply simp
     apply (rule map_val2.Throw)
    apply simp
    apply (rule map_val2.Cons)
    apply simp
    done
  moreover have "map_val2 xs ys (throw e # zs) ⟹ xs = map Val ys @ throw e # zs"
    by (erule map_val2.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)


subsection‹Code generation›

lemma subclsRp_code [code_pred_intro]:
  "⟦ class P C = ⌊(Bs, rest)⌋; Predicate_Compile.contains (set Bs) (Repeats D) ⟧ ⟹ subclsRp P C D"
by(auto intro: subclsRp.intros simp add: contains_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  subclsRp
by(erule subclsRp.cases)(fastforce simp add: Predicate_Compile.contains_def)

lemma subclsR_code [code_pred_inline]:
  "P ⊢ C ≺⇩R D ⟷ subclsRp P C D"
by(simp add: subclsR_def)

lemma subclsSp_code [code_pred_intro]:
  "⟦ class P C = ⌊(Bs, rest)⌋; Predicate_Compile.contains (set Bs) (Shares D) ⟧ ⟹ subclsSp P C D"
by(auto intro: subclsSp.intros simp add: Predicate_Compile.contains_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  subclsSp
by(erule subclsSp.cases)(fastforce simp add: Predicate_Compile.contains_def)

declare SubobjsR_Base [code_pred_intro]
lemma SubobjsR_Rep_code [code_pred_intro]:
  "⟦subclsRp P C D; Subobjs⇩R P D Cs⟧ ⟹ Subobjs⇩R P C (C # Cs)"
by(simp add: SubobjsR_Rep subclsR_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  Subobjs⇩R
by(erule Subobjs⇩R.cases)(auto simp add: subclsR_code)

lemma subcls1p_code [code_pred_intro]:
  "⟦class P C = Some (Bs,rest); Predicate_Compile.contains (baseClasses Bs) D ⟧ ⟹ subcls1p P C D"
by(auto intro: subcls1p.intros simp add: Predicate_Compile.contains_def)

code_pred (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  subcls1p
by(fastforce elim!: subcls1p.cases simp add: Predicate_Compile.contains_def) 

declare Subobjs_Rep [code_pred_intro]
lemma Subobjs_Sh_code [code_pred_intro]:
  "⟦ (subcls1p P)^** C C'; subclsSp P C' D; Subobjs⇩R P D Cs⟧
  ⟹ Subobjs P C Cs"
by(rule Subobjs_Sh)(simp_all add: rtrancl_def subcls1_def subclsS_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  Subobjs
by(erule Subobjs.cases)(auto simp add: rtrancl_def subcls1_def subclsS_def)

definition widen_unique :: "prog ⇒ cname ⇒ cname ⇒ path ⇒ bool"
where "widen_unique P C D Cs ⟷ (∀Cs'. Subobjs P C Cs' ⟶ last Cs' = D ⟶ Cs = Cs')"

code_pred [inductify, skip_proof] widen_unique .

lemma widen_subcls':
  "⟦Subobjs P C Cs'; last Cs' = D; widen_unique P C D Cs' ⟧
⟹ P ⊢ Class C ≤ Class D"
by(rule widen_subcls,auto simp:path_unique_def widen_unique_def)

declare 
  widen_refl [code_pred_intro]
  widen_subcls' [code_pred_intro widen_subcls]
  widen_null [code_pred_intro]

code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool)
  widen
by(erule widen.cases)(auto simp add: path_unique_def widen_unique_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ o ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ o ⇒ bool)
  leq_path1p 
.

lemma leq_path_unfold: "P,C ⊢ Cs ⊑ Ds ⟷ (leq_path1p P C)^** Cs Ds"
by(simp add: leq_path1_def rtrancl_def)

code_pred
   (modes: i => i => i => o => bool, i => i => i => i =>  bool)
   [inductify,skip_proof] 
   path_via 
.


lemma path_unique_eq [code_pred_def]: "P ⊢ Path C to D unique ⟷
  (∃Cs. Subobjs P C Cs ∧ last Cs = D ∧ (∀Cs'. Subobjs P C Cs' ⟶ last Cs' = D ⟶ Cs = Cs'))"
by(auto simp add: path_unique_def)

code_pred
   (modes: i => i => o => bool, i => i => i => bool) 
   [inductify, skip_proof]
   path_unique .

text ‹Redefine MethodDefs and FieldDecls›

(* FIXME: These predicates should be defined inductively in the first place! *)

definition MethodDefs' :: "prog ⇒ cname ⇒ mname ⇒ path ⇒ method ⇒ bool" where
  "MethodDefs' P C M Cs mthd ≡ (Cs, mthd) ∈ MethodDefs P C M"

lemma [code_pred_intro]:
  "Subobjs P C Cs ⟹ class P (last Cs) = ⌊(Bs,fs,ms)⌋ ⟹ map_of ms M =  ⌊mthd⌋ ⟹
   MethodDefs' P C M Cs mthd"
 by (simp add: MethodDefs_def MethodDefs'_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  MethodDefs'
by(fastforce simp add: MethodDefs_def MethodDefs'_def)


definition FieldDecls' :: "prog ⇒ cname ⇒ vname ⇒ path ⇒ ty ⇒ bool" where
  "FieldDecls' P C F Cs T ≡ (Cs, T) ∈ FieldDecls P C F"

lemma [code_pred_intro]:
  "Subobjs P C Cs ⟹ class P (last Cs) = ⌊(Bs,fs,ms)⌋ ⟹ map_of fs F =  ⌊T⌋ ⟹
   FieldDecls' P C F Cs T"
by (simp add: FieldDecls_def FieldDecls'_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  FieldDecls'
by(fastforce simp add: FieldDecls_def FieldDecls'_def)



definition MinimalMethodDefs' :: "prog ⇒ cname ⇒ mname ⇒ path ⇒ method ⇒ bool" where
  "MinimalMethodDefs' P C M Cs mthd ≡ (Cs, mthd) ∈ MinimalMethodDefs P C M"

definition MinimalMethodDefs_unique :: "prog ⇒ cname ⇒ mname ⇒ path ⇒ bool"
where
  "MinimalMethodDefs_unique P C M Cs ⟷ 
  (∀Cs' mthd. MethodDefs' P C M Cs' mthd ⟶ (leq_path1p P C)^** Cs' Cs ⟶ Cs' = Cs)"

code_pred [inductify, skip_proof] MinimalMethodDefs_unique .

lemma [code_pred_intro]:
  "MethodDefs' P C M Cs mthd ⟹ MinimalMethodDefs_unique P C M Cs ⟹
   MinimalMethodDefs' P C M Cs mthd"
by (fastforce simp add:MinimalMethodDefs_def MinimalMethodDefs'_def MethodDefs'_def MinimalMethodDefs_unique_def leq_path_unfold)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool)
  MinimalMethodDefs' 
by(fastforce simp add:MinimalMethodDefs_def MinimalMethodDefs'_def MethodDefs'_def MinimalMethodDefs_unique_def leq_path_unfold)



definition LeastMethodDef_unique :: "prog ⇒ cname ⇒ mname ⇒ path ⇒ bool"
where
  "LeastMethodDef_unique P C M Cs ⟷
  (∀Cs' mthd'. MethodDefs' P C M Cs' mthd' ⟶ (leq_path1p P C)^** Cs Cs')"

code_pred [inductify, skip_proof] LeastMethodDef_unique .

lemma LeastMethodDef_unfold:
  "P ⊢ C has least M = mthd via Cs ⟷
   MethodDefs' P C M Cs mthd ∧ LeastMethodDef_unique P C M Cs"
by(fastforce simp add: LeastMethodDef_def MethodDefs'_def leq_path_unfold LeastMethodDef_unique_def)

lemma LeastMethodDef_intro [code_pred_intro]:
  "⟦ MethodDefs' P C M Cs mthd; LeastMethodDef_unique P C M Cs ⟧
  ⟹ P ⊢ C has least M = mthd via Cs"
by(simp add: LeastMethodDef_unfold LeastMethodDef_unique_def)

code_pred (modes: i => i => i => o => o => bool)
  LeastMethodDef
by(simp add: LeastMethodDef_unfold LeastMethodDef_unique_def)


definition OverriderMethodDefs' :: "prog ⇒ subobj ⇒ mname ⇒ path ⇒ method ⇒ bool" where
  "OverriderMethodDefs' P R M Cs mthd ≡ (Cs, mthd) ∈ OverriderMethodDefs P R M"

lemma Overrider1 [code_pred_intro]:
  "P ⊢ (ldc R) has least M = mthd' via Cs' ⟹ 
   MinimalMethodDefs' P (mdc R) M Cs mthd ⟹
   last (snd R) = hd Cs' ⟹ (leq_path1p P (mdc R))^** Cs (snd R @ tl Cs') ⟹
   OverriderMethodDefs' P R M Cs mthd"
apply(simp add:OverriderMethodDefs_def OverriderMethodDefs'_def MinimalMethodDefs'_def appendPath_def leq_path_unfold)
apply(rule_tac x="Cs'" in exI)
apply clarsimp
apply(cases mthd')
apply blast
done

lemma Overrider2 [code_pred_intro]:
  "P ⊢ (ldc R) has least M = mthd' via Cs' ⟹ 
   MinimalMethodDefs' P (mdc R) M Cs mthd ⟹
   last (snd R) ≠ hd Cs' ⟹ (leq_path1p P (mdc R))^** Cs Cs' ⟹
   OverriderMethodDefs' P R M Cs mthd"
by(auto simp add:OverriderMethodDefs_def OverriderMethodDefs'_def MinimalMethodDefs'_def appendPath_def leq_path_unfold simp del: split_paired_Ex)


code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  OverriderMethodDefs'
apply(clarsimp simp add: OverriderMethodDefs'_def MinimalMethodDefs'_def MethodDefs'_def OverriderMethodDefs_def appendPath_def leq_path_unfold)
apply(case_tac "last xb = hd Cs'")
 apply(simp)

apply(thin_tac "PROP _")
apply(simp add: leq_path1_def)
done


definition WTDynCast_ex :: "prog ⇒ cname ⇒ cname ⇒ bool"
where "WTDynCast_ex P D C ⟷ (∃Cs. P ⊢ Path D to C via Cs)"

code_pred [inductify, skip_proof] WTDynCast_ex .

lemma WTDynCast_new:
  "⟦P,E ⊢ e :: Class D; is_class P C;
    P ⊢ Path D to C unique ∨ ¬ WTDynCast_ex P D C⟧ 
  ⟹ P,E ⊢ Cast C e :: Class C"
by(rule WTDynCast)(auto simp add: WTDynCast_ex_def)

definition WTStaticCast_sub :: "prog ⇒ cname ⇒ cname ⇒ bool"
where "WTStaticCast_sub P C D ⟷ 
  P ⊢ Path D to C unique ∨ 
  ((subcls1p P)^** C D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs))"

code_pred [inductify, skip_proof] WTStaticCast_sub .

lemma WTStaticCast_new:
  "⟦P,E ⊢ e :: Class D; is_class P C; WTStaticCast_sub P C D ⟧
  ⟹ P,E ⊢ ⦇C⦈e :: Class C"
by (rule WTStaticCast)(auto simp add: WTStaticCast_sub_def subcls1_def rtrancl_def)

lemma WTBinOp1: "⟦ P,E ⊢ e⇩1 :: T;  P,E ⊢ e⇩2 :: T⟧
  ⟹ P,E ⊢ e⇩1 «Eq» e⇩2 :: Boolean"
  apply (rule WTBinOp)
  apply assumption+
  apply simp
  done

lemma WTBinOp2: "⟦ P,E ⊢ e⇩1 :: Integer;  P,E ⊢ e⇩2 :: Integer ⟧
  ⟹ P,E ⊢ e⇩1 «Add» e⇩2 :: Integer"
  apply (rule WTBinOp)
  apply assumption+
  apply simp
  done


lemma LeastFieldDecl_unfold [code_pred_def]: 
  "P ⊢ C has least F:T via Cs ⟷
   FieldDecls' P C F Cs T ∧ (∀Cs' T'. FieldDecls' P C F Cs' T' ⟶ (leq_path1p P C)^** Cs Cs')"
by(auto simp add: LeastFieldDecl_def FieldDecls'_def leq_path_unfold)

code_pred [inductify, skip_proof] LeastFieldDecl .


lemmas [code_pred_intro] = WT_WTs.WTNew
declare
  WTDynCast_new[code_pred_intro WTDynCast_new]
  WTStaticCast_new[code_pred_intro WTStaticCast_new]
lemmas [code_pred_intro] = WT_WTs.WTVal WT_WTs.WTVar 
declare
  WTBinOp1[code_pred_intro WTBinOp1]
  WTBinOp2 [code_pred_intro WTBinOp2]
lemmas [code_pred_intro] =
  WT_WTs.WTLAss WT_WTs.WTFAcc WT_WTs.WTFAss WT_WTs.WTCall WTStaticCall
  WT_WTs.WTBlock WT_WTs.WTSeq WT_WTs.WTCond WT_WTs.WTWhile WT_WTs.WTThrow
lemmas [code_pred_intro] = WT_WTs.WTNil WT_WTs.WTCons

code_pred
  (modes: WT: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool
   and WTs: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool)
  WT
proof -
  case WT
  from WT.prems show thesis
  proof(cases (no_simp) rule: WT.cases)
    case WTDynCast thus thesis
      by(rule WT.WTDynCast_new[OF refl, unfolded WTDynCast_ex_def, simplified])
  next
    case WTStaticCast thus ?thesis
      unfolding subcls1_def rtrancl_def mem_Collect_eq prod.case
      by(rule WT.WTStaticCast_new[OF refl, unfolded WTStaticCast_sub_def])
  next
    case WTBinOp thus ?thesis
      by(split bop.split_asm)(simp_all, (erule (4) WT.WTBinOp1[OF refl] WT.WTBinOp2[OF refl])+)
  qed(assumption|erule (2) WT.that[OF refl])+
next
  case WTs
  from WTs.prems show thesis
    by(cases (no_simp) rule: WTs.cases)(assumption|erule (2) WTs.that[OF refl])+
qed

lemma casts_to_code [code_pred_intro]:
  "(case T of Class C ⇒ False | _ ⇒ True) ⟹ P ⊢ T casts v to v"
  "P ⊢ Class C casts Null to Null"
  "⟦Subobjs P (last Cs) Cs'; last Cs' = C;
    last Cs = hd Cs'; Cs @ tl Cs' = Ds⟧ 
  ⟹ P ⊢ Class C casts Ref(a,Cs) to Ref(a,Ds)"
  "⟦Subobjs P (last Cs) Cs'; last Cs' = C; last Cs ≠ hd Cs'⟧
  ⟹ P ⊢ Class C casts Ref(a,Cs) to Ref(a,Cs')"
by(auto intro: casts_to.intros simp add: path_via_def appendPath_def)

code_pred (modes: i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ bool)
  casts_to
apply(erule casts_to.cases)
  apply(fastforce split: ty.splits)
 apply simp
apply(fastforce simp add: appendPath_def path_via_def split: if_split_asm)
done

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ bool)
  Casts_to
.


lemma card_eq_1_iff_ex1: "x ∈ A ⟹ card A = 1 ⟷ A = {x}"
apply(rule iffI)
 apply(rule equalityI)
  apply(rule subsetI)
  apply(subgoal_tac "card {x, xa} ≤ card A")
   apply(auto intro: ccontr)[1]
  apply(rule card_mono)
   apply simp_all
apply(metis Suc_n_not_n card.infinite)
done

lemma FinalOverriderMethodDef_unfold [code_pred_def]:
  "P ⊢ R has overrider M = mthd via Cs ⟷
   OverriderMethodDefs' P R M Cs mthd ∧ 
   (∀Cs' mthd'. OverriderMethodDefs' P R M Cs' mthd' ⟶ Cs = Cs' ∧ mthd = mthd')"
by(auto simp add: FinalOverriderMethodDef_def OverriderMethodDefs'_def card_eq_1_iff_ex1 simp del: One_nat_def)

code_pred
  (modes: i => i => i => o => o => bool)
  [inductify, skip_proof]
  FinalOverriderMethodDef
.

code_pred
  (modes: i => i => i => i => o => o => bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  [inductify]
  SelectMethodDef 
.

text ‹Isomorphic subo with mapping instead of a map›

type_synonym subo' = "(path × (vname, val) mapping)"
type_synonym obj'  = "cname × subo' set"

lift_definition init_class_fieldmap' :: "prog ⇒ cname ⇒ (vname, val) mapping" is "init_class_fieldmap" .

lemma init_class_fieldmap'_code [code]:
  "init_class_fieldmap' P C =
     Mapping (map (λ(F,T).(F,default_val T)) (fst(snd(the(class P C)))) )"
by transfer(simp add: init_class_fieldmap_def)

lift_definition init_obj' :: "prog ⇒ cname ⇒ subo' ⇒ bool" is init_obj .

lemma init_obj'_intros [code_pred_intro]: 
  "Subobjs P C Cs ⟹ init_obj' P C (Cs, init_class_fieldmap' P (last Cs))"
by(transfer)(rule init_obj.intros)

code_pred
  (modes: i ⇒ i ⇒ o ⇒ bool as init_obj_pred)
  init_obj'
by transfer(erule init_obj.cases, blast)


lemma init_obj_pred_conv: "set_of_pred (init_obj_pred P C) = Collect (init_obj' P C)"
by(auto elim: init_obj_predE intro: init_obj_predI)

lift_definition blank' :: "prog ⇒ cname ⇒ obj'" is "blank" .

lemma blank'_code [code]:
  "blank' P C = (C, set_of_pred (init_obj_pred P C))"
unfolding init_obj_pred_conv by transfer(simp add: blank_def)

type_synonym heap'  = "addr ⇀ obj'"

abbreviation
  cname_of' :: "heap' ⇒ addr ⇒ cname" where
  "⋀hp. cname_of' hp a == fst (the (hp a))"

lift_definition new_Addr' :: "heap' ⇒ addr option" is "new_Addr" .

lift_definition start_heap' :: "prog ⇒ heap'" is "start_heap" .

lemma start_heap'_code [code]:
  "start_heap' P = Map.empty (addr_of_sys_xcpt NullPointer ↦ blank' P NullPointer,
                        addr_of_sys_xcpt ClassCast ↦ blank' P ClassCast,
                        addr_of_sys_xcpt OutOfMemory ↦ blank' P OutOfMemory)"
by transfer(simp add: start_heap_def)

type_synonym
  state'  = "heap' × locals"

lift_definition hp' :: "state' ⇒ heap'" is hp .

lemma hp'_code [code]: "hp' = fst"
by transfer simp

lift_definition lcl' :: "state' ⇒ locals" is lcl .

lemma lcl_code [code]: "lcl' = snd"
by transfer simp


lift_definition eval' :: "prog ⇒ env ⇒ expr ⇒ state' ⇒ expr ⇒ state' ⇒ bool"
          ("_,_ ⊢ ((1⟨_,/_⟩) ⇒''/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  is eval .
lift_definition evals' :: "prog ⇒ env ⇒ expr list ⇒ state' ⇒ expr list ⇒ state' ⇒ bool"
           ("_,_ ⊢ ((1⟨_,/_⟩) [⇒'']/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  is evals .

lemma New':
  "⟦ new_Addr' h = Some a; h' = h(a↦(blank' P C)) ⟧
  ⟹ P,E ⊢ ⟨new C,(h,l)⟩ ⇒' ⟨ref (a,[C]),(h',l)⟩"
by transfer(unfold blank_def, rule New)

lemma NewFail':
  "new_Addr' h = None ⟹
  P,E ⊢ ⟨new C, (h,l)⟩ ⇒' ⟨THROW OutOfMemory,(h,l)⟩"
by transfer(rule NewFail)

lemma StaticUpCast':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Cs),s⇩1⟩; P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒' ⟨ref (a,Ds),s⇩1⟩"
by transfer(rule StaticUpCast)

lemma StaticDownCast'_new:  (* requires reverse append *)
  "⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Ds),s⇩1⟩; app Cs [C] Ds'; app Ds' Cs' Ds⟧
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒' ⟨ref(a,Cs@[C]),s⇩1⟩"
apply transfer
apply (rule StaticDownCast)
apply (simp add: app_eq)
done

lemma StaticCastNull':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩"
by transfer(rule StaticCastNull)

lemma StaticCastFail'_new: (* manual unfolding of subcls *)
"⟦ P,E ⊢ ⟨e,s⇩0⟩⇒' ⟨ref (a,Cs),s⇩1⟩;  ¬ (subcls1p P)^** (last Cs) C; C ∉ set Cs⟧
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒' ⟨THROW ClassCast,s⇩1⟩"
apply transfer
by (fastforce intro:StaticCastFail simp add: rtrancl_def subcls1_def)

lemma StaticCastThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule StaticCastThrow)

lemma StaticUpDynCast':
  "⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref(a,Cs),s⇩1⟩; P ⊢ Path last Cs to C unique;
    P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
  ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨ref(a,Ds),s⇩1⟩"
by transfer(rule StaticUpDynCast)

lemma StaticDownDynCast'_new: (* requires reverse append *)
  "⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Ds),s⇩1⟩; app Cs [C] Ds'; app Ds' Cs' Ds⟧
  ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨ref(a,Cs@[C]),s⇩1⟩"
apply transfer
apply (rule StaticDownDynCast)
apply (simp add: app_eq)
done

lemma DynCast':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S);
    P ⊢ Path D to C via Cs'; P ⊢ Path D to C unique ⟧
  ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨ref (a,Cs'),(h,l)⟩"
by transfer(rule DynCast)

lemma DynCastNull':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩"
by transfer(rule DynCastNull)

lemma DynCastFail':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩⇒' ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S); ¬ P ⊢ Path D to C unique;
    ¬ P ⊢ Path last Cs to C unique; C ∉ set Cs ⟧
  ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨null,(h,l)⟩"
by transfer(rule DynCastFail)

lemma DynCastThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule DynCastThrow)

lemma Val':
  "P,E ⊢ ⟨Val v,s⟩ ⇒' ⟨Val v,s⟩"
by transfer(rule Val)

lemma BinOp':
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val v⇩2,s⇩2⟩; 
    binop(bop,v⇩1,v⇩2) = Some v ⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩⇒'⟨Val v,s⇩2⟩"
by transfer(rule BinOp)

lemma BinOpThrow1':
  "P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨throw e,s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ ⇒' ⟨throw e,s⇩1⟩"
by transfer(rule BinOpThrow1)

lemma BinOpThrow2':
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨throw e,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒' ⟨throw e,s⇩2⟩"
by transfer(rule BinOpThrow2)

lemma Var':
  "l V = Some v ⟹
  P,E ⊢ ⟨Var V,(h,l)⟩ ⇒' ⟨Val v,(h,l)⟩"
by transfer(rule Var)

lemma LAss':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨Val v,(h,l)⟩; E V = Some T;
     P ⊢ T casts v to v'; l' = l(V↦v') ⟧
  ⟹ P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒' ⟨Val v',(h,l')⟩"
by (transfer) (erule (3) LAss)

lemma LAssThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule LAssThrow)

lemma FAcc'_new: (* iteration over set *)
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Cs'),(h,l)⟩; h a = Some(D,S);
     Ds = Cs'@⇩pCs; Predicate_Compile.contains (Set_project S Ds) fs; Mapping.lookup fs F = Some v ⟧
  ⟹ P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒' ⟨Val v,(h,l)⟩"
unfolding Set_project_def mem_Collect_eq Predicate_Compile.contains_def
by transfer(rule FAcc)

lemma FAccNull':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒' ⟨THROW NullPointer,s⇩1⟩" 
by transfer(rule FAccNull)

lemma FAccThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule FAccThrow)

lemma FAss'_new: (* iteration over set *)
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨ref (a,Cs'),s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val v,(h⇩2,l⇩2)⟩;
     h⇩2 a = Some(D,S); P ⊢ (last Cs') has least F:T via Cs; P ⊢ T casts v to v';
     Ds = Cs'@⇩pCs;  Predicate_Compile.contains (Set_project S Ds) fs; fs' = Mapping.update F v' fs;
     S' = S - {(Ds,fs)} ∪ {(Ds,fs')}; h⇩2' = h⇩2(a↦(D,S'))⟧
  ⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒' ⟨Val v',(h⇩2',l⇩2)⟩"
unfolding Predicate_Compile.contains_def Set_project_def mem_Collect_eq
by transfer(rule FAss)

lemma FAssNull':
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨null,s⇩1⟩;  P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val v,s⇩2⟩ ⟧ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒' ⟨THROW NullPointer,s⇩2⟩" 
by transfer(rule FAssNull)

lemma FAssThrow1':
  "P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule FAssThrow1)

lemma FAssThrow2':
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨throw e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒' ⟨throw e',s⇩2⟩"
by transfer(rule FAssThrow2)

lemma CallObjThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule CallObjThrow)

lemma CallParamsThrow'_new: (* requires inverse map Val and append *)
  "⟦ P,E ⊢ ⟨e,s0⟩ ⇒' ⟨Val v,s1⟩; P,E ⊢ ⟨es,s1⟩ [⇒'] ⟨evs,s2⟩;
     map_val2 evs vs (throw ex # es') ⟧
   ⟹ P,E ⊢ ⟨Call e Copt M es,s0⟩ ⇒' ⟨throw ex,s2⟩"
apply transfer
apply(rule eval_evals.CallParamsThrow, assumption+)
apply(simp add: map_val2_conv[symmetric])
done

lemma Call'_new: (* requires inverse map Val *)
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒'] ⟨evs,(h⇩2,l⇩2)⟩;
     map_val evs vs;
     h⇩2 a = Some(C,S);  P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds;
     P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs'; length vs = length pns; 
     P ⊢ Ts Casts vs to vs'; l⇩2' = [this↦Ref (a,Cs'), pns[↦]vs'];
     new_body = (case T' of Class D ⇒ ⦇D⦈body   | _  ⇒ body);  
     P,E(this↦Class(last Cs'), pns[↦]Ts) ⊢ ⟨new_body,(h⇩2,l⇩2')⟩ ⇒' ⟨e',(h⇩3,l⇩3)⟩ ⟧
  ⟹ P,E ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒' ⟨e',(h⇩3,l⇩2)⟩"
apply transfer
apply(rule Call)
apply assumption+
apply(simp add: map_val_conv[symmetric])
apply assumption+
done

lemma StaticCall'_new: (* requires inverse map Val *)
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒'] ⟨evs,(h⇩2,l⇩2)⟩;
     map_val evs vs;
     P ⊢ Path (last Cs) to C unique; P ⊢ Path (last Cs) to C via Cs'';
     P ⊢ C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@⇩pCs'')@⇩pCs';
     length vs = length pns; P ⊢ Ts Casts vs to vs'; 
     l⇩2' = [this↦Ref (a,Ds), pns[↦]vs'];
     P,E(this↦Class(last Ds), pns[↦]Ts) ⊢ ⟨body,(h⇩2,l⇩2')⟩ ⇒' ⟨e',(h⇩3,l⇩3)⟩ ⟧
  ⟹ P,E ⊢ ⟨e∙(C::)M(ps),s⇩0⟩ ⇒' ⟨e',(h⇩3,l⇩2)⟩"
apply transfer
apply(rule StaticCall)
apply(assumption)+
apply(simp add: map_val_conv[symmetric])
apply assumption+
done

lemma CallNull'_new: (* requires inverse map Val *)
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩;  P,E ⊢ ⟨es,s⇩1⟩ [⇒'] ⟨evs,s⇩2⟩; map_val evs vs ⟧
  ⟹ P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒' ⟨THROW NullPointer,s⇩2⟩"
apply transfer
apply(rule CallNull, assumption+)
apply(simp add: map_val_conv[symmetric])
done

lemma Block':
  "⟦P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0,l⇩0(V:=None))⟩ ⇒' ⟨e⇩1,(h⇩1,l⇩1)⟩ ⟧ ⟹
  P,E ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ ⇒' ⟨e⇩1,(h⇩1,l⇩1(V:=l⇩0 V))⟩"
by transfer(rule Block)

lemma Seq':
  "⟦ P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒' ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒' ⟨e⇩2,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩ ⇒' ⟨e⇩2,s⇩2⟩"
by transfer(rule Seq)

lemma SeqThrow':
  "P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒' ⟨throw e,s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩⇒'⟨throw e,s⇩1⟩"
by transfer(rule SeqThrow)

lemma CondT':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒' ⟨e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒' ⟨e',s⇩2⟩"
by transfer(rule CondT)

lemma CondF':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨false,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒' ⟨e',s⇩2⟩"
by transfer(rule CondF)

lemma CondThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule CondThrow)

lemma WhileF':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨false,s⇩1⟩ ⟹
  P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒' ⟨unit,s⇩1⟩"
by transfer(rule WhileF)

lemma WhileT':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒' ⟨Val v⇩1,s⇩2⟩; 
     P,E ⊢ ⟨while (e) c,s⇩2⟩ ⇒' ⟨e⇩3,s⇩3⟩ ⟧
  ⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒' ⟨e⇩3,s⇩3⟩"
by transfer(rule WhileT)

lemma WhileCondThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule WhileCondThrow)

lemma WhileBodyThrow':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒' ⟨throw e',s⇩2⟩⟧
  ⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒' ⟨throw e',s⇩2⟩"
by transfer(rule WhileBodyThrow)

lemma Throw':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref r,s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒' ⟨Throw r,s⇩1⟩"
by transfer(rule eval_evals.Throw)

lemma ThrowNull':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒' ⟨THROW NullPointer,s⇩1⟩"
by transfer(rule ThrowNull)

lemma ThrowThrow':
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩"
by transfer(rule ThrowThrow)

lemma Nil':
  "P,E ⊢ ⟨[],s⟩ [⇒'] ⟨[],s⟩"
by transfer(rule eval_evals.Nil)

lemma Cons':
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [⇒'] ⟨es',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e#es,s⇩0⟩ [⇒'] ⟨Val v # es',s⇩2⟩"
by transfer(rule eval_evals.Cons)

lemma ConsThrow':
  "P,E ⊢ ⟨e, s⇩0⟩ ⇒' ⟨throw e', s⇩1⟩ ⟹
  P,E ⊢ ⟨e#es, s⇩0⟩ [⇒'] ⟨throw e' # es, s⇩1⟩"
by transfer(rule ConsThrow)

text ‹Axiomatic heap address model refinement›

partial_function (option) lowest :: "(nat ⇒ bool) ⇒ nat ⇒ nat option"
where
  [code]: "lowest P n = (if P n then Some n else lowest P (Suc n))"

axiomatization
where
  new_Addr'_code [code]: "new_Addr' h = lowest (Option.is_none ∘ h) 0"
    ― ‹admissible: a tightening of the specification of @{const new_Addr'}›

lemma eval'_cases
  [consumes 1,
   case_names New NewFail StaticUpCast StaticDownCast StaticCastNull StaticCastFail
    StaticCastThrow StaticUpDynCast StaticDownDynCast DynCast DynCastNull DynCastFail
    DynCastThrow Val BinOp BinOpThrow1 BinOpThrow2 Var LAss LAssThrow FAcc FAccNull FAccThrow
    FAss FAssNull FAssThrow1 FAssThrow2 CallObjThrow CallParamsThrow Call StaticCall CallNull
    Block Seq SeqThrow CondT CondF CondThrow WhileF WhileT WhileCondThrow WhileBodyThrow
    Throw ThrowNull ThrowThrow]:
  assumes "P,x ⊢ ⟨y,z⟩ ⇒' ⟨u,v⟩"
  and "⋀h a h' C E l. x = E ⟹ y = new C ⟹ z = (h, l) ⟹ u = ref (a, [C]) ⟹
    v = (h', l) ⟹ new_Addr' h = ⌊a⌋ ⟹ h' = h(a ↦ blank' P C) ⟹ thesis"
  and "⋀h E C l. x = E ⟹ y = new C ⟹ z = (h, l) ⟹
    u = Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory]) ⟹
    v = (h, l) ⟹ new_Addr' h = None ⟹ thesis"
  and "⋀E e s⇩0 a Cs s⇩1 C Cs' Ds. x = E ⟹ y = ⦇C⦈e ⟹ z = s⇩0 ⟹
    u = ref (a, Ds) ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),s⇩1⟩ ⟹
    P ⊢ Path last Cs to C via Cs'  ⟹ Ds = Cs @⇩p Cs' ⟹ thesis"
  and "⋀E e s⇩0 a Cs C Cs' s⇩1. x = E ⟹ y = ⦇C⦈e ⟹ z = s⇩0 ⟹ u = ref (a, Cs @ [C]) ⟹
    v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs @ [C] @ Cs'),s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 C. x = E ⟹ y = ⦇C⦈e ⟹ z = s⇩0 ⟹ u = null ⟹ v = s⇩1 ⟹
   P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 a Cs s⇩1 C. x = E ⟹ y = ⦇C⦈e ⟹ z = s⇩0 ⟹
    u = Throw (addr_of_sys_xcpt ClassCast, [ClassCast]) ⟹  v = s⇩1 ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),s⇩1⟩ ⟹ (last Cs, C) ∉ (subcls1 P)⇧* ⟹ C ∉ set Cs ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 C. x = E ⟹ y = ⦇C⦈e ⟹ z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 a Cs s⇩1 C Cs' Ds. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹ u = ref (a, Ds) ⟹
    v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),s⇩1⟩ ⟹ P ⊢ Path last Cs to C unique ⟹
    P ⊢ Path last Cs to C via Cs'  ⟹ Ds = Cs @⇩p Cs' ⟹ thesis"
  and "⋀E e s⇩0 a Cs C Cs' s⇩1. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹
    u = ref (a, Cs @ [C]) ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs @ [C] @ Cs'),s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 a Cs h l D S C Cs'. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹
    u = ref (a, Cs') ⟹ v = (h, l) ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),(h, l)⟩ ⟹
    h a = ⌊(D, S)⌋ ⟹ P ⊢ Path D to C via Cs'  ⟹ P ⊢ Path D to C unique ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 C. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹ u = null ⟹ v = s⇩1 ⟹ 
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ thesis" 
  and "⋀E e s⇩0 a Cs h l D S C. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹ u = null ⟹
    v = (h, l) ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),(h, l)⟩ ⟹ h a = ⌊(D, S)⌋ ⟹
    ¬ P ⊢ Path D to C unique ⟹ ¬ P ⊢ Path last Cs to C unique ⟹ C ∉ set Cs ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 C. x = E ⟹ y = Cast C e ⟹ z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1
    ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E va s. x = E ⟹ y = Val va ⟹ z = s ⟹ u = Val va ⟹ v = s ⟹ thesis"
  and "⋀E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 v⇩2 s⇩2 bop va. x = E ⟹ y = e⇩1 «bop» e⇩2 ⟹ z = s⇩0 ⟹
    u = Val va ⟹ v = s⇩2 ⟹ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val v⇩1,s⇩1⟩ ⟹
    P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val v⇩2,s⇩2⟩ ⟹ binop (bop, v⇩1, v⇩2) = ⌊va⌋ ⟹ thesis"
  and "⋀E e⇩1 s⇩0 e s⇩1 bop e⇩2. x = E ⟹ y = e⇩1 «bop» e⇩2 ⟹ z = s⇩0 ⟹ u = throw e ⟹ v = s⇩1  ⟹
    P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨throw e,s⇩1⟩ ⟹ thesis"
  and "⋀E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 e s⇩2 bop. x = E ⟹ y = e⇩1 «bop» e⇩2 ⟹ z = s⇩0 ⟹ u = throw e ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val v⇩1,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨throw e,s⇩2⟩ ⟹ thesis"
  and "⋀l V va E h. x = E ⟹ y = Var V ⟹ z = (h, l) ⟹ u = Val va ⟹ v = (h, l) ⟹
    l V = ⌊va⌋ ⟹ thesis"
  and "⋀E e s⇩0 va h l V T v' l'. x = E ⟹ y = V:=e ⟹ z = s⇩0 ⟹ u = Val v' ⟹
    v = (h, l') ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨Val va,(h, l)⟩ ⟹
    E V = ⌊T⌋ ⟹ P ⊢ T casts va to v'  ⟹ l' = l(V ↦ v') ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 V. x = E ⟹ y = V:=e ⟹ z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 a Cs' h l D S Ds Cs fs F va. x = E ⟹ y = e∙F{Cs} ⟹ z = s⇩0 ⟹
    u = Val va ⟹ v = (h, l) ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs'),(h, l)⟩ ⟹
    h a = ⌊(D, S)⌋ ⟹ Ds = Cs' @⇩p Cs ⟹ (Ds, fs) ∈ S ⟹ Mapping.lookup fs F = ⌊va⌋ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 F Cs. x = E ⟹ y = e∙F{Cs} ⟹ z = s⇩0 ⟹
    u = Throw (addr_of_sys_xcpt NullPointer, [NullPointer]) ⟹
    v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 F Cs. x = E ⟹ y = e∙F{Cs} ⟹ z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e⇩1 s⇩0 a Cs' s⇩1 e⇩2 va h⇩2 l⇩2 D S F T Cs v' Ds fs fs' S' h⇩2'.
    x = E ⟹ y = e⇩1∙F{Cs} := e⇩2 ⟹ z = s⇩0 ⟹ u = Val v' ⟹ v = (h⇩2', l⇩2) ⟹
    P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨ref (a, Cs'),s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val va,(h⇩2, l⇩2)⟩ ⟹
    h⇩2 a = ⌊(D, S)⌋ ⟹ P ⊢ last Cs' has least F:T via Cs ⟹
    P ⊢ T casts va to v'  ⟹ Ds = Cs' @⇩p Cs ⟹ (Ds, fs) ∈ S ⟹ fs' = Mapping.update F v' fs ⟹
    S' = S - {(Ds, fs)} ∪ {(Ds, fs')} ⟹ h⇩2' = h⇩2(a ↦ (D, S')) ⟹ thesis"
  and "⋀E e⇩1 s⇩0 s⇩1 e⇩2 va s⇩2 F Cs. x = E ⟹ y = e⇩1∙F{Cs} := e⇩2 ⟹ z = s⇩0 ⟹
    u = Throw (addr_of_sys_xcpt NullPointer, [NullPointer]) ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨Val va,s⇩2⟩ ⟹ thesis"
  and "⋀E e⇩1 s⇩0 e' s⇩1 F Cs e⇩2. x = E ⟹ y = e⇩1∙F{Cs} := e⇩2 ⟹
    z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e⇩1 s⇩0 va s⇩1 e⇩2 e' s⇩2 F Cs. x = E ⟹ y = e⇩1∙F{Cs} := e⇩2 ⟹ z = s⇩0 ⟹
    u = throw e' ⟹ v = s⇩2 ⟹ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒' ⟨Val va,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨throw e',s⇩2⟩ ⟹ 
    thesis"
  and "⋀E e s⇩0 e' s⇩1 Copt M es. x = E ⟹ y = Call e Copt M es ⟹
    z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 va s⇩1 es vs ex es' s⇩2 Copt M. x = E ⟹ y = Call e Copt M es ⟹
    z = s⇩0 ⟹ u = throw ex ⟹ v = s⇩2 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨Val va,s⇩1⟩ ⟹
    P,E ⊢ ⟨es,s⇩1⟩ [⇒'] ⟨map Val vs @ throw ex # es',s⇩2⟩ ⟹ thesis"
  and "⋀E e s⇩0 a Cs s⇩1 ps vs h⇩2 l⇩2 C S M Ts' T' pns' body' Ds Ts T pns body Cs' vs' l⇩2' new_body e'
    h⇩3 l⇩3. x = E ⟹ y = Call e None M ps ⟹ z = s⇩0 ⟹ u = e' ⟹ v = (h⇩3, l⇩2) ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),s⇩1⟩ ⟹ P,E ⊢ ⟨ps,s⇩1⟩ [⇒'] ⟨map Val vs,(h⇩2, l⇩2)⟩ ⟹
    h⇩2 a = ⌊(C, S)⌋ ⟹ P ⊢ last Cs has least M = (Ts', T', pns', body') via Ds ⟹
    P ⊢ (C,Cs @⇩p Ds) selects M = (Ts, T, pns, body) via Cs' ⟹ length vs = length pns ⟹
    P ⊢ Ts Casts vs to vs'  ⟹ l⇩2' = [this ↦ Ref (a, Cs'), pns [↦] vs'] ⟹
    new_body = (case T' of Class D ⇒ ⦇D⦈body | _ ⇒ body) ⟹
    P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ ⟨new_body,(h⇩2, l⇩2')⟩ ⇒' ⟨e',(h⇩3, l⇩3)⟩ ⟹
    thesis"
  and "⋀E e s⇩0 a Cs s⇩1 ps vs h⇩2 l⇩2 C Cs'' M Ts T pns body Cs' Ds vs' l⇩2' e' h⇩3 l⇩3.
    x = E ⟹ y = Call e ⌊C⌋ M ps ⟹ z = s⇩0 ⟹ u = e' ⟹ v = (h⇩3, l⇩2) ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref (a, Cs),s⇩1⟩ ⟹ P,E ⊢ ⟨ps,s⇩1⟩ [⇒'] ⟨map Val vs,(h⇩2, l⇩2)⟩ ⟹
    P ⊢ Path last Cs to C unique ⟹ P ⊢ Path last Cs to C via Cs''  ⟹
    P ⊢ C has least M = (Ts, T, pns, body) via Cs' ⟹ Ds = (Cs @⇩p Cs'') @⇩p Cs' ⟹
    length vs = length pns ⟹ P ⊢ Ts Casts vs to vs'  ⟹
    l⇩2' = [this ↦ Ref (a, Ds), pns [↦] vs'] ⟹
    P,E(this ↦ Class (last Ds), pns [↦] Ts) ⊢ ⟨body,(h⇩2, l⇩2')⟩ ⇒' ⟨e',(h⇩3, l⇩3)⟩ ⟹
    thesis"
  and "⋀E e s⇩0 s⇩1 es vs s⇩2 Copt M. x = E ⟹ y = Call e Copt M es ⟹ z = s⇩0 ⟹
    u = Throw (addr_of_sys_xcpt NullPointer, [NullPointer]) ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ P,E ⊢ ⟨es,s⇩1⟩ [⇒'] ⟨map Val vs,s⇩2⟩ ⟹ thesis"
  and "⋀E V T e⇩0 h⇩0 l⇩0 e⇩1 h⇩1 l⇩1.
    x = E ⟹ y = {V:T; e⇩0} ⟹ z = (h⇩0, l⇩0) ⟹ u = e⇩1 ⟹
    v = (h⇩1, l⇩1(V := l⇩0 V)) ⟹ P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0, l⇩0(V := None))⟩ ⇒' ⟨e⇩1,(h⇩1, l⇩1)⟩ ⟹ thesis"
  and "⋀E e⇩0 s⇩0 va s⇩1 e⇩1 e⇩2 s⇩2. x = E ⟹ y = e⇩0;; e⇩1 ⟹ z = s⇩0 ⟹ u = e⇩2 ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒' ⟨Val va,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒' ⟨e⇩2,s⇩2⟩ ⟹ thesis"
  and "⋀E e⇩0 s⇩0 e s⇩1 e⇩1. x = E ⟹ y = e⇩0;; e⇩1 ⟹ z = s⇩0 ⟹ u = throw e ⟹ v = s⇩1 ⟹
    P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒' ⟨throw e,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 e⇩1 e' s⇩2 e⇩2. x = E ⟹ y = if (e) e⇩1 else e⇩2 ⟹ z = s⇩0 ⟹ u = e' ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒' ⟨e',s⇩2⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 e⇩2 e' s⇩2 e⇩1. x = E ⟹ y = if (e) e⇩1 else e⇩2 ⟹ z = s⇩0 ⟹
    u = e' ⟹ v = s⇩2 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨false,s⇩1⟩ ⟹ P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒' ⟨e',s⇩2⟩ ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 e⇩1 e⇩2. x = E ⟹ y = if (e) e⇩1 else e⇩2 ⟹
    z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 c. x = E ⟹ y = while (e) c ⟹ z = s⇩0 ⟹ u = unit ⟹ v = s⇩1 ⟹
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨false,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 c v⇩1 s⇩2 e⇩3 s⇩3. x = E ⟹ y = while (e) c ⟹ z = s⇩0 ⟹ u = e⇩3 ⟹
    v = s⇩3 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩ ⟹ P,E ⊢ ⟨c,s⇩1⟩ ⇒' ⟨Val v⇩1,s⇩2⟩ ⟹
    P,E ⊢ ⟨while (e) c,s⇩2⟩ ⇒' ⟨e⇩3,s⇩3⟩ ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1 c. x = E ⟹ y = while (e) c ⟹ z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹ 
    P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1 c e' s⇩2. x = E ⟹ y = while (e) c ⟹ z = s⇩0 ⟹ u = throw e' ⟹
    v = s⇩2 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨true,s⇩1⟩ ⟹ P,E ⊢ ⟨c,s⇩1⟩ ⇒' ⟨throw e',s⇩2⟩ ⟹ thesis"
  and "⋀E e s⇩0 r s⇩1. x = E ⟹ y = throw e ⟹
    z = s⇩0 ⟹ u = Throw r ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨ref r,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 s⇩1. x = E ⟹ y = throw e ⟹ z = s⇩0 ⟹
    u = Throw (addr_of_sys_xcpt NullPointer, [NullPointer]) ⟹
    v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨null,s⇩1⟩ ⟹ thesis"
  and "⋀E e s⇩0 e' s⇩1. x = E ⟹ y = throw e ⟹
    z = s⇩0 ⟹ u = throw e' ⟹ v = s⇩1 ⟹ P,E ⊢ ⟨e,s⇩0⟩ ⇒' ⟨throw e',s⇩1⟩ ⟹ thesis"
  shows thesis
using assms
by(transfer)(erule eval.cases, unfold blank_def, assumption+)

lemmas [code_pred_intro] = New' NewFail' StaticUpCast'
declare StaticDownCast'_new[code_pred_intro StaticDownCast']
lemmas [code_pred_intro] = StaticCastNull'
declare StaticCastFail'_new[code_pred_intro StaticCastFail']
lemmas [code_pred_intro] = StaticCastThrow' StaticUpDynCast'
declare
  StaticDownDynCast'_new[code_pred_intro StaticDownDynCast']
  DynCast'[code_pred_intro DynCast']
lemmas [code_pred_intro] = DynCastNull'
declare DynCastFail'[code_pred_intro DynCastFail']
lemmas [code_pred_intro] = DynCastThrow' Val' BinOp' BinOpThrow1'
declare BinOpThrow2'[code_pred_intro BinOpThrow2']
lemmas [code_pred_intro] = Var' LAss' LAssThrow'
declare FAcc'_new[code_pred_intro FAcc']
lemmas [code_pred_intro] = FAccNull' FAccThrow'
declare FAss'_new[code_pred_intro FAss']
lemmas [code_pred_intro] = FAssNull' FAssThrow1'
declare FAssThrow2'[code_pred_intro FAssThrow2']
lemmas [code_pred_intro] = CallObjThrow'
declare
  CallParamsThrow'_new[code_pred_intro CallParamsThrow']
  Call'_new[code_pred_intro Call']
  StaticCall'_new[code_pred_intro StaticCall']
  CallNull'_new[code_pred_intro CallNull']
lemmas [code_pred_intro] = Block' Seq'
declare SeqThrow'[code_pred_intro SeqThrow']
lemmas [code_pred_intro] = CondT'
declare 
  CondF'[code_pred_intro CondF']
  CondThrow'[code_pred_intro CondThrow']
lemmas [code_pred_intro] = WhileF' WhileT'
declare
  WhileCondThrow'[code_pred_intro WhileCondThrow']
  WhileBodyThrow'[code_pred_intro WhileBodyThrow']
lemmas [code_pred_intro] = Throw'
declare ThrowNull'[code_pred_intro ThrowNull']
lemmas [code_pred_intro] = ThrowThrow'
lemmas [code_pred_intro] = Nil' Cons' ConsThrow'

code_pred 
  (modes: eval': i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool as big_step
   and evals': i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool as big_steps)
  eval'
proof -
  case eval'
  from eval'.prems show thesis
  proof(cases (no_simp) rule: eval'_cases)
    case (StaticDownCast E C e s⇩0 a Cs Cs' s⇩1)
    moreover
    have "app a [Cs] (a @ [Cs])" "app (a @ [Cs]) Cs' (a @ [Cs] @ Cs')"
      by(simp_all add: app_eq)
    ultimately show ?thesis by(rule eval'.StaticDownCast'[OF refl])
  next
    case StaticCastFail thus ?thesis
      unfolding rtrancl_def subcls1_def mem_Collect_eq prod.case
      by(rule eval'.StaticCastFail'[OF refl])
  next
    case (StaticDownDynCast E e s⇩0 a Cs C Cs' s⇩1)
    moreover have "app Cs [C] (Cs @ [C])" "app (Cs @ [C]) Cs' (Cs @ [C] @ Cs')"
      by(simp_all add: app_eq)
    ultimately show thesis by(rule eval'.StaticDownDynCast'[OF refl])
  next
    case DynCast thus ?thesis by(rule eval'.DynCast'[OF refl])
  next
    case DynCastFail thus ?thesis by(rule eval'.DynCastFail'[OF refl])
  next
    case BinOpThrow2 thus ?thesis by(rule eval'.BinOpThrow2'[OF refl])
  next
    case FAcc thus ?thesis
      by(rule eval'.FAcc'[OF refl, unfolded Predicate_Compile.contains_def Set_project_def mem_Collect_eq])
  next
    case FAss thus ?thesis
      by(rule eval'.FAss'[OF refl, unfolded Predicate_Compile.contains_def Set_project_def mem_Collect_eq])
  next
    case FAssThrow2 thus ?thesis by(rule eval'.FAssThrow2'[OF refl])
  next
    case (CallParamsThrow E e s⇩0 v s⇩1 es vs ex es' s⇩2 Copt M)
    moreover have "map_val2 (map Val vs @ throw ex # es') vs (throw ex # es')"
      by(simp add: map_val2_conv[symmetric])
    ultimately show ?thesis by(rule eval'.CallParamsThrow'[OF refl])
  next
    case (Call E e s⇩0 a Cs s⇩1 ps vs)
    moreover have "map_val (map Val vs) vs" by(simp add: map_val_conv[symmetric])
    ultimately show ?thesis by-(rule eval'.Call'[OF refl])
  next
    case (StaticCall E e s⇩0 a Cs s⇩1 ps vs)
    moreover have "map_val (map Val vs) vs" by(simp add: map_val_conv[symmetric])
    ultimately show ?thesis by-(rule eval'.StaticCall'[OF refl])
  next
    case (CallNull E e s⇩0 s⇩1 es vs)
    moreover have "map_val (map Val vs) vs" by(simp add: map_val_conv[symmetric])
    ultimately show ?thesis by-(rule eval'.CallNull'[OF refl])
  next
    case SeqThrow thus ?thesis by(rule eval'.SeqThrow'[OF refl])
  next
    case CondF thus ?thesis by(rule eval'.CondF'[OF refl])
  next
    case CondThrow thus ?thesis by(rule eval'.CondThrow'[OF refl])
  next
    case WhileCondThrow thus ?thesis by(rule eval'.WhileCondThrow'[OF refl])
  next
    case WhileBodyThrow thus ?thesis by(rule eval'.WhileBodyThrow'[OF refl])
  next
    case ThrowNull thus ?thesis by(rule eval'.ThrowNull'[OF refl])
  qed(assumption|erule (4) eval'.that[OF refl])+
next
  case evals'
  from evals'.prems evals'.that[OF refl]
  show thesis by transfer(erule evals.cases)
qed

subsection ‹Examples›

declare [[values_timeout = 180]]

values [expected "{Val (Intg 5)}"]
  "{fst (e', s') | e' s'. 
    [],Map.empty ⊢ ⟨{''V'':Integer; ''V'' :=  Val(Intg 5);; Var ''V''},(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 11)}"]
  "{fst (e', s') | e' s'. 
    [],Map.empty ⊢ ⟨(Val(Intg 5)) «Add» (Val(Intg 6)),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 83)}"]
  "{fst (e', s') | e' s'. 
    [],[''V''↦Integer] ⊢ ⟨(Var ''V'') «Add» (Val(Intg 6)),
                                       (Map.empty,[''V''↦Intg 77])⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Some (Intg 6)}"]
  "{lcl' (snd (e', s')) ''V''  | e' s'. 
    [],[''V''↦Integer] ⊢ ⟨''V'' := Val(Intg 6),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Some (Intg 12)}"]
  "{lcl' (snd (e', s')) ''mult''  | e' s'. 
    [],[''V''↦Integer,''a''↦Integer,''b''↦Integer,''mult''↦Integer]
    ⊢ ⟨(''a'' := Val(Intg 3));;(''b'' := Val(Intg 4));;(''mult'' := Val(Intg 0));;
       (''V'' := Val(Intg 1));;
       while (Var ''V'' «Eq» Val(Intg 1))((''mult'' := Var ''mult'' «Add» Var ''b'');;
         (''a'' := Var ''a'' «Add» Val(Intg (- 1)));;
         (''V'' := (if(Var ''a'' «Eq» Val(Intg 0)) Val(Intg 0) else Val(Intg 1)))),
       (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 30)}"]
  "{fst (e', s') | e' s'. 
    [],[''a''↦Integer, ''b''↦Integer, ''c''↦ Integer, ''cond''↦Boolean]
    ⊢ ⟨''a'' := Val(Intg 17);; ''b'' := Val(Intg 13);; 
       ''c'' := Val(Intg 42);; ''cond'' := true;; 
       if (Var ''cond'') (Var ''a'' «Add» Var ''b'') else (Var ''a'' «Add» Var ''c''),
       (Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"


text ‹progOverrider examples›

definition
  classBottom :: "cdecl" where
  "classBottom = (''Bottom'', [Repeats ''Left'', Repeats ''Right''],
                   [(''x'',Integer)],[])" 

definition
  classLeft :: "cdecl" where
  "classLeft = (''Left'', [Repeats ''Top''],[],[(''f'', [Class ''Top'', Integer],Integer, [''V'',''W''],Var this ∙ ''x'' {[''Left'',''Top'']} «Add» Val (Intg 5))])"

definition
  classRight :: "cdecl" where
  "classRight = (''Right'', [Shares ''Right2''],[],
    [(''f'', [Class ''Top'', Integer], Integer,[''V'',''W''],Var this ∙ ''x'' {[''Right2'',''Top'']} «Add» Val (Intg 7)),(''g'',[],Class ''Left'',[],new ''Left'')])"

definition
  classRight2 :: "cdecl" where
  "classRight2 = (''Right2'', [Repeats ''Top''],[],
    [(''f'', [Class ''Top'', Integer], Integer,[''V'',''W''],Var this ∙ ''x'' {[''Right2'',''Top'']} «Add» Val (Intg 9)),(''g'',[],Class ''Top'',[],new ''Top'')])"

definition
  classTop :: "cdecl" where
  "classTop = (''Top'', [], [(''x'',Integer)],[])"

definition
  progOverrider :: "cdecl list" where
  "progOverrider = [classBottom, classLeft, classRight, classRight2, classTop]"

values [expected "{Val(Ref(0,[''Bottom'',''Left'']))}"] ― ‹dynCastSide›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right''] ⊢
    ⟨''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Ref(0,[''Right'']))}"] ― ‹dynCastViaSh›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right2''] ⊢ 
    ⟨''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 42)}"] ― ‹block›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Integer] 
    ⊢ ⟨''V'' := Val(Intg 42) ;; {''V'':Class ''Left''; ''V'' := new ''Bottom''} ;; Var ''V'',
      (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 8)}"] ― ‹staticCall›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right'',''W''↦Class ''Bottom''] 
    ⊢ ⟨''V'' := new ''Bottom'' ;; ''W'' := new ''Bottom'' ;; 
       ((Cast ''Left'' (Var ''W''))∙''x''{[''Left'',''Top'']} := Val(Intg 3));;
       (Var ''W''∙(''Left''::)''f''([Var ''V'',Val(Intg 2)])),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val (Intg 12)}"] ― ‹call›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right2'',''W''↦Class ''Left''] 
    ⊢ ⟨''V'' := new ''Right'' ;; ''W'' := new ''Left'' ;; 
       (Var ''V''∙''f''([Var ''W'',Val(Intg 42)])) «Add» (Var ''W''∙''f''([Var ''V'',Val(Intg 13)])),
       (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Intg 13)}"] ― ‹callOverrider›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right2'',''W''↦Class ''Left''] 
    ⊢ ⟨''V'' := new ''Bottom'';; (Var ''V'' ∙ ''x'' {[''Right2'',''Top'']} := Val(Intg 6));; 
       ''W'' := new ''Left'' ;; Var ''V''∙''f''([Var ''W'',Val(Intg 42)]),
       (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Ref(1,[''Left'',''Top'']))}"] ― ‹callClass›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right2''] 
    ⊢ ⟨''V'' := new ''Right'' ;; Var ''V''∙''g''([]),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Intg 42)}"] ― ‹fieldAss›
  "{fst (e', s') | e' s'. 
    progOverrider,[''V''↦Class ''Right2''] 
    ⊢ ⟨''V'' := new ''Right'' ;; 
       (Var ''V''∙''x''{[''Right2'',''Top'']} := (Val(Intg 42))) ;; 
       (Var ''V''∙''x''{[''Right2'',''Top'']}),(Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"


text ‹typing rules›

values [expected "{Class ''Bottom''}"] ― ‹typeNew›
  "{T. progOverrider,Map.empty ⊢ new ''Bottom'' :: T}"

values [expected "{Class ''Left''}"] ― ‹typeDynCast›
  "{T. progOverrider,Map.empty ⊢ Cast ''Left'' (new ''Bottom'') :: T}"

values [expected "{Class ''Left''}"] ― ‹typeStaticCast›
  "{T. progOverrider,Map.empty ⊢ ⦇''Left''⦈ (new ''Bottom'') :: T}"

values [expected "{Integer}"] ― ‹typeVal›
  "{T. [],Map.empty ⊢ Val(Intg 17) :: T}"

values [expected "{Integer}"] ― ‹typeVar›
  "{T. [],[''V'' ↦ Integer] ⊢ Var ''V'' :: T}"

values [expected "{Boolean}"] ― ‹typeBinOp›
  "{T. [],Map.empty ⊢ (Val(Intg 5)) «Eq» (Val(Intg 6)) :: T}"

values [expected "{Class ''Top''}"] ― ‹typeLAss›
  "{T. progOverrider,[''V'' ↦ Class ''Top''] ⊢ ''V'' := (new ''Left'') :: T}"

values [expected "{Integer}"] ― ‹typeFAcc›
  "{T. progOverrider,Map.empty ⊢ (new ''Right'')∙''x''{[''Right2'',''Top'']} :: T}"

values [expected "{Integer}"] ― ‹typeFAss›
  "{T. progOverrider,Map.empty ⊢ (new ''Right'')∙''x''{[''Right2'',''Top'']} :: T}"

values [expected "{Integer}"] ― ‹typeStaticCall›
  "{T. progOverrider,[''V''↦Class ''Left''] 
       ⊢ ''V'' := new ''Left'' ;; Var ''V''∙(''Left''::)''f''([new ''Top'', Val(Intg 13)]) :: T}"

values [expected "{Class ''Top''}"] ― ‹typeCall›
  "{T. progOverrider,[''V''↦Class ''Right2''] 
       ⊢ ''V'' := new ''Right'' ;; Var ''V''∙''g''([]) :: T}"

values [expected "{Class ''Top''}"] ― ‹typeBlock›
  "{T. progOverrider,Map.empty ⊢ {''V'':Class ''Top''; ''V'' := new ''Left''} :: T}"

values [expected "{Integer}"] ― ‹typeCond›
  "{T. [],Map.empty ⊢ if (true) Val(Intg 6) else Val(Intg 9) :: T}"

values [expected "{Void}"] ― ‹typeWhile›
  "{T. [],Map.empty ⊢ while (false) Val(Intg 17) :: T}"

values [expected "{Void}"] ― ‹typeThrow›
  "{T. progOverrider,Map.empty ⊢ throw (new ''Bottom'') :: T}"

values [expected "{Integer}"] ― ‹typeBig›
  "{T. progOverrider,[''V''↦Class ''Right2'',''W''↦Class ''Left''] 
       ⊢ ''V'' := new ''Right'' ;; ''W'' := new ''Left'' ;; 
         (Var ''V''∙''f''([Var ''W'', Val(Intg 7)])) «Add» (Var ''W''∙''f''([Var ''V'', Val(Intg 13)])) 
       :: T}"


text ‹progDiamond examples›

definition
  classDiamondBottom :: "cdecl" where
  "classDiamondBottom = (''Bottom'', [Repeats ''Left'', Repeats ''Right''],[(''x'',Integer)],
    [(''g'', [],Integer, [],Var this ∙ ''x'' {[''Bottom'']} «Add» Val (Intg 5))])" 

definition
  classDiamondLeft :: "cdecl" where
  "classDiamondLeft = (''Left'', [Repeats ''TopRep'',Shares ''TopSh''],[],[])"

definition
  classDiamondRight :: "cdecl" where
  "classDiamondRight = (''Right'', [Repeats ''TopRep'',Shares ''TopSh''],[],
    [(''f'', [Integer], Boolean,[''i''], Var ''i'' «Eq» Val (Intg 7))])"

definition
  classDiamondTopRep :: "cdecl" where
  "classDiamondTopRep = (''TopRep'', [], [(''x'',Integer)],
    [(''g'', [],Integer, [], Var this ∙ ''x'' {[''TopRep'']} «Add» Val (Intg 10))])"

definition
  classDiamondTopSh :: "cdecl" where
  "classDiamondTopSh = (''TopSh'', [], [], 
    [(''f'', [Integer], Boolean,[''i''], Var ''i'' «Eq» Val (Intg 3))])"

definition
  progDiamond :: "cdecl list" where
  "progDiamond = [classDiamondBottom, classDiamondLeft, classDiamondRight, classDiamondTopRep, classDiamondTopSh]"

values [expected "{Val(Ref(0,[''Bottom'',''Left'']))}"] ― ‹cast1›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''Left''] ⊢ ⟨''V'' := new ''Bottom'',
                                                      (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Ref(0,[''TopSh'']))}"] ― ‹cast2›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''TopSh''] ⊢ ⟨''V'' := new ''Bottom'',
                                                      (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{}"] ― ‹typeCast3 not typeable›
  "{T. progDiamond,[''V''↦Class ''TopRep''] ⊢ ''V'' := new ''Bottom'' :: T}"

values [expected "{
   Val(Ref(0,[''Bottom'', ''Left'', ''TopRep''])), 
   Val(Ref(0,[''Bottom'', ''Right'', ''TopRep'']))
  }"] ― ‹cast3›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''TopRep''] ⊢ ⟨''V'' := new ''Bottom'', 
                                                      (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

values [expected "{Val(Intg 17)}"] ― ‹fieldAss›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''Bottom''] 
    ⊢ ⟨''V'' := new ''Bottom'' ;; 
       ((Var ''V'')∙''x''{[''Bottom'']} := (Val(Intg 17))) ;; 
       ((Var ''V'')∙''x''{[''Bottom'']}),(Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"

values [expected "{Val Null}"] ― ‹dynCastNull›
  "{fst (e', s') | e' s'. 
    progDiamond,Map.empty ⊢ ⟨Cast ''Right'' null,(Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"

values [expected "{Val (Ref(0, [''Right'']))}"] ― ‹dynCastViaSh›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''TopSh''] 
    ⊢ ⟨''V'' := new ''Right'' ;; Cast ''Right'' (Var ''V''),(Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"

values [expected "{Val Null}"] ― ‹dynCastFail›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''TopRep''] 
    ⊢ ⟨''V'' := new ''Right'' ;; Cast ''Bottom'' (Var ''V''),(Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"

values [expected "{Val (Ref(0, [''Bottom'', ''Left'']))}"] ― ‹dynCastSide›
  "{fst (e', s') | e' s'. 
    progDiamond,[''V''↦Class ''Right'']
    ⊢ ⟨''V'' := new ''Bottom'' ;; Cast ''Left'' (Var ''V''),(Map.empty,Map.empty)⟩ ⇒' ⟨e',s'⟩}"

text ‹failing g++ example›

definition
  classD :: "cdecl" where
  "classD = (''D'', [Shares ''A'', Shares ''B'', Repeats ''C''],[],[])"

definition
  classC :: "cdecl" where
  "classC = (''C'', [Shares ''A'', Shares ''B''],[],
              [(''f'',[],Integer,[],Val(Intg 42))])"

definition
  classB :: "cdecl" where
  "classB = (''B'', [],[],
              [(''f'',[],Integer,[],Val(Intg 17))])"

definition
  classA :: "cdecl" where
  "classA = (''A'', [],[],
              [(''f'',[],Integer,[],Val(Intg 13))])"

definition
  ProgFailing :: "cdecl list" where
  "ProgFailing = [classA,classB,classC,classD]"

values [expected "{Val (Intg 42)}"] ― ‹callFailGplusplus›
  "{fst (e', s') | e' s'. 
    ProgFailing,Map.empty 
    ⊢ ⟨{''V'':Class ''D''; ''V'' := new ''D'';; Var ''V''∙''f''([])},
       (Map.empty,Map.empty)⟩ ⇒' ⟨e', s'⟩}"

end