Theory TypeSafe

(*  Title:      HOL/Bali/TypeSafe.thy
    Author:     David von Oheimb and Norbert Schirmer
*)
subsection ‹The type soundness proof for Java›

theory TypeSafe
imports DefiniteAssignmentCorrect Conform
begin

subsubsection "error free"
 
lemma error_free_halloc:
  assumes halloc: "Gs0 ─halloc oia s1" and
          error_free_s0: "error_free s0"
  shows "error_free s1"
proof -
  from halloc error_free_s0
  obtain abrupt0 store0 abrupt1 store1
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
          halloc': "G(abrupt0,store0) ─halloc oia (abrupt1,store1)" and
          error_free_s0': "error_free (abrupt0,store0)"
    by (cases s0,cases s1) auto
  from halloc' error_free_s0'
  have "error_free (abrupt1,store1)"
  proof (induct)
    case Abrupt 
    then show ?case .
  next
    case New
    then show ?case
      by auto
  qed
  with eqs 
  show ?thesis
    by simp
qed

lemma error_free_sxalloc:
  assumes sxalloc: "Gs0 ─sxalloc→ s1" and error_free_s0: "error_free s0"
  shows "error_free s1"
proof -
  from sxalloc error_free_s0
  obtain abrupt0 store0 abrupt1 store1
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
          sxalloc': "G(abrupt0,store0) ─sxalloc→ (abrupt1,store1)" and
          error_free_s0': "error_free (abrupt0,store0)"
    by (cases s0,cases s1) auto
  from sxalloc' error_free_s0'
  have "error_free (abrupt1,store1)"
  proof (induct)
  qed (auto)
  with eqs 
  show ?thesis 
    by simp
qed

lemma error_free_check_field_access_eq:
 "error_free (check_field_access G accC statDeclC fn stat a s)
  (check_field_access G accC statDeclC fn stat a s) = s"
apply (cases s)
apply (auto simp add: check_field_access_def Let_def error_free_def 
                      abrupt_if_def 
            split: if_split_asm)
done

