src/HOL/Bali/TypeSafe.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 13690 ac335b2f4a39
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
wenzelm@12857
     1
(*  Title:      HOL/Bali/TypeSafe.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12925
     3
    Author:     David von Oheimb and Norbert Schirmer
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* The type soundness proof for Java *}
schirmer@12854
     7
schirmer@13688
     8
theory TypeSafe = DefiniteAssignmentCorrect + Conform:
schirmer@12854
     9
schirmer@12925
    10
section "error free"
schirmer@12925
    11
 
schirmer@12925
    12
lemma error_free_halloc:
wenzelm@12937
    13
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
schirmer@12925
    14
          error_free_s0: "error_free s0"
wenzelm@12937
    15
  shows "error_free s1"
schirmer@12925
    16
proof -
schirmer@12925
    17
  from halloc error_free_s0
schirmer@12925
    18
  obtain abrupt0 store0 abrupt1 store1
schirmer@12925
    19
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
schirmer@12925
    20
          halloc': "G\<turnstile>(abrupt0,store0) \<midarrow>halloc oi\<succ>a\<rightarrow> (abrupt1,store1)" and
schirmer@12925
    21
          error_free_s0': "error_free (abrupt0,store0)"
schirmer@12925
    22
    by (cases s0,cases s1) auto
schirmer@12925
    23
  from halloc' error_free_s0'
schirmer@12925
    24
  have "error_free (abrupt1,store1)"
schirmer@12925
    25
  proof (induct)
schirmer@12925
    26
    case Abrupt 
schirmer@13688
    27
    then show ?case .
schirmer@12925
    28
  next
schirmer@12925
    29
    case New
schirmer@12925
    30
    then show ?case
schirmer@12925
    31
      by (auto split: split_if_asm)
schirmer@12925
    32
  qed
schirmer@12925
    33
  with eqs 
schirmer@12925
    34
  show ?thesis
schirmer@12925
    35
    by simp
schirmer@12925
    36
qed
schirmer@12925
    37
schirmer@12925
    38
lemma error_free_sxalloc:
wenzelm@12937
    39
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
wenzelm@12937
    40
  shows "error_free s1"
schirmer@12925
    41
proof -
schirmer@12925
    42
  from sxalloc error_free_s0
schirmer@12925
    43
  obtain abrupt0 store0 abrupt1 store1
schirmer@12925
    44
    where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
schirmer@12925
    45
          sxalloc': "G\<turnstile>(abrupt0,store0) \<midarrow>sxalloc\<rightarrow> (abrupt1,store1)" and
schirmer@12925
    46
          error_free_s0': "error_free (abrupt0,store0)"
schirmer@12925
    47
    by (cases s0,cases s1) auto
schirmer@12925
    48
  from sxalloc' error_free_s0'
schirmer@12925
    49
  have "error_free (abrupt1,store1)"
schirmer@12925
    50
  proof (induct)
schirmer@12925
    51
  qed (auto)
schirmer@12925
    52
  with eqs 
schirmer@12925
    53
  show ?thesis 
schirmer@12925
    54
    by simp
schirmer@12925
    55
qed
schirmer@12925
    56
schirmer@12925
    57
lemma error_free_check_field_access_eq:
schirmer@12925
    58
 "error_free (check_field_access G accC statDeclC fn stat a s)
schirmer@12925
    59
 \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
schirmer@12925
    60
apply (cases s)
schirmer@12925
    61
apply (auto simp add: check_field_access_def Let_def error_free_def 
schirmer@12925
    62
                      abrupt_if_def 
schirmer@12925
    63
            split: split_if_asm)
schirmer@12925
    64
done
schirmer@12925
    65
schirmer@12925
    66
lemma error_free_check_method_access_eq:
schirmer@12925
    67
"error_free (check_method_access G accC statT mode sig a' s)
schirmer@12925
    68
 \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
schirmer@12925
    69
apply (cases s)
schirmer@12925
    70
apply (auto simp add: check_method_access_def Let_def error_free_def 
schirmer@12925
    71
                      abrupt_if_def 
schirmer@12925
    72
            split: split_if_asm)
schirmer@12925
    73
done
schirmer@12925
    74
schirmer@12925
    75
lemma error_free_FVar_lemma: 
schirmer@12925
    76
     "error_free s 
schirmer@12925
    77
       \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
schirmer@12925
    78
  by (case_tac s) (auto split: split_if) 
schirmer@12925
    79
schirmer@12925
    80
lemma error_free_init_lvars [simp,intro]:
schirmer@12925
    81
"error_free s \<Longrightarrow> 
schirmer@12925
    82
  error_free (init_lvars G C sig mode a pvs s)"
schirmer@12925
    83
by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
schirmer@12925
    84
schirmer@12925
    85
lemma error_free_LVar_lemma:   
schirmer@12925
    86
"error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
schirmer@12925
    87
by (cases s) simp
schirmer@12925
    88
schirmer@12925
    89
lemma error_free_throw [simp,intro]:
schirmer@12925
    90
  "error_free s \<Longrightarrow> error_free (abupd (throw x) s)"
schirmer@12925
    91
by (cases s) (simp add: throw_def)
schirmer@12925
    92
schirmer@12854
    93
schirmer@12854
    94
section "result conformance"
schirmer@12854
    95
schirmer@12854
    96
constdefs
schirmer@12854
    97
  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
schirmer@12854
    98
          ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
schirmer@12925
    99
