Session Jinja

Theory Auxiliary

(*  Title:      Jinja/Common/Basis.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 TU Muenchen
*)

chapter ‹Jinja Source Language \label{cha:j}›

section ‹Auxiliary Definitions›

theory Auxiliary imports Main begin
(* FIXME move and possibly turn into a general simproc *)
lemma nat_add_max_le[simp]:
  "((n::nat) + max i j  m) = (n + i  m  n + j  m)"
 (*<*)by arith(*>*)

lemma Suc_add_max_le[simp]:
  "(Suc(n + max i j)  m) = (Suc(n + i)  m  Suc(n + j)  m)"
(*<*)by arith(*>*)


notation Some  ("(_)")

(*<*)
declare
 option.splits[split]
 Let_def[simp]
 subset_insertI2 [simp]
 Cons_eq_map_conv [iff]
(*>*)


subsection distinct_fst›
 
definition distinct_fst  :: "('a × 'b) list  bool"
where
  "distinct_fst    distinct  map fst"

lemma distinct_fst_Nil [simp]:
  "distinct_fst []"
 (*<*)
apply (unfold distinct_fst_def)
apply (simp (no_asm))
done
(*>*)

lemma distinct_fst_Cons [simp]:
  "distinct_fst ((k,x)#kxs) = (distinct_fst kxs  (y. (k,y)  set kxs))"