lemma error_free_check_method_access_eq:
"error_free (check_method_access G accC statT mode sig a' s)
  (check_method_access G accC statT mode sig a' s) = s"
apply (cases s)
apply (auto simp add: check_method_access_def Let_def error_free_def 
                      abrupt_if_def)
done

lemma error_free_FVar_lemma: 
     "error_free s 
        error_free (abupd (if stat then id else np a) s)"
  by (case_tac s) auto

lemma error_free_init_lvars [simp,intro]:
"error_free s  
  error_free (init_lvars G C sig mode a pvs s)"
by (cases s) (auto simp add: init_lvars_def Let_def)

lemma error_free_LVar_lemma:   
"error_free s  error_free (assign (λv. supd lupd(vnv)) w s)"
by (cases s) simp

lemma error_free_throw [simp,intro]:
  "error_free s  error_free (abupd (throw x) s)"
by (cases s) (simp add: throw_def)


subsubsection "result conformance"

definition
  assign_conforms :: "st  (val  state  state)  ty  env'  bool" ("_≤|__∷≼_" [71,71,71,71] 70)
where
  "s≤|fT∷≼E =
   ((s' w. Norm s'∷≼E  fst E,s'w∷≼T  s≤|s'  assign f w (Norm s')∷≼E) 
    (s' w. error_free s'  (error_free (assign f w s'))))"


definition
  rconf :: "prog  lenv  st  term  vals  tys  bool" ("_,_,___∷≼_" [71,71,71,71,71,71] 70)
where
  "G,L,stv∷≼T =
    (case T of
      Inl T   if ( var. t=In2 var)
                then ( n. (the_In2 t) = LVar n 
                        (fst (the_In2 v) = the (locals s n)) 
                           (locals s n  None  G,sfst (the_In2 v)∷≼T)) 
                    (¬ ( n. the_In2 t=LVar n)  (G,sfst (the_In2 v)∷≼T))
                    (s≤|snd (the_In2 v)T∷≼(G,L))
                else G,sthe_In1 v∷≼T
    | Inr Ts  list_all2 (conf G s) (the_In3 v) Ts)"

text ‹
 With termrconf we describe the conformance of the result value of a term.
 This definition gets rather complicated because of the relations between the
 injections of the different terms, types and values. The main case distinction
 is between single values and value lists. In case of value lists, every 
 value has to conform to its type. For single values we have to do a further
 case distinction, between values of variables termvar. t=In2 var and
 ordinary values. Values of variables are modelled as pairs consisting of the
 current value and an update function which will perform an assignment to the
 variable. This stems form the decision, that we only have one evaluation rule
 for each kind of variable. The decision if we read or write to the 
 variable is made by syntactic enclosing rules. So conformance of 
 variable-values must ensure that both the current value and an update will 
 conform to the type. With the introduction of definite assignment of local
 variables we have to do another case distinction. For the notion of conformance
 local variables are allowed to be termNone, since the definedness is not 
 ensured by conformance but by definite assignment. Field and array variables 
 must contain a value. 
›
 


lemma rconf_In1 [simp]: 
 "G,L,sIn1 ecIn1 v ∷≼Inl T  =  G,sv∷≼T"
apply (unfold rconf_def)
apply (simp (no_asm))
done

lemma rconf_In2_no_LVar [simp]: 
 " n. vaLVar n  
   G,L,sIn2 vaIn2 vf∷≼Inl T  = (G,sfst vf∷≼T  s≤|snd vfT∷≼(G,L))"
apply (unfold rconf_def)
apply auto
done

lemma rconf_In2_LVar [simp]: 
 "va=LVar n  
   G,L,sIn2 vaIn2 vf∷≼Inl T  
    = ((fst vf = the (locals s n)) 
       (locals s n  None  G,sfst vf∷≼T)  s≤|snd vfT∷≼(G,L))"
apply (unfold rconf_def)
by simp

lemma rconf_In3 [simp]: 
 "G,L,sIn3 esIn3 vs∷≼Inr Ts = list_all2 (λv T. G,sv∷≼T) vs Ts"
apply (unfold rconf_def)
apply (simp (no_asm))
done

subsubsection "fits and conf"

(* unused *)
lemma conf_fits: "G,sv∷≼T  G,sv fits T"
apply (unfold fits_def)
apply clarify
apply (erule contrapos_np, simp (no_asm_use))
apply (drule conf_RefTD)
apply auto
done

lemma fits_conf: 
  "G,sv∷≼T; GT≼? T'; G,sv fits T'; ws_prog G  G,sv∷≼T'"
apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
apply (force dest: conf_RefTD intro: conf_AddrI)
done

lemma fits_Array: 
 "G,sv∷≼T; GT'.[]T.[]; G,sv fits T'; ws_prog G  G,sv∷≼T'"
apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
apply (force dest: conf_RefTD intro: conf_AddrI)
done



subsubsection "gext"

lemma halloc_gext: "s1 s2. Gs1 ─halloc oia s2  snd s1≤|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule halloc.induct)
apply  (auto dest!: new_AddrD)
done

lemma sxalloc_gext: "s1 s2. Gs1 ─sxalloc→ s2  snd s1≤|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule sxalloc.induct)
apply   (auto dest!: halloc_gext)
done

lemma eval_gext_lemma [rule_format (no_asm)]: 
 "Gs t≻→ (w,s')  snd s≤|snd s'  (case w of  
    In1 v  True  
  | In2 vf  normal s  (v x s. s≤|snd (assign (snd vf) v (x,s)))  
  | In3 vs  True)"
apply (erule eval_induct)
prefer 26 
  apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
 simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
            check_field_access_def check_method_access_def Let_def
 split del: if_split_asm split: sum3.split)
(* 6 subgoals *)
apply force+
done

lemma evar_gext_f: 
  "GNorm s1 e=≻vf  s2  s≤|snd (assign (snd vf) v (x,s))"
apply (drule eval_gext_lemma [THEN conjunct2])
apply auto
done

lemmas eval_gext = eval_gext_lemma [THEN conjunct1]

lemma eval_gext': "G(x1,s1) t≻→ (w,(x2,s2))  s1≤|s2"
apply (drule eval_gext)
apply auto
done

lemma init_yields_initd: "GNorm s1 Init C s2  initd C s2"
apply (erule eval_cases , auto split del: if_split_asm)
apply (case_tac "inited C (globs s1)")
apply  (clarsimp split del: if_split_asm)+
apply (drule eval_gext')+
apply (drule init_class_obj_inited)
apply (erule inited_gext)
apply (simp (no_asm_use))
done


subsubsection "Lemmas"

lemma obj_ty_obj_class1: 
 "wf_prog G; is_type G (obj_ty obj)  is_class G (obj_class obj)"
apply (case_tac "tag obj")
apply (auto simp add: obj_ty_def obj_class_def)
done

lemma oconf_init_obj: 
 "wf_prog G;  
 (case r of Heap a  is_type G (obj_ty obj) | Stat C  is_class G C)
  G,sobj values:=init_vals (var_tys G (tag obj) r)∷≼√r"
apply (auto intro!: oconf_init_obj_lemma unique_fields)
done

lemma conforms_newG: "globs s oref = None; (x, s)∷≼(G,L);   
  wf_prog G; case oref of Heap a  is_type G (obj_ty tag=oi,values=vs)  
                        | Stat C  is_class G C   
  (x, init_obj G oi oref s)∷≼(G, L)"
apply (unfold init_obj_def)
apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
            )
done

lemma conforms_init_class_obj: 
 "(x,s)∷≼(G, L); wf_prog G; class G C=Some y; ¬ inited C (globs s)  
  (x,init_class_obj G C s)∷≼(G, L)"
apply (rule not_initedD [THEN conforms_newG])
apply    (auto)
done


lemma fst_init_lvars[simp]: 
 "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
  (if is_static m then x else (np a') x)"
apply (simp (no_asm) add: init_lvars_def2)
done


lemma halloc_conforms: "s1. Gs1 ─halloc oia s2; wf_prog G; s1∷≼(G, L); 
  is_type G (obj_ty tag=oi,values=fs)  s2∷≼(G, L)"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (case_tac "aa")
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
       intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
done

lemma halloc_type_sound: 
"s1. Gs1 ─halloc oia (x,s); wf_prog G; s1∷≼(G, L);
  T = obj_ty tag=oi,values=fs; is_type G T   
  (x,s)∷≼(G, L)  (x = None  G,sAddr a∷≼T)"
apply (auto elim!: halloc_conforms)
apply (case_tac "aa")
apply (subst obj_ty_eq)
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
done

lemma sxalloc_type_sound: 
 "s1 s2. Gs1 ─sxalloc→ s2; wf_prog G  
  case fst s1 of  
    None  s2 = s1 
  | Some abr  (case abr of
                   Xcpt x  (a. fst s2 = Some(Xcpt (Loc a))  
                                  (L. s1∷≼(G,L)  s2∷≼(G,L)))
                 | Jump j  s2 = s1
                 | Error e  s2 = s1)"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule sxalloc.induct)
apply   auto
apply (rule halloc_conforms [THEN conforms_xconf])
apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
done

lemma wt_init_comp_ty: 
"is_acc_type G (pid C) T  prg=G,cls=C,lcl=Linit_comp_ty T∷√"
apply (unfold init_comp_ty_def)
apply (clarsimp simp add: accessible_in_RefT_simp 
                          is_acc_type_def is_acc_class_def)
done


declare fun_upd_same [simp]

declare fun_upd_apply [simp del]

definition
  DynT_prop :: "[prog,inv_mode,qtname,ref_ty]  bool" ("____"[71,71,71,71]70)
where
  "GmodeDt = (mode = IntVir  is_class G D  
                     (if (T. t=ArrayT T) then D=Object else GClass DRefT t))"

lemma DynT_propI: 
 "(x,s)∷≼(G, L); G,sa'∷≼RefT statT; wf_prog G; mode = IntVir  a'  Null 
    Gmodeinvocation_class mode s a' statTstatT"
proof (unfold DynT_prop_def)
  assume state_conform: "(x,s)∷≼(G, L)"
     and      statT_a': "G,sa'∷≼RefT statT"
     and            wf: "wf_prog G"
     and          mode: "mode = IntVir  a'  Null"
  let ?invCls = "(invocation_class mode s a' statT)"
  let ?IntVir = "mode = IntVir"
  let ?Concl  = "λinvCls. is_class G invCls 
                          (if T. statT = ArrayT T
                                  then invCls = Object
                                  else GClass invClsRefT statT)"
  show "?IntVir  ?Concl ?invCls"
  proof  
    assume modeIntVir: ?IntVir 
    with mode have not_Null: "a'  Null" ..
    from statT_a' not_Null state_conform 
    obtain a obj 
      where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
                        "Gobj_ty objRefT statT" "is_type G (obj_ty obj)"
      by (blast dest: conforms_RefTD)
    show "?Concl ?invCls"
    proof (cases "tag obj")
      case CInst
      with modeIntVir obj_props
      show ?thesis 
        by (auto dest!: widen_Array2)
    next
      case Arr
      from Arr obtain T where "obj_ty obj = T.[]" by blast
      moreover from Arr have "obj_class obj = Object" 
        by blast
      moreover note modeIntVir obj_props wf 
      ultimately show ?thesis by (auto dest!: widen_Array )
    qed
  qed
qed

lemma invocation_methd:
"wf_prog G; statT  NullT; 
 ( statC. statT = ClassT statC  is_class G statC);
 (     I. statT = IfaceT I  is_iface G I  mode  SuperM);
 (     T. statT = ArrayT T  mode  SuperM);
 Gmodeinvocation_class mode s a' statTstatT;  
 dynlookup G statT (invocation_class mode s a' statT) sig = Some m  
 methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
proof -
  assume         wf: "wf_prog G"
     and  not_NullT: "statT  NullT"
     and statC_prop: "( statC. statT = ClassT statC  is_class G statC)"
     and statI_prop: "( I. statT = IfaceT I  is_iface G I  mode  SuperM)"
     and statA_prop: "(     T. statT = ArrayT T  mode  SuperM)"
     and  invC_prop: "Gmodeinvocation_class mode s a' statTstatT"
     and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
                      = Some m"
  show ?thesis
  proof (cases statT)
    case NullT
    with not_NullT show ?thesis by simp
  next
    case IfaceT
    with statI_prop obtain I 
      where    statI: "statT = IfaceT I" and 
            is_iface: "is_iface G I"     and
          not_SuperM: "mode  SuperM" by blast            
    
    show ?thesis 
    proof (cases mode)
      case Static
      with wf dynlookup statI is_iface 
      show ?thesis
        by (auto simp add: invocation_declclass_def dynlookup_def 
                           dynimethd_def dynmethd_C_C 
                    intro: dynmethd_declclass
                    dest!: wf_imethdsD
                     dest: table_of_map_SomeI)
    next        
      case SuperM
      with not_SuperM show ?thesis ..
    next
      case IntVir
      with wf dynlookup IfaceT invC_prop show ?thesis 
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
                           DynT_prop_def
                    intro: methd_declclass dynmethd_declclass)
    qed
  next
    case ClassT
    show ?thesis
    proof (cases mode)
      case Static
      with wf ClassT dynlookup statC_prop 
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
                               intro: dynmethd_declclass)
    next
      case SuperM
      with wf ClassT dynlookup statC_prop 
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
                               intro: dynmethd_declclass)
    next
      case IntVir
      with wf ClassT dynlookup statC_prop invC_prop 
      show ?thesis
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
                           DynT_prop_def
                    intro: dynmethd_declclass)
    qed
  next
    case ArrayT
    show ?thesis
    proof (cases mode)
      case Static
      with wf ArrayT dynlookup show ?thesis
        by (auto simp add: invocation_declclass_def dynlookup_def 
                           dynimethd_def dynmethd_C_C
                    intro: dynmethd_declclass
                     dest: table_of_map_SomeI)
    next
      case SuperM
      with ArrayT statA_prop show ?thesis by blast
    next
      case IntVir
      with wf ArrayT dynlookup invC_prop show ?thesis
        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
                           DynT_prop_def dynmethd_C_C
                    intro: dynmethd_declclass
                     dest: table_of_map_SomeI)
    qed
  qed
qed

lemma DynT_mheadsD: 
"Ginvmode sm einvCstatT; 
  wf_prog G; prg=G,cls=C,lcl=Le∷-RefT statT; 
  (statDeclT,sm)  mheads G C statT sig; 
  invC = invocation_class (invmode sm e) s a' statT;
  declC =invocation_declclass G (invmode sm e) s a' statT sig
   
   dm. 
  methd G declC sig = Some dm  dynlookup G statT invC sig = Some dm   
  GresTy (mthd dm)resTy sm  
  wf_mdecl G declC (sig, mthd dm) 
  declC = declclass dm 
  is_static dm = is_static sm   
  is_class G invC  is_class G declC   GinvCC declC   
  (if invmode sm e = IntVir
      then ( statC. statT=ClassT statC  GinvC C statC)
      else (  ( statC. statT=ClassT statC  GstatCC declC)
             ( statC. statTClassT statC  declC=Object))  
            statDeclT = ClassT (declclass dm))"
proof -
  assume invC_prop: "Ginvmode sm einvCstatT" 
     and        wf: "wf_prog G" 
     and      wt_e: "prg=G,cls=C,lcl=Le∷-RefT statT"
     and        sm: "(statDeclT,sm)  mheads G C statT sig" 
     and      invC: "invC = invocation_class (invmode sm e) s a' statT"
     and     declC: "declC = 
                    invocation_declclass G (invmode sm e) s a' statT sig"
  from wt_e wf have type_statT: "is_type G (RefT statT)"
    by (auto dest: ty_expr_is_type)
  from sm have not_Null: "statT  NullT" by auto
  from type_statT 
  have wf_C: "( statC. statT = ClassT statC  is_class G statC)"
    by (auto)
  from type_statT wt_e 
  have wf_I: "(I. statT = IfaceT I  is_iface G I  
                                        invmode sm e  SuperM)"
    by (auto dest: invocationTypeExpr_noClassD)
  from wt_e
  have wf_A: "(     T. statT = ArrayT T  invmode sm e  SuperM)"
    by (auto dest: invocationTypeExpr_noClassD)
  show ?thesis
  proof (cases "invmode sm e = IntVir")
    case True
    with invC_prop not_Null
    have invC_prop': " is_class G invC  
                      (if (T. statT=ArrayT T) then invC=Object 
                                              else GClass invCRefT statT)"
      by (auto simp add: DynT_prop_def) 
    from True 
    have "¬ is_static sm"
      by (simp add: invmode_IntVir_eq member_is_static_simp)
    with invC_prop' not_Null
    have "G,statT  invC valid_lookup_cls_for (is_static sm)"
      by (cases statT) auto
    with sm wf type_statT obtain dm where
           dm: "dynlookup G statT invC sig = Some dm" and
      resT_dm: "GresTy (mthd dm)resTy sm"      and
       static: "is_static dm = is_static sm"
      by  - (drule dynamic_mheadsD,force+)
    with declC invC not_Null 
    have declC': "declC = (declclass dm)" 
      by (auto simp add: invocation_declclass_def)
    with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
    have dm': "methd G declC sig = Some dm"
      by - (drule invocation_methd,auto)
    from wf dm invC_prop' declC' type_statT 
    have declC_prop: "GinvC C declC  is_class G declC"
      by (auto dest: dynlookup_declC)
    from wf dm' declC_prop declC' 
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
      by (auto dest: methd_wf_mdecl)
    from invC_prop' 
    have statC_prop: "( statC. statT=ClassT statC  GinvC C statC)"
      by auto
    from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
         dm
    show ?thesis by auto
  next
    case False
    with type_statT wf invC not_Null wf_I wf_A
    have invC_prop': "is_class G invC   
                     (( statC. statT=ClassT statC  invC=statC) 
                      ( statC. statTClassT statC  invC=Object))"
        by (case_tac "statT") (auto simp add: invocation_class_def 
                                       split: inv_mode.splits)
    with not_Null wf
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
                                            dynimethd_def)
    from sm wf wt_e not_Null False invC_prop' obtain "dm" where
                    dm: "methd G invC sig = Some dm"          and
        eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
             eq_mheads:"sm=mhead (mthd dm) "
      by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
    then have static: "is_static dm = is_static sm" by - (auto)
    with declC invC dynlookup_static dm
    have declC': "declC = (declclass dm)"  
      by (auto simp add: invocation_declclass_def)
    from invC_prop' wf declC' dm 
    have dm': "methd G declC sig = Some dm"
      by (auto intro: methd_declclass)
    from dynlookup_static dm 
    have dm'': "dynlookup G statT invC sig = Some dm"
      by simp
    from wf dm invC_prop' declC' type_statT 
    have declC_prop: "GinvC C declC  is_class G declC"
      by (auto dest: methd_declC )
    then have declC_prop1: "invC=Object  declC=Object"  by auto
    from wf dm' declC_prop declC' 
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
      by (auto dest: methd_wf_mdecl)
    from invC_prop' declC_prop declC_prop1
    have statC_prop: "(   ( statC. statT=ClassT statC  GstatCC declC)
                         ( statC. statTClassT statC  declC=Object))" 
      by auto
    from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
         eq_declC_sm_dm eq_mheads static
    show ?thesis by auto
  qed