"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
schirmer@12925
   100
 (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
schirmer@12925
   101
 (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
schirmer@12854
   102
schirmer@13688
   103
schirmer@13688
   104
constdefs
schirmer@12854
   105
  rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
schirmer@12854
   106
          ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_"                               [71,71,71,71,71,71] 70)
schirmer@12854
   107
  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
schirmer@12854
   108
    \<equiv> case T of
schirmer@13688
   109
        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
schirmer@13688
   110
                  then (\<forall> n. (the_In2 t) = LVar n 
schirmer@13688
   111
                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
schirmer@13688
   112
                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
schirmer@13688
   113
                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
schirmer@13688
   114
                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
schirmer@12854
   115
                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
schirmer@12854
   116
      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
schirmer@12854
   117
schirmer@13688
   118
text {*
schirmer@13688
   119
 With @{term rconf} we describe the conformance of the result value of a term.
schirmer@13688
   120
 This definition gets rather complicated because of the relations between the
schirmer@13688
   121
 injections of the different terms, types and values. The main case distinction
schirmer@13688
   122
 is between single values and value lists. In case of value lists, every 
schirmer@13688
   123
 value has to conform to its type. For single values we have to do a further
schirmer@13688
   124
 case distinction, between values of variables @{term "\<exists>var. t=In2 var" } and
schirmer@13688
   125
 ordinary values. Values of variables are modelled as pairs consisting of the
schirmer@13688
   126
 current value and an update function which will perform an assignment to the
schirmer@13688
   127
 variable. This stems form the decision, that we only have one evaluation rule
schirmer@13688
   128
 for each kind of variable. The decision if we read or write to the 
schirmer@13688
   129
 variable is made by syntactic enclosing rules. So conformance of 
schirmer@13688
   130
 variable-values must ensure that both the current value and an update will 
schirmer@13688
   131
 conform to the type. With the introduction of definite assignment of local
schirmer@13688
   132
 variables we have to do another case distinction. For the notion of conformance
schirmer@13688
   133
 local variables are allowed to be @{term None}, since the definedness is not 
schirmer@13688
   134
 ensured by conformance but by definite assignment. Field and array variables 
schirmer@13688
   135
 must contain a value. 
schirmer@13688
   136
*}
schirmer@13688
   137
 
schirmer@13688
   138
schirmer@13688
   139
schirmer@12854
   140
lemma rconf_In1 [simp]: 
schirmer@12854
   141
 "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
schirmer@12854
   142
apply (unfold rconf_def)
schirmer@12854
   143
apply (simp (no_asm))
schirmer@12854
   144
done
schirmer@12854
   145
schirmer@13688
   146
lemma rconf_In2_no_LVar [simp]: 
schirmer@13688
   147
 "\<forall> n. va\<noteq>LVar n \<Longrightarrow> 
schirmer@13688
   148
   G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  = (G,s\<turnstile>fst vf\<Colon>\<preceq>T \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
schirmer@12854
   149
apply (unfold rconf_def)
schirmer@13688
   150
apply auto
schirmer@12854
   151
done
schirmer@12854
   152
schirmer@13688
   153
lemma rconf_In2_LVar [simp]: 
schirmer@13688
   154
 "va=LVar n \<Longrightarrow> 
schirmer@13688
   155
   G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  
schirmer@13688
   156
    = ((fst vf = the (locals s n)) \<and>
schirmer@13688
   157
       (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst vf\<Colon>\<preceq>T) \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
schirmer@13688
   158
apply (unfold rconf_def)
schirmer@13688
   159
by simp
schirmer@13688
   160
schirmer@12854
   161
lemma rconf_In3 [simp]: 
schirmer@12854
   162
 "G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (\<lambda>v T. G,s\<turnstile>v\<Colon>\<preceq>T) vs Ts"
schirmer@12854
   163
apply (unfold rconf_def)
schirmer@12854
   164
apply (simp (no_asm))
schirmer@12854
   165
done
schirmer@12854
   166
schirmer@12854
   167
section "fits and conf"
schirmer@12854
   168
schirmer@12854
   169
(* unused *)
schirmer@12854
   170
lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
schirmer@12854
   171
apply (unfold fits_def)
schirmer@12854
   172
apply clarify
schirmer@12854
   173
apply (erule swap, simp (no_asm_use))
schirmer@12854
   174
apply (drule conf_RefTD)
schirmer@12854
   175
apply auto
schirmer@12854
   176
done
schirmer@12854
   177
schirmer@12854
   178
lemma fits_conf: 
schirmer@12854
   179
  "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
schirmer@12854
   180
apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
schirmer@12854
   181
apply (force dest: conf_RefTD intro: conf_AddrI)
schirmer@12854
   182
done
schirmer@12854
   183
schirmer@12854
   184
lemma fits_Array: 
schirmer@12854
   185
 "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
schirmer@12854
   186
apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
schirmer@12854
   187
apply (force dest: conf_RefTD intro: conf_AddrI)
schirmer@12854
   188
done
schirmer@12854
   189
schirmer@12854
   190
schirmer@12854
   191
schirmer@12854
   192
section "gext"
schirmer@12854
   193
schirmer@12854
   194
lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
schirmer@12854
   195
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
   196
apply (erule halloc.induct)
schirmer@12854
   197
apply  (auto dest!: new_AddrD)
schirmer@12854
   198
done
schirmer@12854
   199
schirmer@12854
   200
lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
schirmer@12854
   201
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
   202
apply (erule sxalloc.induct)
schirmer@12854
   203
apply   (auto dest!: halloc_gext)
schirmer@12854
   204
done
schirmer@12854
   205
schirmer@12854
   206
lemma eval_gext_lemma [rule_format (no_asm)]: 
schirmer@12854
   207
 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
schirmer@12854
   208
    In1 v \<Rightarrow> True  
schirmer@12854
   209
  | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
schirmer@12854
   210
  | In3 vs \<Rightarrow> True)"
schirmer@12854
   211
apply (erule eval_induct)
schirmer@13337
   212
prefer 26 
schirmer@12854
   213
  apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
schirmer@12854
   214
apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
schirmer@12925
   215
 simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
schirmer@12925
   216
            check_field_access_def check_method_access_def Let_def
schirmer@12854
   217
 split del: split_if_asm split add: sum3.split)
schirmer@12854
   218
(* 6 subgoals *)
schirmer@12854
   219
apply force+
schirmer@12854
   220
done
schirmer@12854
   221
schirmer@12854
   222
lemma evar_gext_f: 
schirmer@12854
   223
  "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
schirmer@12854
   224
apply (drule eval_gext_lemma [THEN conjunct2])
schirmer@12854
   225
apply auto
schirmer@12854
   226
done
schirmer@12854
   227
schirmer@12854
   228
lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
schirmer@12854
   229
schirmer@12854
   230
lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2"
schirmer@12854
   231
apply (drule eval_gext)
schirmer@12854
   232
apply auto
schirmer@12854
   233
done
schirmer@12854
   234
schirmer@12854
   235
lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
schirmer@12854
   236
apply (erule eval_cases , auto split del: split_if_asm)
schirmer@12854
   237
apply (case_tac "inited C (globs s1)")
schirmer@12854
   238
apply  (clarsimp split del: split_if_asm)+
schirmer@12854
   239
apply (drule eval_gext')+
schirmer@12854
   240
apply (drule init_class_obj_inited)
schirmer@12854
   241
apply (erule inited_gext)
schirmer@12854
   242
apply (simp (no_asm_use))
schirmer@12854
   243
done
schirmer@12854
   244
schirmer@12854
   245
schirmer@12854
   246
section "Lemmas"
schirmer@12854
   247
schirmer@12854
   248
lemma obj_ty_obj_class1: 
schirmer@12854
   249
 "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
schirmer@12854
   250
apply (case_tac "tag obj")
schirmer@12854
   251
apply (auto simp add: obj_ty_def obj_class_def)
schirmer@12854
   252
done
schirmer@12854
   253
schirmer@12854
   254
lemma oconf_init_obj: 
schirmer@12854
   255
 "\<lbrakk>wf_prog G;  
schirmer@12854
   256
 (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
schirmer@12854
   257
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
schirmer@12854
   258
apply (auto intro!: oconf_init_obj_lemma unique_fields)
schirmer@12854
   259
done
schirmer@12854
   260
schirmer@12854
   261
lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
schirmer@12854
   262
  wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
schirmer@12854
   263
                        | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
schirmer@12854
   264
  (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
schirmer@12854
   265
apply (unfold init_obj_def)
schirmer@12854
   266
apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
schirmer@12854
   267
            simp add: obj.update_defs)
schirmer@12854
   268
done
schirmer@12854
   269
schirmer@12854
   270
lemma conforms_init_class_obj: 
schirmer@12854
   271
 "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
schirmer@12854
   272
  (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
schirmer@12854
   273
apply (rule not_initedD [THEN conforms_newG])
schirmer@12854
   274
apply    (auto)
schirmer@12854
   275
done
schirmer@12854
   276
schirmer@12854
   277
schirmer@12854
   278
lemma fst_init_lvars[simp]: 
schirmer@12854
   279
 "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
schirmer@12925
   280
  (if is_static m then x else (np a') x)"
schirmer@12854
   281
apply (simp (no_asm) add: init_lvars_def2)
schirmer@12854
   282
done
schirmer@12854
   283
schirmer@12854
   284
schirmer@12854
   285
lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
schirmer@12854
   286
  is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
schirmer@12854
   287
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
   288
apply (case_tac "aa")
schirmer@12854
   289
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
schirmer@12854
   290
       intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
schirmer@12854
   291
done
schirmer@12854
   292
schirmer@12925
   293
lemma halloc_type_sound: 
schirmer@12925
   294
"\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
schirmer@12854
   295
  T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
schirmer@12854
   296
  (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
schirmer@12854
   297
apply (auto elim!: halloc_conforms)
schirmer@12854
   298
apply (case_tac "aa")
schirmer@12854
   299
apply (subst obj_ty_eq)
schirmer@12854
   300
apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
schirmer@12854
   301
done
schirmer@12854
   302
schirmer@12854
   303
lemma sxalloc_type_sound: 
schirmer@13688
   304
 "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> 
schirmer@13688
   305
  case fst s1 of  
schirmer@13688
   306
    None \<Rightarrow> s2 = s1 
schirmer@13688
   307
  | Some abr \<Rightarrow> (case abr of
schirmer@13688
   308
                   Xcpt x \<Rightarrow> (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> 
schirmer@13688
   309
                                  (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))
schirmer@13688
   310
                 | Jump j \<Rightarrow> s2 = s1
schirmer@13688
   311
                 | Error e \<Rightarrow> s2 = s1)"
schirmer@12854
   312
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
   313
apply (erule sxalloc.induct)
schirmer@12854
   314
apply   auto
schirmer@12854
   315
apply (rule halloc_conforms [THEN conforms_xconf])
schirmer@12854
   316
apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
schirmer@12854
   317
done
schirmer@12854
   318
schirmer@12854
   319
lemma wt_init_comp_ty: 
schirmer@12854
   320
"is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
schirmer@12854
   321
apply (unfold init_comp_ty_def)
schirmer@12854
   322
apply (clarsimp simp add: accessible_in_RefT_simp 
schirmer@12854
   323
                          is_acc_type_def is_acc_class_def)
schirmer@12854
   324
done
schirmer@12854
   325
schirmer@12854
   326
schirmer@12854
   327
declare fun_upd_same [simp]
schirmer@12854
   328
schirmer@12854
   329
declare fun_upd_apply [simp del]
schirmer@12854
   330
schirmer@12854
   331
schirmer@12854
   332
constdefs
schirmer@12854
   333
  DynT_prop::"[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" 
schirmer@12854
   334
                                              ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
schirmer@12854
   335
 "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
schirmer@12854
   336
                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
schirmer@12854
   337
schirmer@12854
   338
lemma DynT_propI: 
schirmer@12854
   339
 "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
schirmer@12854
   340
  \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
schirmer@12854
   341
proof (unfold DynT_prop_def)
schirmer@12854
   342
  assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
schirmer@12854
   343
     and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
schirmer@12854
   344
     and            wf: "wf_prog G"
schirmer@12854
   345
     and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
schirmer@12854
   346
  let ?invCls = "(invocation_class mode s a' statT)"
schirmer@12854
   347
  let ?IntVir = "mode = IntVir"
schirmer@12854
   348
  let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
schirmer@12854
   349
                          (if \<exists>T. statT = ArrayT T
schirmer@12854
   350
                                  then invCls = Object
schirmer@12854
   351
                                  else G\<turnstile>Class invCls\<preceq>RefT statT)"
schirmer@12854
   352
  show "?IntVir \<longrightarrow> ?Concl ?invCls"
schirmer@12854
   353
  proof  
schirmer@12854
   354
    assume modeIntVir: ?IntVir 
schirmer@12854
   355
    with mode have not_Null: "a' \<noteq> Null" ..
schirmer@12854
   356
    from statT_a' not_Null state_conform 
schirmer@12854
   357
    obtain a obj 
schirmer@12854
   358
      where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
schirmer@12854
   359
                        "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
schirmer@12854
   360
      by (blast dest: conforms_RefTD)
schirmer@12854
   361
    show "?Concl ?invCls"
schirmer@12854
   362
    proof (cases "tag obj")
schirmer@12854
   363
      case CInst
schirmer@12854
   364
      with modeIntVir obj_props
schirmer@12854
   365
      show ?thesis 
schirmer@12854
   366
	by (auto dest!: widen_Array2 split add: split_if)
schirmer@12854
   367
    next
schirmer@12854
   368
      case Arr
schirmer@12854
   369
      from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
schirmer@12854
   370
      moreover from Arr have "obj_class obj = Object" 
schirmer@12854
   371
	by (blast dest: obj_class_Arr1)
schirmer@12854
   372
      moreover note modeIntVir obj_props wf 
schirmer@12854
   373
      ultimately show ?thesis by (auto dest!: widen_Array )
schirmer@12854
   374
    qed
schirmer@12854
   375
  qed
schirmer@12854
   376
qed
schirmer@12854
   377
schirmer@12854
   378
lemma invocation_methd:
schirmer@12854
   379
"\<lbrakk>wf_prog G; statT \<noteq> NullT; 
schirmer@12854
   380
 (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
schirmer@12854
   381
 (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
schirmer@12854
   382
 (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
schirmer@12854
   383
 G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
schirmer@12854
   384
 dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
schirmer@12854
   385
\<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
schirmer@12854
   386
proof -
schirmer@12854
   387
  assume         wf: "wf_prog G"
schirmer@12854
   388
     and  not_NullT: "statT \<noteq> NullT"
schirmer@12854
   389
     and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
schirmer@12854
   390
     and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
schirmer@12854
   391
     and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
schirmer@12854
   392
     and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
schirmer@12854
   393
     and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
schirmer@12854
   394
                      = Some m"
schirmer@12854
   395
  show ?thesis
schirmer@12854
   396
  proof (cases statT)
schirmer@12854
   397
    case NullT
schirmer@12854
   398
    with not_NullT show ?thesis by simp
schirmer@12854
   399
  next
schirmer@12854
   400
    case IfaceT
schirmer@12854
   401
    with statI_prop obtain I 
schirmer@12854
   402
      where    statI: "statT = IfaceT I" and 
schirmer@12854
   403
            is_iface: "is_iface G I"     and
schirmer@12854
   404
          not_SuperM: "mode \<noteq> SuperM" by blast            
schirmer@12854
   405
    
schirmer@12854
   406
    show ?thesis 
schirmer@12854
   407
    proof (cases mode)
schirmer@12854
   408
      case Static
schirmer@12854
   409
      with wf dynlookup statI is_iface 
schirmer@12854
   410
      show ?thesis
schirmer@12854
   411
	by (auto simp add: invocation_declclass_def dynlookup_def 
schirmer@12854
   412
                           dynimethd_def dynmethd_C_C 
schirmer@12854
   413
	            intro: dynmethd_declclass
schirmer@12854
   414
	            dest!: wf_imethdsD
schirmer@12854
   415
                     dest: table_of_map_SomeI
schirmer@12854
   416
                    split: split_if_asm)
schirmer@12854
   417
    next	
schirmer@12854
   418
      case SuperM
schirmer@12854
   419
      with not_SuperM show ?thesis ..
schirmer@12854
   420
    next
schirmer@12854
   421
      case IntVir
schirmer@12854
   422
      with wf dynlookup IfaceT invC_prop show ?thesis 
schirmer@12854
   423
	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
schirmer@12854
   424
                           DynT_prop_def
schirmer@12854
   425
	            intro: methd_declclass dynmethd_declclass
schirmer@12854
   426
	            split: split_if_asm)
schirmer@12854
   427
    qed
schirmer@12854
   428
  next
schirmer@12854
   429
    case ClassT
schirmer@12854
   430
    show ?thesis
schirmer@12854
   431
    proof (cases mode)
schirmer@12854
   432
      case Static
schirmer@12854
   433
      with wf ClassT dynlookup statC_prop 
schirmer@12854
   434
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
schirmer@12854
   435
                               intro: dynmethd_declclass)
schirmer@12854
   436
    next
schirmer@12854
   437
      case SuperM
schirmer@12854
   438
      with wf ClassT dynlookup statC_prop 
schirmer@12854
   439
      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
schirmer@12854
   440
                               intro: dynmethd_declclass)
schirmer@12854
   441
    next
schirmer@12854
   442
      case IntVir
schirmer@12854
   443
      with wf ClassT dynlookup statC_prop invC_prop 
schirmer@12854
   444
      show ?thesis
schirmer@12854
   445
	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
schirmer@12854
   446
                           DynT_prop_def
schirmer@12854
   447
	            intro: dynmethd_declclass)
schirmer@12854
   448
    qed
schirmer@12854
   449
  next
schirmer@12854
   450
    case ArrayT
schirmer@12854
   451
    show ?thesis
schirmer@12854
   452
    proof (cases mode)
schirmer@12854
   453
      case Static
schirmer@12854
   454
      with wf ArrayT dynlookup show ?thesis
schirmer@12854
   455
	by (auto simp add: invocation_declclass_def dynlookup_def 
schirmer@12854
   456
                           dynimethd_def dynmethd_C_C
schirmer@12854
   457
                    intro: dynmethd_declclass
schirmer@12854
   458
                     dest: table_of_map_SomeI)
schirmer@12854
   459
    next
schirmer@12854
   460
      case SuperM
schirmer@12854
   461
      with ArrayT statA_prop show ?thesis by blast
schirmer@12854
   462
    next
schirmer@12854
   463
      case IntVir
schirmer@12854
   464
      with wf ArrayT dynlookup invC_prop show ?thesis
schirmer@12854
   465
	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
schirmer@12854
   466
                           DynT_prop_def dynmethd_C_C
schirmer@12854
   467
                    intro: dynmethd_declclass
schirmer@12854
   468
                     dest: table_of_map_SomeI)
schirmer@12854
   469
    qed
schirmer@12854
   470
  qed
schirmer@12854
   471
qed
schirmer@12925
   472
schirmer@12854
   473
lemma DynT_mheadsD: 
schirmer@12925
   474
"\<lbrakk>G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT; 
schirmer@12854
   475
  wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
schirmer@12925
   476
  (statDeclT,sm) \<in> mheads G C statT sig; 
schirmer@12925
   477
  invC = invocation_class (invmode sm e) s a' statT;
schirmer@12925
   478
  declC =invocation_declclass G (invmode sm e) s a' statT sig
schirmer@12854
   479
 \<rbrakk> \<Longrightarrow> 
schirmer@12854
   480
  \<exists> dm. 
schirmer@12925
   481
  methd G declC sig = Some dm \<and> dynlookup G statT invC sig = Some dm  \<and> 
schirmer@12925
   482
  G\<turnstile>resTy (mthd dm)\<preceq>resTy sm \<and> 
schirmer@12854
   483
  wf_mdecl G declC (sig, mthd dm) \<and>
schirmer@12854
   484
  declC = declclass dm \<and>
schirmer@12854
   485
  is_static dm = is_static sm \<and>  
schirmer@12854
   486
  is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
schirmer@12925
   487
  (if invmode sm e = IntVir
schirmer@12854
   488
      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
schirmer@12854
   489
      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
schirmer@12854
   490
            \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
schirmer@12925
   491
            statDeclT = ClassT (declclass dm))"
schirmer@12854
   492
proof -
schirmer@12925
   493
  assume invC_prop: "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" 
schirmer@12854
   494
     and        wf: "wf_prog G" 
schirmer@12854
   495
     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
schirmer@12925
   496
     and        sm: "(statDeclT,sm) \<in> mheads G C statT sig" 
schirmer@12925
   497
     and      invC: "invC = invocation_class (invmode sm e) s a' statT"
schirmer@12854
   498
     and     declC: "declC = 
schirmer@12925
   499
                    invocation_declclass G (invmode sm e) s a' statT sig"
schirmer@12854
   500
  from wt_e wf have type_statT: "is_type G (RefT statT)"
schirmer@12854
   501
    by (auto dest: ty_expr_is_type)
schirmer@12854
   502
  from sm have not_Null: "statT \<noteq> NullT" by auto
schirmer@12854
   503
  from type_statT 
schirmer@12854
   504
  have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
schirmer@12854
   505
    by (auto)
schirmer@12854
   506
  from type_statT wt_e 
schirmer@12854
   507
  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
schirmer@12925
   508
                                        invmode sm e \<noteq> SuperM)"
schirmer@12854
   509
    by (auto dest: invocationTypeExpr_noClassD)
schirmer@12854
   510
  from wt_e
schirmer@12925
   511
  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode sm e \<noteq> SuperM)"
schirmer@12854
   512
    by (auto dest: invocationTypeExpr_noClassD)
schirmer@12854
   513
  show ?thesis
schirmer@12925
   514
  proof (cases "invmode sm e = IntVir")
schirmer@12854
   515
    case True
schirmer@12854
   516
    with invC_prop not_Null
schirmer@12854
   517
    have invC_prop': " is_class G invC \<and> 
schirmer@12854
   518
                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
schirmer@12854
   519
                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
schirmer@12854
   520
      by (auto simp add: DynT_prop_def) 
schirmer@12854
   521
    from True 
schirmer@12854
   522
    have "\<not> is_static sm"
schirmer@12925
   523
      by (simp add: invmode_IntVir_eq member_is_static_simp)
schirmer@12854
   524
    with invC_prop' not_Null
schirmer@12854
   525
    have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
schirmer@12854
   526
      by (cases statT) auto
schirmer@12854
   527
    with sm wf type_statT obtain dm where
schirmer@12854
   528
           dm: "dynlookup G statT invC sig = Some dm" and
schirmer@12925
   529
      resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy sm"      and
schirmer@12854
   530
       static: "is_static dm = is_static sm"
schirmer@12925
   531
      by  - (drule dynamic_mheadsD,force+)
schirmer@12854
   532
    with declC invC not_Null 
schirmer@12854
   533
    have declC': "declC = (declclass dm)" 
schirmer@12854
   534
      by (auto simp add: invocation_declclass_def)
schirmer@12854
   535
    with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
schirmer@12854
   536
    have dm': "methd G declC sig = Some dm"
schirmer@12854
   537
      by - (drule invocation_methd,auto)
schirmer@12854
   538
    from wf dm invC_prop' declC' type_statT 
schirmer@12854
   539
    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
schirmer@12854
   540
      by (auto dest: dynlookup_declC)
schirmer@12854
   541
    from wf dm' declC_prop declC' 
schirmer@12854
   542
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
schirmer@12854
   543
      by (auto dest: methd_wf_mdecl)
schirmer@12854
   544
    from invC_prop' 
schirmer@12854
   545
    have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
schirmer@12854
   546
      by auto
schirmer@12854
   547
    from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
schirmer@12925
   548
         dm
schirmer@12854
   549
    show ?thesis by auto
schirmer@12854
   550
  next
schirmer@12854
   551
    case False
schirmer@12854
   552
    with type_statT wf invC not_Null wf_I wf_A
schirmer@12854
   553
    have invC_prop': "is_class G invC \<and>  
schirmer@12854
   554
                     ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
schirmer@12925
   555
                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object))"
schirmer@12854
   556
        by (case_tac "statT") (auto simp add: invocation_class_def 
schirmer@12854
   557
                                       split: inv_mode.splits)
schirmer@12854
   558
    with not_Null wf
schirmer@12854
   559
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
schirmer@12854
   560
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
schirmer@12854
   561
                                            dynimethd_def)
schirmer@12854
   562
    from sm wf wt_e not_Null False invC_prop' obtain "dm" where
schirmer@12854
   563
                    dm: "methd G invC sig = Some dm"          and
schirmer@12925
   564
	eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
schirmer@12925
   565
	     eq_mheads:"sm=mhead (mthd dm) "
schirmer@12925
   566
      by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
schirmer@12925
   567
    then have static: "is_static dm = is_static sm" by - (auto)
schirmer@12854
   568
    with declC invC dynlookup_static dm
schirmer@12854
   569
    have declC': "declC = (declclass dm)"  
schirmer@12854
   570
      by (auto simp add: invocation_declclass_def)
schirmer@12854
   571
    from invC_prop' wf declC' dm 
schirmer@12854
   572
    have dm': "methd G declC sig = Some dm"
schirmer@12854
   573
      by (auto intro: methd_declclass)
schirmer@12925
   574
    from dynlookup_static dm 
schirmer@12925
   575
    have dm'': "dynlookup G statT invC sig = Some dm"
schirmer@12925
   576
      by simp
schirmer@12854
   577
    from wf dm invC_prop' declC' type_statT 
schirmer@12854
   578
    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
schirmer@12854
   579
      by (auto dest: methd_declC )
schirmer@12854
   580
    then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
schirmer@12854
   581
    from wf dm' declC_prop declC' 
schirmer@12854
   582
    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
schirmer@12854
   583
      by (auto dest: methd_wf_mdecl)
schirmer@12854
   584
    from invC_prop' declC_prop declC_prop1
schirmer@12854
   585
    have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
schirmer@12854
   586
                       \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
schirmer@12854
   587
      by auto
schirmer@12925
   588
    from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
schirmer@12854
   589
         eq_declC_sm_dm eq_mheads static
schirmer@12854
   590
    show ?thesis by auto
schirmer@12854
   591
  qed
schirmer@13688
   592
qed
schirmer@13688
   593
schirmer@13688
   594
corollary DynT_mheadsE [consumes 7]: 
schirmer@13688
   595
--{* Same as @{text DynT_mheadsD} but better suited for application in 
schirmer@13688
   596
typesafety proof   *}
schirmer@13688
   597
 assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
schirmer@13688
   598
     and wf: "wf_prog G" 
schirmer@13688
   599
     and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
schirmer@13688
   600
     and mheads: "(statDeclT,sm) \<in> mheads G C statT sig"
schirmer@13688
   601
     and mode: "mode=invmode sm e" 
schirmer@13688
   602
     and invC: "invC = invocation_class mode s a' statT"
schirmer@13688
   603
     and declC: "declC =invocation_declclass G mode s a' statT sig"
schirmer@13688
   604
     and dm: "\<And> dm. \<lbrakk>methd G declC sig = Some dm; 
schirmer@13688
   605
                      dynlookup G statT invC sig = Some dm; 
schirmer@13688
   606
                      G\<turnstile>resTy (mthd dm)\<preceq>resTy sm; 
schirmer@13688
   607
                      wf_mdecl G declC (sig, mthd dm);
schirmer@13688
   608
                      declC = declclass dm;
schirmer@13688
   609
                      is_static dm = is_static sm;  
schirmer@13688
   610
                      is_class G invC; is_class G declC; G\<turnstile>invC\<preceq>\<^sub>C declC;  
schirmer@13688
   611
                      (if invmode sm e = IntVir
schirmer@13688
   612
                      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
schirmer@13688
   613
                      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
schirmer@13688
   614
                             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and>
schirmer@13688
   615
                             statDeclT = ClassT (declclass dm))\<rbrakk> \<Longrightarrow> P"
schirmer@13688
   616
   shows "P"
schirmer@13688
   617
proof -
schirmer@13688
   618
    from invC_compatible mode have "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" by simp 
schirmer@13688
   619
    moreover note wf wt_e mheads
schirmer@13688
   620
    moreover from invC mode 
schirmer@13688
   621
    have "invC = invocation_class (invmode sm e) s a' statT" by simp
schirmer@13688
   622
    moreover from declC mode 
schirmer@13688
   623
    have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
schirmer@13688
   624
    ultimately show ?thesis
schirmer@13688
   625
      by (rule DynT_mheadsD [THEN exE,rule_format])
schirmer@13688
   626
         (elim conjE,rule dm)
schirmer@13688
   627
qed
schirmer@13688
   628
   
schirmer@12854
   629
schirmer@12854
   630
lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
schirmer@12854
   631
 isrtype G (statT);
schirmer@12854
   632
 G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
schirmer@12854
   633
  mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
schirmer@12854
   634
                    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
schirmer@12854
   635
 \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
schirmer@12854
   636
apply (case_tac "mode = IntVir")
schirmer@12854
   637
apply (drule conf_RefTD)
schirmer@12854
   638
apply (force intro!: conf_AddrI 
schirmer@12854
   639
            simp add: obj_class_def split add: obj_tag.split_asm)
schirmer@12854
   640
apply  clarsimp
schirmer@12854
   641
apply  safe
schirmer@12854
   642
apply    (erule (1) widen.subcls [THEN conf_widen])
schirmer@12854
   643
apply    (erule wf_ws_prog)
schirmer@12854
   644
schirmer@12854
   645
apply    (frule widen_Object) apply (erule wf_ws_prog)
schirmer@12854
   646
apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
schirmer@12854
   647
done
schirmer@12854
   648
schirmer@12925
   649
lemma Ass_lemma:
schirmer@12925
   650
"\<lbrakk> G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2;
schirmer@12925
   651
   G,s2\<turnstile>v\<Colon>\<preceq>eT;s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk>
schirmer@12925
   652
\<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and>
schirmer@12925
   653
      (normal (assign f v (Norm s2)) \<longrightarrow> G,store (assign f v (Norm s2))\<turnstile>v\<Colon>\<preceq>eT)"
schirmer@12854
   654
apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
schirmer@12854
   655
apply (drule eval_gext', clarsimp)
schirmer@12854
   656
apply (erule conf_gext)
schirmer@12854
   657
apply simp
schirmer@12854
   658
done
schirmer@12854
   659
schirmer@12854
   660
lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
schirmer@12854
   661
    x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
schirmer@12854
   662
apply (auto split add: split_abrupt_if simp add: throw_def2)
schirmer@12854
   663
apply (erule conforms_xconf)
schirmer@12854
   664
apply (frule conf_RefTD)
schirmer@12854
   665
apply (auto elim: widen.subcls [THEN conf_widen])
schirmer@12854
   666
done
schirmer@12854
   667
schirmer@12854
   668
lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
schirmer@12854
   669
 (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
schirmer@12854
   670
 \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
schirmer@12854
   671
apply (rule conforms_allocL)
schirmer@12854
   672
apply  (erule conforms_NormI)
schirmer@12854
   673
apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
schirmer@12854
   674
apply (auto intro!: conf_AddrI)
schirmer@12854
   675
done
schirmer@12854
   676
schirmer@12854
   677
lemma Fin_lemma: 
schirmer@13688
   678
"\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L);
schirmer@13688
   679
  dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
schirmer@12854
   680
\<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
schirmer@13688
   681
apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
schirmer@12854
   682
done
schirmer@12854
   683
schirmer@12925
   684
lemma FVar_lemma1: 
schirmer@12925
   685
"\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
schirmer@12925
   686
  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; 
schirmer@12925
   687
  statDeclC \<noteq> Object; 
schirmer@12925
   688
  class G statDeclC = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; 
schirmer@12925
   689
  inited statDeclC (globs s1); 
schirmer@12854
   690
  (if static f then id else np a) x2 = None\<rbrakk> 
schirmer@12854
   691
 \<Longrightarrow>  
schirmer@12925
   692
  \<exists>obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
schirmer@12925
   693
                  = Some obj \<and> 
schirmer@12925
   694
  var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
schirmer@12925
   695
          (Inl(fn,statDeclC)) = Some (type f)"
schirmer@12854
   696
apply (drule initedD)
schirmer@12854
   697
apply (frule subcls_is_class2, simp (no_asm_simp))
schirmer@12854
   698
apply (case_tac "static f")
schirmer@12854
   699
apply  clarsimp
schirmer@12854
   700
apply  (drule (1) rev_gext_objD, clarsimp)
schirmer@12854
   701
apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
schirmer@12854
   702
apply  (rule var_tys_Some_eq [THEN iffD2])
schirmer@12854
   703
apply  clarsimp
schirmer@12854
   704
apply  (erule fields_table_SomeI, simp (no_asm))
schirmer@12854
   705
apply clarsimp
schirmer@12854
   706
apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
schirmer@12854
   707
apply (auto dest!: widen_Array split add: obj_tag.split)
schirmer@12854
   708
apply (rule fields_table_SomeI)
schirmer@12854
   709
apply (auto elim!: fields_mono subcls_is_class2)
schirmer@12854
   710
done
schirmer@12854
   711
schirmer@12925
   712
lemma FVar_lemma2: "error_free state
schirmer@12925
   713
       \<Longrightarrow> error_free
schirmer@12925
   714
           (assign
schirmer@12925
   715
             (\<lambda>v. supd
schirmer@12925
   716
                   (upd_gobj
schirmer@12925
   717
                     (if static field then Inr statDeclC
schirmer@12925
   718
                      else Inl (the_Addr a))
schirmer@12925
   719
                     (Inl (fn, statDeclC)) v))
schirmer@12925
   720
             w state)"
schirmer@12925
   721
proof -
schirmer@12925
   722
  assume error_free: "error_free state"
schirmer@12925
   723
  obtain a s where "state=(a,s)"
schirmer@12925
   724
    by (cases state) simp
schirmer@12925
   725
  with error_free
schirmer@12925
   726
  show ?thesis
schirmer@12925
   727
    by (cases a) auto
schirmer@12925
   728
qed
schirmer@12925
   729
schirmer@12925
   730
declare split_paired_All [simp del] split_paired_Ex [simp del] 
schirmer@12925
   731
declare split_if     [split del] split_if_asm     [split del] 
schirmer@12925
   732
        option.split [split del] option.split_asm [split del]
schirmer@12925
   733
ML_setup {*
schirmer@12925
   734
simpset_ref() := simpset() delloop "split_all_tac";
schirmer@12925
   735
claset_ref () := claset () delSWrapper "split_all_tac"
schirmer@12925
   736
*}
schirmer@12854
   737
lemma FVar_lemma: 
schirmer@12925
   738
"\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
schirmer@12925
   739
  G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
schirmer@12925
   740
  table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
schirmer@12925
   741
  wf_prog G;   
schirmer@12925
   742
  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class statC; 
schirmer@12925
   743
  statDeclC \<noteq> Object; class G statDeclC = Some y;   
schirmer@12925
   744
  (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited statDeclC (globs s1)\<rbrakk> \<Longrightarrow>  
schirmer@12854
   745
  G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
schirmer@12854
   746
apply (unfold assign_conforms_def)
schirmer@12854
   747
apply (drule sym)
schirmer@12854
   748
apply (clarsimp simp add: fvar_def2)
schirmer@12854
   749
apply (drule (9) FVar_lemma1)
schirmer@12854
   750
apply (clarsimp)
schirmer@12854
   751
apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
schirmer@12854
   752
apply clarsimp
schirmer@12925
   753
apply (rule conjI)
schirmer@12925
   754
apply   clarsimp
schirmer@12925
   755
apply   (drule (1) rev_gext_objD)
schirmer@12925
   756
apply   (force elim!: conforms_upd_gobj)
schirmer@12925
   757
schirmer@12925
   758
apply   (blast intro: FVar_lemma2)
schirmer@12854
   759
done
schirmer@12925
   760
declare split_paired_All [simp] split_paired_Ex [simp] 
schirmer@12925
   761
declare split_if     [split] split_if_asm     [split] 
schirmer@12925
   762
        option.split [split] option.split_asm [split]
schirmer@12925
   763
ML_setup {*
schirmer@12925
   764
claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
schirmer@12925
   765
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
schirmer@12925
   766
*}
schirmer@12854
   767
schirmer@12854
   768
schirmer@12854
   769
lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
schirmer@12854
   770
 the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
schirmer@12854
   771
\<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
schirmer@12854
   772
apply (erule widen_Array_Array [THEN conf_widen])
schirmer@12854
   773
apply  (erule_tac [2] wf_ws_prog)
schirmer@12854
   774
apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
schirmer@12854
   775
defer apply assumption
schirmer@12854
   776
apply (force intro: var_tys_Some_eq [THEN iffD2])
schirmer@12854
   777
done
schirmer@12854
   778
schirmer@12854
   779
lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
schirmer@12854
   780
proof record_split
schirmer@12854
   781
  fix tag values more
schirmer@12854
   782
  show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
schirmer@12854
   783
    by auto
schirmer@12854
   784
qed
schirmer@12854
   785
 
schirmer@12925
   786
lemma AVar_lemma2: "error_free state 
schirmer@12925
   787
       \<Longrightarrow> error_free
schirmer@12925
   788
           (assign
schirmer@12925
   789
             (\<lambda>v (x, s').
schirmer@12925
   790
                 ((raise_if (\<not> G,s'\<turnstile>v fits T) ArrStore) x,
schirmer@12925
   791
                  upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
schirmer@12925
   792
             w state)"
schirmer@12925
   793
proof -
schirmer@12925
   794
  assume error_free: "error_free state"
schirmer@12925
   795
  obtain a s where "state=(a,s)"
schirmer@12925
   796
    by (cases state) simp
schirmer@12925
   797
  with error_free
schirmer@12925
   798
  show ?thesis
schirmer@12925
   799
    by (cases a) auto
schirmer@12925
   800
qed
schirmer@12925
   801
schirmer@12854
   802
lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
schirmer@12854
   803
  ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
schirmer@12854
   804
  (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>v\<Colon>\<preceq>Ta \<and> s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)"
schirmer@12854
   805
apply (unfold assign_conforms_def)
schirmer@12854
   806
apply (drule sym)
schirmer@12854
   807
apply (clarsimp simp add: avar_def2)
schirmer@12854
   808
apply (drule (1) conf_gext)
schirmer@12854
   809
apply (drule conf_RefTD, clarsimp)
schirmer@12854
   810
apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
schirmer@12854
   811
defer
schirmer@12854
   812
apply   (rule obj_split)
schirmer@12854
   813
apply clarify
schirmer@12854
   814
apply (frule obj_ty_widenD)
schirmer@12854
   815
apply (auto dest!: widen_Class)
schirmer@12925
   816
apply   (force dest: AVar_lemma1)
schirmer@12925
   817
schirmer@12925
   818
apply   (force elim!: fits_Array dest: gext_objD 
schirmer@12925
   819
         intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
schirmer@12854
   820
done
schirmer@12854
   821
schirmer@13688
   822
schirmer@12925
   823
section "Call"
schirmer@12854
   824
schirmer@12854
   825
lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
schirmer@13688
   826
  wf_mhead G P sig mh;
schirmer@12854
   827
  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
schirmer@13688
   828
  G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
schirmer@13688
   829
      [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
schirmer@12854
   830
apply (unfold wf_mhead_def)
schirmer@12854
   831
apply clarify
schirmer@13688
   832
apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
schirmer@12854
   833
apply (drule wf_ws_prog)
schirmer@12854
   834
apply (erule (2) conf_list_widen)
schirmer@12854
   835
done
schirmer@12854
   836
schirmer@12854
   837
schirmer@12854
   838
lemma lconf_map_lname [simp]: 
schirmer@12854
   839
  "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
schirmer@12854
   840
   =
schirmer@12854
   841
  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
schirmer@12854
   842
apply (unfold lconf_def)
schirmer@13688
   843
apply (auto split add: lname.splits)
schirmer@13688
   844
done
schirmer@13688
   845
schirmer@13688
   846
lemma wlconf_map_lname [simp]: 
schirmer@13688
   847
  "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
schirmer@13688
   848
   =
schirmer@13688
   849
  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
schirmer@13688
   850
apply (unfold wlconf_def)
schirmer@13688
   851
apply (auto split add: lname.splits)
schirmer@12854
   852
done
schirmer@12854
   853
schirmer@12854
   854
lemma lconf_map_ename [simp]:
schirmer@12854
   855
  "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
schirmer@12854
   856
   =
schirmer@12854
   857
  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
schirmer@12854
   858
apply (unfold lconf_def)
schirmer@13688
   859
apply (auto split add: ename.splits)
schirmer@12854
   860
done
schirmer@12854
   861
schirmer@13688
   862
lemma wlconf_map_ename [simp]:
schirmer@13688
   863
  "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
schirmer@13688
   864
   =
schirmer@13688
   865
  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
schirmer@13688
   866
apply (unfold wlconf_def)
schirmer@13688
   867
apply (auto split add: ename.splits)
schirmer@13688
   868
done
schirmer@13688
   869
schirmer@13688
   870
schirmer@12854
   871
schirmer@12854
   872
lemma defval_conf1 [rule_format (no_asm), elim]: 
schirmer@12854
   873
  "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
schirmer@12854
   874
apply (unfold conf_def)
schirmer@12854
   875
apply (induct "T")
schirmer@12854
   876
apply (auto intro: prim_ty.induct)
schirmer@12854
   877
done
schirmer@12854
   878
schirmer@13688
   879
lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
schirmer@13688
   880
by (auto simp add: abrupt_if_def)
schirmer@13688
   881
schirmer@12925
   882
declare split_paired_All [simp del] split_paired_Ex [simp del] 
schirmer@12925
   883
declare split_if     [split del] split_if_asm     [split del] 
schirmer@12925
   884
        option.split [split del] option.split_asm [split del]
schirmer@12925
   885
ML_setup {*
schirmer@12925
   886
simpset_ref() := simpset() delloop "split_all_tac";
schirmer@12925
   887
claset_ref () := claset () delSWrapper "split_all_tac"
schirmer@12925
   888
*}
schirmer@12854
   889
lemma conforms_init_lvars: 
schirmer@12854
   890
"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
schirmer@12854
   891
  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
schirmer@12854
   892
  (x, s)\<Colon>\<preceq>(G, L); 
schirmer@12854
   893
  methd G declC sig = Some dm;  
schirmer@12854
   894
  isrtype G statT;
schirmer@12854
   895
  G\<turnstile>invC\<preceq>\<^sub>C declC; 
schirmer@12854
   896
  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
schirmer@12854
   897
  invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
schirmer@12854
   898
  invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
schirmer@12854
   899
       (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
schirmer@12854
   900
    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
schirmer@12854
   901
  invC  = invocation_class (invmode (mhd sm) e) s a' statT;
schirmer@12854
   902
  declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
schirmer@13688
   903
  x\<noteq>Some (Jump Ret) 
schirmer@12854
   904
 \<rbrakk> \<Longrightarrow>  
schirmer@12854
   905
  init_lvars G declC sig (invmode (mhd sm) e) a'  
schirmer@12854
   906
  pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
schirmer@12854
   907
                (case k of
schirmer@12854
   908
                   EName e \<Rightarrow> (case e of 
schirmer@12854
   909
                                 VNam v 
schirmer@12854
   910
                                  \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
schirmer@12854
   911
                                        (pars (mthd dm)[\<mapsto>]parTs sig)) v
schirmer@12854
   912
                               | Res \<Rightarrow> Some (resTy (mthd dm)))
schirmer@12925
   913
                 | This \<Rightarrow> if (is_static (mthd sm)) 
schirmer@12854
   914
                              then None else Some (Class declC)))"
schirmer@12854
   915
apply (simp add: init_lvars_def2)
schirmer@12854
   916
apply (rule conforms_set_locals)
schirmer@12854
   917
apply  (simp (no_asm_simp) split add: split_if)
schirmer@12854
   918
apply (drule  (4) DynT_conf)
schirmer@12854
   919
apply clarsimp
schirmer@12854
   920
(* apply intro *)
schirmer@13688
   921
apply (drule (3) conforms_init_lvars_lemma 
schirmer@13688
   922
                 [where ?lvars="(lcls (mbody (mthd dm)))"])
schirmer@12854
   923
apply (case_tac "dm",simp)
schirmer@12854
   924
apply (rule conjI)
schirmer@13688
   925
apply (unfold wlconf_def, clarify)
schirmer@13688
   926
apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
schirmer@13688
   927
apply   (case_tac "is_static sm")
schirmer@13688
   928
apply     simp
schirmer@13688
   929
apply     simp
schirmer@13688
   930
schirmer@13688
   931
apply   simp
schirmer@13688
   932
apply   (case_tac "is_static sm")
schirmer@13688
   933
apply     simp
schirmer@13688
   934
apply     (simp add: np_no_jump)
schirmer@12854
   935
done
schirmer@12925
   936
declare split_paired_All [simp] split_paired_Ex [simp] 
schirmer@12925
   937
declare split_if     [split] split_if_asm     [split] 
schirmer@12925
   938
        option.split [split] option.split_asm [split]
schirmer@12925
   939
ML_setup {*
schirmer@12925
   940
claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
schirmer@12925
   941
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
schirmer@12925
   942
*}
schirmer@12854
   943
schirmer@12854
   944
schirmer@12854
   945
subsection "accessibility"
schirmer@12854
   946
schirmer@13384
   947
text {* 
schirmer@13384
   948
\par
schirmer@13384
   949
*} (* dummy text command to break paragraph for latex;
schirmer@13384
   950
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@12925
   951
schirmer@12854
   952
theorem dynamic_field_access_ok:
wenzelm@12937
   953
  assumes wf: "wf_prog G" and
wenzelm@12937
   954
    not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
wenzelm@12937
   955
   conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
wenzelm@12937
   956
   conform_s: "s\<Colon>\<preceq>(G, L)" and 
wenzelm@12937
   957
    normal_s: "normal s" and
wenzelm@12937
   958
        wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
wenzelm@12937
   959
           f: "accfield G accC statC fn = Some f" and
wenzelm@12937
   960
        dynC: "if stat then dynC=declclass f  
wenzelm@12937
   961
                       else dynC=obj_class (lookup_obj (store s) a)" and
wenzelm@12937
   962
        stat: "if stat then (is_static f) else (\<not> is_static f)"
schirmer@13688
   963
  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<and>
schirmer@13688
   964
         G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
schirmer@12854
   965
proof (cases "stat")
schirmer@12854
   966
  case True
schirmer@12925
   967
  with stat have static: "(is_static f)" by simp
schirmer@12925
   968
  from True dynC 
schirmer@12925
   969
  have dynC': "dynC=declclass f" by simp
schirmer@12854
   970
  with f
schirmer@12925
   971
  have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
schirmer@12854
   972
    by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
schirmer@12925
   973
  moreover
schirmer@12925
   974
  from wt_e wf have "is_class G statC"
schirmer@12925
   975
    by (auto dest!: ty_expr_is_type)
schirmer@12925
   976
  moreover note wf dynC'
schirmer@12925
   977
  ultimately have
schirmer@12925
   978
     "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
schirmer@12925
   979
    by (auto dest: fields_declC)
schirmer@12925
   980
  with dynC' f static wf
schirmer@12854
   981
  show ?thesis
schirmer@12925
   982
    by (auto dest: static_to_dynamic_accessible_from_static
schirmer@12925
   983
            dest!: accfield_accessibleD )
schirmer@12854
   984
next
schirmer@12854
   985
  case False
schirmer@12925
   986
  with wf conform_a not_Null conform_s dynC
schirmer@12854
   987
  obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
schirmer@12854
   988
    "is_class G dynC"
schirmer@12925
   989
    by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
schirmer@12854
   990
              dest: obj_ty_obj_class1
schirmer@12854
   991
          simp add: obj_ty_obj_class )
schirmer@12854
   992
  with wf f
schirmer@12854
   993
  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
schirmer@12854
   994
    by (auto simp add: accfield_def Let_def
schirmer@12854
   995
                 dest: fields_mono
schirmer@12854
   996
                dest!: table_of_remap_SomeD)
schirmer@12854
   997
  moreover
schirmer@12854
   998
  from f subclseq
schirmer@12854
   999
  have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
schirmer@12854
  1000
    by (auto intro!: static_to_dynamic_accessible_from 
schirmer@12854
  1001
               dest: accfield_accessibleD)
schirmer@12854
  1002
  ultimately show ?thesis
schirmer@12854
  1003
    by blast
schirmer@12854
  1004
qed
schirmer@12854
  1005
schirmer@12925
  1006
lemma error_free_field_access:
wenzelm@12937
  1007
  assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
schirmer@12925
  1008
              wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@12925
  1009
         eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
schirmer@12925
  1010
            eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
schirmer@12925
  1011
           conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
  1012
            conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
schirmer@12925
  1013
              fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
schirmer@12925
  1014
                wf: "wf_prog G"   
wenzelm@12937
  1015
  shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
schirmer@12925
  1016
proof -
schirmer@12925
  1017
  from fvar
schirmer@12925
  1018
  have store_s2': "store s2'=store s2"
schirmer@12925
  1019
    by (cases s2) (simp add: fvar_def2)
schirmer@12925
  1020
  with fvar conf_s2 
schirmer@12925
  1021
  have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
schirmer@12925
  1022
    by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
schirmer@12925
  1023
  from eval_init 
schirmer@12925
  1024
  have initd_statDeclC_s1: "initd statDeclC s1"
schirmer@12925
  1025
    by (rule init_yields_initd)
schirmer@12925
  1026
  with eval_e store_s2'
schirmer@12925
  1027
  have initd_statDeclC_s2': "initd statDeclC s2'"
schirmer@12925
  1028
    by (auto dest: eval_gext intro: inited_gext)
schirmer@12925
  1029
  show ?thesis
schirmer@12925
  1030
  proof (cases "normal s2'")
schirmer@12925
  1031
    case False
schirmer@12925
  1032
    then show ?thesis 
schirmer@12925
  1033
      by (auto simp add: check_field_access_def Let_def)
schirmer@12925
  1034
  next
schirmer@12925
  1035
    case True
schirmer@12925
  1036
    with fvar store_s2' 
schirmer@12925
  1037
    have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
schirmer@12925
  1038
      by (cases s2) (auto simp add: fvar_def2)
schirmer@12925
  1039
    from True fvar store_s2'
schirmer@12925
  1040
    have "normal s2"
schirmer@12925
  1041
      by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
schirmer@12925
  1042
    with conf_a store_s2'
schirmer@12925
  1043
    have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@12925
  1044
      by simp
schirmer@12925
  1045
    from conf_a' conf_s2' True initd_statDeclC_s2' 
schirmer@12925
  1046
      dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
schirmer@12925
  1047
                                   True wt_e accfield ] 
schirmer@12925
  1048
    show ?thesis
schirmer@12925
  1049
      by  (cases "is_static f")
schirmer@12925
  1050
          (auto dest!: initedD
schirmer@12925
  1051
           simp add: check_field_access_def Let_def)
schirmer@12925
  1052
  qed
schirmer@12925
  1053
qed
schirmer@12925
  1054
schirmer@12925
  1055
lemma call_access_ok:
wenzelm@12937
  1056
  assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
wenzelm@12937
  1057
      and        wf: "wf_prog G" 
wenzelm@12937
  1058
      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
wenzelm@12937
  1059
      and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
wenzelm@12937
  1060
      and      invC: "invC = invocation_class (invmode statM e) s a statT"
wenzelm@12937
  1061
  shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
schirmer@12854
  1062
  G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
schirmer@12854
  1063
proof -
schirmer@12854
  1064
  from wt_e wf have type_statT: "is_type G (RefT statT)"
schirmer@12854
  1065
    by (auto dest: ty_expr_is_type)
schirmer@12854
  1066
  from statM have not_Null: "statT \<noteq> NullT" by auto
schirmer@12854
  1067
  from type_statT wt_e 
schirmer@12854
  1068
  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
schirmer@12925
  1069
                                        invmode statM e \<noteq> SuperM)"
schirmer@12854
  1070
    by (auto dest: invocationTypeExpr_noClassD)
schirmer@12854
  1071
  from wt_e
schirmer@12925
  1072
  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
schirmer@12854
  1073
    by (auto dest: invocationTypeExpr_noClassD)
schirmer@12854
  1074
  show ?thesis
schirmer@12925
  1075
  proof (cases "invmode statM e = IntVir")
schirmer@12854
  1076
    case True
schirmer@12854
  1077
    with invC_prop not_Null
schirmer@12854
  1078
    have invC_prop': "is_class G invC \<and>  
schirmer@12854
  1079
                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
schirmer@12854
  1080
                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
schirmer@12854
  1081
      by (auto simp add: DynT_prop_def)
schirmer@12854
  1082
    with True not_Null
schirmer@12854
  1083
    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
schirmer@12925
  1084
     by (cases statT) (auto simp add: invmode_def) 
schirmer@12854
  1085
    with statM type_statT wf 
schirmer@12854
  1086
    show ?thesis
schirmer@12854
  1087
      by - (rule dynlookup_access,auto)
schirmer@12854
  1088
  next
schirmer@12854
  1089
    case False
schirmer@12854
  1090
    with type_statT wf invC not_Null wf_I wf_A
schirmer@12854
  1091
    have invC_prop': " is_class G invC \<and>
schirmer@12854
  1092
                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
schirmer@12854
  1093
                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
schirmer@12854
  1094
        by (case_tac "statT") (auto simp add: invocation_class_def 
schirmer@12854
  1095
                                       split: inv_mode.splits)
schirmer@12854
  1096
    with not_Null wf
schirmer@12854
  1097
    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
schirmer@12854
  1098
      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
schirmer@12854
  1099
                                            dynimethd_def)
schirmer@12854
  1100
   from statM wf wt_e not_Null False invC_prop' obtain dynM where
schirmer@12854
  1101
                "accmethd G accC invC sig = Some dynM" 
schirmer@12854
  1102
     by (auto dest!: static_mheadsD)
schirmer@12854
  1103
   from invC_prop' False not_Null wf_I
schirmer@12854
  1104
   have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
schirmer@12925
  1105
     by (cases statT) (auto simp add: invmode_def) 
schirmer@12854
  1106
   with statM type_statT wf 
schirmer@12854
  1107
    show ?thesis
schirmer@12854
  1108
      by - (rule dynlookup_access,auto)
schirmer@12854
  1109
  qed
schirmer@12854
  1110
qed
schirmer@12854
  1111
schirmer@12925
  1112
lemma error_free_call_access:
wenzelm@12937
  1113
  assumes
schirmer@12925
  1114
   eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
schirmer@12925
  1115
        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
schirmer@12925
  1116
       statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
schirmer@12925
  1117
               = {((statDeclT, statM), pTs')}" and
schirmer@12925
  1118
     conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
  1119
      conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
schirmer@12925
  1120
     invProp: "normal s3 \<Longrightarrow>
schirmer@12925
  1121
                G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
schirmer@12925
  1122
          s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
schirmer@12925
  1123
                        (invmode statM e) a vs s2" and
schirmer@12925
  1124
        invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
schirmer@12925
  1125
    invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
schirmer@12925
  1126
                             a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
schirmer@12925
  1127
          wf: "wf_prog G"
wenzelm@12937
  1128
  shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
schirmer@12925
  1129
   = s3"
schirmer@12925
  1130
proof (cases "normal s2")
schirmer@12925
  1131
  case False
schirmer@12925
  1132
  with s3 
schirmer@12925
  1133
  have "abrupt s3 = abrupt s2"  
schirmer@12925
  1134
    by (auto simp add: init_lvars_def2)
schirmer@12925
  1135
  with False
schirmer@12925
  1136
  show ?thesis
schirmer@12925
  1137
    by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1138
next
schirmer@12925
  1139
  case True
schirmer@12925
  1140
  note normal_s2 = True
schirmer@12925
  1141
  with eval_args
schirmer@12925
  1142
  have normal_s1: "normal s1"
schirmer@12925
  1143
    by (cases "normal s1") auto
schirmer@12925
  1144
  with conf_a eval_args 
schirmer@12925
  1145
  have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
schirmer@12925
  1146
    by (auto dest: eval_gext intro: conf_gext)
schirmer@12925
  1147
  show ?thesis
schirmer@12925
  1148
  proof (cases "a=Null \<longrightarrow> (is_static statM)")
schirmer@12925
  1149
    case False
schirmer@12925
  1150
    then obtain "\<not> is_static statM" "a=Null" 
schirmer@12925
  1151
      by blast
schirmer@12925
  1152
    with normal_s2 s3
schirmer@12925
  1153
    have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
schirmer@12925
  1154
      by (auto simp add: init_lvars_def2)
schirmer@12925
  1155
    then show ?thesis
schirmer@12925
  1156
      by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1157
  next
schirmer@12925
  1158
    case True
schirmer@12925
  1159
    from statM 
schirmer@12925
  1160
    obtain
schirmer@12925
  1161
      statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
schirmer@12925
  1162
      by (blast dest: max_spec2mheads)
schirmer@12925
  1163
    from True normal_s2 s3
schirmer@12925
  1164
    have "normal s3"
schirmer@12925
  1165
      by (auto simp add: init_lvars_def2)
schirmer@12925
  1166
    then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
schirmer@12925
  1167
      by (rule invProp)
schirmer@12925
  1168
    with wt_e statM' wf invC
schirmer@12925
  1169
    obtain dynM where 
schirmer@12925
  1170
      dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@12925
  1171
      acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
schirmer@12925
  1172
                          in invC dyn_accessible_from accC"
schirmer@12925
  1173
      by (force dest!: call_access_ok)
schirmer@12925
  1174
    moreover
schirmer@12925
  1175
    from s3 invC
schirmer@12925
  1176
    have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
schirmer@12925
  1177
      by (cases s2,cases "invmode statM e") 
schirmer@12925
  1178
         (simp add: init_lvars_def2 del: invmode_Static_eq)+
schirmer@12925
  1179
    ultimately
schirmer@12925
  1180
    show ?thesis
schirmer@12925
  1181
      by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1182
  qed
schirmer@12925
  1183
qed
schirmer@12925
  1184
schirmer@13688
  1185
lemma map_upds_eq_length_append_simp:
schirmer@13688
  1186
  "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
schirmer@13688
  1187
proof (induct ps) 
schirmer@13688
  1188
  case Nil thus ?case by simp
schirmer@13688
  1189
next
schirmer@13688
  1190
  case (Cons p ps tab qs)
schirmer@13688
  1191
  have "length (p#ps) = length qs" .
schirmer@13688
  1192
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
schirmer@13688
  1193
    by (cases qs) auto
schirmer@13688
  1194
  from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
schirmer@13688
  1195
    by (rule Cons.hyps)
schirmer@13688
  1196
  with qs show ?case 
schirmer@13688
  1197
    by simp
schirmer@13688
  1198
qed
schirmer@13688
  1199
schirmer@13688
  1200
lemma map_upds_upd_eq_length_simp:
schirmer@13688
  1201
  "\<And> tab qs x y. length ps = length qs 
schirmer@13688
  1202
                  \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
schirmer@13688
  1203
proof (induct "ps")
schirmer@13688
  1204
  case Nil thus ?case by simp
schirmer@13688
  1205
next
schirmer@13688
  1206
  case (Cons p ps tab qs x y)
schirmer@13688
  1207
  have "length (p#ps) = length qs" .
schirmer@13688
  1208
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
schirmer@13688
  1209
    by (cases qs) auto
schirmer@13688
  1210
  from eq_length 
schirmer@13688
  1211
  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
schirmer@13688
  1212
    by (rule Cons.hyps)
schirmer@13688
  1213
  with qs show ?case
schirmer@13688
  1214
    by simp
schirmer@13688
  1215
qed
schirmer@13688
  1216
schirmer@13688
  1217
schirmer@13688
  1218
lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
schirmer@13688
  1219
by simp
schirmer@13688
  1220
schirmer@13688
  1221
lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) z"
schirmer@13688
  1222
by (simp add: fun_upd_def)
schirmer@13688
  1223
schirmer@13688
  1224
lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
schirmer@13688
  1225
by (cases xs) simp+
schirmer@13688
  1226
schirmer@13688
  1227
lemma map_upds_cong_ext: 
schirmer@13688
  1228
 "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) z"
schirmer@13688
  1229
proof (induct xs)
schirmer@13688
  1230
  case Nil thus ?case by simp
schirmer@13688
  1231
next
schirmer@13688
  1232
  case (Cons x xs tab tab' ys)
schirmer@13688
  1233
  have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
schirmer@13688
  1234
    by (rule Cons.hyps) (rule map_upd_cong_ext)
schirmer@13688
  1235
  thus ?case
schirmer@13688
  1236
    by simp
schirmer@13688
  1237
qed
schirmer@13688
  1238
   
schirmer@13688
  1239
lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
schirmer@13688
  1240
  by simp
schirmer@13688
  1241
schirmer@13688
  1242
schirmer@13688
  1243
lemma map_upds_override_cong:
schirmer@13688
  1244
"\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
schirmer@13688
  1245
 (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
schirmer@13688
  1246
proof (induct ws)
schirmer@13688
  1247
  case Nil thus ?case by simp
schirmer@13688
  1248
next
schirmer@13688
  1249
  case (Cons w ws tab tab' zs)
schirmer@13688
  1250
  have x: "x \<in> set (w#ws)" .
schirmer@13688
  1251
  show ?case
schirmer@13688
  1252
  proof (cases "x=w")
schirmer@13688
  1253
    case True thus ?thesis
schirmer@13688
  1254
      by simp (rule map_upds_cong_ext, rule map_upd_override)
schirmer@13688
  1255
  next
schirmer@13688
  1256
    case False
schirmer@13688
  1257
    with x have "x \<in> set ws"
schirmer@13688
  1258
      by simp
schirmer@13688
  1259
    with Cons.hyps show ?thesis
schirmer@13688
  1260
      by simp
schirmer@13688
  1261
  qed
schirmer@13688
  1262
qed
schirmer@13688
  1263
schirmer@13688
  1264
lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
schirmer@13688
  1265
 shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
schirmer@13688
  1266
proof (induct ps)
schirmer@13688
  1267
  case Nil thus ?case by simp
schirmer@13688
  1268
next
schirmer@13688
  1269
  case (Cons p ps tab qs)
schirmer@13688
  1270
  have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
schirmer@13688
  1271
          =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
schirmer@13688
  1272
    by (rule Cons.hyps)
schirmer@13688
  1273
  moreover
schirmer@13688
  1274
  have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
schirmer@13688
  1275
    by (cases qs) simp+
schirmer@13688
  1276
  ultimately show ?case
schirmer@13688
  1277
    by simp (rule map_upds_override_cong)
schirmer@13688
  1278
qed
schirmer@13688
  1279
 
schirmer@13688
  1280
schirmer@13688
  1281
lemma map_upds_eq_length_suffix: "\<And> tab qs. 
schirmer@13688
  1282
        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
schirmer@13688
  1283
proof (induct ps)
schirmer@13688
  1284
  case Nil thus ?case by simp
schirmer@13688
  1285
next
schirmer@13688
  1286
  case (Cons p ps tab qs)
schirmer@13688
  1287
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
schirmer@13688
  1288
    by (cases qs) auto
schirmer@13688
  1289
  from eq_length
schirmer@13688
  1290
  have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
schirmer@13688
  1291
    by (rule Cons.hyps)
schirmer@13688
  1292
  with qs show ?case 
schirmer@13688
  1293
    by simp
schirmer@13688
  1294
qed
schirmer@13688
  1295
  
schirmer@13688
  1296
  
schirmer@13688
  1297
lemma map_upds_upds_eq_length_prefix_simp:
schirmer@13688
  1298
  "\<And> tab qs. length ps = length qs
schirmer@13688
  1299
              \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
schirmer@13688
  1300
proof (induct ps)
schirmer@13688
  1301
  case Nil thus ?case by simp
schirmer@13688
  1302
next
schirmer@13688
  1303
  case (Cons p ps tab qs)
schirmer@13688
  1304
  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
schirmer@13688
  1305
    by (cases qs) auto
schirmer@13688
  1306
  from eq_length 
schirmer@13688
  1307
  have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
schirmer@13688
  1308
    by (rule Cons.hyps)
schirmer@13688
  1309
  with qs 
schirmer@13688
  1310
  show ?case by simp
schirmer@13688
  1311
qed
schirmer@13688
  1312
schirmer@13688
  1313
lemma map_upd_cut_irrelevant:
schirmer@13688
  1314
"\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<rbrakk>
schirmer@13688
  1315
    \<Longrightarrow> tab vn = Some el"
schirmer@13688
  1316
by (cases "tab' vn = None") (simp add: fun_upd_def)+
schirmer@13688
  1317
schirmer@13688
  1318
lemma map_upd_Some_expand:
schirmer@13688
  1319
"\<lbrakk>tab vn = Some z\<rbrakk>
schirmer@13688
  1320
    \<Longrightarrow> \<exists> z. (tab(x\<mapsto>y)) vn = Some z"
schirmer@13688
  1321
by (simp add: fun_upd_def)
schirmer@13688
  1322
schirmer@13688
  1323
lemma map_upds_Some_expand:
schirmer@13688
  1324
"\<And> tab ys z. \<lbrakk>tab vn = Some z\<rbrakk>
schirmer@13688
  1325
    \<Longrightarrow> \<exists> z. (tab(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1326
proof (induct xs)
schirmer@13688
  1327
  case Nil thus ?case by simp
schirmer@13688
  1328
next
schirmer@13688
  1329
  case (Cons x xs tab ys z)
schirmer@13688
  1330
  have "tab vn = Some z" .
schirmer@13688
  1331
  then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
schirmer@13688
  1332
    by (rule map_upd_Some_expand [of tab,elim_format]) blast
schirmer@13688
  1333
  hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
schirmer@13688
  1334
    by (rule Cons.hyps)
schirmer@13688
  1335
  thus ?case
schirmer@13688
  1336
    by simp
schirmer@13688
  1337
qed
schirmer@13688
  1338
schirmer@13688
  1339
schirmer@13688
  1340
lemma map_upd_Some_swap:
schirmer@13688
  1341
 "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
schirmer@13688
  1342
by (simp add: fun_upd_def)
schirmer@13688
  1343
schirmer@13688
  1344
lemma map_upd_None_swap:
schirmer@13688
  1345
 "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
schirmer@13688
  1346
by (simp add: fun_upd_def)
schirmer@13688
  1347
schirmer@13688
  1348
schirmer@13688
  1349
lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
schirmer@13688
  1350
by (simp add: fun_upd_def)
schirmer@13688
  1351
schirmer@13688
  1352
lemma map_eq_upds_eq: 
schirmer@13688
  1353
  "\<And> tab tab' ys. 
schirmer@13688
  1354
   tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
schirmer@13688
  1355
proof (induct xs)
schirmer@13688
  1356
  case Nil thus ?case by simp 
schirmer@13688
  1357
next
schirmer@13688
  1358
  case (Cons x xs tab tab' ys)
schirmer@13688
  1359
  have "tab vn = tab' vn" .
schirmer@13688
  1360
  hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
schirmer@13688
  1361
    by (rule map_eq_upd_eq)
schirmer@13688
  1362
  hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
schirmer@13688
  1363
    by (rule Cons.hyps)
schirmer@13688
  1364
  thus ?case 
schirmer@13688
  1365
    by simp
schirmer@13688
  1366
qed
schirmer@13688
  1367
schirmer@13688
  1368
lemma map_upd_in_expansion_map_swap:
schirmer@13688
  1369
 "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
schirmer@13688
  1370
                 \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
schirmer@13688
  1371
by (simp add: fun_upd_def)
schirmer@13688
  1372
schirmer@13688
  1373
lemma map_upds_in_expansion_map_swap:
schirmer@13688
  1374
 "\<And>tab tab' ys z. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
schirmer@13688
  1375
                 \<Longrightarrow>  (tab'(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1376
proof (induct xs)
schirmer@13688
  1377
  case Nil thus ?case by simp
schirmer@13688
  1378
next
schirmer@13688
  1379
  case (Cons x xs tab tab' ys z)
schirmer@13688
  1380
  from Cons.prems obtain 
schirmer@13688
  1381
    some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
schirmer@13688
  1382
    tab_not_z: "tab vn \<noteq> Some z"
schirmer@13688
  1383
    by simp
schirmer@13688
  1384
  show ?case
schirmer@13688
  1385
  proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
schirmer@13688
  1386
    case True
schirmer@13688
  1387
    with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
schirmer@13688
  1388
      by (rule Cons.hyps)
schirmer@13688
  1389
    thus ?thesis 
schirmer@13688
  1390
      by simp
schirmer@13688
  1391
  next
schirmer@13688
  1392
    case False
schirmer@13688
  1393
    hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
schirmer@13688
  1394
    moreover
schirmer@13688
  1395
    from tabx_z tab_not_z
schirmer@13688
  1396
    have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
schirmer@13688
  1397
      by (rule map_upd_in_expansion_map_swap)
schirmer@13688
  1398
    ultimately
schirmer@13688
  1399
    have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
schirmer@13688
  1400
      by simp
schirmer@13688
  1401
    hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
schirmer@13688
  1402
      by (rule map_eq_upds_eq)
schirmer@13688
  1403
    with some 
schirmer@13688
  1404
    show ?thesis 
schirmer@13688
  1405
      by simp
schirmer@13688
  1406
  qed
schirmer@13688
  1407
qed
schirmer@13688
  1408
   
schirmer@13688
  1409
lemma map_upds_Some_swap: 
schirmer@13688
  1410
 assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1411
    shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1412
proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
schirmer@13688
  1413
  case True
schirmer@13688
  1414
  then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
schirmer@13688
  1415
    by (rule map_upd_Some_swap [elim_format]) blast
schirmer@13688
  1416
  thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1417
    by (rule map_upds_Some_expand)
schirmer@13688
  1418
next
schirmer@13688
  1419
  case False
schirmer@13688
  1420
  with r_u
schirmer@13688
  1421
  have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1422
    by (rule map_upds_in_expansion_map_swap)
schirmer@13688
  1423
  thus ?thesis
schirmer@13688
  1424
    by simp
schirmer@13688
  1425
qed
schirmer@13688
  1426
 
schirmer@13688
  1427
lemma map_upds_Some_insert:
schirmer@13688
  1428
  assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1429
    shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1430
proof (cases "\<exists> z. tab vn = Some z")
schirmer@13688
  1431
  case True
schirmer@13688
  1432
  then obtain z' where "tab vn = Some z'" by blast
schirmer@13688
  1433
  then obtain z'' where "(tab(u\<mapsto>v)) vn = Some z''"
schirmer@13688
  1434
    by (rule map_upd_Some_expand [elim_format]) blast
schirmer@13688
  1435
  thus ?thesis
schirmer@13688
  1436
    by (rule map_upds_Some_expand)
schirmer@13688
  1437
next
schirmer@13688
  1438
  case False
schirmer@13688
  1439
  hence "tab vn \<noteq> Some z" by simp
schirmer@13688
  1440
  with z
schirmer@13688
  1441
  have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
schirmer@13688
  1442
    by (rule map_upds_in_expansion_map_swap)
schirmer@13688
  1443
  thus ?thesis ..
schirmer@13688
  1444
qed
schirmer@13688
  1445
   
schirmer@13688
  1446
lemma map_upds_None_cut:
schirmer@13688
  1447
assumes expand_None: "(tab(xs[\<mapsto>]ys)) vn = None"
schirmer@13688
  1448
  shows "tab vn = None"
schirmer@13688
  1449
proof (cases "tab vn = None")
schirmer@13688
  1450
  case True thus ?thesis by simp
schirmer@13688
  1451
next
schirmer@13688
  1452
  case False then obtain z where "tab vn = Some z" by blast
schirmer@13688
  1453
  then obtain z' where "(tab(xs[\<mapsto>]ys)) vn = Some z'"
schirmer@13688
  1454
    by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
schirmer@13688
  1455
  with expand_None show ?thesis
schirmer@13688
  1456
    by simp
schirmer@13688
  1457
qed
schirmer@13688
  1458
    
schirmer@13688
  1459
schirmer@13688
  1460
lemma map_upds_cut_irrelevant:
schirmer@13688
  1461
"\<And> tab tab' ys. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some el; (tab'(xs[\<mapsto>]ys)) vn = None\<rbrakk>
schirmer@13688
  1462
                  \<Longrightarrow> tab vn = Some el"
schirmer@13688
  1463
proof  (induct "xs")
schirmer@13688
  1464
  case Nil thus ?case by simp
schirmer@13688
  1465
next
schirmer@13688
  1466
  case (Cons x xs tab tab' ys)
schirmer@13688
  1467
  from Cons.prems
schirmer@13688
  1468
  have "(tab(x\<mapsto>hd ys)) vn = Some el"
schirmer@13688
  1469
    by - (rule Cons.hyps,auto)
schirmer@13688
  1470
  moreover from Cons.prems 
schirmer@13688
  1471
  have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
schirmer@13688
  1472
    by simp
schirmer@13688
  1473
  hence "(tab'(x\<mapsto>hd ys)) vn = None"
schirmer@13688
  1474
    by (rule map_upds_None_cut)
schirmer@13688
  1475
  ultimately show "tab vn = Some el" 
schirmer@13688
  1476
    by (rule map_upd_cut_irrelevant)
schirmer@13688
  1477
qed
schirmer@13688
  1478
   
schirmer@13688
  1479
lemma dom_vname_split:
schirmer@13688
  1480
 "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
schirmer@13688
  1481
   = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
schirmer@13688
  1482
     dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
schirmer@13688
  1483
  (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
schirmer@13688
  1484
proof 
schirmer@13688
  1485
  show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
schirmer@13688
  1486
  proof 
schirmer@13688
  1487
    fix el 
schirmer@13688
  1488
    assume el_in_list: "el \<in> ?List x xs y ys"
schirmer@13688
  1489
    show "el \<in>  ?Hd x y \<union> ?Tl xs ys"
schirmer@13688
  1490
    proof (cases el)
schirmer@13688
  1491
      case This
schirmer@13688
  1492
      with el_in_list show ?thesis by (simp add: dom_def)
schirmer@13688
  1493
    next
schirmer@13688
  1494
      case (EName en)
schirmer@13688
  1495
      show ?thesis
schirmer@13688
  1496
      proof (cases en)
schirmer@13688
  1497
	case Res
schirmer@13688
  1498
	with EName el_in_list show ?thesis by (simp add: dom_def)
schirmer@13688
  1499
      next
schirmer@13688
  1500
	case (VNam vn)
schirmer@13688
  1501
	with EName el_in_list show ?thesis 
schirmer@13688
  1502
	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
schirmer@13688
  1503
      qed
schirmer@13688
  1504
    qed
schirmer@13688
  1505
  qed
schirmer@13688
  1506
next
schirmer@13688
  1507
  show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
schirmer@13688
  1508
  proof 
schirmer@13688
  1509
    fix el 
schirmer@13688
  1510
    assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
schirmer@13688
  1511
    show "el \<in> ?List x xs y ys"
schirmer@13688
  1512
    proof (cases el)
schirmer@13688
  1513
      case This
schirmer@13688
  1514
      with el_in_hd_tl show ?thesis by (simp add: dom_def)
schirmer@13688
  1515
    next
schirmer@13688
  1516
      case (EName en)
schirmer@13688
  1517
      show ?thesis
schirmer@13688
  1518
      proof (cases en)
schirmer@13688
  1519
	case Res
schirmer@13688
  1520
	with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
schirmer@13688
  1521
      next
schirmer@13688
  1522
	case (VNam vn)
schirmer@13688
  1523
	with EName el_in_hd_tl show ?thesis 
schirmer@13688
  1524
	  by (auto simp add: dom_def intro: map_upds_Some_expand 
schirmer@13688
  1525
                                            map_upds_Some_insert)
schirmer@13688
  1526
      qed
schirmer@13688
  1527
    qed
schirmer@13688
  1528
  qed
schirmer@13688
  1529
qed
schirmer@13688
  1530
schirmer@13688
  1531
lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
schirmer@13688
  1532
by (auto simp add: dom_def fun_upd_def)
schirmer@13688
  1533
schirmer@13688
  1534
lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
schirmer@13688
  1535
proof (induct xs)
schirmer@13688
  1536
  case Nil thus ?case by (simp add: dom_def)
schirmer@13688
  1537
next
schirmer@13688
  1538
  case (Cons x xs tab ys)
schirmer@13688
  1539
  have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
schirmer@13688
  1540
  moreover 
schirmer@13688
  1541
  have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
schirmer@13688
  1542
    by (rule dom_map_upd)
schirmer@13688
  1543
  ultimately
schirmer@13688
  1544
  show ?case
schirmer@13688
  1545
    by simp
schirmer@13688
  1546
qed
schirmer@13688
  1547
 
schirmer@13688
  1548
schirmer@13688
  1549
schirmer@13688
  1550
lemma dom_ename_case_None_simp:
schirmer@13688
  1551
 "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
schirmer@13688
  1552
  apply (auto simp add: dom_def image_def )
schirmer@13688
  1553
  apply (case_tac "x")
schirmer@13688
  1554
  apply auto
schirmer@13688
  1555
  done
schirmer@13688
  1556
schirmer@13688
  1557
lemma dom_ename_case_Some_simp:
schirmer@13688
  1558
 "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
schirmer@13688
  1559
  apply (auto simp add: dom_def image_def )
schirmer@13688
  1560
  apply (case_tac "x")
schirmer@13688
  1561
  apply auto
schirmer@13688
  1562
  done
schirmer@13688
  1563
schirmer@13688
  1564
lemma dom_lname_case_None_simp:
schirmer@13688
  1565
  "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
schirmer@13688
  1566
  apply (auto simp add: dom_def image_def )
schirmer@13688
  1567
  apply (case_tac "x")
schirmer@13688
  1568
  apply auto
schirmer@13688
  1569
  done
schirmer@13688
  1570
schirmer@13688
  1571
lemma dom_lname_case_Some_simp:
schirmer@13688
  1572
 "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
schirmer@13688
  1573
  apply (auto simp add: dom_def image_def)
schirmer@13688
  1574
  apply (case_tac "x")
schirmer@13688
  1575
  apply auto
schirmer@13688
  1576
  done
schirmer@13688
  1577
schirmer@13688
  1578
lemmas dom_lname_ename_case_simps =  
schirmer@13688
  1579
     dom_ename_case_None_simp dom_ename_case_Some_simp 
schirmer@13688
  1580
     dom_lname_case_None_simp dom_lname_case_Some_simp
schirmer@13688
  1581
schirmer@13688
  1582
lemma image_comp: 
schirmer@13688
  1583
 "f ` g ` A = (f \<circ> g) ` A"
schirmer@13688
  1584
by (auto simp add: image_def)
schirmer@13688
  1585
schirmer@13688
  1586
lemma dom_locals_init_lvars: 
schirmer@13688
  1587
  assumes m: "m=(mthd (the (methd G C sig)))"  
schirmer@13688
  1588
  shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
schirmer@13688
  1589
           = parameters m"
schirmer@13688
  1590
proof -
schirmer@13688
  1591
  from m
schirmer@13688
  1592
  have static_m': "is_static m = static m"
schirmer@13688
  1593
    by simp
schirmer@13688
  1594
  have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
schirmer@13688
  1595
    by (simp add: dom_map_upds)
schirmer@13688
  1596
  show ?thesis
schirmer@13688
  1597
  proof (cases "static m")
schirmer@13688
  1598
    case True
schirmer@13688
  1599
    with static_m' dom_vnames m
schirmer@13688
  1600
    show ?thesis
schirmer@13688
  1601
      by (cases s) (simp add: init_lvars_def Let_def parameters_def
schirmer@13688
  1602
                              dom_lname_ename_case_simps image_comp)
schirmer@13688
  1603
  next
schirmer@13688
  1604
    case False
schirmer@13688
  1605
    with static_m' dom_vnames m
schirmer@13688
  1606
    show ?thesis
schirmer@13688
  1607
      by (cases s) (simp add: init_lvars_def Let_def parameters_def
schirmer@13688
  1608
                              dom_lname_ename_case_simps image_comp)
schirmer@13688
  1609
  qed
schirmer@13688
  1610
qed
schirmer@13688
  1611
schirmer@13688
  1612
lemma da_e2_BinOp:
schirmer@13688
  1613
  assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1614
                  \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
schirmer@13688
  1615
    and wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T"
schirmer@13688
  1616
    and wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" 
schirmer@13688
  1617
    and wt_binop: "wt_binop G binop e1T e2T" 
schirmer@13688
  1618
    and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1619
    and normal_s1: "normal s1"
schirmer@13688
  1620
    and	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
schirmer@13688
  1621
    and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
schirmer@13688
  1622
    and wf: "wf_prog G"
schirmer@13688
  1623
  shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
schirmer@13688
  1624
         \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
schirmer@13688
  1625
proof -
schirmer@13688
  1626
  note inj_term_simps [simp]
schirmer@13688
  1627
  from da obtain E1 where
schirmer@13688
  1628
    da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
schirmer@13688
  1629
    by cases simp+
schirmer@13688
  1630
  obtain E2 where
schirmer@13688
  1631
    "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
schirmer@13688
  1632
      \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
schirmer@13688
  1633
  proof (cases "need_second_arg binop v1")
schirmer@13688
  1634
    case False
schirmer@13688
  1635
    obtain S where
schirmer@13688
  1636
      daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1637
                  \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>Skip\<rangle>\<^sub>s\<guillemotright> S"
schirmer@13688
  1638
      by (auto intro: da_Skip [simplified] assigned.select_convs)
schirmer@13688
  1639
    thus ?thesis
schirmer@13688
  1640
      using that by (simp add: False)
schirmer@13688
  1641
  next
schirmer@13688
  1642
    case True
schirmer@13688
  1643
    from eval_e1 have 
schirmer@13688
  1644
      s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1645
      by (rule dom_locals_eval_mono_elim)
schirmer@13688
  1646
    {
schirmer@13688
  1647
      assume condAnd: "binop=CondAnd"
schirmer@13688
  1648
      have ?thesis
schirmer@13688
  1649
      proof -
schirmer@13688
  1650
	from da obtain E2' where
schirmer@13688
  1651
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1652
             \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
schirmer@13688
  1653
	  by cases (simp add: condAnd)+
schirmer@13688
  1654
	moreover
schirmer@13688
  1655
	have "dom (locals (store s0)) 
schirmer@13688
  1656
          \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1657
	proof -
schirmer@13688
  1658
	  from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
schirmer@13688
  1659
	    by simp
schirmer@13688
  1660
	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
schirmer@13688
  1661
	    by (auto dest: conf_Boolean)
schirmer@13688
  1662
	  with True condAnd
schirmer@13688
  1663
	  have v1: "v1=Bool True"
schirmer@13688
  1664
	    by simp
schirmer@13688
  1665
	  from eval_e1 normal_s1 
schirmer@13688
  1666
	  have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1667
	    by (rule assigns_if_good_approx' [elim_format])
schirmer@13688
  1668
	       (insert wt_e1, simp_all add: e1T v1)
schirmer@13688
  1669
	  with s0_s1 show ?thesis by (rule Un_least)
schirmer@13688
  1670
	qed
schirmer@13688
  1671
	ultimately
schirmer@13688
  1672
	show ?thesis
schirmer@13688
  1673
	  using that by (cases rule: da_weakenE) (simp add: True)
schirmer@13688
  1674
      qed
schirmer@13688
  1675
    }
schirmer@13688
  1676
    moreover
schirmer@13688
  1677
    { 
schirmer@13688
  1678
      assume condOr: "binop=CondOr"
schirmer@13688
  1679
      have ?thesis
schirmer@13688
  1680
	(* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
schirmer@13688
  1681
      proof -
schirmer@13688
  1682
	from da obtain E2' where
schirmer@13688
  1683
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1684
              \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
schirmer@13688
  1685
	  by cases (simp add: condOr)+
schirmer@13688
  1686
	moreover
schirmer@13688
  1687
	have "dom (locals (store s0)) 
schirmer@13688
  1688
                     \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1689
	proof -
schirmer@13688
  1690
	  from condOr wt_binop have e1T: "e1T=PrimT Boolean"
schirmer@13688
  1691
	    by simp
schirmer@13688
  1692
	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
schirmer@13688
  1693
	    by (auto dest: conf_Boolean)
schirmer@13688
  1694
	  with True condOr
schirmer@13688
  1695
	  have v1: "v1=Bool False"
schirmer@13688
  1696
	    by simp
schirmer@13688
  1697
	  from eval_e1 normal_s1 
schirmer@13688
  1698
	  have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1699
	    by (rule assigns_if_good_approx' [elim_format])
schirmer@13688
  1700
	       (insert wt_e1, simp_all add: e1T v1)
schirmer@13688
  1701
	  with s0_s1 show ?thesis by (rule Un_least)
schirmer@13688
  1702
	qed
schirmer@13688
  1703
	ultimately
schirmer@13688
  1704
	show ?thesis
schirmer@13688
  1705
	  using that by (rule da_weakenE) (simp add: True)
schirmer@13688
  1706
      qed
schirmer@13688
  1707
    }
schirmer@13688
  1708
    moreover
schirmer@13688
  1709
    {
schirmer@13688
  1710
      assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
schirmer@13688
  1711
      have ?thesis
schirmer@13688
  1712
      proof -
schirmer@13688
  1713
	from da notAndOr obtain E1' where
schirmer@13688
  1714
          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1715
                  \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
schirmer@13688
  1716
	  and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
schirmer@13688
  1717
	  by cases simp+
schirmer@13688
  1718
	from eval_e1 wt_e1 da_e1 wf normal_s1 
schirmer@13688
  1719
	have "nrm E1' \<subseteq> dom (locals (store s1))"
schirmer@13688
  1720
	  by (cases rule: da_good_approxE') rules
schirmer@13688
  1721
	with da_e2 show ?thesis
schirmer@13688
  1722
	  using that by (rule da_weakenE) (simp add: True)
schirmer@13688
  1723
      qed
schirmer@13688
  1724
    }
schirmer@13688
  1725
    ultimately show ?thesis
schirmer@13688
  1726
      by (cases binop) auto
schirmer@13688
  1727
  qed
schirmer@13688
  1728
  thus ?thesis ..
schirmer@13688
  1729
qed
schirmer@13688
  1730
schirmer@12854
  1731
section "main proof of type safety"
schirmer@13688
  1732
    
schirmer@12925
  1733
lemma eval_type_sound:
schirmer@13688
  1734
  assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
schirmer@13688
  1735
   and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
schirmer@13688
  1736
   and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
schirmer@13688
  1737
   and      wf: "wf_prog G" 
schirmer@13688
  1738
   and conf_s0: "s0\<Colon>\<preceq>(G,L)"           
wenzelm@12937
  1739
  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
schirmer@12925
  1740
         (error_free s0 = error_free s1)"
schirmer@12925
  1741
proof -
schirmer@13688
  1742
  note inj_term_simps [simp]
schirmer@13688
  1743
  let ?TypeSafeObj = "\<lambda> s0 s1 t v. 
schirmer@13688
  1744
          \<forall>  L accC T A. s0\<Colon>\<preceq>(G,L) \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T
schirmer@13688
  1745
                      \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A  
schirmer@13688
  1746
                      \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
schirmer@13688
  1747
                          \<and> (error_free s0 = error_free s1)"
schirmer@12925
  1748
  from eval 
schirmer@13688
  1749
  have "\<And> L accC T A. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
schirmer@13688
  1750
                      \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
schirmer@12925
  1751
        \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
schirmer@12925
  1752
            \<and> (error_free s0 = error_free s1)"
schirmer@12925
  1753
   (is "PROP ?TypeSafe s0 s1 t v"
schirmer@13688
  1754
    is "\<And> L accC T A. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
schirmer@13688
  1755
                 \<Longrightarrow> ?DefAss L accC s0 t A 
schirmer@12925
  1756
                 \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
schirmer@12925
  1757
                     ?ErrorFree s0 s1")
schirmer@12925
  1758
  proof (induct)
schirmer@13688
  1759
    case (Abrupt s t xc L accC T A) 
schirmer@12925
  1760
    have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
schirmer@12925
  1761
    then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
schirmer@12925
  1762
      (normal (Some xc, s) 
schirmer@12925
  1763
      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
schirmer@12925
  1764
      (error_free (Some xc, s) = error_free (Some xc, s))"
schirmer@12925
  1765
      by (simp)
schirmer@12925
  1766
  next
schirmer@13688
  1767
    case (Skip s L accC T A)
schirmer@12925
  1768
    have "Norm s\<Colon>\<preceq>(G, L)" and  
schirmer@12925
  1769
           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
schirmer@12925
  1770
    then show "Norm s\<Colon>\<preceq>(G, L) \<and>
schirmer@12925
  1771
              (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
schirmer@12925
  1772
              (error_free (Norm s) = error_free (Norm s))"
schirmer@12925
  1773
      by (simp)
schirmer@12925
  1774
  next
schirmer@13688
  1775
    case (Expr e s0 s1 v L accC T A)
schirmer@12925
  1776
    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
schirmer@12925
  1777
    have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
schirmer@12925
  1778
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@13688
  1779
    moreover
schirmer@12925
  1780
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
schirmer@12925
  1781
    then obtain eT 
schirmer@12925
  1782
      where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
schirmer@12925
  1783
      by (rule wt_elim_cases) (blast)
schirmer@13688
  1784
    moreover
schirmer@13688
  1785
    from Expr.prems obtain E where
schirmer@13688
  1786
      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
schirmer@13688
  1787
      by (elim da_elim_cases) simp
schirmer@13688
  1788
    ultimately 
schirmer@12925
  1789
    obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
schirmer@13688
  1790
      by (rule hyp [elim_format]) simp
schirmer@12925
  1791
    with wt
schirmer@12925
  1792
    show "s1\<Colon>\<preceq>(G, L) \<and>
schirmer@12925
  1793
          (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
schirmer@12925
  1794
          (error_free (Norm s0) = error_free s1)"
schirmer@12925
  1795
      by (simp)
schirmer@12925
  1796
  next
schirmer@13688
  1797
    case (Lab c l s0 s1 L accC T A)
schirmer@12925
  1798
    have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
schirmer@12925
  1799
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@13688
  1800
    moreover
schirmer@12925
  1801
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
schirmer@12925
  1802
    then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@12925
  1803
      by (rule wt_elim_cases) (blast)
schirmer@13688
  1804
    moreover from Lab.prems obtain C where
schirmer@13688
  1805
     "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
schirmer@13688
  1806
      by (elim da_elim_cases) simp
schirmer@13688
  1807
    ultimately
schirmer@12925
  1808
    obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
schirmer@12925
  1809
           error_free_s1: "error_free s1" 
schirmer@13688
  1810
      by (rule hyp [elim_format]) simp
schirmer@13337
  1811
    from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1812
      by (cases s1) (auto intro: conforms_absorb)
schirmer@12925
  1813
    with wt error_free_s1
schirmer@13337
  1814
    show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
schirmer@13337
  1815
          (normal (abupd (absorb l) s1)
schirmer@13337
  1816
           \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
schirmer@13337
  1817
          (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
schirmer@12925
  1818
      by (simp)
schirmer@12925
  1819
  next
schirmer@13688
  1820
    case (Comp c1 c2 s0 s1 s2 L accC T A)
schirmer@13688
  1821
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
schirmer@13688
  1822
    have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
schirmer@12925
  1823
    have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
schirmer@12925
  1824
    have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
schirmer@12925
  1825
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1826
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
schirmer@12925
  1827
    then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@12925
  1828
                wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@12925
  1829
      by (rule wt_elim_cases) (blast)
schirmer@13688
  1830
    from Comp.prems
schirmer@13688
  1831
    obtain C1 C2
schirmer@13688
  1832
      where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
schirmer@13688
  1833
                      dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and 
schirmer@13688
  1834
            da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>In1r c2\<guillemotright> C2" 
schirmer@13688
  1835
      by (elim da_elim_cases) simp
schirmer@13688
  1836
    from conf_s0 wt_c1 da_c1
schirmer@13688
  1837
    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
schirmer@13688
  1838
           error_free_s1: "error_free s1"
schirmer@13688
  1839
      by (rule hyp_c1 [elim_format]) simp
schirmer@12925
  1840
    show "s2\<Colon>\<preceq>(G, L) \<and>
schirmer@12925
  1841
          (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
schirmer@12925
  1842
          (error_free (Norm s0) = error_free s2)"
schirmer@13688
  1843
    proof (cases "normal s1")
schirmer@13688
  1844
      case False
schirmer@13688
  1845
      with eval_c2 have "s2=s1" by auto
schirmer@13688
  1846
      with conf_s1 error_free_s1 False wt show ?thesis
schirmer@13688
  1847
	by simp
schirmer@13688
  1848
    next
schirmer@13688
  1849
      case True
schirmer@13688
  1850
      obtain C2' where 
schirmer@13688
  1851
	"\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
schirmer@13688
  1852
      proof -
schirmer@13688
  1853
	from eval_c1 wt_c1 da_c1 wf True
schirmer@13688
  1854
	have "nrm C1 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1855
	  by (cases rule: da_good_approxE') rules
schirmer@13688
  1856
	with da_c2 show ?thesis
schirmer@13688
  1857
	  by (rule da_weakenE)
schirmer@13688
  1858
      qed
schirmer@13688
  1859
      with conf_s1 wt_c2 
schirmer@13688
  1860
      obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
schirmer@13688
  1861
	by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
schirmer@13688
  1862
      thus ?thesis
schirmer@13688
  1863
	using wt by simp
schirmer@13688
  1864
    qed
schirmer@12925
  1865
  next
schirmer@12925
  1866
    case (If b c1 c2 e s0 s1 s2 L accC T)
schirmer@13688
  1867
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
schirmer@13688
  1868
    have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
schirmer@12925
  1869
    have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
schirmer@12925
  1870
    have hyp_then_else: 
schirmer@12925
  1871
            "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
schirmer@12925
  1872
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1873
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
schirmer@13688
  1874
    then obtain 
schirmer@13688
  1875
              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
schirmer@13688
  1876
      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
schirmer@13688
  1877
      (*
schirmer@13688
  1878
                wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@13688
  1879
                wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
schirmer@12925
  1880
      by (rule wt_elim_cases) (auto split add: split_if)
schirmer@13688
  1881
    from If.prems obtain E C where
schirmer@13688
  1882
      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1883
                                       \<guillemotright>In1l e\<guillemotright> E" and
schirmer@13688
  1884
      da_then_else: 
schirmer@13688
  1885
      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
schirmer@13688
  1886
         (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
schirmer@13688
  1887
          \<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C"
schirmer@13688
  1888
     (*
schirmer@13688
  1889
     da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1890
                                      \<union> assigns_if True e) \<guillemotright>In1r c1\<guillemotright> C1" and
schirmer@13688
  1891
     da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1892
                                       \<union> assigns_if False e) \<guillemotright>In1r c2\<guillemotright> C2" *)
schirmer@13688
  1893
      by (elim da_elim_cases) (cases "the_Bool b",auto)
schirmer@13688
  1894
    from conf_s0 wt_e da_e  
schirmer@13688
  1895
    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
schirmer@13688
  1896
      by (rule hyp_e [elim_format]) simp
schirmer@12925
  1897
    show "s2\<Colon>\<preceq>(G, L) \<and>
schirmer@12925
  1898
           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
schirmer@12925
  1899
           (error_free (Norm s0) = error_free s2)"
schirmer@13688
  1900
    proof (cases "normal s1")
schirmer@13688
  1901
      case False
schirmer@13688
  1902
      with eval_then_else have "s2=s1" by auto
schirmer@13688
  1903
      with conf_s1 error_free_s1 False wt show ?thesis
schirmer@13688
  1904
	by simp
schirmer@13688
  1905
    next
schirmer@13688
  1906
      case True
schirmer@13688
  1907
      obtain C' where
schirmer@13688
  1908
	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
schirmer@13688
  1909
          (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
schirmer@13688
  1910
      proof -
schirmer@13688
  1911
	from eval_e have 
schirmer@13688
  1912
	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1913
	  by (rule dom_locals_eval_mono_elim)
schirmer@13688
  1914
        moreover
schirmer@13688
  1915
	from eval_e True wt_e 
schirmer@13688
  1916
	have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
schirmer@13688
  1917
	  by (rule assigns_if_good_approx')
schirmer@13688
  1918
	ultimately 
schirmer@13688
  1919
	have "dom (locals (store ((Norm s0)::state))) 
schirmer@13688
  1920
                \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
schirmer@13688
  1921
	  by (rule Un_least)
schirmer@13688
  1922
	with da_then_else show ?thesis
schirmer@13688
  1923
	  by (rule da_weakenE)
schirmer@13688
  1924
      qed
schirmer@13688
  1925
      with conf_s1 wt_then_else  
schirmer@13688
  1926
      obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
schirmer@13688
  1927
	by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
schirmer@13688
  1928
      with wt show ?thesis
schirmer@13688
  1929
	by simp
schirmer@13688
  1930
    qed
schirmer@13688
  1931
    -- {* Note that we don't have to show that @{term b} really is a boolean 
schirmer@13688
  1932
          value. With @{term the_Bool} we enforce to get a value of boolean 
schirmer@13688
  1933
          type. So execution will be type safe, even if b would be
schirmer@13688
  1934
          a string, for example. We might not expect such a behaviour to be
schirmer@13688
  1935
          called type safe. To remedy the situation we would have to change
schirmer@13688
  1936
          the evaulation rule, so that it only has a type safe evaluation if
schirmer@13688
  1937
          we actually get a boolean value for the condition. That b is actually
schirmer@13688
  1938
          a boolean value is part of @{term hyp_e}. See also Loop 
schirmer@13688
  1939
       *}
schirmer@12925
  1940
  next
schirmer@13688
  1941
    case (Loop b c e l s0 s1 s2 s3 L accC T A)
schirmer@13688