(*<*)
apply (unfold distinct_fst_def)
apply (auto simp:image_def)
done
(*>*)
(*
lemma distinct_fst_append:
 "⟦ distinct_fst kxs'; distinct_fst kxs; ∀(k,x) ∈ set kxs. ∀(k',x') ∈ set kxs'. k' ≠ k ⟧
  ⟹ distinct_fst(kxs @ kxs')"
by (induct kxs) (auto dest: fst_in_set_lemma)

lemma distinct_fst_map_inj:
  "⟦ distinct_fst kxs; inj f ⟧ ⟹ distinct_fst (map (λ(k,x). (f k, g k x)) kxs)"
by (induct kxs) (auto dest: fst_in_set_lemma simp: inj_eq)
*)

lemma map_of_SomeI:
  " distinct_fst kxs; (k,x)  set kxs   map_of kxs k = Some x"
(*<*)by (induct kxs) (auto simp:fun_upd_apply)(*>*)


subsection ‹Using @{term list_all2} for relations›

definition fun_of :: "('a × 'b) set  'a  'b  bool"
where
  "fun_of S  λx y. (x,y)  S"

text ‹Convenience lemmas›
(*<*)
declare fun_of_def [simp]
(*>*)
lemma rel_list_all2_Cons [iff]:
  "list_all2 (fun_of S) (x#xs) (y#ys) = 
   ((x,y)  S  list_all2 (fun_of S) xs ys)"
  (*<*)by simp(*>*)

lemma rel_list_all2_Cons1:
  "list_all2 (fun_of S) (x#xs) ys = 
  (z zs. ys = z#zs  (x,z)  S  list_all2 (fun_of S) xs zs)"
  (*<*)by (cases ys) auto(*>*)

lemma rel_list_all2_Cons2:
  "list_all2 (fun_of S) xs (y#ys) = 
  (z zs. xs = z#zs  (z,y)  S  list_all2 (fun_of S) zs ys)"
  (*<*)by (cases xs) auto(*>*)

lemma rel_list_all2_refl:
  "(x. (x,x)  S)  list_all2 (fun_of S) xs xs"
  (*<*)by (simp add: list_all2_refl)(*>*)

lemma rel_list_all2_antisym:
  " (x y. (x,y)  S; (y,x)  T  x = y); 
     list_all2 (fun_of S) xs ys; list_all2 (fun_of T) ys xs   xs = ys"
  (*<*)by (rule list_all2_antisym) auto(*>*)

lemma rel_list_all2_trans: 
  " a b c. (a,b)  R; (b,c)  S  (a,c)  T;
    list_all2 (fun_of R) as bs; list_all2 (fun_of S) bs cs 
   list_all2 (fun_of T) as cs"
  (*<*)by (rule list_all2_trans) auto(*>*)

lemma rel_list_all2_update_cong:
  " i<size xs; list_all2 (fun_of S) xs ys; (x,y)  S  
   list_all2 (fun_of S) (xs[i:=x]) (ys[i:=y])"
  (*<*)by (simp add: list_all2_update_cong)(*>*)

lemma rel_list_all2_nthD:
  " list_all2 (fun_of S) xs ys; p < size xs   (xs!p,ys!p)  S"
  (*<*)by (drule list_all2_nthD) auto(*>*)

lemma rel_list_all2I:
  " length a = length b; n. n < length a  (a!n,b!n)  S   list_all2 (fun_of S) a b"
  (*<*)by (erule list_all2_all_nthI) simp(*>*)

(*<*)declare fun_of_def [simp del](*>*)

end

Theory Type

(*  Title:      Jinja/Common/Type.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Jinja types›

theory Type imports Auxiliary begin

type_synonym cname = string ― ‹class names›
type_synonym mname = string ― ‹method name›
type_synonym vname = string ― ‹names for local/field variables›

definition Object :: cname
where
  "Object  ''Object''"

definition this :: vname
where
  "this  ''this''"

― ‹types›
datatype ty
  = Void          ― ‹type of statements›
  | Boolean
  | Integer
  | NT            ― ‹null type›
  | Class cname   ― ‹class type›

definition is_refT :: "ty  bool"
where
  "is_refT T    T = NT  (C. T = Class C)"

lemma [iff]: "is_refT NT"
(*<*)by(simp add:is_refT_def)(*>*)

lemma [iff]: "is_refT(Class C)"
(*<*)by(simp add:is_refT_def)(*>*)

lemma refTE:
  "is_refT T; T = NT  P; C. T = Class C  P   P"
(*<*)by (auto simp add: is_refT_def)(*>*)

lemma not_refTE:
  " ¬is_refT T; T = Void  T = Boolean  T = Integer  P   P"
(*<*)by (cases T, auto simp add: is_refT_def)(*>*)

end

Theory Decl

(*  Title:      HOL/MicroJava/J/Decl.thy

    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Class Declarations and Programs›

theory Decl imports Type begin

type_synonym 
  fdecl    = "vname × ty"        ― ‹field declaration›
type_synonym
  'm mdecl = "mname × ty list × ty × 'm"     ― ‹method = name, arg.\ types, return type, body›
type_synonym
  'm "class" = "cname × fdecl list × 'm mdecl list"       ― ‹class = superclass, fields, methods›
type_synonym
  'm cdecl = "cname × 'm class"  ― ‹class declaration›
type_synonym
  'm prog  = "'m cdecl list"     ― ‹program›

(*<*)
translations
  (type) "fdecl"   <= (type) "vname × ty"
  (type) "'c mdecl" <= (type) "mname × ty list × ty × 'c"
  (type) "'c class" <= (type) "cname × fdecl list × ('c mdecl) list"
  (type) "'c cdecl" <= (type) "cname × ('c class)"
  (type) "'c prog" <= (type) "('c cdecl) list"
(*>*)

definition "class" :: "'m prog  cname  'm class"
where
  "class    map_of"

definition is_class :: "'m prog  cname  bool"
where
  "is_class P C    class P C  None"

lemma finite_is_class: "finite {C. is_class P C}"

(*<*)
apply (unfold is_class_def class_def)
apply (fold dom_def)
apply (rule finite_dom_map_of)
done
(*>*)

definition is_type :: "'m prog  ty  bool"
where
  "is_type P T  
  (case T of Void  True | Boolean  True | Integer  True | NT  True
   | Class C  is_class P C)"

lemma is_type_simps [simp]:
  "is_type P Void  is_type P Boolean  is_type P Integer 
  is_type P NT  is_type P (Class C) = is_class P C"
(*<*)by(simp add:is_type_def)(*>*)


abbreviation
  "types P == Collect (is_type P)"

end

Theory TypeRel

(*  Title:      Jinja/Common/TypeRel.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Relations between Jinja Types›

theory TypeRel imports 
  "HOL-Library.Transitive_Closure_Table"
  Decl 
begin

subsection‹The subclass relations›

inductive_set
  subcls1 :: "'m prog  (cname × cname) set"
  and subcls1' :: "'m prog  [cname, cname]  bool" ("_  _ 1 _" [71,71,71] 70)
  for P :: "'m prog"
where
  "P  C  1 D  (C,D)  subcls1 P"
| subcls1I: "class P C = Some (D,rest); C  Object  P  C 1 D"

abbreviation
  subcls  :: "'m prog  [cname, cname]  bool" ("_  _ * _"  [71,71,71] 70)
  where "P  C  *  D  (C,D)  (subcls1 P)*"

lemma subcls1D: "P  C 1 D  C  Object  (fs ms. class P C = Some (D,fs,ms))"
(*<*)by(erule subcls1.induct)(fastforce simp add:is_class_def)(*>*)

lemma [iff]: "¬ P  Object 1 C"
(*<*)by(fastforce dest:subcls1D)(*>*)

lemma [iff]: "(P  Object * C) = (C = Object)"
(*<*)
apply(rule iffI)
 apply(erule converse_rtranclE)
  apply simp_all
done
(*>*)

lemma subcls1_def2:
  "subcls1 P =
     (SIGMA C:{C. is_class P C}. {D. CObject  fst (the (class P C))=D})"
(*<*)
  by (fastforce simp:is_class_def dest: subcls1D elim: subcls1I)
(*>*)

lemma finite_subcls1: "finite (subcls1 P)"
(*<*)
apply (simp add: subcls1_def2)
apply(rule finite_SigmaI [OF finite_is_class])
apply(rule_tac B = "{fst (the (class P C))}" in finite_subset)
apply  auto
done
(*>*)
(*
lemma subcls_is_class: "(C,D) ∈ (subcls1 P)+ ⟹ is_class P C"
apply (unfold is_class_def)
apply(erule trancl_trans_induct)
apply (auto dest!: subcls1D)
done

lemma subcls_is_class: "P ⊢ C ≼* D ⟹ is_class P D ⟶ is_class P C"
apply (unfold is_class_def)
apply (erule rtrancl_induct)
apply  (drule_tac [2] subcls1D)
apply  auto
done
*)


subsection‹The subtype relations›

inductive
  widen   :: "'m prog  ty  ty  bool" ("_  _  _"   [71,71,71] 70)
  for P :: "'m prog"
where
  widen_refl[iff]: "P  T  T"
| widen_subcls: "P  C * D    P  Class C  Class D"
| widen_null[iff]: "P  NT  Class C"

abbreviation
  widens :: "'m prog  ty list  ty list  bool"
    ("_  _ [≤] _" [71,71,71] 70) where
  "widens P Ts Ts'  list_all2 (widen P) Ts Ts'"

lemma [iff]: "(P  T  Void) = (T = Void)"
(*<*)by (auto elim: widen.cases)(*>*)

lemma [iff]: "(P  T  Boolean) = (T = Boolean)"
(*<*)by (auto elim: widen.cases)(*>*)

lemma [iff]: "(P  T  Integer) = (T = Integer)"
(*<*)by (auto elim: widen.cases)(*>*)

lemma [iff]: "(P  Void  T) = (T = Void)"
(*<*)by (auto elim: widen.cases)(*>*)

lemma [iff]: "(P  Boolean  T) = (T = Boolean)"
(*<*)by (auto elim: widen.cases)(*>*)

lemma [iff]: "(P  Integer  T) = (T = Integer)"
(*<*)by (auto elim: widen.cases)(*>*)


lemma Class_widen: "P  Class C  T    D. T = Class D"
(*<*)
apply (ind_cases "P  Class C  T")
apply auto
done
(*>*)

lemma [iff]: "(P  T  NT) = (T = NT)"
(*<*)
apply(cases T)
apply(auto dest:Class_widen)
done
(*>*)

lemma Class_widen_Class [iff]: "(P  Class C  Class D) = (P  C * D)"
(*<*)
apply (rule iffI)
apply (ind_cases "P  Class C  Class D")
apply (auto elim: widen_subcls)
done
(*>*)

lemma widen_Class: "(P  T  Class C) = (T = NT  (D. T = Class D  P  D * C))"
(*<*)by(induct T, auto)(*>*)


lemma widen_trans[trans]: "P  S  U; P  U  T  P  S  T"
(*<*)
proof -
  assume "PS  U" thus "T. P  U  T  P  S  T"
  proof induct
    case (widen_refl T T') thus "P  T  T'" .
  next
    case (widen_subcls C D T)
    then obtain E where "T = Class E" by (blast dest: Class_widen)
    with widen_subcls show "P  Class C  T" by (auto elim: rtrancl_trans)
  next
    case (widen_null C RT)
    then obtain D where "RT = Class D" by (blast dest: Class_widen)
    thus "P  NT  RT" by auto
  qed
qed
(*>*)

lemma widens_trans [trans]: "P  Ss [≤] Ts; P  Ts [≤] Us  P  Ss [≤] Us"
(*<*)by (rule list_all2_trans, rule widen_trans)(*>*)


(*<*)
lemmas widens_refl [iff] = list_all2_refl [of "widen P", OF widen_refl] for P
lemmas widens_Cons [iff] = list_all2_Cons1 [of "widen P"] for P
(*>*)


subsection‹Method lookup›

inductive
  Methods :: "['m prog, cname, mname  (ty list × ty × 'm) × cname]  bool"
                    ("_  _ sees'_methods _" [51,51,51] 50)
  for P :: "'m prog"
where
  sees_methods_Object:
 " class P Object = Some(D,fs,ms); Mm = map_option (λm. (m,Object))  map_of ms 
   P  Object sees_methods Mm"
| sees_methods_rec:
 " class P C = Some(D,fs,ms); C  Object; P  D sees_methods Mm;
    Mm' = Mm ++ (map_option (λm. (m,C))  map_of ms) 
   P  C sees_methods Mm'"

lemma sees_methods_fun:
assumes 1: "P  C sees_methods Mm"
shows "Mm'. P  C sees_methods Mm'  Mm' = Mm"
 (*<*)
using 1
proof induct
  case (sees_methods_rec C D fs ms Dres Cres Cres')
  have "class": "class P C = Some (D, fs, ms)"
   and notObj: "C  Object" and Dmethods: "P  D sees_methods Dres"
   and IH: "Dres'. P  D sees_methods Dres'  Dres' = Dres"
   and Cres: "Cres = Dres ++ (map_option (λm. (m,C))  map_of ms)"
   and Cmethods': "P  C sees_methods Cres'" by fact+
  from Cmethods' notObj "class" obtain Dres'
    where Dmethods': "P  D sees_methods Dres'"
     and Cres': "Cres' = Dres' ++ (map_option (λm. (m,C))  map_of ms)"
    by(auto elim: Methods.cases)
  from Cres Cres' IH[OF Dmethods'] show "Cres' = Cres" by simp
next
  case sees_methods_Object thus ?case by(auto elim: Methods.cases)
qed
(*>*)

lemma visible_methods_exist:
  "P  C sees_methods Mm  Mm M = Some(m,D) 
   (D' fs ms. class P D = Some(D',fs,ms)  map_of ms M = Some m)"
 (*<*)by(induct rule:Methods.induct) auto(*>*)

lemma sees_methods_decl_above:
assumes Csees: "P  C sees_methods Mm"
shows "Mm M = Some(m,D)  P  C * D"
 (*<*)
using Csees
proof induct
  case sees_methods_Object thus ?case by auto
next
  case sees_methods_rec thus ?case
    by(fastforce simp:map_option_case split:option.splits
                elim:converse_rtrancl_into_rtrancl[OF subcls1I])
qed
(*>*)

lemma sees_methods_idemp:
assumes Cmethods: "P  C sees_methods Mm"
shows "m D. Mm M = Some(m,D) 
              Mm'. (P  D sees_methods Mm')  Mm' M = Some(m,D)"
(*<*)
using Cmethods
proof induct
  case sees_methods_Object thus ?case
    by(fastforce dest: Methods.sees_methods_Object)
next
  case sees_methods_rec thus ?case
    by(fastforce split:option.splits dest: Methods.sees_methods_rec)
qed
(*>*)

(*FIXME something wrong with induct: need to attache [consumes 1]
directly to proof of thm, declare does not work. *)

lemma sees_methods_decl_mono:
assumes sub: "P  C' * C"
shows "P  C sees_methods Mm 
       Mm' Mm2. P  C' sees_methods Mm'  Mm' = Mm ++ Mm2 
                 (M m D. Mm2 M = Some(m,D)  P  D * C)"
(*<*)
      (is "_  Mm' Mm2. ?Q C' C Mm' Mm2")
using sub
proof (induct rule:converse_rtrancl_induct)
  assume "P  C sees_methods Mm"
  hence "?Q C C Mm Map.empty" by simp
  thus "Mm' Mm2. ?Q C C Mm' Mm2" by blast
next
  fix C'' C'
  assume sub1: "P  C'' 1 C'" and sub: "P  C' * C"
  and IH: "P  C sees_methods Mm 
           Mm' Mm2. P  C' sees_methods Mm' 
                Mm' = Mm ++ Mm2  (M m D. Mm2 M = Some(m,D)  P  D * C)"
  and Csees: "P  C sees_methods Mm"
  from IH[OF Csees] obtain Mm' Mm2 where C'sees: "P  C' sees_methods Mm'"
    and Mm': "Mm' = Mm ++ Mm2"
    and subC:"M m D. Mm2 M = Some(m,D)  P  D * C" by blast
  obtain fs ms where "class": "class P C'' = Some(C',fs,ms)" "C''  Object"
    using subcls1D[OF sub1] by blast
  let ?Mm3 = "map_option (λm. (m,C''))  map_of ms"
  have "P  C'' sees_methods (Mm ++ Mm2) ++ ?Mm3"
    using sees_methods_rec[OF "class" C'sees refl] Mm' by simp
  hence "?Q C'' C ((Mm ++ Mm2) ++ ?Mm3) (Mm2++?Mm3)"
    using converse_rtrancl_into_rtrancl[OF sub1 sub]
    by simp (simp add:map_add_def subC split:option.split)
  thus "Mm' Mm2. ?Q C'' C Mm' Mm2" by blast
qed
(*>*)


definition Method :: "'m prog  cname  mname  ty list  ty  'm  cname  bool"
            ("_  _ sees _: __ = _ in _" [51,51,51,51,51,51,51] 50)
where
  "P  C sees M: TsT = m in D  
  Mm. P  C sees_methods Mm  Mm M = Some((Ts,T,m),D)"

definition has_method :: "'m prog  cname  mname  bool" ("_  _ has _" [51,0,51] 50)
where
  "P  C has M  Ts T m D. P  C sees M:TsT = m in D"

lemma sees_method_fun:
  "P  C sees M:TST = m in D; P  C sees M:TS'T' = m' in D' 
    TS' = TS  T' = T  m' = m  D' = D"
 (*<*)by(fastforce dest: sees_methods_fun simp:Method_def)(*>*)

lemma sees_method_decl_above:
  "P  C sees M:TsT = m in D  P  C * D"
 (*<*)by(clarsimp simp:Method_def sees_methods_decl_above)(*>*)

lemma visible_method_exists:
  "P  C sees M:TsT = m in D 
  D' fs ms. class P D = Some(D',fs,ms)  map_of ms M = Some(Ts,T,m)"
(*<*)by(fastforce simp:Method_def dest!: visible_methods_exist)(*>*)


lemma sees_method_idemp:
  "P  C sees M:TsT=m in D  P  D sees M:TsT=m in D"
 (*<*)by(fastforce simp: Method_def intro:sees_methods_idemp)(*>*)

lemma sees_method_decl_mono:
  " P  C' * C; P  C sees M:TsT = m in D;
     P  C' sees M:Ts'T' = m' in D'   P  D' * D"
 (*<*)
apply(frule sees_method_decl_above)
apply(unfold Method_def)
apply clarsimp
apply(drule (1) sees_methods_decl_mono)
apply clarsimp
apply(drule (1) sees_methods_fun)
apply clarsimp
apply(blast intro:rtrancl_trans)
done
(*>*)

lemma sees_method_is_class:
  " P  C sees M:TsT = m in D   is_class P C"
(*<*)by (auto simp add: is_class_def Method_def elim: Methods.induct)(*>*)


subsection‹Field lookup›

inductive
  Fields :: "['m prog, cname, ((vname × cname) × ty) list]  bool"
                  ("_  _ has'_fields _" [51,51,51] 50)
  for P :: "'m prog"
where
  has_fields_rec:
  " class P C = Some(D,fs,ms); C  Object; P  D has_fields FDTs;
     FDTs' = map (λ(F,T). ((F,C),T)) fs @ FDTs 
    P  C has_fields FDTs'"
| has_fields_Object:
  " class P Object = Some(D,fs,ms); FDTs = map (λ(F,T). ((F,Object),T)) fs 
    P  Object has_fields FDTs"

lemma has_fields_fun:
assumes 1: "P  C has_fields FDTs"
shows "FDTs'. P  C has_fields FDTs'  FDTs' = FDTs"
 (*<*)
using 1
proof induct
  case (has_fields_rec C D fs ms Dres Cres Cres')
  have "class": "class P C = Some (D, fs, ms)"
   and notObj: "C  Object" and DFields: "P  D has_fields Dres"
   and IH: "Dres'. P  D has_fields Dres'  Dres' = Dres"
   and Cres: "Cres = map (λ(F,T). ((F,C),T)) fs @ Dres"
   and CFields': "P  C has_fields Cres'" by fact+
  from CFields' notObj "class" obtain Dres'
    where DFields': "P  D has_fields Dres'"
     and Cres': "Cres' = map (λ(F,T). ((F,C),T)) fs @ Dres'"
    by(auto elim: Fields.cases)
  from Cres Cres' IH[OF DFields'] show "Cres' = Cres" by simp
next
  case has_fields_Object thus ?case by(auto elim: Fields.cases)
qed
(*>*)

lemma all_fields_in_has_fields:
assumes sub: "P  C has_fields FDTs"
shows " P  C * D; class P D = Some(D',fs,ms); (F,T)  set fs 
        ((F,D),T)  set FDTs"
(*<*)
using sub apply(induct)
 apply(simp add:image_def)
 apply(erule converse_rtranclE)
  apply(force)
 apply(drule subcls1D)
 apply fastforce
apply(force simp:image_def)
done
(*>*)


lemma has_fields_decl_above:
assumes fields: "P  C has_fields FDTs"
shows "((F,D),T)  set FDTs  P  C * D"
(*<*)
using fields apply(induct)
 prefer 2 apply fastforce
apply clarsimp
apply(erule disjE)
 apply(clarsimp simp add:image_def)
apply simp
apply(blast dest:subcls1I converse_rtrancl_into_rtrancl)
done
(*>*)


lemma subcls_notin_has_fields:
assumes fields: "P  C has_fields FDTs"
shows "((F,D),T)  set FDTs  (D,C)  (subcls1 P)+"
(*<*)
using fields apply(induct)
 prefer 2 apply(fastforce dest: tranclD)
apply clarsimp
apply(erule disjE)
 apply(clarsimp simp add:image_def)
 apply(drule tranclD)
 apply clarify
 apply(frule subcls1D)
 apply(fastforce dest:all_fields_in_has_fields)
apply simp
apply(blast dest:subcls1I trancl_into_trancl)
done
(*>*)


lemma has_fields_mono_lem:
assumes sub: "P  D * C"
shows "P  C has_fields FDTs
          pre. P  D has_fields pre@FDTs  dom(map_of pre)  dom(map_of FDTs) = {}"
(*<*)
using sub apply(induct rule:converse_rtrancl_induct)
 apply(rule_tac x = "[]" in exI)
 apply simp
apply clarsimp
apply(rename_tac D' D pre)
apply(subgoal_tac "(D',C) : (subcls1 P)^+")
 prefer 2 apply(erule (1) rtrancl_into_trancl2)
apply(drule subcls1D)
apply clarsimp
apply(rename_tac fs ms)
apply(drule (2) has_fields_rec)
 apply(rule refl)
apply(rule_tac x = "map (λ(F,T). ((F,D'),T)) fs @ pre" in exI)
apply simp
apply(simp add:Int_Un_distrib2)
apply(rule equals0I)
apply(auto dest: subcls_notin_has_fields simp:dom_map_of_conv_image_fst image_def)
done
(*>*)

(* FIXME why is Field not displayed correctly? TypeRel qualifier seems to confuse printer*)
definition has_field :: "'m prog  cname  vname  ty  cname  bool"
                   ("_  _ has _:_ in _" [51,51,51,51,51] 50)
where
  "P  C has F:T in D  
  FDTs. P  C has_fields FDTs  map_of FDTs (F,D) = Some T"

lemma has_field_mono:
  " P  C has F:T in D; P  C' * C   P  C' has F:T in D"
(*<*)
apply(clarsimp simp:has_field_def)
apply(drule (1) has_fields_mono_lem)
apply(fastforce simp: map_add_def split:option.splits)
done
(*>*)


definition sees_field :: "'m prog  cname  vname  ty  cname  bool"
                  ("_  _ sees _:_ in _" [51,51,51,51,51] 50)
where
  "P  C sees F:T in D  
  FDTs. P  C has_fields FDTs 
            map_of (map (λ((F,D),T). (F,(D,T))) FDTs) F = Some(D,T)"

lemma map_of_remap_SomeD:
  "map_of (map (λ((k,k'),x). (k,(k',x))) t) k = Some (k',x)  map_of t (k, k') = Some x"
(*<*)by (induct t) (auto simp:fun_upd_apply split: if_split_asm)(*>*)


lemma has_visible_field:
  "P  C sees F:T in D  P  C has F:T in D"
(*<*)by(auto simp add:has_field_def sees_field_def map_of_remap_SomeD)(*>*)


lemma sees_field_fun:
  "P  C sees F:T in D; P  C sees F:T' in D'  T' = T  D' = D"
(*<*)by(fastforce simp:sees_field_def dest:has_fields_fun)(*>*)


lemma sees_field_decl_above:
  "P  C sees F:T in D  P  C * D"
(*<*)
apply(auto simp:sees_field_def)
apply(blast  intro: has_fields_decl_above map_of_SomeD map_of_remap_SomeD)
done
(*>*)

(* FIXME ugly *)  
lemma sees_field_idemp:
  "P  C sees F:T in D  P  D sees F:T in D"
(*<*)
  apply (unfold sees_field_def)
  apply clarsimp
  apply (rule_tac P = "map_of xs F = y" for xs y in mp)
   prefer 2 
   apply assumption 
  apply (thin_tac "map_of xs F = y" for xs y)
  apply (erule Fields.induct)
   apply clarsimp
   apply (frule map_of_SomeD)
   apply clarsimp
   apply (fastforce intro: has_fields_rec)
  apply clarsimp
  apply (frule map_of_SomeD)
  apply clarsimp
  apply (fastforce intro: has_fields_Object)
  done
(*>*)

subsection "Functional lookup"

definition "method" :: "'m prog  cname  mname  cname × ty list × ty × 'm"
where
  "method P C M    THE (D,Ts,T,m). P  C sees M:Ts  T = m in D"

definition field  :: "'m prog  cname  vname  cname × ty"
where
  "field P C F    THE (D,T). P  C sees F:T in D"
                                                        
definition fields :: "'m prog  cname  ((vname × cname) × ty) list" 
where
  "fields P C    THE FDTs. P  C has_fields FDTs"                

lemma fields_def2 [simp]: "P  C has_fields FDTs  fields P C = FDTs"
(*<*)by (unfold fields_def) (auto dest: has_fields_fun)(*>*)

lemma field_def2 [simp]: "P  C sees F:T in D  field P C F = (D,T)"
(*<*)by (unfold field_def) (auto dest: sees_field_fun)(*>*)

lemma method_def2 [simp]: "P  C sees M: TsT = m in D  method P C M = (D,Ts,T,m)"
(*<*)by (unfold method_def) (auto dest: sees_method_fun)(*>*)

subsection "Code generator setup"

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  subcls1p 
.
declare subcls1_def [code_pred_def]

code_pred 
  (modes: i ⇒ i × o ⇒ bool, i ⇒ i × i ⇒ bool)
  [inductify]
  subcls1 
.
definition subcls' where "subcls' G = (subcls1p G)^**"
code_pred
  (modes: i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ o ⇒ bool)
  [inductify]
  subcls'
.

lemma subcls_conv_subcls' [code_unfold]:
  "(subcls1 G)^* = {(C, D). subcls' G C D}"
  by (simp add: subcls'_def subcls1_def rtrancl_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ bool)
  widen 
.

code_pred 
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Fields
.

lemma has_field_code [code_pred_intro]:
  " P  C has_fields FDTs; map_of FDTs (F, D) = T 
   P  C has F:T in D"
by(auto simp add: has_field_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  has_field
by(auto simp add: has_field_def)

lemma sees_field_code [code_pred_intro]:
  " P  C has_fields FDTs; map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = (D, T) 
   P  C sees F:T in D"
by(auto simp add: sees_field_def)

code_pred 
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ i ⇒ bool, 
          i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  sees_field
by(auto simp add: sees_field_def)

code_pred
  (modes: i ⇒ i ⇒ o ⇒ bool)
  Methods 
.

lemma Method_code [code_pred_intro]:
  " P  C sees_methods Mm; Mm M = ((Ts, T, m), D) 
   P  C sees M: TsT = m in D"
by(auto simp add: Method_def)

code_pred
  (modes: i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ o ⇒ bool,
          i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
  Method
by(auto simp add: Method_def)

lemma eval_Method_i_i_i_o_o_o_o_conv:
  "Predicate.eval (Method_i_i_i_o_o_o_o P C M) = (λ(Ts, T, m, D). P  C sees M:TsT=m in D)"
by(auto intro: Method_i_i_i_o_o_o_oI elim: Method_i_i_i_o_o_o_oE intro!: ext)

lemma method_code [code]:
  "method P C M = 
  Predicate.the (Predicate.bind (Method_i_i_i_o_o_o_o P C M) (λ(Ts, T, m, D). Predicate.single (D, Ts, T, m)))"
apply (rule sym, rule the_eqI)
apply (simp add: method_def eval_Method_i_i_i_o_o_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done

lemma eval_Fields_conv:
  "Predicate.eval (Fields_i_i_o P C) = (λFDTs. P  C has_fields FDTs)"
by(auto intro: Fields_i_i_oI elim: Fields_i_i_oE intro!: ext)

lemma fields_code [code]:
  "fields P C = Predicate.the (Fields_i_i_o P C)"
by(simp add: fields_def Predicate.the_def eval_Fields_conv)

lemma eval_sees_field_i_i_i_o_o_conv:
  "Predicate.eval (sees_field_i_i_i_o_o P C F) = (λ(T, D). P  C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_oI elim: sees_field_i_i_i_o_oE)

lemma eval_sees_field_i_i_i_o_i_conv:
  "Predicate.eval (sees_field_i_i_i_o_i P C F D) = (λT. P  C sees F:T in D)"
by(auto intro!: ext intro: sees_field_i_i_i_o_iI elim: sees_field_i_i_i_o_iE)

lemma field_code [code]:
  "field P C F = Predicate.the (Predicate.bind (sees_field_i_i_i_o_o P C F) (λ(T, D). Predicate.single (D, T)))"
apply (rule sym, rule the_eqI)
apply (simp add: field_def eval_sees_field_i_i_i_o_o_conv)
apply (rule arg_cong [where f=The])
apply (auto simp add: Sup_fun_def Sup_bool_def fun_eq_iff)
done

(*<*)
end
(*>*)

Theory Value

(*  Title:      Jinja/Common/Value.thy
    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Jinja Values›

theory Value imports TypeRel begin

type_synonym addr = nat

datatype val
  = Unit        ― ‹dummy result value of void expressions›
  | Null        ― ‹null reference›
  | Bool bool   ― ‹Boolean value›
  | Intg int    ― ‹integer value› 
  | Addr addr   ― ‹addresses of objects in the heap›

primrec the_Intg :: "val  int" where
  "the_Intg (Intg i) = i"

primrec the_Addr :: "val  addr" where
  "the_Addr (Addr a) = a"

primrec default_val :: "ty  val"   ― ‹default value for all types› where
  "default_val Void      = Unit"
| "default_val Boolean   = Bool False"
| "default_val Integer   = Intg 0"
| "default_val NT        = Null"
| "default_val (Class C) = Null"

end

Theory Objects

(*  Title:      HOL/MicroJava/J/State.thy

    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Objects and the Heap›

theory Objects imports TypeRel Value begin

subsection‹Objects›

type_synonym
  fields = "vname × cname  val"  ― ‹field name, defining class, value›
type_synonym
  obj = "cname × fields"    ― ‹class instance with class name and fields›

definition obj_ty  :: "obj  ty"
where
  "obj_ty obj    Class (fst obj)"

definition init_fields :: "((vname × cname) × ty) list  fields"
where
  "init_fields    map_of  map (λ(F,T). (F,default_val T))"
  
  ― ‹a new, blank object with default values in all fields:›
definition blank :: "'m prog  cname  obj"
where
  "blank P C    (C,init_fields (fields P C))" 

lemma [simp]: "obj_ty (C,fs) = Class C"
(*<*)by (simp add: obj_ty_def)(*>*)

subsection‹Heap›

type_synonym heap  = "addr  obj"

abbreviation
  cname_of :: "heap  addr  cname" where
  "cname_of hp a == fst (the (hp a))"

definition new_Addr  :: "heap  addr option"
where
  "new_Addr h    if a. h a = None then Some(LEAST a. h a = None) else None"

definition cast_ok :: "'m prog  cname  heap  val  bool"
where
  "cast_ok P C h v    v = Null  P  cname_of h (the_Addr v) * C"

definition hext :: "heap  heap  bool" ("_  _" [51,51] 50)
where
  "h  h'    a C fs. h a = Some(C,fs)  (fs'. h' a = Some(C,fs'))"

primrec typeof_h :: "heap  val  ty option"  ("typeof⇘_")
where
  "typeofh  Unit    = Some Void"
| "typeofh  Null    = Some NT"
| "typeofh (Bool b) = Some Boolean"
| "typeofh (Intg i) = Some Integer"
| "typeofh (Addr a) = (case h a of None  None | Some(C,fs)  Some(Class C))"

lemma new_Addr_SomeD:
  "new_Addr h = Some a  h a = None"
 (*<*)by(fastforce simp add:new_Addr_def split:if_splits intro:LeastI)(*>*)

lemma [simp]: "(typeofh v = Some Boolean) = (b. v = Bool b)"
 (*<*)by(induct v) auto(*>*)

lemma [simp]: "(typeofh v = Some Integer) = (i. v = Intg i)"
(*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeofh v = Some NT) = (v = Null)"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeofh v = Some(Class C)) = (a fs. v = Addr a  h a = Some(C,fs))"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "h a = Some(C,fs)  typeof(h(a(C,fs'))) v = typeofh v"
 (*<*)by(induct v) (auto simp:fun_upd_apply)(*>*)

text‹For literal values the first parameter of @{term typeof} can be
set to @{term Map.empty} because they do not contain addresses:›

abbreviation
  typeof :: "val  ty option" where
  "typeof v == typeof_h Map.empty v"

lemma typeof_lit_typeof:
  "typeof v = Some T  typeofh v = Some T"
 (*<*)by(cases v) auto(*>*)

lemma typeof_lit_is_type: 
  "typeof v = Some T  is_type P T"
 (*<*)by (induct v) (auto simp:is_type_def)(*>*)


subsection ‹Heap extension ⊴›

lemma hextI: "a C fs. h a = Some(C,fs)  (fs'. h' a = Some(C,fs'))  h  h'"
(*<*)
apply (unfold hext_def)
apply auto
done
(*>*)

lemma hext_objD: " h  h'; h a = Some(C,fs)   fs'. h' a = Some(C,fs')"
(*<*)
apply (unfold hext_def)
apply (force)
done
(*>*)

lemma hext_refl [iff]: "h  h"
(*<*)
apply (rule hextI)
apply (fast)
done
(*>*)

lemma hext_new [simp]: "h a = None  h  h(ax)"
(*<*)
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
(*>*)

lemma hext_trans: " h  h'; h'  h''   h  h''"
(*<*)
apply (rule hextI)
apply (fast dest: hext_objD)
done
(*>*)

lemma hext_upd_obj: "h a = Some (C,fs)  h  h(a(C,fs'))"
(*<*)
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
(*>*)

lemma hext_typeof_mono: " h  h'; typeofh v = Some T   typeofh' v = Some T"
(*<*)
apply(cases v)
    apply simp
   apply simp
  apply simp
 apply simp
apply(fastforce simp:hext_def)
done
(*>*)

text ‹Code generator setup for @{term "new_Addr"}

definition gen_new_Addr :: "heap  addr  addr option"
where "gen_new_Addr h n  if a. a  n  h a = None then Some(LEAST a. a  n  h a = None) else None"

lemma new_Addr_code_code [code]:
  "new_Addr h = gen_new_Addr h 0"
by(simp add: new_Addr_def gen_new_Addr_def split del: if_split cong: if_cong)

lemma gen_new_Addr_code [code]:
  "gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
apply(simp add: gen_new_Addr_def)
apply(rule impI)
apply(rule conjI)
 apply safe[1]
  apply(fastforce intro: Least_equality)
 apply(rule arg_cong[where f=Least])
 apply(rule ext)
 apply(case_tac "n = ac")
  apply simp
 apply(auto)[1]
apply clarify
apply(subgoal_tac "a = n")
 apply simp
 apply(rule Least_equality)
 apply auto[2]
apply(rule ccontr)
apply(erule_tac x="a" in allE)
apply simp
done

end

Theory Exceptions

(*  Title:      HOL/MicroJava/J/Exceptions.thy

    Author:     Gerwin Klein, Martin Strecker
    Copyright   2002 Technische Universitaet Muenchen
*)

section ‹Exceptions›

theory Exceptions imports Objects begin

definition NullPointer :: cname
where
  "NullPointer  ''NullPointer''"

definition ClassCast :: cname
where
  "ClassCast  ''ClassCast''"

definition OutOfMemory :: cname
where
  "OutOfMemory  ''OutOfMemory''"

definition sys_xcpts :: "cname set"
where
  "sys_xcpts    {NullPointer, ClassCast, OutOfMemory}"

definition addr_of_sys_xcpt :: "cname  addr"
where
  "addr_of_sys_xcpt s  if s = NullPointer then 0 else
                        if s = ClassCast then 1 else
                        if s = OutOfMemory then 2 else undefined"

definition start_heap :: "'c prog  heap"
where
  "start_heap G  Map.empty (addr_of_sys_xcpt NullPointer  blank G NullPointer)
                        (addr_of_sys_xcpt ClassCast  blank G ClassCast)
                        (addr_of_sys_xcpt OutOfMemory  blank G OutOfMemory)"

definition preallocated :: "heap  bool"
where
  "preallocated h  C  sys_xcpts. fs. h(addr_of_sys_xcpt C) = Some (C,fs)"


subsection "System exceptions"

lemma [simp]: "NullPointer  sys_xcpts  OutOfMemory  sys_xcpts  ClassCast  sys_xcpts"
(*<*)by(simp add: sys_xcpts_def)(*>*)


lemma sys_xcpts_cases [consumes 1, cases set]:
  " C  sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast  P C"
(*<*)by (auto simp add: sys_xcpts_def)(*>*)


subsection "@{term preallocated}"

lemma preallocated_dom [simp]: 
  " preallocated h; C  sys_xcpts   addr_of_sys_xcpt C  dom h"
(*<*)by (fastforce simp:preallocated_def dom_def)(*>*)


lemma preallocatedD:
  " preallocated h; C  sys_xcpts   fs. h(addr_of_sys_xcpt C) = Some (C, fs)"
(*<*)by(auto simp add: preallocated_def sys_xcpts_def)(*>*)


lemma preallocatedE [elim?]:
  " preallocated h;  C  sys_xcpts; fs. h(addr_of_sys_xcpt C) = Some(C,fs)  P h C
   P h C"
(*<*)by (fast dest: preallocatedD)(*>*)


lemma cname_of_xcp [simp]:
  " preallocated h; C  sys_xcpts   cname_of h (addr_of_sys_xcpt C) = C"
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_ClassCast [simp]:
  "preallocated h  typeofh (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_OutOfMemory [simp]:
  "preallocated h  typeofh (Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_NullPointer [simp]:
  "preallocated h  typeofh (Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma preallocated_hext:
  " preallocated h; h  h'   preallocated h'"
(*<*)by (simp add: preallocated_def hext_def)(*>*)

(*<*)
lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new  = preallocated_hext [OF _ hext_new]
(*>*)


lemma preallocated_start:
  "preallocated (start_heap P)"
(*<*)by (auto simp add: start_heap_def blank_def sys_xcpts_def fun_upd_apply
                     addr_of_sys_xcpt_def preallocated_def)(*>*)


end

Theory Expr

(*  Title:      Jinja/J/Expr.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Expressions›

theory Expr
imports "../Common/Exceptions"
begin

datatype bop = Eq | Add     ― ‹names of binary operations›

datatype 'a exp
  = new cname      ― ‹class instance creation›
  | Cast cname "('a exp)"      ― ‹type cast›
  | Val val      ― ‹value›
  | BinOp "('a exp)" bop "('a exp)"     ("_ «_» _" [80,0,81] 80)      ― ‹binary operation›
  | Var 'a                                               ― ‹local variable (incl. parameter)›
  | LAss 'a "('a exp)"     ("_:=_" [90,90]90)                    ― ‹local assignment›
  | FAcc "('a exp)" vname cname     ("__{_}" [10,90,99]90)      ― ‹field access›
  | FAss "('a exp)" vname cname "('a exp)"     ("__{_} := _" [10,90,99,90]90)      ― ‹field assignment›
  | Call "('a exp)" mname "('a exp list)"     ("__'(_')" [90,99,0] 90)            ― ‹method call›
  | Block 'a ty "('a exp)"     ("'{_:_; _}")
  | Seq "('a exp)" "('a exp)"     ("_;;/ _"             [61,60]60)
  | Cond "('a exp)" "('a exp)" "('a exp)"     ("if '(_') _/ else _" [80,79,79]70)
  | While "('a exp)" "('a exp)"     ("while '(_') _"     [80,79]70)
  | throw "('a exp)"
  | TryCatch "('a exp)" cname 'a "('a exp)"     ("try _/ catch'(_ _') _"  [0,99,80,79] 70)

type_synonym
  expr = "vname exp"            ― ‹Jinja expression›
type_synonym
  J_mb = "vname list × expr"    ― ‹Jinja method body: parameter names and expression›
type_synonym
  J_prog = "J_mb prog"          ― ‹Jinja program›

text‹The semantics of binary operators:›

fun binop :: "bop × val × val  val option" where
  "binop(Eq,v1,v2) = Some(Bool (v1 = v2))"
| "binop(Add,Intg i1,Intg i2) = Some(Intg(i1+i2))"
| "binop(bop,v1,v2) = None"

lemma [simp]:
  "(binop(Add,v1,v2) = Some v) = (i1 i2. v1 = Intg i1  v2 = Intg i2  v = Intg(i1+i2))"
(*<*)
apply(cases v1)
apply auto
apply(cases v2)
apply auto
done
(*>*)


subsection "Syntactic sugar"

abbreviation (input)
  InitBlock:: "'a  ty  'a exp  'a exp  'a exp"   ("(1'{_:_ := _;/ _})") where
  "InitBlock V T e1 e2 == {V:T; V := e1;; e2}"

abbreviation unit where "unit == Val Unit"
abbreviation null where "null == Val Null"
abbreviation "addr a == Val(Addr a)"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
  Throw :: "addr  'a exp" where
  "Throw a == throw(Val(Addr a))"

abbreviation
  THROW :: "cname  'a exp" where
  "THROW xc == Throw(addr_of_sys_xcpt xc)"


subsection‹Free Variables›

primrec fv :: "expr  vname set" and fvs :: "expr list  vname set" where
  "fv(new C) = {}"
| "fv(Cast C e) = fv e"
| "fv(Val v) = {}"
| "fv(e1 «bop» e2) = fv e1  fv e2"
| "fv(Var V) = {V}"
| "fv(LAss V e) = {V}  fv e"
| "fv(eF{D}) = fv e"
| "fv(e1F{D}:=e2) = fv e1  fv e2"
| "fv(eM(es)) = fv e  fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e1;;e2) = fv e1  fv e2"
| "fv(if (b) e1 else e2) = fv b  fv e1  fv e2"
| "fv(while (b) e) = fv b  fv e"
| "fv(throw e) = fv e"
| "fv(try e1 catch(C V) e2) = fv e1  (fv e2 - {V})"
| "fvs([]) = {}"
| "fvs(e#es) = fv e  fvs es"

lemma [simp]: "fvs(es1 @ es2) = fvs es1  fvs es2"
(*<*)by (induct es1 type:list) auto(*>*)

lemma [simp]: "fvs(map Val vs) = {}"
(*<*)by (induct vs) auto(*>*)

end

Theory State

(*  Title:      Jinja/J/State.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Program State›

theory State imports "../Common/Exceptions" begin

type_synonym
  locals = "vname  val"      ― ‹local vars, incl. params and ``this''›
type_synonym
  state  = "heap × locals"

definition hp :: "state  heap"
where
  "hp    fst"
definition lcl :: "state  locals"
where
  "lcl    snd"

(*<*)
declare hp_def[simp] lcl_def[simp]
(*>*)
end

Theory BigStep

(*  Title:      Jinja/J/BigStep.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Big Step Semantics›

theory BigStep imports Expr State begin

inductive
  eval :: "J_prog  expr  state  expr  state  bool"
          ("_  ((1_,/_) / (1_,/_))" [51,0,0,0,0] 81)
  and evals :: "J_prog  expr list  state  expr list  state  bool"
           ("_  ((1_,/_) [⇒]/ (1_,/_))" [51,0,0,0,0] 81)
  for P :: J_prog
where

  New:
  " new_Addr h = Some a; P  C has_fields FDTs; h' = h(a(C,init_fields FDTs)) 
   P  new C,(h,l)  addr a,(h',l)"

| NewFail:
  "new_Addr h = None 
  P  new C, (h,l)  THROW OutOfMemory,(h,l)"

| Cast:
  " P  e,s0  addr a,(h,l); h a = Some(D,fs); P  D * C 
   P  Cast C e,s0  addr a,(h,l)"

| CastNull:
  "P  e,s0  null,s1 
  P  Cast C e,s0  null,s1"

| CastFail:
  " P  e,s0 addr a,(h,l); h a = Some(D,fs); ¬ P  D * C 
   P  Cast C e,s0  THROW ClassCast,(h,l)"

| CastThrow:
  "P  e,s0  throw e',s1 
  P  Cast C e,s0  throw e',s1"

| Val:
  "P  Val v,s  Val v,s"

| BinOp:
  " P  e1,s0  Val v1,s1; P  e2,s1  Val v2,s2; binop(bop,v1,v2) = Some v 
   P  e1 «bop» e2,s0Val v,s2"

| BinOpThrow1:
  "P  e1,s0  throw e,s1 
  P  e1 «bop» e2, s0  throw e,s1"

| BinOpThrow2:
  " P  e1,s0  Val v1,s1; P  e2,s1  throw e,s2 
   P  e1 «bop» e2,s0  throw e,s2"

| Var:
  "l V = Some v 
  P  Var V,(h,l)  Val v,(h,l)"

| LAss:
  " P  e,s0  Val v,(h,l); l' = l(Vv) 
   P  V:=e,s0  unit,(h,l')"

| LAssThrow:
  "P  e,s0  throw e',s1 
  P  V:=e,s0  throw e',s1"

| FAcc:
  " P  e,s0  addr a,(h,l); h a = Some(C,fs); fs(F,D) = Some v 
   P  eF{D},s0  Val v,(h,l)"

| FAccNull:
  "P  e,s0  null,s1 
  P  eF{D},s0  THROW NullPointer,s1"

| FAccThrow:
  "P  e,s0  throw e',s1 
  P  eF{D},s0  throw e',s1"

| FAss:
  " P  e1,s0  addr a,s1; P  e2,s1  Val v,(h2,l2);
     h2 a = Some(C,fs); fs' = fs((F,D)v); h2' = h2(a(C,fs')) 
   P  e1F{D}:=e2,s0  unit,(h2',l2)"

| FAssNull:
  " P  e1,s0  null,s1;  P  e2,s1  Val v,s2  
  P  e1F{D}:=e2,s0  THROW NullPointer,s2"

| FAssThrow1:
  "P  e1,s0  throw e',s1 
  P  e1F{D}:=e2,s0  throw e',s1"

| FAssThrow2:
  " P  e1,s0  Val v,s1; P  e2,s1  throw e',s2 
   P  e1F{D}:=e2,s0  throw e',s2"

| CallObjThrow:
  "P  e,s0  throw e',s1 
  P  eM(ps),s0  throw e',s1"

| CallParamsThrow:
  " P  e,s0  Val v,s1; P  es,s1 [⇒] map Val vs @ throw ex # es',s2 
    P  eM(es),s0  throw ex,s2"

| CallNull:
  " P  e,s0  null,s1;  P  ps,s1 [⇒] map Val vs,s2 
   P  eM(ps),s0  THROW NullPointer,s2"

| Call:
  " P  e,s0  addr a,s1;  P  ps,s1 [⇒] map Val vs,(h2,l2);
     h2 a = Some(C,fs);  P  C sees M:TsT = (pns,body) in D;
     length vs = length pns;  l2' = [thisAddr a, pns[↦]vs];
     P  body,(h2,l2')  e',(h3,l3) 
   P  eM(ps),s0  e',(h3,l2)"

| Block:
  "P  e0,(h0,l0(V:=None))  e1,(h1,l1) 
  P  {V:T; e0},(h0,l0)  e1,(h1,l1(V:=l0 V))"

| Seq:
  " P  e0,s0  Val v,s1; P  e1,s1  e2,s2 
   P  e0;;e1,s0  e2,s2"

| SeqThrow:
  "P  e0,s0  throw e,s1 
  P  e0;;e1,s0throw e,s1"

| CondT:
  " P  e,s0  true,s1; P  e1,s1  e',s2 
   P  if (e) e1 else e2,s0  e',s2"

| CondF:
  " P  e,s0  false,s1; P  e2,s1  e',s2 
   P  if (e) e1 else e2,s0  e',s2"

| CondThrow:
  "P  e,s0  throw e',s1 
  P  if (e) e1 else e2, s0  throw e',s1"

| WhileF:
  "P  e,s0  false,s1 
  P  while (e) c,s0  unit,s1"

| WhileT:
  " P  e,s0  true,s1; P  c,s1  Val v1,s2; P  while (e) c,s2  e3,s3 
   P  while (e) c,s0  e3,s3"

| WhileCondThrow:
  "P  e,s0   throw e',s1 
  P  while (e) c,s0  throw e',s1"

| WhileBodyThrow:
  " P  e,s0  true,s1; P  c,s1  throw e',s2
   P  while (e) c,s0  throw e',s2"

| Throw:
  "P  e,s0  addr a,s1 
  P  throw e,s0  Throw a,s1"

| ThrowNull:
  "P  e,s0  null,s1 
  P  throw e,s0  THROW NullPointer,s1"

| ThrowThrow:
  "P  e,s0  throw e',s1 
  P  throw e,s0  throw e',s1"

| Try:
  "P  e1,s0  Val v1,s1 
  P  try e1 catch(C V) e2,s0  Val v1,s1"

| TryCatch:
  " P  e1,s0  Throw a,(h1,l1);  h1 a = Some(D,fs);  P  D * C;
     P  e2,(h1,l1(VAddr a))  e2',(h2,l2) 
   P  try e1 catch(C V) e2,s0  e2',(h2,l2(V:=l1 V))"

| TryThrow:
  " P  e1,s0  Throw a,(h1,l1);  h1 a = Some(D,fs);  ¬ P  D * C 
   P  try e1 catch(C V) e2,s0  Throw a,(h1,l1)"

| Nil:
  "P  [],s [⇒] [],s"

| Cons:
  " P  e,s0  Val v,s1; P  es,s1 [⇒] es',s2 
   P  e#es,s0 [⇒] Val v # es',s2"

| ConsThrow:
  "P  e, s0  throw e', s1 
  P  e#es, s0 [⇒] throw e' # es, s1"

(*<*)
lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]
  and eval_evals_inducts = eval_evals.inducts [split_format (complete)]

inductive_cases eval_cases [cases set]:
 "P  Cast C e,s  e',s'"
 "P  Val v,s  e',s'"
 "P  e1 «bop» e2,s  e',s'"
 "P  V:=e,s  e',s'"
 "P  eF{D},s  e',s'"
 "P  e1F{D}:=e2,s  e',s'"
 "P  eM{D}(es),s  e',s'"
 "P  {V:T;e1},s  e',s'"
 "P  e1;;e2,s  e',s'"
 "P  if (e) e1 else e2,s  e',s'"
 "P  while (b) c,s  e',s'"
 "P  throw e,s  e',s'"
 "P  try e1 catch(C V) e2,s  e',s'"
 
inductive_cases evals_cases [cases set]:
 "P  [],s [⇒] e',s'"
 "P  e#es,s [⇒] e',s'"
(*>*) 


subsection"Final expressions"

definition final :: "'a exp  bool"
where
  "final e    (v. e = Val v)  (a. e = Throw a)"

definition finals:: "'a exp list  bool"
where
  "finals es    (vs. es = map Val vs)  (vs a es'. es = map Val vs @ Throw a # es')"

lemma [simp]: "final(Val v)"
(*<*)by(simp add:final_def)(*>*)

lemma [simp]: "final(throw e) = (a. e = addr a)"
(*<*)by(simp add:final_def)(*>*)

lemma finalE: " final e;  v. e = Val v  R;  a. e = Throw a  R   R"
(*<*)by(auto simp:final_def)(*>*)

lemma [iff]: "finals []"
(*<*)by(simp add:finals_def)(*>*)

lemma [iff]: "finals (Val v # es) = finals es"
(*<*)
apply(clarsimp simp add: finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply simp
 apply(rule disjI2)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastforce
apply(erule disjE)
 apply clarsimp
apply(rule disjI2)
apply clarsimp
apply(rule_tac x = "v#vs" in exI)
apply simp
done
(*>*)

lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
(*<*)by(induct_tac vs, auto)(*>*)

lemma [iff]: "finals (map Val vs)"
(*<*)using finals_app_map[of vs "[]"]by(simp)(*>*)

lemma [iff]: "finals (throw e # es) = (a. e = addr a)"
(*<*)
apply(simp add:finals_def)
apply(rule iffI)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastforce
apply clarsimp
apply(rule_tac x = "[]" in exI)
apply simp
done
(*>*)

lemma not_finals_ConsI: "¬ final e  ¬ finals(e#es)"
 (*<*)
apply(clarsimp simp add:finals_def final_def)
apply(case_tac vs)
apply auto
done
(*>*)


lemma eval_final: "P  e,s  e',s'  final e'"
 and evals_final: "P  es,s [⇒] es',s'  finals es'"
(*<*)by(induct rule:eval_evals.inducts, simp_all)(*>*)


lemma eval_lcl_incr: "P  e,(h0,l0)  e',(h1,l1)  dom l0  dom l1"
 and evals_lcl_incr: "P  es,(h0,l0) [⇒] es',(h1,l1)  dom l0  dom l1"
(*<*)
proof (induct rule: eval_evals_inducts)
  case BinOp show ?case by(rule subset_trans)(rule BinOp.hyps)+
next
  case Call thus ?case
    by(simp del: fun_upd_apply) 
next
  case Seq show ?case by(rule subset_trans)(rule Seq.hyps)+
next
  case CondT show ?case by(rule subset_trans)(rule CondT.hyps)+
next
  case CondF show ?case by(rule subset_trans)(rule CondF.hyps)+
next
  case WhileT thus ?case by(blast)
next
  case TryCatch thus ?case by(clarsimp simp:dom_def split:if_split_asm) blast
next
  case Cons show ?case by(rule subset_trans)(rule Cons.hyps)+
next
  case Block thus ?case by(auto simp del:fun_upd_apply)
qed auto
(*>*)

text‹Only used later, in the small to big translation, but is already a
good sanity check:›

lemma eval_finalId:  "final e  P  e,s  e,s"
(*<*)by (erule finalE) (iprover intro: eval_evals.intros)+(*>*)


lemma eval_finalsId:
assumes finals: "finals es" shows "P  es,s [⇒] es,s"
(*<*)
  using finals
proof (induct es type: list)
  case Nil show ?case by (rule eval_evals.intros)
next
  case (Cons e es)
  have hyp: "finals es  P  es,s [⇒] es,s"
   and finals: "finals (e # es)" by fact+
  show "P  e # es,s [⇒] e # es,s"
  proof cases
    assume "final e"
    thus ?thesis
    proof (cases rule: finalE)
      fix v assume e: "e = Val v"
      have "P  Val v,s  Val v,s" by (simp add: eval_finalId)
      moreover from finals e have "P  es,s [⇒] es,s" by(fast intro:hyp)
      ultimately have "P  Val v#es,s [⇒] Val v#es,s"
        by (rule eval_evals.intros)
      with e show ?thesis by simp
    next
      fix a assume e: "e = Throw a"
      have "P  Throw a,s  Throw a,s" by (simp add: eval_finalId)
      hence "P  Throw a#es,s [⇒] Throw a#es,s" by (rule eval_evals.intros)
      with e show ?thesis by simp
    qed
  next
    assume "¬ final e"
    with not_finals_ConsI finals have False by blast
    thus ?thesis ..
  qed
qed
(*>*)


theorem eval_hext: "P  e,(h,l)  e',(h',l')  h  h'"
and evals_hext:  "P  es,(h,l) [⇒] es',(h',l')  h  h'"
(*<*)
proof (induct rule: eval_evals_inducts)
  case New thus ?case
    by(fastforce intro!: hext_new intro:LeastI simp:new_Addr_def
                split:if_split_asm simp del:fun_upd_apply)
next
  case BinOp thus ?case by (fast elim!:hext_trans)
next
  case BinOpThrow2 thus ?case by(fast elim!: hext_trans)
next
  case FAss thus ?case
    by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
            elim!: hext_trans)
next
  case FAssNull thus ?case by (fast elim!:hext_trans)
next
  case FAssThrow2 thus ?case by (fast elim!:hext_trans)
next
  case CallParamsThrow thus ?case by(fast elim!: hext_trans)
next
  case CallNull thus ?case by(fast elim!: hext_trans)
next
  case Call thus ?case by(fast elim!: hext_trans)
next
  case Seq thus ?case by(fast elim!: hext_trans)
next
  case CondT thus ?case by(fast elim!: hext_trans)
next
  case CondF thus ?case by(fast elim!: hext_trans)
next
  case WhileT thus ?case by(fast elim!: hext_trans)
next
  case WhileBodyThrow thus ?case by (fast elim!: hext_trans)
next
  case TryCatch thus ?case  by(fast elim!: hext_trans)
next
  case Cons thus ?case by (fast intro: hext_trans)
qed auto
(*>*)


end

Theory SmallStep

(*  Title:      Jinja/J/SmallStep.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Small Step Semantics›

theory SmallStep
imports Expr State
begin

fun blocks :: "vname list * ty list * val list * expr  expr"
where
 "blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}"
|"blocks([],[],[],e) = e"

lemmas blocks_induct = blocks.induct[split_format (complete)]

lemma [simp]:
  " size vs = size Vs; size Ts = size Vs   fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"
(*<*)
by (induct rule:blocks_induct) auto
(*>*)


definition assigned :: "vname  expr  bool"
where
  "assigned V e    v e'. e = (V := Val v;; e')"

inductive_set
  red  :: "J_prog  ((expr × state) × (expr × state)) set"
  and reds  :: "J_prog  ((expr list × state) × (expr list × state)) set"
  and red' :: "J_prog  expr  state  expr  state  bool"
          ("_  ((1_,/_) / (1_,/_))" [51,0,0,0,0] 81)
  and reds' :: "J_prog  expr list  state  expr list  state  bool"
          ("_  ((1_,/_) [→]/ (1_,/_))" [51,0,0,0,0] 81)
  for P :: J_prog
where

  "P  e,s  e',s'  ((e,s), e',s')  red P"
| "P  es,s [→] es',s'  ((es,s), es',s')  reds P"

| RedNew:
  " new_Addr h = Some a; P  C has_fields FDTs; h' = h(a(C,init_fields FDTs)) 
   P  new C, (h,l)  addr a, (h',l)"

| RedNewFail:
  "new_Addr h = None 
  P  new C, (h,l)  THROW OutOfMemory, (h,l)"

| CastRed:
  "P  e,s  e',s' 
  P  Cast C e, s  Cast C e', s'"

| RedCastNull:
  "P  Cast C null, s  null,s"

| RedCast:
 " hp s a = Some(D,fs); P  D * C 
   P  Cast C (addr a), s  addr a, s"

| RedCastFail:
  " hp s a = Some(D,fs); ¬ P  D * C 
   P  Cast C (addr a), s  THROW ClassCast, s"

| BinOpRed1:
  "P  e,s  e',s' 
  P  e «bop» e2, s  e' «bop» e2, s'"

| BinOpRed2:
  "P  e,s  e',s' 
  P  (Val v1) «bop» e, s  (Val v1) «bop» e', s'"

| RedBinOp:
  "binop(bop,v1,v2) = Some v 
  P  (Val v1) «bop» (Val v2), s  Val v,s"

| RedVar:
  "lcl s V = Some v 
  P  Var V,s  Val v,s"

| LAssRed:
  "P  e,s  e',s' 
  P  V:=e,s  V:=e',s'"

| RedLAss:
  "P  V:=(Val v), (h,l)  unit, (h,l(Vv))"

| FAccRed:
  "P  e,s  e',s' 
  P  eF{D}, s  e'F{D}, s'"

| RedFAcc:
  " hp s a = Some(C,fs); fs(F,D) = Some v 
   P  (addr a)F{D}, s  Val v,s"

| RedFAccNull:
  "P  nullF{D}, s  THROW NullPointer, s"

| FAssRed1:
  "P  e,s  e',s' 
  P  eF{D}:=e2, s  e'F{D}:=e2, s'"

| FAssRed2:
  "P  e,s  e',s' 
  P  Val vF{D}:=e, s  Val vF{D}:=e', s'"

| RedFAss:
  "h a = Some(C,fs) 
  P  (addr a)F{D}:=(Val v), (h,l)  unit, (h(a  (C,fs((F,D)  v))),l)"

| RedFAssNull:
  "P  nullF{D}:=Val v, s  THROW NullPointer, s"

| CallObj:
  "P  e,s  e',s' 
  P  eM(es),s  e'M(es),s'"

| CallParams:
  "P  es,s [→] es',s' 
  P  (Val v)M(es),s  (Val v)M(es'),s'"

| RedCall:
  " hp s a = Some(C,fs); P  C sees M:TsT = (pns,body) in D; size vs = size pns; size Ts = size pns 
   P  (addr a)M(map Val vs), s  blocks(this#pns, Class D#Ts, Addr a#vs, body), s"

| RedCallNull:
  "P  nullM(map Val vs),s  THROW NullPointer,s"

| BlockRedNone:
  " P  e, (h,l(V:=None))  e', (h',l'); l' V = None; ¬ assigned V e 
   P  {V:T; e}, (h,l)  {V:T; e'}, (h',l'(V := l V))"

| BlockRedSome:
  " P  e, (h,l(V:=None))  e', (h',l'); l' V = Some v;¬ assigned V e 
   P  {V:T; e}, (h,l)  {V:T := Val v; e'}, (h',l'(V := l V))"

| InitBlockRed:
  " P  e, (h,l(Vv))  e', (h',l'); l' V = Some v' 
   P  {V:T := Val v; e}, (h,l)  {V:T := Val v'; e'}, (h',l'(V := l V))"

| RedBlock:
  "P  {V:T; Val u}, s  Val u, s"

| RedInitBlock:
  "P  {V:T := Val v; Val u}, s  Val u, s"

| SeqRed:
  "P  e,s  e',s' 
  P  e;;e2, s  e';;e2, s'"

| RedSeq:
  "P  (Val v);;e2, s  e2, s"

| CondRed:
  "P  e,s  e',s' 
  P  if (e) e1 else e2, s  if (e') e1 else e2, s'"

| RedCondT:
  "P  if (true) e1 else e2, s  e1, s"

| RedCondF:
  "P  if (false) e1 else e2, s  e2, s"

| RedWhile:
  "P  while(b) c, s  if(b) (c;;while(b) c) else unit, s"

| ThrowRed:
  "P  e,s  e',s' 
  P  throw e, s  throw e', s'"

| RedThrowNull:
  "P  throw null, s  THROW NullPointer, s"

| TryRed:
  "P  e,s  e',s' 
  P  try e catch(C V) e2, s  try e' catch(C V) e2, s'"

| RedTry:
  "P  try (Val v) catch(C V) e2, s  Val v, s"

| RedTryCatch:
  " hp s a = Some(D,fs); P  D * C 
   P  try (Throw a) catch(C V) e2, s  {V:Class C := addr a; e2}, s"

| RedTryFail:
  " hp s a = Some(D,fs); ¬ P  D * C 
   P  try (Throw a) catch(C V) e2, s  Throw a, s"

| ListRed1:
  "P  e,s  e',s' 
  P  e#es,s [→] e'#es,s'"

| ListRed2:
  "P  es,s [→] es',s' 
  P  Val v # es,s [→] Val v # es',s'"

― ‹Exception propagation›

| CastThrow: "P  Cast C (throw e), s  throw e, s"
| BinOpThrow1: "P  (throw e) «bop» e2, s  throw e, s"
| BinOpThrow2: "P  (Val v1) «bop» (throw e), s  throw e, s"
| LAssThrow: "P  V:=(throw e), s  throw e, s"
| FAccThrow: "P  (throw e)F{D}, s  throw e, s"
| FAssThrow1: "P  (throw e)F{D}:=e2, s  throw e,s"
| FAssThrow2: "P  Val vF{D}:=(throw e), s  throw e, s"
| CallThrowObj: "P  (throw e)M(es), s  throw e, s"
| CallThrowParams: " es = map Val vs @ throw e # es'   P  (Val v)M(es), s  throw e, s"
| BlockThrow: "P  {V:T; Throw a}, s  Throw a, s"
| InitBlockThrow: "P  {V:T := Val v; Throw a}, s  Throw a, s"
| SeqThrow: "P  (throw e);;e2, s  throw e, s"
| CondThrow: "P  if (throw e) e1 else e2, s  throw e, s"
| ThrowThrow: "P  throw(throw e), s  throw e, s"
(*<*)
lemmas red_reds_induct = red_reds.induct [split_format (complete)]
  and red_reds_inducts = red_reds.inducts [split_format (complete)]

inductive_cases [elim!]:
 "P  V:=e,s  e',s'"
 "P  e1;;e2,s  e',s'"
(*>*)

subsection‹The reflexive transitive closure›

abbreviation
  Step :: "J_prog  expr  state  expr  state  bool"
          ("_  ((1_,/_) →*/ (1_,/_))" [51,0,0,0,0] 81)
  where "P  e,s →* e',s'  ((e,s), e',s')  (red P)*"

abbreviation
  Steps :: "J_prog  expr list  state  expr list  state  bool"
          ("_  ((1_,/_) [→]*/ (1_,/_))" [51,0,0,0,0] 81)
  where "P  es,s [→]* es',s'  ((es,s), es',s')  (reds P)*"

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P  e,(h,l) →* e',(h',l')"
and "e h l. R e h l e h l"
and "e0 h0 l0 e1 h1 l1 e' h' l'.
        P  e0,(h0,l0)  e1,(h1,l1); R e1 h1 l1 e' h' l'   R e0 h0 l0 e' h' l'"
shows "R e h l e' h' l'"
(*<*)
proof -
  { fix s s'
    assume reds: "P  e,s →* e',s'"
       and base: "e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
       and red1: "e0 s0 e1 s1 e' s'.
            P  e0,s0  e1,s1; R e1 (hp s1) (lcl s1) e' (hp s') (lcl s') 
            R e0 (hp s0) (lcl s0) e' (hp s') (lcl s')"
    from reds have "R e (hp s) (lcl s) e' (hp s') (lcl s')"
    proof (induct rule:converse_rtrancl_induct2)
      case refl show ?case by(rule base)
    next
      case (step e0 s0 e s)
      thus ?case by(blast intro:red1)
    qed
    }
  with assms show ?thesis by fastforce
qed
(*>*)


subsection‹Some easy lemmas›

lemma [iff]: "¬ P  [],s [→] es',s'"
(*<*)by(blast elim: reds.cases)(*>*)

lemma [iff]: "¬ P  Val v,s  e',s'"
(*<*)by(fastforce elim: red.cases)(*>*)

lemma [iff]: "¬ P  Throw a,s  e',s'"
(*<*)by(fastforce elim: red.cases)(*>*)


lemma red_hext_incr: "P  e,(h,l)  e',(h',l')   h  h'"
  and reds_hext_incr: "P  es,(h,l) [→] es',(h',l')   h  h'"
(*<*)
proof(induct rule:red_reds_inducts)
  case RedNew thus ?case
    by(fastforce dest:new_Addr_SomeD simp:hext_def split:if_splits)
next
  case RedFAss thus ?case by(simp add:hext_def split:if_splits)
qed simp_all
(*>*)


lemma red_lcl_incr: "P  e,(h0,l0)  e',(h1,l1)  dom l0  dom l1"
and "P  es,(h0,l0) [→] es',(h1,l1)  dom l0  dom l1"
(*<*)by(induct rule: red_reds_inducts)(auto simp del:fun_upd_apply)(*>*)


lemma red_lcl_add: "P  e,(h,l)  e',(h',l')  (l0. P  e,(h,l0++l)  e',(h',l0++l'))"
and "P  es,(h,l) [→] es',(h',l')  (l0. P  es,(h,l0++l) [→] es',(h',l0++l'))"
(*<*)
proof (induct rule:red_reds_inducts)
  case RedCast thus ?case by(fastforce intro:red_reds.intros)
next
  case RedCastFail thus ?case by(force intro:red_reds.intros)
next
  case RedFAcc thus ?case by(fastforce intro:red_reds.intros)
next
  case RedCall thus ?case by(fastforce intro:red_reds.intros)
next
  case (InitBlockRed e h l V v e' h' l' v' T l0)
  have IH: "l0. P  e,(h, l0 ++ l(V  v))  e',(h', l0 ++ l')"
    and l'V: "l' V = Some v'" by fact+
  from IH have IH': "P  e,(h, (l0 ++ l)(V  v))  e',(h', l0 ++ l')"
    by simp
  have "(l0 ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(rule ext)(simp add:map_add_def)
  with red_reds.InitBlockRed[OF IH'] l'V show ?case by(simp del:fun_upd_apply)
next
  case (BlockRedNone e h l V e' h' l' T l0)
  have IH: "l0. P  e,(h, l0 ++ l(V := None))  e',(h', l0 ++ l')"
    and l'V: "l' V = None" and unass: "¬ assigned V e" by fact+
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:fun_eq_iff map_add_def)
  hence IH': "P  e,(h, (l0++l)(V := None))  e',(h', l0(V := None) ++ l')"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:fun_eq_iff map_add_def)
  with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
    by(simp add: map_add_def)
next
  case (BlockRedSome e h l V e' h' l' v T l0)
  have IH: "l0. P  e,(h, l0 ++ l(V := None))  e',(h', l0 ++ l')"
    and l'V: "l' V = Some v" and unass: "¬ assigned V e" by fact+
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:fun_eq_iff map_add_def)
  hence IH': "P  e,(h, (l0++l)(V := None))  e',(h', l0(V := None) ++ l')"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:fun_eq_iff map_add_def)
  with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
    by(simp add:map_add_def)
next
  case RedTryCatch thus ?case by(fastforce intro:red_reds.intros)
next
  case RedTryFail thus ?case by(force intro!:red_reds.intros)
qed (simp_all add:red_reds.intros)
(*>*)


lemma Red_lcl_add:
assumes "P  e,(h,l) →* e',(h',l')" shows "P  e,(h,l0++l) →* e',(h',l0++l')"
(*<*)
using assms
proof(induct rule:converse_rtrancl_induct_red)
  case 1 thus ?case by simp
next
  case 2 thus ?case
    by (blast dest: red_lcl_add intro: converse_rtrancl_into_rtrancl)
qed
(*>*)


end

Theory SystemClasses

(*  Title:      HOL/MicroJava/J/SystemClasses.thy

    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

section ‹System Classes›

theory SystemClasses
imports Decl Exceptions
begin

text ‹
  This theory provides definitions for the Object› class,
  and the system exceptions.
›

definition ObjectC :: "'m cdecl"
where
  "ObjectC  (Object, (undefined,[],[]))"

definition NullPointerC :: "'m cdecl"
where
  "NullPointerC  (NullPointer, (Object,[],[]))"

definition ClassCastC :: "'m cdecl"
where
  "ClassCastC  (ClassCast, (Object,[],[]))"

definition OutOfMemoryC :: "'m cdecl"
where
  "OutOfMemoryC  (OutOfMemory, (Object,[],[]))"

definition SystemClasses :: "'m cdecl list"
where
  "SystemClasses  [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"

end

Theory WellForm

(*  Title:      Jinja/J/WellForm.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Generic Well-formedness of programs›

theory WellForm imports TypeRel SystemClasses begin

text ‹\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies.  Hence it works
for both Jinja and JVM programs. Well-typing of expressions is defined
elsewhere (in theory WellType›).

Because Jinja does not have method overloading, its policy for method
overriding is the classical one: \emph{covariant in the result type
but contravariant in the argument types.} This means the result type
of the overriding method becomes more specific, the argument types
become more general.
›

type_synonym 'm wf_mdecl_test = "'m prog  cname  'm mdecl  bool"

definition wf_fdecl :: "'m prog  fdecl  bool"
where
  "wf_fdecl P  λ(F,T). is_type P T"

definition wf_mdecl :: "'m wf_mdecl_test  'm wf_mdecl_test"
where
  "wf_mdecl wf_md P C  λ(M,Ts,T,mb).
  (Tset Ts. is_type P T)  is_type P T  wf_md P C (M,Ts,T,mb)"

definition wf_cdecl :: "'m wf_mdecl_test  'm prog  'm cdecl  bool"
where
  "wf_cdecl wf_md P    λ(C,(D,fs,ms)).
  (fset fs. wf_fdecl P f)   distinct_fst fs 
  (mset ms. wf_mdecl wf_md P C m)   distinct_fst ms 
  (C  Object 
   is_class P D  ¬ P  D * C 
   ((M,Ts,T,m)set ms.
      D' Ts' T' m'. P  D sees M:Ts'  T' = m' in D' 
                       P  Ts' [≤] Ts  P  T  T'))"

definition wf_syscls :: "'m prog  bool"
where
  "wf_syscls P    {Object}  sys_xcpts  set(map fst P)"

definition wf_prog :: "'m wf_mdecl_test  'm prog  bool"
where
  "wf_prog wf_md P    wf_syscls P  (c  set P. wf_cdecl wf_md P c)  distinct_fst P"


subsection‹Well-formedness lemmas›

lemma class_wf: 
  "class P C = Some c; wf_prog wf_md P  wf_cdecl wf_md P (C,c)"
(*<*)
apply (unfold wf_prog_def class_def)
apply (fast dest: map_of_SomeD)
done
(*>*)


lemma class_Object [simp]: 
  "wf_prog wf_md P  C fs ms. class P Object = Some (C,fs,ms)"
(*<*)
apply (unfold wf_prog_def wf_syscls_def class_def)
apply (auto simp: map_of_SomeI)
done
(*>*)


lemma is_class_Object [simp]:
  "wf_prog wf_md P  is_class P Object"
(*<*)by (simp add: is_class_def)(*>*)
(* Unused
lemma is_class_supclass:
assumes wf: "wf_prog wf_md P" and sub: "P ⊢ C ≼* D"
shows "is_class P C ⟹ is_class P D"
using sub apply(induct)
 apply assumption
apply(fastforce simp:wf_cdecl_def subcls1_def is_class_def
               dest:class_wf[OF _ wf])
done

This is NOT true because P ⊢ NT ≤ Class C for any Class C
lemma is_type_suptype: "⟦ wf_prog p P; is_type P T; P ⊢ T ≤ T' ⟧
 ⟹ is_type P T'"
*)

lemma is_class_xcpt:
  " C  sys_xcpts; wf_prog wf_md P   is_class P C"
(*<*)
  apply (simp add: wf_prog_def wf_syscls_def is_class_def class_def)
  apply (fastforce intro!: map_of_SomeI)
  done
(*>*)


lemma subcls1_wfD:
  " P  C 1 D; wf_prog wf_md P   D  C  (D,C)  (subcls1 P)+"
(*<*)
apply( frule r_into_trancl)
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def)
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
done
(*>*)


lemma wf_cdecl_supD: 
  "wf_cdecl wf_md P (C,D,r); C  Object  is_class P D"
(*<*)by (auto simp: wf_cdecl_def)(*>*)


lemma subcls_asym:
  " wf_prog wf_md P; (C,D)  (subcls1 P)+   (D,C)  (subcls1 P)+"
(*<*)
apply(erule tranclE)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: trancl_trans)
done
(*>*)


lemma subcls_irrefl:
  " wf_prog wf_md P; (C,D)  (subcls1 P)+   C  D"
(*<*)
apply (erule trancl_trans_induct)
apply  (auto dest: subcls1_wfD subcls_asym)
done
(*>*)


lemma acyclic_subcls1:
  "wf_prog wf_md P  acyclic (subcls1 P)"
(*<*)
apply (unfold acyclic_def)
apply (fast dest: subcls_irrefl)
done
(*>*)


lemma wf_subcls1:
  "wf_prog wf_md P  wf ((subcls1 P)¯)"
(*<*)
apply (rule finite_acyclic_wf)
apply ( subst finite_converse)
apply ( rule finite_subcls1)
apply (subst acyclic_converse)
apply (erule acyclic_subcls1)
done
(*>*)


lemma single_valued_subcls1:
  "wf_prog wf_md G  single_valued (subcls1 G)"
(*<*)
by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)
(*>*)


lemma subcls_induct: 
  " wf_prog wf_md P; C. D. (C,D)  (subcls1 P)+  Q D  Q C   Q C"
(*<*)
  (is "?A  PROP ?P  _")
proof -
  assume p: "PROP ?P"
  assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wf_trancl)
apply(simp only: trancl_converse)
apply(erule_tac a = C in wf_induct)
apply(rule p)
apply(auto)
done
qed
(*>*)


lemma subcls1_induct_aux:
  " is_class P C; wf_prog wf_md P; Q Object;
    C D fs ms.
     C  Object; is_class P C; class P C = Some (D,fs,ms) 
      wf_cdecl wf_md P (C,D,fs,ms)  P  C 1 D  is_class P D  Q D  Q C 
   Q C"
(*<*)
  (is "?A  ?B  ?C  PROP ?P  _")
proof -
  assume p: "PROP ?P"
  assume ?A ?B ?C thus ?thesis apply -
apply(unfold is_class_def)
apply( rule impE)
prefer 2
apply(   assumption)
prefer 2
apply(  assumption)
apply( erule thin_rl)
apply( rule subcls_induct)
apply(  assumption)
apply( rule impI)
apply( case_tac "C = Object")
apply(  fast)
apply safe
apply( frule (1) class_wf)
apply( frule (1) wf_cdecl_supD)

apply( subgoal_tac "P  C 1 a")
apply( erule_tac [2] subcls1I)
apply(  rule p)
apply (unfold is_class_def)
apply auto
done
qed
(*>*)

(* FIXME can't we prove this one directly?? *)
lemma subcls1_induct [consumes 2, case_names Object Subcls]:
  " wf_prog wf_md P; is_class P C; Q Object;
    C D. C  Object; P  C 1 D; is_class P D; Q D  Q C 
   Q C"
(*<*)
  apply (erule subcls1_induct_aux, assumption, assumption)
  apply blast
  done
(*>*)


lemma subcls_C_Object:
  " is_class P C; wf_prog wf_md P   P  C * Object"
(*<*)
apply(erule (1) subcls1_induct)
 apply( fast)
apply(erule (1) converse_rtrancl_into_rtrancl)
done
(*>*)


lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms)  set P" and "(M,Ts,T,m)  set ms"
shows "set Ts  types P"
(*<*)
proof
  from assms have "wf_mdecl wf_md P C (M,Ts,T,m)" 
    by (unfold wf_prog_def wf_cdecl_def) auto  
  hence "t  set Ts. is_type P t" by (unfold wf_mdecl_def) auto
  moreover fix t assume "t  set Ts"
  ultimately have "is_type P t" by blast
  thus "t  types P" ..
qed
(*>*)


subsection‹Well-formedness and method lookup›

lemma sees_wf_mdecl:
  " wf_prog wf_md P; P  C sees M:TsT = m in D   wf_mdecl wf_md P D (M,Ts,T,m)"
(*<*)
apply(drule visible_method_exists)
apply(fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)
done
(*>*)


lemma sees_method_mono [rule_format (no_asm)]: 
  " P  C' * C; wf_prog wf_md P  
  D Ts T m. P  C sees M:TsT = m in D 
     (D' Ts' T' m'. P  C' sees M:Ts'T' = m' in D'  P  Ts [≤] Ts'  P  T'  T)"
(*<*)
apply( drule rtranclD)
apply( erule disjE)
apply(  fastforce)
apply( erule conjE)
apply( erule trancl_trans_induct)
prefer 2
apply(  clarify)
apply(  drule spec, drule spec, drule spec, drule spec, erule (1) impE)
apply clarify
apply(  fast elim: widen_trans widens_trans)
apply( clarify)
apply( drule subcls1D)
apply( clarify)
apply(clarsimp simp:Method_def)
apply(frule (2) sees_methods_rec)
apply(rule refl)
apply(case_tac "map_of ms M")
apply(rule_tac x = D in exI)
apply(rule_tac x = Ts in exI)
apply(rule_tac x = T in exI)
apply simp
apply(rule_tac x = m in exI)
apply(fastforce simp add:map_add_def split:option.split)
apply clarsimp
apply(rename_tac Ts' T' m')
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def Method_def)
apply( frule map_of_SomeD)
apply auto
apply(drule (1) bspec, simp)
apply(erule_tac x=D in allE, erule_tac x=Ts in allE, erule_tac x=T in allE)
apply(fastforce simp:map_add_def split:option.split)
done
(*>*)


lemma sees_method_mono2:
  " P  C' * C; wf_prog wf_md P;
     P  C sees M:TsT = m in D; P  C' sees M:Ts'T' = m' in D' 
   P  Ts [≤] Ts'  P  T'  T"
(*<*)by(blast dest:sees_method_mono sees_method_fun)(*>*)


lemma mdecls_visible:
assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
shows "D fs ms. class P C = Some(D,fs,ms)
          Mm. P  C sees_methods Mm  ((M,Ts,T,m)  set ms. Mm M = Some((Ts,T,m),C))"
(*<*)
using wf "class"
proof (induct rule:subcls1_induct)
  case Object
  with wf have "distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
  with Object show ?case by(fastforce intro!: sees_methods_Object map_of_SomeI)
next
  case Subcls
  with wf have "distinct_fst ms"
    by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
  with Subcls show ?case
    by(fastforce elim:sees_methods_rec dest:subcls1D map_of_SomeI
                simp:is_class_def)
qed
(*>*)


lemma mdecl_visible:
assumes wf: "wf_prog wf_md P" and C: "(C,S,fs,ms)  set P" and  m: "(M,Ts,T,m)  set ms"
shows "P  C sees M:TsT = m in C"
(*<*)
proof -
  from wf C have "class": "class P C = Some (S,fs,ms)"
    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
  from "class" have "is_class P C" by(auto simp:is_class_def)                   
  with assms "class" show ?thesis
    by(bestsimp simp:Method_def dest:mdecls_visible)
qed
(*>*)


lemma Call_lemma:
  " P  C sees M:TsT = m in D; P  C' * C; wf_prog wf_md P 
   D' Ts' T' m'.
       P  C' sees M:Ts'T' = m' in D'  P  Ts [≤] Ts'  P  T'  T  P  C' * D'
        is_type P T'  (Tset Ts'. is_type P T)  wf_md P D' (M,Ts',T',m')"
(*<*)
apply(frule (2) sees_method_mono)
apply(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
               simp: wf_mdecl_def)
done
(*>*)


lemma wf_prog_lift:
  assumes wf: "wf_prog (λP C bd. A P C bd) P"
  and rule:
  "wf_md C M Ts C T m bd.
   wf_prog wf_md P 
   P  C sees M:TsT = m in C    
   set Ts   types P 
   bd = (M,Ts,T,m) 
   A P C bd 
   B P C bd"
  shows "wf_prog (λP C bd. B P C bd) P"
(*<*)
proof -
  from wf show ?thesis
    apply (unfold wf_prog_def wf_cdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply (unfold wf_mdecl_def)
    apply clarsimp
    apply (drule bspec, assumption)
    apply clarsimp
    apply (frule mdecl_visible [OF wf], assumption+)
    apply (frule is_type_pTs [OF wf], assumption+)
    apply (drule rule [OF wf], assumption+)
    apply auto
    done
qed
(*>*)


subsection‹Well-formedness and field lookup›

lemma wf_Fields_Ex:
  " wf_prog wf_md P; is_class P C   FDTs. P  C has_fields FDTs"
(*<*)
apply(frule class_Object)
apply(erule (1) subcls1_induct)
 apply(blast intro:has_fields_Object)
apply(blast intro:has_fields_rec dest:subcls1D)
done
(*>*)


lemma has_fields_types:
  " P  C has_fields FDTs; (FD,T)  set FDTs; wf_prog wf_md P   is_type P T"
(*<*)
apply(induct rule:Fields.induct)
 apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
done
(*>*)


lemma sees_field_is_type:
  " P  C sees F:T in D; wf_prog wf_md P   is_type P T"
(*<*)
by(fastforce simp: sees_field_def
            elim: has_fields_types map_of_SomeD[OF map_of_remap_SomeD])
(*>*)

lemma wf_syscls:
  "set SystemClasses  set P  wf_syscls P"
(*<*)
apply (simp add: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
                 ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 apply force
done
(*>*)

end

Theory WWellForm

(*  Title:      Jinja/J/WWellForm.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Weak well-formedness of Jinja programs›

theory WWellForm imports "../Common/WellForm" Expr begin

definition wwf_J_mdecl :: "J_prog  cname  J_mb mdecl  bool"
where
  "wwf_J_mdecl P C    λ(M,Ts,T,(pns,body)).
  length Ts = length pns  distinct pns  this  set pns  fv body  {this}  set pns"

lemma wwf_J_mdecl[simp]:
  "wwf_J_mdecl P C (M,Ts,T,pns,body) =
  (length Ts = length pns  distinct pns  this  set pns  fv body  {this}  set pns)"
(*<*)by(simp add:wwf_J_mdecl_def)(*>*)

abbreviation
  wwf_J_prog :: "J_prog  bool" where
  "wwf_J_prog == wf_prog wwf_J_mdecl"

end

Theory Equivalence

(*  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'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CastRed)
done
(*>*)

lemma CastRedsNull:
  "P  e,s →* null,s'  P  Cast C e,s →* null,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CastReds)
apply(rule RedCastNull)
done
(*>*)

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'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CastReds)
apply(erule (1) RedCast)
done
(*>*)

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'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CastReds)
apply(erule (1) RedCastFail)
done
(*>*)

lemma CastRedsThrow:
  " P  e,s →* throw a,s'   P  Cast C e,s →* throw a,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CastReds)
apply(rule red_reds.CastThrow)
done
(*>*)

subsubsection "LAss"

lemma LAssReds:
  "P  e,s →* e',s'  P   V:=e,s →*  V:=e',s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule LAssRed)
done
(*>*)

lemma LAssRedsVal:
  " P  e,s →* Val v,(h',l')   P   V:=e,s →* unit,(h',l'(Vv))"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule LAssReds)
apply(rule RedLAss)
done
(*>*)

lemma LAssRedsThrow:
  " P  e,s →* throw a,s'   P   V:=e,s →* throw a,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule LAssReds)
apply(rule red_reds.LAssThrow)
done
(*>*)

subsubsection "BinOp"

lemma BinOp1Reds:
  "P  e,s →* e',s'  P   e «bop» e2, s →* e' «bop» e2, s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule BinOpRed1)
done
(*>*)

lemma BinOp2Reds:
  "P  e,s →* e',s'  P  (Val v) «bop» e, s →* (Val v) «bop» e', s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule BinOpRed2)
done
(*>*)

lemma BinOpRedsVal:
  " P  e1,s0 →* Val v1,s1; P  e2,s1 →* Val v2,s2; binop(bop,v1,v2) = Some v 
   P  e1 «bop» e2, s0 →* Val v,s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp2Reds)
apply(rule RedBinOp)
apply simp
done
(*>*)

lemma BinOpRedsThrow1:
  "P  e,s →* throw e',s'  P  e «bop» e2, s →* throw e', s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp1Reds)
apply(rule red_reds.BinOpThrow1)
done
(*>*)

lemma BinOpRedsThrow2:
  " P  e1,s0 →* Val v1,s1; P  e2,s1 →* throw e,s2
   P  e1 «bop» e2, s0 →* throw e,s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp2Reds)
apply(rule red_reds.BinOpThrow2)
done
(*>*)

subsubsection "FAcc"

lemma FAccReds:
  "P  e,s →* e',s'  P  eF{D}, s →* e'F{D}, s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAccRed)
done
(*>*)

lemma FAccRedsVal:
  "P  e,s →* addr a,s'; hp s' a = Some(C,fs); fs(F,D) = Some v 
   P  eF{D},s →* Val v,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply(erule (1) RedFAcc)
done
(*>*)

lemma FAccRedsNull:
  "P  e,s →* null,s'  P  eF{D},s →* THROW NullPointer,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply(rule RedFAccNull)
done
(*>*)

lemma FAccRedsThrow:
  "P  e,s →* throw a,s'  P  eF{D},s →* throw a,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply(rule red_reds.FAccThrow)
done
(*>*)

subsubsection "FAss"

lemma FAssReds1:
  "P  e,s →* e',s'  P  eF{D}:=e2, s →* e'F{D}:=e2, s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAssRed1)
done
(*>*)

lemma FAssReds2:
  "P  e,s →* e',s'  P  Val vF{D}:=e, s →* Val vF{D}:=e', s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAssRed2)
done
(*>*)

lemma FAssRedsVal:
  " P  e1,s0 →* addr a,s1; P  e2,s1 →* Val v,(h2,l2); Some(C,fs) = h2 a  
  P  e1F{D}:=e2, s0 →* unit, (h2(a(C,fs((F,D)v))),l2)"
(*<*)
apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(rule RedFAss)
apply simp
done
(*>*)

lemma FAssRedsNull:
  " P  e1,s0 →* null,s1; P  e2,s1 →* Val v,s2  
  P  e1F{D}:=e2, s0 →* THROW NullPointer, s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(rule RedFAssNull)
done
(*>*)

lemma FAssRedsThrow1:
  "P  e,s →* throw e',s'  P  eF{D}:=e2, s →* throw e', s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds1)
apply(rule red_reds.FAssThrow1)
done
(*>*)

lemma FAssRedsThrow2:
  " P  e1,s0 →* Val v,s1; P  e2,s1 →* throw e,s2 
   P  e1F{D}:=e2,s0 →* throw e,s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(rule red_reds.FAssThrow2)
done
(*>*)

subsubsection";;"

lemma  SeqReds:
  "P  e,s →* e',s'  P  e;;e2, s →* e';;e2, s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule SeqRed)
done
(*>*)

lemma SeqRedsThrow:
  "P  e,s →* throw e',s'  P  e;;e2, s →* throw e', s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule SeqReds)
apply(rule red_reds.SeqThrow)
done
(*>*)

lemma SeqReds2:
  " P  e1,s0 →* Val v1,s1; P  e2,s1 →* e2',s2   P  e1;;e2, s0 →* e2',s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedSeq)
apply assumption
done
(*>*)


subsubsection"If"

lemma CondReds:
  "P  e,s →* e',s'  P  if (e) e1 else e2,s →* if (e') e1 else e2,s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CondRed)
done
(*>*)

lemma CondRedsThrow:
  "P  e,s →* throw a,s'  P  if (e) e1 else e2, s →* throw a,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(rule red_reds.CondThrow)
done
(*>*)

lemma CondReds2T:
  "P  e,s0 →* true,s1; P  e1, s1 →* e',s2   P  if (e) e1 else e2, s0 →* e',s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedCondT)
apply assumption
done
(*>*)

lemma CondReds2F:
  "P  e,s0 →* false,s1; P  e2, s1 →* e',s2   P  if (e) e1 else e2, s0 →* e',s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedCondF)
apply assumption
done
(*>*)


subsubsection "While"

lemma WhileFReds:
  "P  b,s →* false,s'  P  while (b) c,s →* unit,s'"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedWhile)
apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(rule RedCondF)
done
(*>*)

lemma WhileRedsThrow:
  "P  b,s →* throw e,s'  P  while (b) c,s →* throw e,s'"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedWhile)
apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(rule red_reds.CondThrow)
done
(*>*)

lemma WhileTReds:
  " P  b,s0 →* true,s1; P  c,s1 →* Val v1,s2; P  while (b) c,s2 →* e,s3 
   P  while (b) c,s0 →* e,s3"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedWhile)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedCondT)
apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedSeq)
apply assumption
done
(*>*)

lemma WhileTRedsThrow:
  " P  b,s0 →* true,s1; P  c,s1 →* throw e,s2 
   P  while (b) c,s0 →* throw e,s2"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedWhile)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedCondT)
apply(rule rtrancl_into_rtrancl)
 apply(erule SeqReds)
apply(rule red_reds.SeqThrow)
done
(*>*)

subsubsection"Throw"

lemma ThrowReds:
  "P  e,s →* e',s'  P  throw e,s →* throw e',s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ThrowRed)
done
(*>*)

lemma ThrowRedsNull:
  "P  e,s →* null,s'  P  throw e,s →* THROW NullPointer,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule ThrowReds)
apply(rule RedThrowNull)
done
(*>*)

lemma ThrowRedsThrow:
  "P  e,s →* throw a,s'  P  throw e,s →* throw a,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule ThrowReds)
apply(rule red_reds.ThrowThrow)
done
(*>*)

subsubsection "InitBlock"

lemma InitBlockReds_aux:
  "P  e,s →* e',s' 
  h l h' l' v. s = (h,l(Vv))  s' = (h',l') 
  P  {V:T := Val v; e},(h,l) →* {V:T := Val(the(l' V)); e'},(h',l'(V:=(l V)))"
(*<*)
apply(erule converse_rtrancl_induct2)
 apply(fastforce simp: fun_upd_same simp del:fun_upd_apply)
apply clarify
apply(rename_tac e0 X Y e1 h1 l1 h0 l0 h2 l2 v0)
apply(subgoal_tac "V  dom l1")
 prefer 2
 apply(drule red_lcl_incr)
 apply simp
apply clarsimp
apply(rename_tac v1)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule InitBlockRed)
  apply assumption
 apply simp
apply(erule_tac x = "l1(V := l0 V)" in allE)
apply(erule_tac x = v1 in allE)
apply(erule impE)
 apply(rule ext)
 apply(simp add:fun_upd_def)
apply(simp add:fun_upd_def)
done
(*>*)

lemma InitBlockReds:
 "P  e, (h,l(Vv)) →* 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(Vv)) →* e',(h',l'); final e'  
  P  {V:T := Val v; e},(h,l) →* e',(h', l'(V := l V))"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule InitBlockReds)
apply(fast elim!:finalE intro:RedInitBlock InitBlockThrow)
done
(*>*)


subsubsection "Block"

lemma BlockRedsFinal:
assumes reds: "P  e0,s0 →* e2,(h2,l2)" and fin: "final e2"
shows "h0 l0. s0 = (h0,l0(V:=None))  P  {V:T; e0},(h0,l0) →* e2,(h2,l2(V:=l0 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 e0 s0 e1 s1)
  have red: "P  e0,s0  e1,s1"
   and reds: "P  e1,s1 →* e2,(h2,l2)"
   and IH: "h l. s1 = (h,l(V := None))
                 P  {V:T; e1},(h,l) →* e2,(h2, l2(V := l V))"
   and s0: "s0 = (h0, l0(V := None))" by fact+
  obtain h1 l1 where s1: "s1 = (h1,l1)" by fastforce
  show ?case
  proof cases
    assume "assigned V e0"
    then obtain v e where e0: "e0 = V := Val v;; e"
      by (unfold assigned_def)blast
    from red e0 s0 have e1: "e1 = unit;;e" and s1: "s1 = (h0, l0(V  v))"
      by auto
    from e1 fin have "e1  e2" by (auto simp:final_def)
    then obtain e' s' where red1: "P  e1,s1  e',s'"
      and reds': "P  e',s' →* e2,(h2,l2)"
      using converse_rtranclE2[OF reds] by blast
    from red1 e1 have es': "e' = e" "s' = s1" by auto
    show ?case using e0 s1 es' reds'
      by(fastforce intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply)
  next
    assume unass: "¬ assigned V e0"
    show ?thesis
    proof (cases "l1 V")
      assume None: "l1 V = None"
      hence "P  {V:T; e0},(h0,l0)  {V:T; e1},(h1, l1(V := l0 V))"
        using s0 s1 red by(simp add: BlockRedNone[OF _ _ unass])
      moreover
      have "P  {V:T; e1},(h1, l1(V := l0 V)) →* e2,(h2, l2(V := l0 V))"
        using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem)
      ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
    next
      fix v assume Some: "l1 V = Some v"
      hence "P  {V:T;e0},(h0,l0)  {V:T := Val v; e1},(h1,l1(V := l0 V))"
        using s0 s1 red by(simp add: BlockRedSome[OF _ _ unass])
      moreover
      have "P  {V:T := Val v; e1},(h1,l1(V:= l0 V)) →*
                e2,(h2,l2(V:=l0 V))"
        using InitBlockRedsFinal[OF _ fin,of _ _ "l1(V:=l0 V)" V]
              Some reds s1 by(simp add:fun_upd_idem)
      ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
    qed
  qed
qed
(*>*)


subsubsection "try-catch"

lemma TryReds:
  "P  e,s →* e',s'  P  try e catch(C V) e2,s →* try e' catch(C V) e2,s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule TryRed)
done
(*>*)

lemma TryRedsVal:
  "P  e,s →* Val v,s'  P  try e catch(C V) e2,s →* Val v,s'"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule TryReds)
apply(rule RedTry)
done
(*>*)

lemma TryCatchRedsFinal:
  " P  e1,s0 →* Throw a,(h1,l1);  h1 a = Some(D,fs); P  D * C;
     P  e2, (h1, l1(V  Addr a)) →* e2', (h2,l2); final e2' 
   P  try e1 catch(C V) e2, s0 →* e2', (h2, l2(V := l1 V))"
(*<*)
apply(rule rtrancl_trans)
 apply(erule TryReds)
apply(rule converse_rtrancl_into_rtrancl)
 apply(rule RedTryCatch)
  apply fastforce
 apply assumption
apply(rule InitBlockRedsFinal)
 apply assumption
apply(simp)
done
(*>*)

lemma TryRedsFail:
  " P  e1,s →* Throw a,(h,l); h a = Some(D,fs); ¬ P  D * C 
   P  try e1 catch(C V) e2,s →* Throw a,(h,l)"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule TryReds)
apply(fastforce intro!: RedTryFail)
done
(*>*)

subsubsection "List"

lemma ListReds1:
  "P  e,s →* e',s'  P  e#es,s [→]* e' # es,s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ListRed1)
done
(*>*)

lemma ListReds2:
  "P  es,s [→]* es',s'  P  Val v # es,s [→]* Val v # es',s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ListRed2)
done
(*>*)

lemma ListRedsVal:
  " P  e,s0 →* Val v,s1; P  es,s1 [→]* es',s2 
   P  e#es,s0 [→]* Val v # es',s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule ListReds1)
apply(erule ListReds2)
done
(*>*)

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:
  " wwf_J_prog P; P  e,(h,l) →* e',(h',l')   dom l'  dom l  fv e"
(*<*)
apply(erule converse_rtrancl_induct_red)
 apply blast
apply(blast dest: Red_fv Red_dom_lcl)
done
(*>*)

text‹Now a few lemmas on the behaviour of blocks during reduction.›

(* If you want to avoid the premise "distinct" further down …
consts upd_vals :: "locals ⇒ vname list ⇒ val list ⇒ val list"
primrec
"upd_vals l [] vs = []"
"upd_vals l (V#Vs) vs = (if V ∈ set Vs then hd vs else the(l V)) #
                        upd_vals l Vs (tl vs)"

lemma [simp]: "⋀vs. length(upd_vals l Vs vs) = length Vs"
by(induct Vs, auto)
*)
lemma override_on_upd_lemma:
  "(override_on f (g(ab)) A)(a := g a) = override_on f g (insert a A)"
(*<*)
apply(rule ext)
apply(simp add:override_on_def)
done

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(Vv)"]] "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  eM(es),s →* e'M(es),s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CallObj)
done
(*>*)


lemma CallRedsParams:
 "P  es,s [→]* es',s'  P  (Val v)M(es),s →* (Val v)M(es'),s'"
(*<*)
apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CallParams)
done
(*>*)


lemma CallRedsFinal:
assumes wwf: "wwf_J_prog P"
and "P  e,s0 →* addr a,s1"
      "P  es,s1 [→]* map Val vs,(h2,l2)"
      "h2 a = Some(C,fs)" "P  C sees M:TsT = (pns,body) in D"
      "size vs = size pns"
and l2': "l2' = [this  Addr a, pns[↦]vs]"
and body: "P  body,(h2,l2') →* ef,(h3,l3)"
and "final ef"
shows "P  eM(es), s0 →* ef,(h3,l2)"
(*<*)
proof -
  have wf: "size Ts = size pns  distinct pns  this  set pns"
    and wt: "fv body  {this}  set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  from body[THEN Red_lcl_add, of l2]
  have body': "P  body,(h2,l2(this Addr a, pns[↦]vs)) →* ef,(h3,l2++l3)"
    by (simp add:l2')
  have "dom l3  {this}  set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
  hence eql2: "override_on (l2++l3) l2 ({this}  set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have "P  eM(es),s0 →* (addr a)M(es),s1" by(rule CallRedsObj)(rule assms(2))
  also have "P  (addr a)M(es),s1 →*
                 (addr a)M(map Val vs),(h2,l2)"
    by(rule CallRedsParams)(rule assms(3))
  also have "P  (addr a)M(map Val vs), (h2,l2) 
                 blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2)"
    by(rule RedCall)(auto simp: assms wf, rule assms(5))
  also (rtrancl_into_rtrancl) have "P  blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2)
                 →* ef,(h3,override_on (l2++l3) l2 ({this}  set pns))"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally show ?thesis using eql2 by simp
qed
(*>*)


lemma CallRedsThrowParams:
  " P  e,s0 →* Val v,s1;  P  es,s1 [→]* map Val vs1 @ throw a # es2,s2 
   P  eM(es),s0 →* throw a,s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsParams)
apply(rule CallThrowParams)
apply simp
done
(*>*)


lemma CallRedsThrowObj:
  "P  e,s0 →* throw a,s1  P  eM(es),s0 →* throw a,s1"
(*<*)
apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsObj)
apply(rule CallThrowObj)
done
(*>*)


lemma CallRedsNull:
  " P  e,s0 →* null,s1; P  es,s1 [→]* map Val vs,s2 
   P  eM(es),s0 →* THROW NullPointer,s2"
(*<*)
apply(rule rtrancl_trans)
 apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsParams)
apply(rule RedCallNull)
done
(*>*)

subsubsection "The main Theorem"

lemma assumes wwf: "wwf_J_prog P"
shows big_by_small: "P  e,s  e',s'  P  e,s →* e',s'"
and bigs_by_smalls: "P  es,s [⇒] es',s'  P  es,s [→]* es',s'"
(*<*)
proof (induct rule: eval_evals.inducts)
  case New thus ?case by (auto simp:RedNew)
next
  case NewFail thus ?case by (auto simp:RedNewFail)
next
  case Cast thus ?case by(fastforce intro:CastRedsAddr)
next
  case CastNull thus ?case by(simp add:CastRedsNull)
next
  case CastFail thus ?case by(fastforce intro!:CastRedsFail)
next
  case CastThrow thus ?case by(auto dest!:eval_final simp:CastRedsThrow)
next
  case Val thus ?case by simp
next
  case BinOp thus ?case by(auto simp:BinOpRedsVal)
next
  case BinOpThrow1 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow1)
next
  case BinOpThrow2 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow2)
next
  case Var thus ?case by (auto simp:RedVar)
next
  case LAss thus ?case by(auto simp: LAssRedsVal)
next
  case LAssThrow thus ?case by(auto dest!:eval_final simp: LAssRedsThrow)
next
  case FAcc thus ?case by(auto intro:FAccRedsVal)
next
  case FAccNull thus ?case by(simp add:FAccRedsNull)
next
  case FAccThrow thus ?case by(auto dest!:eval_final simp:FAccRedsThrow)
next
  case FAss thus ?case by(auto simp:FAssRedsVal)
next
  case FAssNull thus ?case by(auto simp:FAssRedsNull)
next
  case FAssThrow1 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow1)
next
  case FAssThrow2 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow2)
next
  case CallObjThrow thus ?case by(auto dest!:eval_final simp:CallRedsThrowObj)
next
  case CallNull thus ?case by(simp add:CallRedsNull)
next
  case CallParamsThrow thus ?case
    by(auto dest!:evals_final simp:CallRedsThrowParams)
next
  case (Call e s0 a s1 ps vs h2 l2 C fs M Ts T pns body D l2' e' h3 l3)
  have IHe: "P  e,s0 →* addr a,s1"
    and IHes: "P  ps,s1 [→]* map Val vs,(h2,l2)"
    and h2a: "h2 a = Some(C,fs)"
    and "method": "P  C sees M:TsT = (pns,body) in D"
    and same_length: "length vs = length pns"
    and l2': "l2' = [this  Addr a, pns[↦]vs]"
    and eval_body: "P  body,(h2, l2')  e',(h3, l3)"
    and IHbody: "P  body,(h2,l2') →* e',(h3,l3)" by fact+
  show "P  eM(ps),s0 →* e',(h3, l2)"
    using "method" same_length l2' h2a IHbody eval_final[OF eval_body]
    by(fastforce intro:CallRedsFinal[OF wwf IHe IHes])
next
  case Block thus ?case by(auto simp: BlockRedsFinal dest:eval_final)
next
  case Seq thus ?case by(auto simp:SeqReds2)
next
  case SeqThrow thus ?case by(auto dest!:eval_final simp: SeqRedsThrow)
next
  case CondT thus ?case by(auto simp:CondReds2T)
next
  case CondF thus ?case by(auto simp:CondReds2F)
next
  case CondThrow thus ?case by(auto dest!:eval_final simp:CondRedsThrow)
next
  case WhileF thus ?case by(auto simp:WhileFReds)
next
  case WhileT thus ?case by(auto simp: WhileTReds)
next
  case WhileCondThrow thus ?case by(auto dest!:eval_final simp: WhileRedsThrow)
next
  case WhileBodyThrow thus ?case by(auto dest!:eval_final simp: WhileTRedsThrow)
next
  case Throw thus ?case by(auto simp:ThrowReds)
next
  case ThrowNull thus ?case by(auto simp:ThrowRedsNull)
next
  case ThrowThrow thus ?case by(auto dest!:eval_final simp:ThrowRedsThrow)
next
  case Try thus ?case by(simp add:TryRedsVal)
next
  case TryCatch thus ?case by(fast intro!: TryCatchRedsFinal dest!:eval_final)
next
  case TryThrow thus ?case by(fastforce intro!:TryRedsFail)
next
  case Nil thus ?case by simp
next
  case Cons thus ?case
    by(fastforce intro!:Cons_eq_appendI[OF refl refl] ListRedsVal)
next
  case ConsThrow thus ?case by(fastforce