qed

corollary DynT_mheadsE [consumes 7]: 
― ‹Same as DynT_mheadsD› but better suited for application in 
typesafety proof›
 assumes invC_compatible: "GmodeinvCstatT" 
     and wf: "wf_prog G" 
     and wt_e: "prg=G,cls=C,lcl=Le∷-RefT statT"
     and mheads: "(statDeclT,sm)  mheads G C statT sig"
     and mode: "mode=invmode sm e" 
     and invC: "invC = invocation_class mode s a' statT"
     and declC: "declC =invocation_declclass G mode s a' statT sig"
     and dm: " dm. methd G declC sig = Some dm; 
                      dynlookup G statT invC sig = Some dm; 
                      GresTy (mthd dm)resTy sm; 
                      wf_mdecl G declC (sig, mthd dm);
                      declC = declclass dm;
                      is_static dm = is_static sm;  
                      is_class G invC; is_class G declC; GinvCC declC;  
                      (if invmode sm e = IntVir
                      then ( statC. statT=ClassT statC  GinvC C statC)
                      else (  ( statC. statT=ClassT statC  GstatCC declC)
                              ( statC. statTClassT statC  declC=Object)) 
                             statDeclT = ClassT (declclass dm))  P"
   shows "P"
proof -
    from invC_compatible mode have "Ginvmode sm einvCstatT" by simp 
    moreover note wf wt_e mheads
    moreover from invC mode 
    have "invC = invocation_class (invmode sm e) s a' statT" by simp
    moreover from declC mode 
    have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
    ultimately show ?thesis
      by (rule DynT_mheadsD [THEN exE,rule_format])
         (elim conjE,rule dm)
qed
   

lemma DynT_conf: "Ginvocation_class mode s a' statT C declC; wf_prog G;
 isrtype G (statT);
 G,sa'∷≼RefT statT; mode = IntVir  a'  Null;  
  mode  IntVir     ( statC. statT=ClassT statC  GstatCC declC)
                      ( statC. statTClassT statC  declC=Object) 
 G,sa'∷≼ Class declC"
apply (case_tac "mode = IntVir")
apply (drule conf_RefTD)
apply (force intro!: conf_AddrI 
            simp add: obj_class_def split: obj_tag.split_asm)
apply  clarsimp
apply  safe
apply    (erule (1) widen.subcls [THEN conf_widen])
apply    (erule wf_ws_prog)

apply    (frule widen_Object) apply (erule wf_ws_prog)
apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
done

lemma Ass_lemma:
" GNorm s0 var=≻(w, f) Norm s1; GNorm s1 e-≻v Norm s2;
   G,s2v∷≼eT;s1≤|s2  assign f v (Norm s2)∷≼(G, L)
 assign f v (Norm s2)∷≼(G, L) 
      (normal (assign f v (Norm s2))  G,store (assign f v (Norm s2))v∷≼eT)"
apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
apply (drule eval_gext', clarsimp)
apply (erule conf_gext)
apply simp
done

lemma Throw_lemma: "GtnC SXcpt Throwable; wf_prog G; (x1,s1)∷≼(G, L);  
    x1 = None  G,s1a'∷≼ Class tn  (throw a' x1, s1)∷≼(G, L)"
apply (auto split: split_abrupt_if simp add: throw_def2)
apply (erule conforms_xconf)
apply (frule conf_RefTD)
apply (auto elim: widen.subcls [THEN conf_widen])
done

lemma Try_lemma: "Gobj_ty (the (globs s1' (Heap a))) Class tn; 
 (Some (Xcpt (Loc a)), s1')∷≼(G, L); wf_prog G 
  Norm (lupd(vnAddr a) s1')∷≼(G, L(vnClass tn))"
apply (rule conforms_allocL)
apply  (erule conforms_NormI)
apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
apply (auto intro!: conf_AddrI)
done

lemma Fin_lemma: 
"GNorm s1 c2 (x2,s2); wf_prog G; (Some a, s1)∷≼(G, L); (x2,s2)∷≼(G, L);
  dom (locals s1)  dom (locals s2) 
  (abrupt_if True (Some a) x2, s2)∷≼(G, L)"
apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if)
done

lemma FVar_lemma1: 
"table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
  x2 = None  G,s2a∷≼ Class statC; wf_prog G; GstatCC statDeclC; 
  statDeclC  Object; 
  class G statDeclC = Some y; (x2,s2)∷≼(G, L); s1≤|s2; 
  inited statDeclC (globs s1); 
  (if static f then id else np a) x2 = None 
   
  obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
                  = Some obj  
  var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
          (Inl(fn,statDeclC)) = Some (type f)"
apply (drule initedD)
apply (frule subcls_is_class2, simp (no_asm_simp))
apply (case_tac "static f")
apply  clarsimp
apply  (drule (1) rev_gext_objD, clarsimp)
apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
apply  (rule var_tys_Some_eq [THEN iffD2])
apply  clarsimp
apply  (erule fields_table_SomeI, simp (no_asm))
apply clarsimp
apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
apply (auto dest!: widen_Array split: obj_tag.split)
apply (rule fields_table_SomeI)
apply (auto elim!: fields_mono subcls_is_class2)
done

lemma FVar_lemma2: "error_free state
        error_free
           (assign
             (λv. supd
                   (upd_gobj
                     (if static field then Inr statDeclC
                      else Inl (the_Addr a))
                     (Inl (fn, statDeclC)) v))
             w state)"
proof -
  assume error_free: "error_free state"
  obtain a s where "state=(a,s)"
    by (cases state)
  with error_free
  show ?thesis
    by (cases a) auto
qed

declare split_paired_All [simp del] split_paired_Ex [simp del] 
declare if_split     [split del] if_split_asm     [split del] 
        option.split [split del] option.split_asm [split del]
setup map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")
setup map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")

lemma FVar_lemma: 
"((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
  GstatCC statDeclC;  
  table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
  wf_prog G;   
  x2 = None  G,s2a∷≼Class statC; 
  statDeclC  Object; class G statDeclC = Some y;   
  (x2, s2)∷≼(G, L); s1≤|s2; inited statDeclC (globs s1)   
  G,s2'v∷≼type field  s2'≤|ftype field∷≼(G, L)"
apply (unfold assign_conforms_def)
apply (drule sym)
apply (clarsimp simp add: fvar_def2)
apply (drule (9) FVar_lemma1)
apply (clarsimp)
apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
apply clarsimp
apply (rule conjI)
apply   clarsimp
apply   (drule (1) rev_gext_objD)
apply   (force elim!: conforms_upd_gobj)

apply   (blast intro: FVar_lemma2)
done
declare split_paired_All [simp] split_paired_Ex [simp] 
declare if_split     [split] if_split_asm     [split] 
        option.split [split] option.split_asm [split]
setup map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))
setup map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))


lemma AVar_lemma1: "globs s (Inl a) = Some obj;tag obj=Arr ty i; 
 the_Intg i' in_bounds i; wf_prog G; Gty.[]Tb.[]; Norm s∷≼(G, L)
  G,sthe ((values obj) (Inr (the_Intg i')))∷≼Tb"
apply (erule widen_Array_Array [THEN conf_widen])
apply  (erule_tac [2] wf_ws_prog)
apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
defer apply assumption
apply (force intro: var_tys_Some_eq [THEN iffD2])
done

lemma obj_split: " t vs. obj = tag=t,values=vs"
  by (cases obj) auto
 
lemma AVar_lemma2: "error_free state 
        error_free
           (assign
             (λv (x, s').
                 ((raise_if (¬ G,s'v fits T) ArrStore) x,
                  upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
             w state)"
proof -
  assume error_free: "error_free state"
  obtain a s where "state=(a,s)"
    by (cases state)
  with error_free
  show ?thesis
    by (cases a) auto
qed

lemma AVar_lemma: "wf_prog G; G(x1, s1) e2-≻i (x2, s2);  
  ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None  G,s1a∷≼Ta.[];  
  (x2, s2)∷≼(G, L); s1≤|s2  G,s2'v∷≼Ta  s2'≤|fTa∷≼(G, L)"
apply (unfold assign_conforms_def)
apply (drule sym)
apply (clarsimp simp add: avar_def2)
apply (drule (1) conf_gext)
apply (drule conf_RefTD, clarsimp)
apply (subgoal_tac " t vs. obj = tag=t,values=vs")
defer
apply   (rule obj_split)
apply clarify
apply (frule obj_ty_widenD)
apply (auto dest!: widen_Class)
apply   (force dest: AVar_lemma1)

apply   (force elim!: fits_Array dest: gext_objD 
         intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
done


subsubsection "Call"

lemma conforms_init_lvars_lemma: "wf_prog G;  
  wf_mhead G P sig mh;
  list_all2 (conf G s) pvs pTsa; GpTsa[≼](parTs sig)   
  G,sMap.empty (pars mh[↦]pvs)
      [∼∷≼](table_of lvars)(pars mh[↦]parTs sig)"
apply (unfold wf_mhead_def)
apply clarify
apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
apply (drule wf_ws_prog)
apply (erule (2) conf_list_widen)
done


lemma lconf_map_lname [simp]: 
  "G,s(case_lname l1 l2)[∷≼](case_lname L1 L2)
   =
  (G,sl1[∷≼]L1  G,s(λx::unit . l2)[∷≼](λx::unit. L2))"
apply (unfold lconf_def)
apply (auto split: lname.splits)
done

lemma wlconf_map_lname [simp]: 
  "G,s(case_lname l1 l2)[∼∷≼](case_lname L1 L2)
   =
  (G,sl1[∼∷≼]L1  G,s(λx::unit . l2)[∼∷≼](λx::unit. L2))"
apply (unfold wlconf_def)
apply (auto split: lname.splits)
done

lemma lconf_map_ename [simp]:
  "G,s(case_ename l1 l2)[∷≼](case_ename L1 L2)
   =
  (G,sl1[∷≼]L1  G,s(λx::unit. l2)[∷≼](λx::unit. L2))"
apply (unfold lconf_def)
apply (auto split: ename.splits)
done

lemma wlconf_map_ename [simp]:
  "G,s(case_ename l1 l2)[∼∷≼](case_ename L1 L2)
   =
  (G,sl1[∼∷≼]L1  G,s(λx::unit. l2)[∼∷≼](λx::unit. L2))"
apply (unfold wlconf_def)
apply (auto split: ename.splits)
done



lemma defval_conf1 [rule_format (no_asm), elim]: 
  "is_type G T  (vSome (default_val T): G,sv∷≼T)"
apply (unfold conf_def)
apply (induct "T")
apply (auto intro: prim_ty.induct)
done

lemma np_no_jump: "xSome (Jump j)  (np a') x  Some (Jump j)"
by (auto simp add: abrupt_if_def)

declare split_paired_All [simp del] split_paired_Ex [simp del] 
declare if_split     [split del] if_split_asm     [split del] 
        option.split [split del] option.split_asm [split del]
setup map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")
setup map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")

lemma conforms_init_lvars: 
"wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
  list_all2 (conf G s) pvs pTsa; GpTsa[≼](parTs sig);  
  (x, s)∷≼(G, L); 
  methd G declC sig = Some dm;  
  isrtype G statT;
  GinvCC declC; 
  G,sa'∷≼RefT statT;  
  invmode (mhd sm) e = IntVir  a'  Null; 
  invmode (mhd sm) e  IntVir   
       ( statC. statT=ClassT statC  GstatCC declC)
      ( statC. statTClassT statC  declC=Object);
  invC  = invocation_class (invmode (mhd sm) e) s a' statT;
  declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
  xSome (Jump Ret) 
    
  init_lvars G declC sig (invmode (mhd sm) e) a'  
  pvs (x,s)∷≼(G,λ k. 
                (case k of
                   EName e  (case e of 
                                 VNam v 
                                   ((table_of (lcls (mbody (mthd dm))))
                                        (pars (mthd dm)[↦]parTs sig)) v
                               | Res  Some (resTy (mthd dm)))
                 | This  if (is_static (mthd sm)) 
                              then None else Some (Class declC)))"
apply (simp add: init_lvars_def2)
apply (rule conforms_set_locals)
apply  (simp (no_asm_simp) split: if_split)
apply (drule  (4) DynT_conf)
apply clarsimp
(* apply intro *)
apply (drule (3) conforms_init_lvars_lemma 
                 [where ?lvars="(lcls (mbody (mthd dm)))"])
apply (case_tac "dm",simp)
apply (rule conjI)
apply (unfold wlconf_def, clarify)
apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
apply   (case_tac "is_static sm")
apply     simp
apply     simp

apply   simp
apply   (case_tac "is_static sm")
apply     simp
apply     (simp add: np_no_jump)
done
declare split_paired_All [simp] split_paired_Ex [simp] 
declare if_split     [split] if_split_asm     [split] 
        option.split [split] option.split_asm [split]
setup map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))
setup map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))


subsection "accessibility"

theorem dynamic_field_access_ok:
  assumes wf: "wf_prog G" and
    not_Null: "¬ stat  aNull" and
   conform_a: "G,(store s)a∷≼ Class statC" and
   conform_s: "s∷≼(G, L)" and 
    normal_s: "normal s" and
        wt_e: "prg=G,cls=accC,lcl=Le∷-Class statC" and
           f: "accfield G accC statC fn = Some f" and
        dynC: "if stat then dynC=declclass f  
                       else dynC=obj_class (lookup_obj (store s) a)" and
        stat: "if stat then (is_static f) else (¬ is_static f)"
  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)
         G⊢Field fn f in dynC dyn_accessible_from accC"
proof (cases "stat")
  case True
  with stat have static: "(is_static f)" by simp
  from True dynC 
  have dynC': "dynC=declclass f" by simp
  with f
  have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
    by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
  moreover
  from wt_e wf have "is_class G statC"
    by (auto dest!: ty_expr_is_type)
  moreover note wf dynC'
  ultimately have
     "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
    by (auto dest: fields_declC)
  with dynC' f static wf
  show ?thesis
    by (auto dest: static_to_dynamic_accessible_from_static
            dest!: accfield_accessibleD )
next
  case False
  with wf conform_a not_Null conform_s dynC
  obtain subclseq: "GdynC C statC" and
    "is_class G dynC"
    by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
              dest: obj_ty_obj_class1
          simp add: obj_ty_obj_class )
  with wf f
  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
    by (auto simp add: accfield_def Let_def
                 dest: fields_mono
                dest!: table_of_remap_SomeD)
  moreover
  from f subclseq
  have "G⊢Field fn f in dynC dyn_accessible_from accC"
    by (auto intro!: static_to_dynamic_accessible_from wf
               dest: accfield_accessibleD)
  ultimately show ?thesis
    by blast
qed

lemma error_free_field_access:
  assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
              wt_e: "prg = G, cls = accC, lcl = Le∷-Class statC" and
         eval_init: "GNorm s0 Init statDeclC s1" and
            eval_e: "Gs1 e-≻a s2" and
           conf_s2: "s2∷≼(G, L)" and
            conf_a: "normal s2  G, store s2a∷≼Class statC" and
              fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
                wf: "wf_prog G"   
  shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
proof -
  from fvar
  have store_s2': "store s2'=store s2"
    by (cases s2) (simp add: fvar_def2)
  with fvar conf_s2 
  have conf_s2': "s2'∷≼(G, L)"
    by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  from eval_init 
  have initd_statDeclC_s1: "initd statDeclC s1"
    by (rule init_yields_initd)
  with eval_e store_s2'
  have initd_statDeclC_s2': "initd statDeclC s2'"
    by (auto dest: eval_gext intro: inited_gext)
  show ?thesis
  proof (cases "normal s2'")
    case False
    then show ?thesis 
      by (auto simp add: check_field_access_def Let_def)
  next
    case True
    with fvar store_s2' 
    have not_Null: "¬ (is_static f)  aNull" 
      by (cases s2) (auto simp add: fvar_def2)
    from True fvar store_s2'
    have "normal s2"
      by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
    with conf_a store_s2'
    have conf_a': "G,store s2'a∷≼Class statC"
      by simp
    from conf_a' conf_s2' True initd_statDeclC_s2' 
      dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
                                   True wt_e accfield ] 
    show ?thesis
      by  (cases "is_static f")
          (auto dest!: initedD
           simp add: check_field_access_def Let_def)
  qed
qed

lemma call_access_ok:
  assumes invC_prop: "Ginvmode statM einvCstatT" 
      and        wf: "wf_prog G" 
      and      wt_e: "prg=G,cls=C,lcl=Le∷-RefT statT"
      and     statM: "(statDeclT,statM)  mheads G accC statT sig" 
      and      invC: "invC = invocation_class (invmode statM e) s a statT"
  shows " dynM. dynlookup G statT invC sig = Some dynM 
  G⊢Methd sig dynM in invC dyn_accessible_from accC"
proof -
  from wt_e wf have type_statT: "is_type G (RefT statT)"
    by (auto dest: ty_expr_is_type)
  from statM have not_Null: "statT  NullT" by auto
  from type_statT wt_e 
  have wf_I: "(I. statT = IfaceT I  is_iface G I  
                                        invmode statM e  SuperM)"
    by (auto dest: invocationTypeExpr_noClassD)
  from wt_e
  have wf_A: "(     T. statT = ArrayT T  invmode statM e  SuperM)"
    by (auto dest: invocationTypeExpr_noClassD)
  show ?thesis
  proof (cases "invmode statM e = IntVir")
    case True
    with invC_prop not_Null
    have invC_prop': "is_class G invC   
                      (if (T. statT=ArrayT T) then invC=Object 
                                              else GClass invCRefT statT)"
      by (auto simp add: DynT_prop_def)
    with True not_Null
    have "G,statT  invC valid_lookup_cls_for is_static statM"
     by (cases statT) (auto simp add: invmode_def) 
    with statM type_statT wf 
    show ?thesis
      by - (rule dynlookup_access,auto)
  next
    case False
    with type_statT wf invC not_Null wf_I wf_A
    have invC_prop': " is_class G invC 
                      (( statC. statT=ClassT statC  invC=statC) 
                      ( statC. statTClassT statC  invC=Object)) "
        by (case_tac "statT") (auto simp add: invocation_class_def 
                                       split: inv_mode.splits)
    with not_Null wf
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
                                            dynimethd_def)
   from statM wf wt_e not_Null False invC_prop' obtain dynM where
                "accmethd G accC invC sig = Some dynM" 
     by (auto dest!: static_mheadsD)
   from invC_prop' False not_Null wf_I
   have "G,statT  invC valid_lookup_cls_for is_static statM"
     by (cases statT) (auto simp add: invmode_def) 
   with statM type_statT wf 
    show ?thesis
      by - (rule dynlookup_access,auto)
  qed
qed

lemma error_free_call_access:
  assumes
   eval_args: "Gs1 args≐≻vs s2" and
        wt_e: "prg = G, cls = accC, lcl = Le∷-(RefT statT)" and  
       statM: "max_spec G accC statT name = mn, parTs = pTs 
               = {((statDeclT, statM), pTs')}" and
     conf_s2: "s2∷≼(G, L)" and
      conf_a: "normal s1  G, store s1a∷≼RefT statT" and
     invProp: "normal s3 
                Ginvmode statM einvCstatT" and
          s3: "s3=init_lvars G invDeclC name = mn, parTs = pTs' 
                        (invmode statM e) a vs s2" and
        invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
    invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
                             a statT name = mn, parTs = pTs'" and
          wf: "wf_prog G"
  shows "check_method_access G accC statT (invmode statM e) name=mn,parTs=pTs' a s3
   = s3"
proof (cases "normal s2")
  case False
  with s3 
  have "abrupt s3 = abrupt s2"  
    by (auto simp add: init_lvars_def2)
  with False
  show ?thesis
    by (auto simp add: check_method_access_def Let_def)
next
  case True
  note normal_s2 = True
  with eval_args
  have normal_s1: "normal s1"
    by (cases "normal s1") auto
  with conf_a eval_args 
  have conf_a_s2: "G, store s2a∷≼RefT statT"
    by (auto dest: eval_gext intro: conf_gext)
  show ?thesis
  proof (cases "a=Null  (is_static statM)")
    case False
    then obtain "¬ is_static statM" "a=Null" 
      by blast
    with normal_s2 s3
    have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
      by (auto simp add: init_lvars_def2)
    then show ?thesis
      by (auto simp add: check_method_access_def Let_def)
  next
    case True
    from statM 
    obtain
      statM': "(statDeclT,statM)mheads G accC statT name=mn,parTs=pTs'" 
      by (blast dest: max_spec2mheads)
    from True normal_s2 s3
    have "normal s3"
      by (auto simp add: init_lvars_def2)
    then have "Ginvmode statM einvCstatT"
      by (rule invProp)
    with wt_e statM' wf invC
    obtain dynM where 
      dynM: "dynlookup G statT invC  name=mn,parTs=pTs' = Some dynM" and
      acc_dynM: "G ⊢Methd  name=mn,parTs=pTs' dynM 
                          in invC dyn_accessible_from accC"
      by (force dest!: call_access_ok)
    moreover
    from s3 invC
    have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
      by (cases s2,cases "invmode statM e") 
         (simp add: init_lvars_def2 del: invmode_Static_eq)+
    ultimately
    show ?thesis
      by (auto simp add: check_method_access_def Let_def)
  qed
qed

lemma map_upds_eq_length_append_simp:
  " tab qs. length ps = length qs   tab(ps[↦]qs@zs) = tab(ps[↦]qs)"
proof (induct ps) 
  case Nil thus ?case by simp
next
  case (Cons p ps tab qs)
  from length (p#ps) = length qs
  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
    by (cases qs) auto
  from eq_length have "(tab(pq))(ps[↦]qs'@zs)=(tab(pq))(ps[↦]qs')"
    by (rule Cons.hyps)
  with qs show ?case 
    by simp
qed

lemma map_upds_upd_eq_length_simp:
  " tab qs x y. length ps = length qs 
                   tab(ps[↦]qs, xy) = tab(ps@[x][↦]qs@[y])"
proof (induct "ps")
  case Nil thus ?case by simp
next
  case (Cons p ps tab qs x y)
  from length (p#ps) = length qs
  obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
    by (cases qs) auto
  from eq_length 
  have "(tab(pq))(ps[↦]qs', xy) = (tab(pq))(ps@[x][↦]qs'@[y])"
    by (rule Cons.hyps)
  with qs show ?case
    by simp
qed


lemma map_upd_cong: "tab=tab' tab(xy) = tab'(xy)"
by simp

lemma map_upd_cong_ext: "tab z=tab' z (tab(xy)) z = (tab'(xy)) z"
by (simp add: fun_upd_def)

lemma map_upds_cong: "tab=tab' tab(xs[↦]ys) = tab'(xs[↦]ys)"
by (cases xs) simp+

lemma map_upds_cong_ext: 
 " tab tab' ys. tab z=tab' z  (tab(xs[↦]ys)) z = (tab'(xs[↦]ys)) z"
proof (induct xs)
  case Nil thus ?case by simp
next
  case (Cons x xs tab tab' ys)
  note Hyps = this
  show ?case
  proof (cases ys)
    case Nil
    with Hyps
    show ?thesis by simp
  next
    case (Cons y ys')
    have "(tab(xy, xs[↦]ys')) z = (tab'(xy, xs[↦]ys')) z"
      by (iprover intro: Hyps map_upd_cong_ext)
    with Cons show ?thesis
      by simp
  qed
qed
   
lemma map_upd_override: "(tab(xy)) x = (tab'(xy)) x"
  by simp

lemma map_upds_eq_length_suffix: " tab qs. 
        length ps = length qs  tab(ps@xs[↦]qs) = tab(ps[↦]qs, xs[↦][])"
proof (induct ps)
  case Nil thus ?case by simp
next
  case (Cons p ps tab qs)
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
    by (cases qs) auto
  from eq_length
  have "tab(pq, ps @ xs[↦]qs') = tab(pq, ps[↦]qs', xs[↦][])"
    by (rule Cons.hyps)
  with qs show ?case 
    by simp
qed
  
  
lemma map_upds_upds_eq_length_prefix_simp:
  " tab qs. length ps = length qs
               tab(ps[↦]qs, xs[↦]ys) = tab(ps@xs[↦]qs@ys)"
proof (induct ps)
  case Nil thus ?case by simp
next
  case (Cons p ps tab qs)
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
    by (cases qs) auto
  from eq_length 
  have "tab(pq, ps[↦]qs', xs[↦]ys) = tab(pq, ps @ xs[↦](qs' @ ys))"
    by (rule Cons.hyps)
  with qs 
  show ?case by simp
qed

lemma map_upd_cut_irrelevant:
"(tab(xy)) vn = Some el; (tab'(xy)) vn = None
     tab vn = Some el"
by (cases "tab' vn = None") (simp add: fun_upd_def)+

lemma map_upd_Some_expand:
"tab vn = Some z
      z. (tab(xy)) vn = Some z"
by (simp add: fun_upd_def)

lemma map_upds_Some_expand:
" tab ys z. tab vn = Some z
      z. (tab(xs[↦]ys)) vn = Some z"
proof (induct xs)
  case Nil thus ?case by simp
next
  case (Cons x xs tab ys z)
  note z = tab vn = Some z
  show ?case
  proof (cases ys)
    case Nil
    with z show ?thesis by simp
  next
    case (Cons y ys')
    note ys = ys = y#ys'
    from z obtain z' where "(tab(xy)) vn = Some z'"
      by (rule map_upd_Some_expand [of tab,elim_format]) blast
    hence "z. ((tab(xy))(xs[↦]ys')) vn = Some z"
      by (rule Cons.hyps)
    with ys show ?thesis
      by simp
  qed
qed


lemma map_upd_Some_swap:
 "(tab(rw, uv)) vn = Some z   z. (tab(uv, rw)) vn = Some z"
by (simp add: fun_upd_def)

lemma map_upd_None_swap:
 "(tab(rw, uv)) vn = None  (tab(uv, rw)) vn = None"
by (simp add: fun_upd_def)


lemma map_eq_upd_eq: "tab vn = tab' vn  (tab(xy)) vn = (tab'(xy)) vn"
by (simp add: fun_upd_def)

lemma map_upd_in_expansion_map_swap:
 "(tab(xy)) vn = Some z;tab vn  Some z 
                   (tab'(xy)) vn = Some z"
by (simp add: fun_upd_def)

lemma map_upds_in_expansion_map_swap:
 "tab tab' ys z. (tab(xs[↦]ys)) vn = Some z;tab vn  Some z 
                   (tab'(xs[↦]ys)) vn = Some z"
proof (induct xs)
  case Nil thus ?case by simp
next
  case (Cons x xs tab tab' ys z)
  note some = (tab(x # xs[↦]ys)) vn = Some z
  note tab_not_z = tab vn  Some z
  show ?case
  proof (cases ys)
    case Nil with some tab_not_z show ?thesis by simp
  next
    case (Cons y tl)
    note ys = ys = y#tl
    show ?thesis
    proof (cases "(tab(xy)) vn  Some z")
      case True
      with some ys have "(tab'(xy, xs[↦]tl)) vn = Some z"
        by (fastforce intro: Cons.hyps)
      with ys show ?thesis 
        by simp
    next
      case False
      hence tabx_z: "(tab(xy)) vn = Some z" by blast
      moreover
      from tabx_z tab_not_z
      have "(tab'(xy)) vn = Some z" 
        by (rule map_upd_in_expansion_map_swap)
      ultimately
      have "(tab(xy)) vn =(tab'(xy)) vn"
        by simp
      hence "(tab(xy, xs[↦]tl)) vn = (tab'(xy, xs[↦]tl)) vn"
        by (rule map_upds_cong_ext)
      with some ys
      show ?thesis 
        by simp
    qed
  qed
qed
   
lemma map_upds_Some_swap: 
 assumes r_u: "(tab(rw, uv, xs[↦]ys)) vn = Some z"
    shows " z. (tab(uv, rw, xs[↦]ys)) vn = Some z"
proof (cases "(tab(rw, uv)) vn = Some z")
  case True
  then obtain z' where "(tab(uv, rw)) vn = Some z'"
    by (rule map_upd_Some_swap [elim_format]) blast
  thus " z. (tab(uv, rw, xs[↦]ys)) vn = Some z"
    by (rule map_upds_Some_expand)
next
  case False
  with r_u
  have "(tab(uv, rw, xs[↦]ys)) vn = Some z"
    by (rule map_upds_in_expansion_map_swap)
  thus ?thesis
    by simp
qed
 
lemma map_upds_Some_insert:
  assumes z: "(tab(xs[↦]ys)) vn = Some z"
    shows " z. (tab(uv, xs[↦]ys)) vn = Some z"
proof (cases " z. tab vn = Some z")
  case True
  then obtain z' where "tab vn = Some z'" by blast
  then obtain z'' where "(tab(uv)) vn = Some z''"
    by (rule map_upd_Some_expand [elim_format]) blast
  thus ?thesis
    by (rule map_upds_Some_expand)
next
  case False
  hence "tab vn  Some z" by simp
  with z
  have "(tab(uv, xs[↦]ys)) vn = Some z"
    by (rule map_upds_in_expansion_map_swap)
  thus ?thesis ..
qed
   
lemma map_upds_None_cut:
assumes expand_None: "(tab(xs[↦]ys)) vn = None"
  shows "tab vn = None"
proof (cases "tab vn = None")
  case True thus ?thesis by simp
next
  case False then obtain z where "tab vn = Some z" by blast
  then obtain z' where "(tab(xs[↦]ys)) vn = Some z'"
    by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
  with expand_None show ?thesis
    by simp
qed
    

lemma map_upds_cut_irrelevant:
" tab tab' ys. (tab(xs[↦]ys)) vn = Some el; (tab'(xs[↦]ys)) vn = None
                   tab vn = Some el"
proof  (induct "xs")
  case Nil thus ?case by simp
next
  case (Cons x xs tab tab' ys)
  note tab_vn = (tab(x # xs[↦]ys)) vn = Some el
  note tab'_vn = (tab'(x # xs[↦]ys)) vn = None
  show ?case
  proof (cases ys)
    case Nil
    with tab_vn show ?thesis by simp
  next
    case (Cons y tl)
    note ys = ys=y#tl
    with tab_vn tab'_vn 
    have "(tab(xy)) vn = Some el"
      by - (rule Cons.hyps,auto)
    moreover from tab'_vn ys
    have "(tab'(xy, xs[↦]tl)) vn = None" 
      by simp
    hence "(tab'(xy)) vn = None"
      by (rule map_upds_None_cut)
    ultimately show "tab vn = Some el" 
      by (rule map_upd_cut_irrelevant)
  qed
qed

   
lemma dom_vname_split:
 "dom (case_lname (case_ename (tab(xy, xs[↦]ys)) a) b)
   = dom (case_lname (case_ename (tab(xy)) a) b)  
     dom (case_lname (case_ename (tab(xs[↦]ys)) a) b)"
  (is "?List x xs y ys = ?Hd x y  ?Tl xs ys")
proof 
  show "?List x xs y ys  ?Hd x y  ?Tl xs ys"
  proof 
    fix el 
    assume el_in_list: "el  ?List x xs y ys"
    show "el   ?Hd x y  ?Tl xs ys"
    proof (cases el)
      case This
      with el_in_list show ?thesis by (simp add: dom_def)
    next
      case (EName en)
      show ?thesis
      proof (cases en)
        case Res
        with EName el_in_list show ?thesis by (simp add: dom_def)
      next
        case (VNam vn)
        with EName el_in_list show ?thesis 
          by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
      qed
    qed
  qed
next
  show "?Hd x y  ?Tl xs ys   ?List x xs y ys" 
  proof (rule subsetI)
    fix el 
    assume  el_in_hd_tl: "el   ?Hd x y  ?Tl xs ys"
    show "el  ?List x xs y ys"
    proof (cases el)
      case This
      with el_in_hd_tl show ?thesis by (simp add: dom_def)
    next
      case (EName en)
      show ?thesis
      proof (cases en)
        case Res
        with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
      next
        case (VNam vn)
        with EName el_in_hd_tl show ?thesis 
          by (auto simp add: dom_def intro: map_upds_Some_expand 
                                            map_upds_Some_insert)
      qed
    qed
  qed
qed

lemma dom_map_upd: " tab. dom (tab(xy)) = dom tab  {x}"
by (auto simp add: dom_def fun_upd_def)

lemma dom_map_upds: " tab ys. length xs = length ys 
   dom (tab(xs[↦]ys)) = dom tab  set xs"
proof (induct xs)
  case Nil thus ?case by (simp add: dom_def)
next
  case (Cons x xs tab ys)
  note Hyp = Cons.hyps
  note len = length (x#xs)=length ys
  show ?case
  proof (cases ys)
    case Nil with len show ?thesis by simp
  next
    case (Cons y tl)
    with len have "dom (tab(xy, xs[↦]tl)) = dom (tab(xy))  set xs"
      by - (rule Hyp,simp)
    moreover 
    have "dom (tab(xhd ys)) = dom tab  {x}"
      by (rule dom_map_upd)
    ultimately
    show ?thesis using Cons
      by simp
  qed
qed
 
lemma dom_case_ename_None_simp:
 "dom (case_ename vname_tab None) = VNam ` (dom vname_tab)"
  apply (auto simp add: dom_def image_def )
  apply (case_tac "x")
  apply auto
  done

lemma dom_case_ename_Some_simp:
 "dom (case_ename vname_tab (Some a)) = VNam ` (dom vname_tab)  {Res}"
  apply (auto simp add: dom_def image_def )
  apply (case_tac "x")
  apply auto
  done

lemma dom_case_lname_None_simp:
  "dom (case_lname ename_tab None) = EName ` (dom ename_tab)"
  apply (auto simp add: dom_def image_def )
  apply (case_tac "x")
  apply auto
  done

lemma dom_case_lname_Some_simp:
 "dom (case_lname ename_tab (Some a)) = EName ` (dom ename_tab)  {This}"
  apply (auto simp add: dom_def image_def)
  apply (case_tac "x")
  apply auto
  done

lemmas dom_lname_case_ename_simps =  
     dom_case_ename_None_simp dom_case_ename_Some_simp 
     dom_case_lname_None_simp dom_case_lname_Some_simp

lemma image_comp: 
 "f ` g ` A = (f  g) ` A"
by (auto simp add: image_def)


lemma dom_locals_init_lvars: 
  assumes m: "m=(mthd (the (methd G C sig)))"  
  assumes len: "length (pars m) = length pvs"
  shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
           = parameters m"
proof -
  from m
  have static_m': "is_static m = static m"
    by simp
  from len
  have dom_vnames: "dom (Map.empty(pars m[↦]pvs))=set (pars m)"
    by (simp add: dom_map_upds)
  show ?thesis
  proof (cases "static m")
    case True
    with static_m' dom_vnames m
    show ?thesis
      by (cases s) (simp add: init_lvars_def Let_def parameters_def
                              dom_lname_case_ename_simps image_comp)
  next
    case False
    with static_m' dom_vnames m
    show ?thesis
      by (cases s) (simp add: init_lvars_def Let_def parameters_def
                              dom_lname_case_ename_simps image_comp)
  qed
qed


lemma da_e2_BinOp:
  assumes da: "prg=G,cls=accC,lcl=L
                  dom (locals (store s0)) »BinOp binop e1 e2e» A"
    and wt_e1: "prg=G,cls=accC,lcl=Le1∷-e1T"
    and wt_e2: "prg=G,cls=accC,lcl=Le2∷-e2T" 
    and wt_binop: "wt_binop G binop e1T e2T" 
    and conf_s0: "s0∷≼(G,L)"  
    and normal_s1: "normal s1"
    and eval_e1: "Gs0 e1-≻v1 s1"
    and conf_v1: "G,store s1v1∷≼e1T"
    and wf: "wf_prog G"
  shows " E2. prg=G,cls=accC,lcl=L dom (locals (store s1)) 
         »(if need_second_arg binop v1 then e2e else Skips)» E2"
proof -
  note inj_term_simps [simp]
  from da obtain E1 where
    da_e1: "prg=G,cls=accC,lcl=L  dom (locals (store s0)) »e1e» E1"
    by cases simp+
  obtain E2 where
    "prg=G,cls=accC,lcl=L dom (locals (store s1)) 
      »(if need_second_arg binop v1 then e2e else Skips)» E2"
  proof (cases "need_second_arg binop v1")
    case False
    obtain S where
      daSkip: "prg=G,cls=accC,lcl=L
                   dom (locals (store s1)) »Skips» S"
      by (auto intro: da_Skip [simplified] assigned.select_convs)
    thus ?thesis
      using that by (simp add: False)
  next
    case True
    from eval_e1 have 
      s0_s1:"dom (locals (store s0))  dom (locals (store s1))"
      by (rule dom_locals_eval_mono_elim)
    {
      assume condAnd: "binop=CondAnd"
      have ?thesis
      proof -
        from da obtain E2' where
          "prg=G,cls=accC,lcl=L
              dom (locals (store s0))  assigns_if True e1 »e2e» E2'"
          by cases (simp add: condAnd)+
        moreover
        have "dom (locals (store s0)) 
           assigns_if True e1  dom (locals (store s1))"
        proof -
          from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
            by simp
          with normal_s1 conf_v1 obtain b where "v1=Bool b"
            by (auto dest: conf_Boolean)
          with True condAnd
          have v1: "v1=Bool True"
            by simp
          from eval_e1 normal_s1 
          have "assigns_if True e1  dom (locals (store s1))"
            by (rule assigns_if_good_approx' [elim_format])
               (insert wt_e1, simp_all add: e1T v1)
          with s0_s1 show ?thesis by (rule Un_least)
        qed
        ultimately
        show ?thesis
          using that by (cases rule: da_weakenE) (simp add: True)
      qed
    }
    moreover
    { 
      assume condOr: "binop=CondOr"
      have ?thesis
        (* Beweis durch Analogie/Example/Pattern?, True→False; And→Or *)
      proof -
        from da obtain E2' where
          "prg=G,cls=accC,lcl=L
               dom (locals (store s0))  assigns_if False e1 »e2e» E2'"
          by cases (simp add: condOr)+
        moreover
        have "dom (locals (store s0)) 
                      assigns_if False e1  dom (locals (store s1))"
        proof -
          from condOr wt_binop have e1T: "e1T=PrimT Boolean"
            by simp
          with normal_s1 conf_v1 obtain b where "v1=Bool b"
            by (auto dest: conf_Boolean)
          with True condOr
          have v1: "v1=Bool False"
            by simp
          from eval_e1 normal_s1 
          have "assigns_if False e1  dom (locals (store s1))"
            by (rule assigns_if_good_approx' [elim_format])
               (insert wt_e1, simp_all add: e1T v1)
          with s0_s1 show ?thesis by (rule Un_least)
        qed
        ultimately
        show ?thesis
          using that by (rule da_weakenE) (simp add: True)
      qed
    }
    moreover
    {
      assume notAndOr: "binopCondAnd" "binopCondOr"
      have ?thesis
      proof -
        from da notAndOr obtain E1' where
          da_e1: "prg=G,cls=accC,lcl=L
                   dom (locals (store s0)) »e1e» E1'"
          and da_e2: "prg=G,cls=accC,lcl=L nrm E1' »In1l e2» A"
          by cases simp+
        from eval_e1 wt_e1 da_e1 wf normal_s1 
        have "nrm E1'  dom (locals (store s1))"
          by (cases rule: da_good_approxE') iprover
        with da_e2 show ?thesis
          using that by (rule da_weakenE) (simp add: True)
      qed
    }
    ultimately show ?thesis
      by (cases binop) auto
  qed
  thus ?thesis ..
qed

subsubsection "main proof of type safety"
    
lemma eval_type_sound:
  assumes  eval: "Gs0 t≻→ (v,s1)" 
   and      wt: "prg=G,cls=accC,lcl=LtT" 
   and      da: "prg=G,cls=accC,lcl=Ldom (locals (store s0))»t»A"
   and      wf: "wf_prog G" 
   and conf_s0: "s0∷≼(G,L)"           
  shows "s1∷≼(G,L)   (normal s1  G,L,store s1tv∷≼T)  
         (error_free s0 = error_free s1)"
proof -
  note inj_term_simps [simp]
  let ?TypeSafeObj = "λ s0 s1 t v. 
            L accC T A. s0∷≼(G,L)  prg=G,cls=accC,lcl=LtT
                       prg=G,cls=accC,lcl=Ldom (locals (store s0))»t»A  
                       s1∷≼(G,L)  (normal s1  G,L,store s1tv∷≼T)
                           (error_free s0 = error_free s1)"
  from eval 
  have " L accC T A. s0∷≼(G,L);prg=G,cls=accC,lcl=LtT;
                      prg=G,cls=accC,lcl=Ldom (locals (store s0))»t»A  
         s1∷≼(G,L)  (normal s1  G,L,store s1tv∷≼T)
             (error_free s0 = error_free s1)"
   (is "PROP ?TypeSafe s0 s1 t v"
    is " L accC T A. ?Conform L s0  ?WellTyped L accC T t  
                  ?DefAss L accC s0 t A 
                  ?Conform L s1  ?ValueTyped L T s1 t v 
                     ?ErrorFree s0 s1")
  proof (induct)
    case (Abrupt xc s t L accC T A) 
    from (Some xc, s)∷≼(G,L)
    show "(Some xc, s)∷≼(G,L)  
      (normal (Some xc, s) 
       G,L,store (Some xc,s)tundefined3 t∷≼T)  
      (error_free (Some xc, s) = error_free (Some xc, s))"
      by simp
  next
    case (Skip s L accC T A)
    from Norm s∷≼(G, L) and
      prg = G, cls = accC, lcl = LIn1r SkipT
    show "Norm s∷≼(G, L) 
              (normal (Norm s)  G,L,store (Norm s)In1r Skip∷≼T)  
              (error_free (Norm s) = error_free (Norm s))"
      by simp
  next
    case (Expr s0 e v s1 L accC T A)
    note GNorm s0 e-≻v s1
    note hyp = PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)
    note conf_s0 = Norm s0∷≼(G, L)
    moreover
    note wt = prg = G, cls = accC, lcl = LIn1r (Expr e)T
    then obtain eT 
      where "prg = G, cls = accC, lcl = LIn1l eeT"
      by (rule wt_elim_cases) blast
    moreover
    from Expr.prems obtain E where
      "prg=G,cls=accC, lcl=Ldom (locals (store ((Norm s0)::state)))»In1l e»E"
      by (elim da_elim_cases) simp
    ultimately 
    obtain "s1∷≼(G, L)" and "error_free s1"
      by (rule hyp [elim_format]) simp
    with wt
    show "s1∷≼(G, L) 
          (normal s1  G,L,store s1In1r (Expr e)∷≼T)  
          (error_free (Norm s0) = error_free s1)"
      by (simp)
  next
    case (Lab s0 c s1 l L accC T A)
    note hyp = PROP ?TypeSafe (Norm s0) s1 (In1r c) 
    note conf_s0 = Norm s0∷≼(G, L)
    moreover
    note wt = prg = G, cls = accC, lcl = LIn1r (l c)T
    then have "prg = G, cls = accC, lcl = Lc∷√"
      by (rule wt_elim_cases) blast
    moreover from Lab.prems obtain C where
     "prg=G,cls=accC, lcl=Ldom (locals (store ((Norm s0)::state)))»In1r c»C"
      by (elim da_elim_cases) simp
    ultimately
    obtain       conf_s1: "s1∷≼(G, L)" and 
           error_free_s1: "error_free s1" 
      by (rule hyp [elim_format]) simp
    from conf_s1 have "abupd (absorb l) s1∷≼(G, L)"
      by (cases s1) (auto intro: conforms_absorb)
    with wt error_free_s1
    show "abupd (absorb l) s1∷≼(G, L) 
          (normal (abupd (absorb l) s1)
            G,L,store (abupd (absorb l) s1)In1r (l c)∷≼T) 
          (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
      by (simp)
  next
    case (Comp s0 c1 s1 c2 s2 L accC T A)
    note eval_c1 = GNorm s0 c1 s1
    note eval_c2 = Gs1 c2 s2
    note hyp_c1 = PROP ?TypeSafe (Norm s0) s1 (In1r c1) 
    note hyp_c2 = PROP ?TypeSafe s1        s2 (In1r c2) 
    note conf_s0 = Norm s0∷≼(G, L)
    note wt = prg = G, cls = accC, lcl = LIn1r (c1;; c2)T
    then obtain wt_c1: "prg = G, cls = accC, lcl = Lc1∷√" and
                wt_c2: "prg = G, cls = accC, lcl = Lc2∷√"
      by (rule wt_elim_cases) blast
    from Comp.prems
    obtain C1 C2
      where da_c1: "prg=G, cls=accC, lcl=L 
                      dom (locals (store ((Norm s0)::state))) »In1r c1» C1" and 
            da_c2: "prg=G, cls=accC, lcl=L  nrm C1 »In1r c2» C2" 
      by (elim da_elim_cases) simp
    from conf_s0 wt_c1 da_c1
    obtain conf_s1: "s1∷≼(G, L)" and 
           error_free_s1: "error_free s1"
      by (rule hyp_c1 [elim_format]) simp
    show "s2∷≼(G, L) 
          (normal s2  G,L,store s2In1r (c1;; c2)∷≼T) 
          (error_free (Norm s0) = error_free s2)"
    proof (cases "normal s1")
      case False
      with eval_c2 have "s2=s1" by auto
      with conf_s1 error_free_s1 False wt show ?thesis
        by simp
    next
      case True
      obtain C2' where 
        "prg=G, cls=