src/HOL/Bali/AxSound.thy
author haftmann
Fri Jun 11 17:14:02 2010 +0200 (2010-06-11)
changeset 37407 61dd8c145da7
parent 35069 09154b995ed8
child 37956 ee939247b2fb
permissions -rw-r--r--
declare lex_prod_def [code del]
     1 (*  Title:      HOL/Bali/AxSound.thy
     2     Author:     David von Oheimb and Norbert Schirmer
     3 *)
     4 header {* Soundness proof for Axiomatic semantics of Java expressions and 
     5           statements
     6        *}
     7 
     8 theory AxSound imports AxSem begin
     9 
    10 section "validity"
    11 
    12 consts
    13 
    14  triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
    15                                                 (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
    16     ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
    17                                                 ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
    18 
    19 defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
    20  \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
    21  \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
    22                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
    23  (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
    24 
    25 text {* This definition differs from the ordinary  @{text triple_valid_def} 
    26 manly in the conclusion: We also ensures conformance of the result state. So
    27 we don't have to apply the type soundness lemma all the time during
    28 induction. This definition is only introduced for the soundness
    29 proof of the axiomatic semantics, in the end we will conclude to 
    30 the ordinary definition.
    31 *}
    32  
    33 defs  ax_valids2_def:    "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
    34 
    35 lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
    36  (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
    37   (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
    38                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
    39   Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
    40 apply (unfold triple_valid2_def)
    41 apply (simp (no_asm) add: split_paired_All)
    42 apply blast
    43 done
    44 
    45 lemma triple_valid2_eq [rule_format (no_asm)]: 
    46   "wf_prog G ==> triple_valid2 G = triple_valid G"
    47 apply (rule ext)
    48 apply (rule ext)
    49 apply (rule triple.induct)
    50 apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2)
    51 apply (rule iffI)
    52 apply  fast
    53 apply clarify
    54 apply (tactic "smp_tac 3 1")
    55 apply (case_tac "normal s")
    56 apply  clarsimp
    57 apply  (elim conjE impE)
    58 apply    blast
    59 
    60 apply    (tactic "smp_tac 2 1")
    61 apply    (drule evaln_eval)
    62 apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
    63 apply    simp
    64 
    65 apply    clarsimp
    66 done
    67 
    68 
    69 lemma ax_valids2_eq: "wf_prog G \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts = G,A|\<Turnstile>ts"
    70 apply (unfold ax_valids_def ax_valids2_def)
    71 apply (force simp add: triple_valid2_eq)
    72 done
    73 
    74 lemma triple_valid2_Suc [rule_format (no_asm)]: "G\<Turnstile>Suc n\<Colon>t \<longrightarrow> G\<Turnstile>n\<Colon>t"
    75 apply (induct_tac "t")
    76 apply (subst triple_valid2_def2)
    77 apply (subst triple_valid2_def2)
    78 apply (fast intro: evaln_nonstrict_Suc)
    79 done
    80 
    81 lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
    82 apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
    83 done
    84 
    85 lemma Methd_triple_valid2_SucI: 
    86 "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
    87   \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
    88 apply (simp (no_asm_use) add: triple_valid2_def2)
    89 apply (intro strip, tactic "smp_tac 3 1", clarify)
    90 apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
    91 apply (unfold body_def Let_def)
    92 apply (clarsimp simp add: inj_term_simps)
    93 apply blast
    94 done
    95 
    96 lemma triples_valid2_Suc: 
    97  "Ball ts (triple_valid2 G (Suc n)) \<Longrightarrow> Ball ts (triple_valid2 G n)"
    98 apply (fast intro: triple_valid2_Suc)
    99 done
   100 
   101 lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)"
   102 oops
   103 
   104 
   105 section "soundness"
   106 
   107 lemma Methd_sound: 
   108   assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
   109   shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
   110 proof -
   111   {
   112     fix n
   113     assume recursive: "\<And> n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
   114                               \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
   115     have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
   116     proof (induct n)
   117       case 0
   118       show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
   119       proof -
   120         {
   121           fix C sig
   122           assume "(C,sig) \<in> ms" 
   123           have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
   124             by (rule Methd_triple_valid2_0)
   125         }
   126         thus ?thesis
   127           by (simp add: mtriples_def split_def)
   128       qed
   129     next
   130       case (Suc m)
   131       note hyp = `\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t`
   132       note prem = `\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t`
   133       show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
   134       proof -
   135         {
   136           fix C sig
   137           assume m: "(C,sig) \<in> ms" 
   138           have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
   139           proof -
   140             from prem have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
   141               by (rule triples_valid2_Suc)
   142             hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
   143               by (rule hyp)
   144             with prem_m
   145             have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
   146               by (simp add: ball_Un)
   147             hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
   148               by (rule recursive)
   149             with m have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
   150               by (auto simp add: mtriples_def split_def)
   151             thus ?thesis
   152               by (rule Methd_triple_valid2_SucI)
   153           qed
   154         }
   155         thus ?thesis
   156           by (simp add: mtriples_def split_def)
   157       qed
   158     qed
   159   }
   160   with recursive show ?thesis
   161     by (unfold ax_valids2_def) blast
   162 qed
   163 
   164 
   165 lemma valids2_inductI: "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow>    
   166   Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. P Y s Z \<longrightarrow>  
   167   (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> 
   168     (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<and> 
   169                             \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A) \<longrightarrow>
   170     Q Y' s' Z \<and> s'\<Colon>\<preceq>(G, L)))) \<Longrightarrow>  
   171   G,A|\<Turnstile>\<Colon>{ {P} c\<succ> {Q}}"
   172 apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2)
   173 apply clarsimp
   174 done
   175 
   176 lemma da_good_approx_evalnE [consumes 4]:
   177   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
   178      and     wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"
   179      and     da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"
   180      and     wf: "wf_prog G"
   181      and   elim: "\<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
   182                   \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
   183                         \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
   184                    \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
   185                    \<Longrightarrow>Result \<in> dom (locals (store s1))
   186                   \<rbrakk> \<Longrightarrow> P"
   187   shows "P"
   188 proof -
   189   from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
   190     by (rule evaln_eval)
   191   from this wt da wf elim show P
   192     by (rule da_good_approxE') iprover+
   193 qed
   194 
   195 lemma validI: 
   196    assumes I: "\<And> n s0 L accC T C v s1 Y Z.
   197                \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); 
   198                normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
   199                normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C;
   200                G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1); P Y s0 Z\<rbrakk> \<Longrightarrow> Q v s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
   201   shows "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
   202 apply (simp add: ax_valids2_def triple_valid2_def2)
   203 apply (intro allI impI)
   204 apply (case_tac "normal s")
   205 apply   clarsimp 
   206 apply   (rule I,(assumption|simp)+)
   207 
   208 apply   (rule I,auto)
   209 done
   210   
   211 
   212 declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
   213 
   214 lemma valid_stmtI: 
   215    assumes I: "\<And> n s0 L accC C s1 Y Z.
   216              \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); 
   217               normal s0\<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
   218               normal s0\<Longrightarrow>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
   219               G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1; P Y s0 Z\<rbrakk> \<Longrightarrow> Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
   220   shows "G,A|\<Turnstile>\<Colon>{ {P} \<langle>c\<rangle>\<^sub>s\<succ> {Q} }"
   221 apply (simp add: ax_valids2_def triple_valid2_def2)
   222 apply (intro allI impI)
   223 apply (case_tac "normal s")
   224 apply   clarsimp 
   225 apply   (rule I,(assumption|simp)+)
   226 
   227 apply   (rule I,auto)
   228 done
   229 
   230 lemma valid_stmt_NormalI: 
   231    assumes I: "\<And> n s0 L accC C s1 Y Z.
   232                \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
   233                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
   234                G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> \<Longrightarrow> Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
   235   shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>c\<rangle>\<^sub>s\<succ> {Q} }"
   236 apply (simp add: ax_valids2_def triple_valid2_def2)
   237 apply (intro allI impI)
   238 apply (elim exE conjE)
   239 apply (rule I)
   240 by auto
   241 
   242 lemma valid_var_NormalI: 
   243    assumes I: "\<And> n s0 L accC T C vf s1 Y Z.
   244                \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
   245                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>=T;
   246                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>v\<guillemotright>C;
   247                 G\<turnstile>s0 \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
   248                \<Longrightarrow> Q (In2 vf) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
   249    shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>v\<succ> {Q} }"
   250 apply (simp add: ax_valids2_def triple_valid2_def2)
   251 apply (intro allI impI)
   252 apply (elim exE conjE)
   253 apply simp
   254 apply (rule I)
   255 by auto
   256 
   257 lemma valid_expr_NormalI: 
   258    assumes I: "\<And> n s0 L accC T C v s1 Y Z.
   259                \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
   260                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>-T;
   261                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>e\<guillemotright>C;
   262                 G\<turnstile>s0 \<midarrow>t-\<succ>v\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
   263                \<Longrightarrow> Q (In1 v) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
   264    shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>e\<succ> {Q} }"
   265 apply (simp add: ax_valids2_def triple_valid2_def2)
   266 apply (intro allI impI)
   267 apply (elim exE conjE)
   268 apply simp
   269 apply (rule I)
   270 by auto
   271 
   272 lemma valid_expr_list_NormalI: 
   273    assumes I: "\<And> n s0 L accC T C vs s1 Y Z.
   274                \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
   275                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>\<doteq>T;
   276                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>l\<guillemotright>C;
   277                 G\<turnstile>s0 \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
   278                 \<Longrightarrow> Q (In3 vs) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
   279    shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>l\<succ> {Q} }"
   280 apply (simp add: ax_valids2_def triple_valid2_def2)
   281 apply (intro allI impI)
   282 apply (elim exE conjE)
   283 apply simp
   284 apply (rule I)
   285 by auto
   286 
   287 lemma validE [consumes 5]: 
   288   assumes valid: "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
   289    and    P: "P Y s0 Z"
   290    and    valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   291    and    conf: "s0\<Colon>\<preceq>(G,L)"
   292    and    eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   293    and    wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
   294    and    da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
   295    and    elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl" 
   296   shows concl
   297 using prems
   298 by (simp add: ax_valids2_def triple_valid2_def2) fast
   299 (* why consumes 5?. If I want to apply this lemma in a context wgere
   300    \<not> normal s0 holds,
   301    I can chain "\<not> normal s0" as fact number 6 and apply the rule with
   302    cases. Auto will then solve premise 6 and 7.
   303 *)
   304 
   305 lemma all_empty: "(!x. P) = P"
   306 by simp
   307 
   308 corollary evaln_type_sound:
   309   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
   310              wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
   311              da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and
   312         conf_s0: "s0\<Colon>\<preceq>(G,L)" and
   313              wf: "wf_prog G"                         
   314   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
   315          (error_free s0 = error_free s1)"
   316 proof -
   317   from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   318     by (rule evaln_eval)
   319   from this wt da wf conf_s0 show ?thesis
   320     by (rule eval_type_sound)
   321 qed
   322 
   323 corollary dom_locals_evaln_mono_elim [consumes 1]: 
   324   assumes   
   325   evaln: "G\<turnstile> s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
   326     hyps: "\<lbrakk>dom (locals (store s0)) \<subseteq> dom (locals (store s1));
   327            \<And> vv s val. \<lbrakk>v=In2 vv; normal s1\<rbrakk> 
   328                         \<Longrightarrow> dom (locals (store s)) 
   329                              \<subseteq> dom (locals (store ((snd vv) val s)))\<rbrakk> \<Longrightarrow> P"
   330  shows "P"
   331 proof -
   332   from evaln have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by (rule evaln_eval)
   333   from this hyps show ?thesis
   334     by (rule dom_locals_eval_mono_elim) iprover+
   335 qed
   336 
   337 
   338 
   339 lemma evaln_no_abrupt: 
   340    "\<And>s s'. \<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s'); normal s'\<rbrakk> \<Longrightarrow> normal s"
   341 by (erule evaln_cases,auto)
   342 
   343 declare inj_term_simps [simp]
   344 lemma ax_sound2: 
   345   assumes    wf: "wf_prog G" 
   346     and   deriv: "G,A|\<turnstile>ts"
   347   shows "G,A|\<Turnstile>\<Colon>ts"
   348 using deriv
   349 proof (induct)
   350   case (empty A)
   351   show ?case
   352     by (simp add: ax_valids2_def triple_valid2_def2)
   353 next
   354   case (insert A t ts)
   355   note valid_t = `G,A|\<Turnstile>\<Colon>{t}`
   356   moreover
   357   note valid_ts = `G,A|\<Turnstile>\<Colon>ts`
   358   {
   359     fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   360     have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
   361     proof -
   362       from valid_A valid_t show "G\<Turnstile>n\<Colon>t"
   363         by (simp add: ax_valids2_def)
   364     next
   365       from valid_A valid_ts show "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
   366         by (unfold ax_valids2_def) blast
   367     qed
   368     hence "\<forall>t'\<in>insert t ts. G\<Turnstile>n\<Colon>t'"
   369       by simp
   370   }
   371   thus ?case
   372     by (unfold ax_valids2_def) blast
   373 next
   374   case (asm ts A)
   375   from `ts \<subseteq> A`
   376   show "G,A|\<Turnstile>\<Colon>ts"
   377     by (auto simp add: ax_valids2_def triple_valid2_def)
   378 next
   379   case (weaken A ts' ts)
   380   note `G,A|\<Turnstile>\<Colon>ts'`
   381   moreover note `ts \<subseteq> ts'`
   382   ultimately show "G,A|\<Turnstile>\<Colon>ts"
   383     by (unfold ax_valids2_def triple_valid2_def) blast
   384 next
   385   case (conseq P A t Q)
   386   note con = `\<forall>Y s Z. P Y s Z \<longrightarrow> 
   387               (\<exists>P' Q'.
   388                   (G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
   389                   (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))`
   390   show "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
   391   proof (rule validI)
   392     fix n s0 L accC T C v s1 Y Z
   393     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t" 
   394     assume conf: "s0\<Colon>\<preceq>(G,L)"
   395     assume wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
   396     assume da: "normal s0 
   397                  \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>t\<guillemotright> C"
   398     assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
   399     assume P: "P Y s0 Z"
   400     show "Q v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   401     proof -
   402       from valid_A conf wt da eval P con
   403       have "Q v s1 Z"
   404         apply (simp add: ax_valids2_def triple_valid2_def2)
   405         apply (tactic "smp_tac 3 1")
   406         apply clarify
   407         apply (tactic "smp_tac 1 1")
   408         apply (erule allE,erule allE, erule mp)
   409         apply (intro strip)
   410         apply (tactic "smp_tac 3 1")
   411         apply (tactic "smp_tac 2 1")
   412         apply (tactic "smp_tac 1 1")
   413         by blast
   414       moreover have "s1\<Colon>\<preceq>(G, L)"
   415       proof (cases "normal s0")
   416         case True
   417         from eval wt [OF True] da [OF True] conf wf 
   418         show ?thesis
   419           by (rule evaln_type_sound [elim_format]) simp
   420       next
   421         case False
   422         with eval have "s1=s0"
   423           by auto
   424         with conf show ?thesis by simp
   425       qed
   426       ultimately show ?thesis ..
   427     qed
   428   qed
   429 next
   430   case (hazard A P t Q)
   431   show "G,A|\<Turnstile>\<Colon>{ {P \<and>. Not \<circ> type_ok G t} t\<succ> {Q} }"
   432     by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast
   433 next
   434   case (Abrupt A P t)
   435   show "G,A|\<Turnstile>\<Colon>{ {P\<leftarrow>undefined3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
   436   proof (rule validI)
   437     fix n s0 L accC T C v s1 Y Z 
   438     assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
   439     assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
   440     assume "(P\<leftarrow>undefined3 t \<and>. Not \<circ> normal) Y s0 Z"
   441     then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "\<not> normal s0"
   442       by simp
   443     from eval abrupt_s0 obtain "s1=s0" and "v=undefined3 t"
   444       by auto
   445     with P conf_s0
   446     show "P v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   447       by simp
   448   qed
   449 next
   450   case (LVar A P vn)
   451   show "G,A|\<Turnstile>\<Colon>{ {Normal (\<lambda>s.. P\<leftarrow>In2 (lvar vn s))} LVar vn=\<succ> {P} }"
   452   proof (rule valid_var_NormalI)
   453     fix n s0 L accC T C vf s1 Y Z
   454     assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
   455     assume normal_s0: "normal s0"
   456     assume wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>LVar vn\<Colon>=T"
   457     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>LVar vn\<rangle>\<^sub>v\<guillemotright> C"
   458     assume eval: "G\<turnstile>s0 \<midarrow>LVar vn=\<succ>vf\<midarrow>n\<rightarrow> s1" 
   459     assume P: "(Normal (\<lambda>s.. P\<leftarrow>In2 (lvar vn s))) Y s0 Z"
   460     show "P (In2 vf) s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   461     proof 
   462       from eval normal_s0 obtain "s1=s0" "vf=lvar vn (store s0)"
   463         by (fastsimp elim: evaln_elim_cases)
   464       with P show "P (In2 vf) s1 Z"
   465         by simp
   466     next
   467       from eval wt da conf_s0 wf
   468       show "s1\<Colon>\<preceq>(G, L)"
   469         by (rule evaln_type_sound [elim_format]) simp
   470     qed
   471   qed
   472 next
   473   case (FVar A P statDeclC Q e stat fn R accC)
   474   note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }`
   475   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }`
   476   show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
   477   proof (rule valid_var_NormalI)
   478     fix n s0 L accC' T V vf s3 Y Z
   479     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   480     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
   481     assume normal_s0: "normal s0"
   482     assume wt: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>{accC,statDeclC,stat}e..fn\<Colon>=T"
   483     assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
   484                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
   485     assume eval: "G\<turnstile>s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<midarrow>n\<rightarrow> s3"
   486     assume P: "(Normal P) Y s0 Z"
   487     show "R \<lfloor>vf\<rfloor>\<^sub>v s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
   488     proof -
   489       from wt obtain statC f where
   490         wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   491         accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   492         eq_accC: "accC=accC'" and
   493         stat: "stat=is_static f" and
   494         T: "T=(type f)"
   495         by (cases) (auto simp add: member_is_static_simp)
   496       from da eq_accC
   497       have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> V"
   498         by cases simp
   499       from eval obtain a s1 s2 s2' where
   500         eval_init: "G\<turnstile>s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" and 
   501         eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" and 
   502         fvar: "(vf,s2')=fvar statDeclC stat fn a s2" and
   503         s3: "s3 = check_field_access G accC statDeclC fn stat a s2'"
   504         using normal_s0 by (fastsimp elim: evaln_elim_cases) 
   505       have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
   506       proof -
   507         from wf wt_e 
   508         have iscls_statC: "is_class G statC"
   509           by (auto dest: ty_expr_is_type type_is_class)
   510         with wf accfield 
   511         have iscls_statDeclC: "is_class G statDeclC"
   512           by (auto dest!: accfield_fields dest: fields_declC)
   513         thus ?thesis by simp
   514       qed
   515       obtain I where 
   516         da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   517                     \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
   518         by (auto intro: da_Init [simplified] assigned.select_convs)
   519       from valid_init P valid_A conf_s0 eval_init wt_init da_init
   520       obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
   521         by (rule validE)
   522       obtain 
   523         R: "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and 
   524         conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   525         conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
   526       proof (cases "normal s1")
   527         case True
   528         obtain V' where 
   529           da_e':
   530           "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> V'"
   531         proof -
   532           from eval_init 
   533           have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
   534             by (rule dom_locals_evaln_mono_elim)
   535           with da_e show thesis
   536             by (rule da_weakenE) (rule that)
   537         qed
   538         with valid_e Q valid_A conf_s1 eval_e wt_e
   539         obtain "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
   540           by (rule validE) (simp add: fvar [symmetric])
   541         moreover
   542         from eval_e wt_e da_e' conf_s1 wf
   543         have "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
   544           by (rule evaln_type_sound [elim_format]) simp
   545         ultimately show ?thesis ..
   546       next
   547         case False
   548         with valid_e Q valid_A conf_s1 eval_e
   549         obtain  "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
   550           by (cases rule: validE) (simp add: fvar [symmetric])+
   551         moreover from False eval_e have "\<not> normal s2"
   552           by auto
   553         hence "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
   554           by auto
   555         ultimately show ?thesis ..
   556       qed
   557       from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat s3 wf
   558       have eq_s3_s2': "s3=s2'"  
   559         using normal_s0 by (auto dest!: error_free_field_access evaln_eval)
   560       moreover
   561       from eval wt da conf_s0 wf
   562       have "s3\<Colon>\<preceq>(G, L)"
   563         by (rule evaln_type_sound [elim_format]) simp
   564       ultimately show ?thesis using Q R by simp
   565     qed
   566   qed
   567 next
   568   case (AVar A P e1 Q e2 R)
   569   note valid_e1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }`
   570   have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
   571     using AVar.hyps by simp
   572   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e1.[e2]=\<succ> {R} }"
   573   proof (rule valid_var_NormalI)
   574     fix n s0 L accC T V vf s2' Y Z
   575     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   576     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   577     assume normal_s0: "normal s0"
   578     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1.[e2]\<Colon>=T"
   579     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   580                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1.[e2]\<rangle>\<^sub>v\<guillemotright> V"
   581     assume eval: "G\<turnstile>s0 \<midarrow>e1.[e2]=\<succ>vf\<midarrow>n\<rightarrow> s2'"
   582     assume P: "(Normal P) Y s0 Z"
   583     show "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z \<and> s2'\<Colon>\<preceq>(G, L)"
   584     proof -
   585       from wt obtain 
   586         wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-T.[]" and
   587         wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" 
   588         by (rule wt_elim_cases) simp
   589       from da obtain E1 where
   590         da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1" and
   591         da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> V"
   592         by (rule da_elim_cases) simp
   593       from eval obtain s1 a i s2 where
   594         eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1" and
   595         eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2" and
   596         avar: "avar G i a s2 =(vf, s2')"
   597         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   598       from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
   599       obtain Q: "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
   600         by (rule validE)
   601       from Q have Q': "\<And> v. (Q\<leftarrow>In1 a) v s1 Z"
   602         by simp
   603       have "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z"
   604       proof (cases "normal s1")
   605         case True
   606         obtain V' where 
   607           "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> V'"
   608         proof -
   609           from eval_e1  wt_e1 da_e1 wf True
   610           have "nrm E1 \<subseteq> dom (locals (store s1))"
   611             by (cases rule: da_good_approx_evalnE) iprover
   612           with da_e2 show thesis
   613             by (rule da_weakenE) (rule that)
   614         qed
   615         with valid_e2 Q' valid_A conf_s1 eval_e2 wt_e2 
   616         show ?thesis
   617           by (rule validE) (simp add: avar)
   618       next
   619         case False
   620         with valid_e2 Q' valid_A conf_s1 eval_e2
   621         show ?thesis
   622           by (cases rule: validE) (simp add: avar)+
   623       qed
   624       moreover
   625       from eval wt da conf_s0 wf
   626       have "s2'\<Colon>\<preceq>(G, L)"
   627         by (rule evaln_type_sound [elim_format]) simp
   628       ultimately show ?thesis ..
   629     qed
   630   qed
   631 next
   632   case (NewC A P C Q)
   633   note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }`
   634   show "G,A|\<Turnstile>\<Colon>{ {Normal P} NewC C-\<succ> {Q} }"
   635   proof (rule valid_expr_NormalI)
   636     fix n s0 L accC T E v s2 Y Z
   637     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   638     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   639     assume normal_s0: "normal s0"
   640     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>NewC C\<Colon>-T"
   641     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   642                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>NewC C\<rangle>\<^sub>e\<guillemotright> E"
   643     assume eval: "G\<turnstile>s0 \<midarrow>NewC C-\<succ>v\<midarrow>n\<rightarrow> s2"
   644     assume P: "(Normal P) Y s0 Z"
   645     show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
   646     proof -
   647       from wt obtain is_cls_C: "is_class G C" 
   648         by (rule wt_elim_cases) (auto dest: is_acc_classD)
   649       hence wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" 
   650         by auto
   651       obtain I where 
   652         da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> I"
   653         by (auto intro: da_Init [simplified] assigned.select_convs)
   654       from eval obtain s1 a where
   655         eval_init: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1" and 
   656         alloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" and
   657         v: "v=Addr a"
   658         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   659       from valid_init P valid_A conf_s0 eval_init wt_init da_init
   660       obtain "(Alloc G (CInst C) Q) \<diamondsuit> s1 Z" 
   661         by (rule validE)
   662       with alloc v have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
   663         by simp
   664       moreover
   665       from eval wt da conf_s0 wf
   666       have "s2\<Colon>\<preceq>(G, L)"
   667         by (rule evaln_type_sound [elim_format]) simp
   668       ultimately show ?thesis ..
   669     qed
   670   qed
   671 next
   672   case (NewA A P T Q e R)
   673   note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }`
   674   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; 
   675                                             Alloc G (Arr T (the_Intg i)) R}}`
   676   show "G,A|\<Turnstile>\<Colon>{ {Normal P} New T[e]-\<succ> {R} }"
   677   proof (rule valid_expr_NormalI)
   678     fix n s0 L accC arrT E v s3 Y Z
   679     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   680     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   681     assume normal_s0: "normal s0"
   682     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>New T[e]\<Colon>-arrT"
   683     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>New T[e]\<rangle>\<^sub>e\<guillemotright> E"
   684     assume eval: "G\<turnstile>s0 \<midarrow>New T[e]-\<succ>v\<midarrow>n\<rightarrow> s3"
   685     assume P: "(Normal P) Y s0 Z"
   686     show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
   687     proof -
   688       from wt obtain
   689         wt_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and 
   690         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" 
   691         by (rule wt_elim_cases) (auto intro: wt_init_comp_ty )
   692       from da obtain
   693         da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
   694         by cases simp
   695       from eval obtain s1 i s2 a where
   696         eval_init: "G\<turnstile>s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1" and 
   697         eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n\<rightarrow> s2" and
   698         alloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" and
   699         v: "v=Addr a"
   700         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   701       obtain I where
   702         da_init:
   703         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>init_comp_ty T\<rangle>\<^sub>s\<guillemotright> I"
   704       proof (cases "\<exists>C. T = Class C")
   705         case True
   706         thus ?thesis
   707           by - (rule that, (auto intro: da_Init [simplified] 
   708                                         assigned.select_convs
   709                               simp add: init_comp_ty_def))
   710          (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
   711       next
   712         case False
   713         thus ?thesis
   714           by - (rule that, (auto intro: da_Skip [simplified] 
   715                                       assigned.select_convs
   716                            simp add: init_comp_ty_def))
   717          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
   718       qed
   719       with valid_init P valid_A conf_s0 eval_init wt_init 
   720       obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
   721         by (rule validE)
   722       obtain E' where
   723        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
   724       proof -
   725         from eval_init 
   726         have "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
   727           by (rule dom_locals_evaln_mono_elim)
   728         with da_e show thesis
   729           by (rule da_weakenE) (rule that)
   730       qed
   731       with valid_e Q valid_A conf_s1 eval_e wt_e
   732       have "(\<lambda>Val:i:. abupd (check_neg i) .; 
   733                       Alloc G (Arr T (the_Intg i)) R) \<lfloor>i\<rfloor>\<^sub>e s2 Z"
   734         by (rule validE)
   735       with alloc v have "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
   736         by simp
   737       moreover 
   738       from eval wt da conf_s0 wf
   739       have "s3\<Colon>\<preceq>(G, L)"
   740         by (rule evaln_type_sound [elim_format]) simp
   741       ultimately show ?thesis ..
   742     qed
   743   qed
   744 next
   745   case (Cast A P e T Q)
   746   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> 
   747                  {\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
   748                   Q\<leftarrow>In1 v} }`
   749   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Cast T e-\<succ> {Q} }"
   750   proof (rule valid_expr_NormalI)
   751     fix n s0 L accC castT E v s2 Y Z
   752     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   753     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   754     assume normal_s0: "normal s0"
   755     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Cast T e\<Colon>-castT"
   756     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Cast T e\<rangle>\<^sub>e\<guillemotright> E"
   757     assume eval: "G\<turnstile>s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
   758     assume P: "(Normal P) Y s0 Z"
   759     show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
   760     proof -
   761       from wt obtain eT where 
   762         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
   763         by cases simp
   764       from da obtain
   765         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
   766         by cases simp
   767       from eval obtain s1 where
   768         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1" and
   769         s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits T) ClassCast) s1"
   770         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   771       from valid_e P valid_A conf_s0 eval_e wt_e da_e
   772       have "(\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
   773                   Q\<leftarrow>In1 v) \<lfloor>v\<rfloor>\<^sub>e s1 Z"
   774         by (rule validE)
   775       with s2 have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
   776         by simp
   777       moreover
   778       from eval wt da conf_s0 wf
   779       have "s2\<Colon>\<preceq>(G, L)"
   780         by (rule evaln_type_sound [elim_format]) simp
   781       ultimately show ?thesis ..
   782     qed
   783   qed
   784 next
   785   case (Inst A P e Q T)
   786   assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ>
   787                {\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T))} }"
   788   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e InstOf T-\<succ> {Q} }"
   789   proof (rule valid_expr_NormalI)
   790     fix n s0 L accC instT E v s1 Y Z
   791     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   792     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   793     assume normal_s0: "normal s0"
   794     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e InstOf T\<Colon>-instT"
   795     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e InstOf T\<rangle>\<^sub>e\<guillemotright> E"
   796     assume eval: "G\<turnstile>s0 \<midarrow>e InstOf T-\<succ>v\<midarrow>n\<rightarrow> s1"
   797     assume P: "(Normal P) Y s0 Z"
   798     show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   799     proof -
   800       from wt obtain eT where 
   801         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
   802         by cases simp
   803       from da obtain
   804         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
   805         by cases simp
   806       from eval obtain a where
   807         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
   808         v: "v = Bool (a \<noteq> Null \<and> G,store s1\<turnstile>a fits RefT T)"
   809         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   810       from valid_e P valid_A conf_s0 eval_e wt_e da_e
   811       have "(\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T))) 
   812               \<lfloor>a\<rfloor>\<^sub>e s1 Z"
   813         by (rule validE)
   814       with v have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
   815         by simp
   816       moreover
   817       from eval wt da conf_s0 wf
   818       have "s1\<Colon>\<preceq>(G, L)"
   819         by (rule evaln_type_sound [elim_format]) simp
   820       ultimately show ?thesis ..
   821     qed
   822   qed
   823 next
   824   case (Lit A P v)
   825   show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>In1 v)} Lit v-\<succ> {P} }"
   826   proof (rule valid_expr_NormalI)
   827     fix n L s0 s1 v'  Y Z
   828     assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
   829     assume normal_s0: " normal s0"
   830     assume eval: "G\<turnstile>s0 \<midarrow>Lit v-\<succ>v'\<midarrow>n\<rightarrow> s1"
   831     assume P: "(Normal (P\<leftarrow>In1 v)) Y s0 Z"
   832     show "P \<lfloor>v'\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   833     proof -
   834       from eval have "s1=s0" and  "v'=v"
   835         using normal_s0 by (auto elim: evaln_elim_cases)
   836       with P conf_s0 show ?thesis by simp
   837     qed
   838   qed
   839 next
   840   case (UnOp A P e Q unop)
   841   assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P}e-\<succ>{\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)} }"
   842   show "G,A|\<Turnstile>\<Colon>{ {Normal P} UnOp unop e-\<succ> {Q} }"
   843   proof (rule valid_expr_NormalI)
   844     fix n s0 L accC T E v s1 Y Z
   845     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   846     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   847     assume normal_s0: "normal s0"
   848     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>UnOp unop e\<Colon>-T"
   849     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>UnOp unop e\<rangle>\<^sub>e\<guillemotright>E"
   850     assume eval: "G\<turnstile>s0 \<midarrow>UnOp unop e-\<succ>v\<midarrow>n\<rightarrow> s1"
   851     assume P: "(Normal P) Y s0 Z"
   852     show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   853     proof -
   854       from wt obtain eT where 
   855         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
   856         by cases simp
   857       from da obtain
   858         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
   859         by cases simp
   860       from eval obtain ve where
   861         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>ve\<midarrow>n\<rightarrow> s1" and
   862         v: "v = eval_unop unop ve"
   863         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   864       from valid_e P valid_A conf_s0 eval_e wt_e da_e
   865       have "(\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)) \<lfloor>ve\<rfloor>\<^sub>e s1 Z"
   866         by (rule validE)
   867       with v have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
   868         by simp
   869       moreover
   870       from eval wt da conf_s0 wf
   871       have "s1\<Colon>\<preceq>(G, L)"
   872         by (rule evaln_type_sound [elim_format]) simp
   873       ultimately show ?thesis ..
   874     qed
   875   qed
   876 next
   877   case (BinOp A P e1 Q binop e2 R)
   878   assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" 
   879   have valid_e2: "\<And> v1.  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
   880               (if need_second_arg binop v1 then In1l e2 else In1r Skip)\<succ>
   881               {\<lambda>Val:v2:. R\<leftarrow>In1 (eval_binop binop v1 v2)} }"
   882     using BinOp.hyps by simp
   883   show "G,A|\<Turnstile>\<Colon>{ {Normal P} BinOp binop e1 e2-\<succ> {R} }"
   884   proof (rule valid_expr_NormalI)
   885     fix n s0 L accC T E v s2 Y Z
   886     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   887     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   888     assume normal_s0: "normal s0"
   889     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>BinOp binop e1 e2\<Colon>-T"
   890     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   891                   \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> E"
   892     assume eval: "G\<turnstile>s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   893     assume P: "(Normal P) Y s0 Z"
   894     show "R \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
   895     proof -
   896       from wt obtain e1T e2T where
   897         wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T" and
   898         wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" and
   899         wt_binop: "wt_binop G binop e1T e2T" 
   900         by cases simp
   901       have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
   902         by simp
   903       (*
   904       obtain S where
   905         daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   906                    \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
   907         by (auto intro: da_Skip [simplified] assigned.select_convs) *)
   908       from da obtain E1 where
   909         da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
   910         by cases simp+
   911       from eval obtain v1 s1 v2 where
   912         eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1" and
   913         eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)
   914                         \<succ>\<midarrow>n\<rightarrow> (\<lfloor>v2\<rfloor>\<^sub>e, s2)" and
   915         v: "v=eval_binop binop v1 v2"
   916         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   917       from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
   918       obtain Q: "Q \<lfloor>v1\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
   919         by (rule validE)
   920       from Q have Q': "\<And> v. (Q\<leftarrow>In1 v1) v s1 Z"
   921         by simp
   922       have "(\<lambda>Val:v2:. R\<leftarrow>In1 (eval_binop binop v1 v2)) \<lfloor>v2\<rfloor>\<^sub>e s2 Z"
   923       proof (cases "normal s1")
   924         case True
   925         from eval_e1 wt_e1 da_e1 conf_s0 wf
   926         have conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" 
   927           by (rule evaln_type_sound [elim_format]) (insert True,simp)
   928         from eval_e1 
   929         have "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
   930           by (rule evaln_eval)
   931         from da wt_e1 wt_e2 wt_binop conf_s0 True this conf_v1 wf
   932         obtain E2 where
   933           da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
   934                    \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
   935           by (rule da_e2_BinOp [elim_format]) iprover
   936         from wt_e2 wt_Skip obtain T2 
   937           where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   938                   \<turnstile>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<Colon>T2"
   939           by (cases "need_second_arg binop v1") auto
   940         note ve=validE [OF valid_e2,OF  Q' valid_A conf_s1 eval_e2 this da_e2]
   941         (* chaining Q', without extra OF causes unification error *)
   942         thus ?thesis
   943           by (rule ve)
   944       next
   945         case False
   946         note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2]
   947         with False show ?thesis
   948           by iprover
   949       qed
   950       with v have "R \<lfloor>v\<rfloor>\<^sub>e s2 Z"
   951         by simp
   952       moreover
   953       from eval wt da conf_s0 wf
   954       have "s2\<Colon>\<preceq>(G, L)"
   955         by (rule evaln_type_sound [elim_format]) simp
   956       ultimately show ?thesis ..
   957     qed
   958   qed
   959 next
   960   case (Super A P)
   961   show "G,A|\<Turnstile>\<Colon>{ {Normal (\<lambda>s.. P\<leftarrow>In1 (val_this s))} Super-\<succ> {P} }"
   962   proof (rule valid_expr_NormalI)
   963     fix n L s0 s1 v  Y Z
   964     assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
   965     assume normal_s0: " normal s0"
   966     assume eval: "G\<turnstile>s0 \<midarrow>Super-\<succ>v\<midarrow>n\<rightarrow> s1"
   967     assume P: "(Normal (\<lambda>s.. P\<leftarrow>In1 (val_this s))) Y s0 Z"
   968     show "P \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   969     proof -
   970       from eval have "s1=s0" and  "v=val_this (store s0)"
   971         using normal_s0 by (auto elim: evaln_elim_cases)
   972       with P conf_s0 show ?thesis by simp
   973     qed
   974   qed
   975 next
   976   case (Acc A P var Q)
   977   note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }`
   978   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
   979   proof (rule valid_expr_NormalI)
   980     fix n s0 L accC T E v s1 Y Z
   981     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
   982     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   983     assume normal_s0: "normal s0"
   984     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Acc var\<Colon>-T"
   985     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Acc var\<rangle>\<^sub>e\<guillemotright>E"
   986     assume eval: "G\<turnstile>s0 \<midarrow>Acc var-\<succ>v\<midarrow>n\<rightarrow> s1"
   987     assume P: "(Normal P) Y s0 Z"
   988     show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
   989     proof -
   990       from wt obtain 
   991         wt_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var\<Colon>=T" 
   992         by cases simp
   993       from da obtain V where 
   994         da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
   995         by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
   996       from eval obtain w upd where
   997         eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
   998         using normal_s0 by (fastsimp elim: evaln_elim_cases)
   999       from valid_var P valid_A conf_s0 eval_var wt_var da_var
  1000       have "(\<lambda>Var:(v, f):. Q\<leftarrow>In1 v) \<lfloor>(v, upd)\<rfloor>\<^sub>v s1 Z"
  1001         by (rule validE)
  1002       then have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
  1003         by simp
  1004       moreover
  1005       from eval wt da conf_s0 wf
  1006       have "s1\<Colon>\<preceq>(G, L)"
  1007         by (rule evaln_type_sound [elim_format]) simp
  1008       ultimately show ?thesis ..
  1009     qed
  1010   qed
  1011 next
  1012   case (Ass A P var Q e R)
  1013   note valid_var = `G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }`
  1014   have valid_e: "\<And> vf. 
  1015                   G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
  1016     using Ass.hyps by simp
  1017   show "G,A|\<Turnstile>\<Colon>{ {Normal P} var:=e-\<succ> {R} }"
  1018   proof (rule valid_expr_NormalI)
  1019     fix n s0 L accC T E v s3 Y Z
  1020     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1021     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1022     assume normal_s0: "normal s0"
  1023     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var:=e\<Colon>-T"
  1024     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>var:=e\<rangle>\<^sub>e\<guillemotright>E"
  1025     assume eval: "G\<turnstile>s0 \<midarrow>var:=e-\<succ>v\<midarrow>n\<rightarrow> s3"
  1026     assume P: "(Normal P) Y s0 Z"
  1027     show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
  1028     proof -
  1029       from wt obtain varT  where
  1030         wt_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var\<Colon>=varT" and
  1031         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-T" 
  1032         by cases simp
  1033       from eval obtain w upd s1 s2 where
  1034         eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(w, upd)\<midarrow>n\<rightarrow> s1" and
  1035         eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s2" and
  1036         s3: "s3=assign upd v s2"
  1037         using normal_s0 by (auto elim: evaln_elim_cases)
  1038       have "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
  1039       proof (cases "\<exists> vn. var = LVar vn")
  1040         case False
  1041         with da obtain V where
  1042           da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1043                       \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V" and
  1044           da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
  1045           by cases simp+
  1046         from valid_var P valid_A conf_s0 eval_var wt_var da_var
  1047         obtain Q: "Q \<lfloor>(w,upd)\<rfloor>\<^sub>v s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
  1048           by (rule validE) 
  1049         hence Q': "\<And> v. (Q\<leftarrow>In2 (w,upd)) v s1 Z"
  1050           by simp
  1051         have "(\<lambda>Val:v:. assign (snd (w,upd)) v .; R) \<lfloor>v\<rfloor>\<^sub>e s2 Z"
  1052         proof (cases "normal s1")
  1053           case True
  1054           obtain E' where 
  1055             da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
  1056           proof -
  1057             from eval_var wt_var da_var wf True
  1058             have "nrm V \<subseteq>  dom (locals (store s1))"
  1059               by (cases rule: da_good_approx_evalnE) iprover
  1060             with da_e show thesis
  1061               by (rule da_weakenE) (rule that)
  1062           qed
  1063           note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
  1064           show ?thesis
  1065             by (rule ve)
  1066         next
  1067           case False
  1068           note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
  1069           with False show ?thesis
  1070             by iprover
  1071         qed
  1072         with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
  1073           by simp
  1074       next
  1075         case True
  1076         then obtain vn where 
  1077           vn: "var = LVar vn" 
  1078           by auto
  1079         with da obtain E where
  1080             da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
  1081           by cases simp+
  1082         from da.LVar vn obtain  V where
  1083           da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1084                       \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
  1085           by auto
  1086         from valid_var P valid_A conf_s0 eval_var wt_var da_var
  1087         obtain Q: "Q \<lfloor>(w,upd)\<rfloor>\<^sub>v s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
  1088           by (rule validE) 
  1089         hence Q': "\<And> v. (Q\<leftarrow>In2 (w,upd)) v s1 Z"
  1090           by simp
  1091         have "(\<lambda>Val:v:. assign (snd (w,upd)) v .; R) \<lfloor>v\<rfloor>\<^sub>e s2 Z"
  1092         proof (cases "normal s1")
  1093           case True
  1094           obtain E' where
  1095             da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1096                        \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
  1097           proof -
  1098             from eval_var
  1099             have "dom (locals (store s0)) \<subseteq> dom (locals (store (s1)))"
  1100               by (rule dom_locals_evaln_mono_elim)
  1101             with da_e show thesis
  1102               by (rule da_weakenE) (rule that)
  1103           qed
  1104           note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
  1105           show ?thesis
  1106             by (rule ve)
  1107         next
  1108           case False
  1109           note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
  1110           with False show ?thesis
  1111             by iprover
  1112         qed
  1113         with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
  1114           by simp
  1115       qed
  1116       moreover
  1117       from eval wt da conf_s0 wf
  1118       have "s3\<Colon>\<preceq>(G, L)"
  1119         by (rule evaln_type_sound [elim_format]) simp
  1120       ultimately show ?thesis ..
  1121     qed
  1122   qed
  1123 next
  1124   case (Cond A P e0 P' e1 e2 Q)
  1125   note valid_e0 = `G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }`
  1126   have valid_then_else:"\<And> b.  G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
  1127     using Cond.hyps by simp
  1128   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e0 ? e1 : e2-\<succ> {Q} }"
  1129   proof (rule valid_expr_NormalI)
  1130     fix n s0 L accC T E v s2 Y Z
  1131     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1132     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1133     assume normal_s0: "normal s0"
  1134     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e0 ? e1 : e2\<Colon>-T"
  1135     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e0 ? e1:e2\<rangle>\<^sub>e\<guillemotright>E"
  1136     assume eval: "G\<turnstile>s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
  1137     assume P: "(Normal P) Y s0 Z"
  1138     show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
  1139     proof -
  1140       from wt obtain T1 T2 where
  1141         wt_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  1142         wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-T1" and
  1143         wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-T2" 
  1144         by cases simp
  1145       from da obtain E0 E1 E2 where
  1146         da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e0\<rangle>\<^sub>e\<guillemotright> E0" and
  1147         da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1148                  \<turnstile>(dom (locals (store s0)) \<union> assigns_if True e0)\<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1" and
  1149         da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1150                  \<turnstile>(dom (locals (store s0)) \<union> assigns_if False e0)\<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2"
  1151         by cases simp+
  1152       from eval obtain b s1 where
  1153         eval_e0: "G\<turnstile>s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1" and
  1154         eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2"
  1155         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1156       from valid_e0 P valid_A conf_s0 eval_e0 wt_e0 da_e0
  1157       obtain "P' \<lfloor>b\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
  1158         by (rule validE)
  1159       hence P': "\<And> v. (P'\<leftarrow>=(the_Bool b)) v s1 Z"
  1160         by (cases "normal s1") auto
  1161       have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
  1162       proof (cases "normal s1")
  1163         case True
  1164         note normal_s1=this
  1165         from wt_e1 wt_e2 obtain T' where
  1166           wt_then_else: 
  1167           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(if the_Bool b then e1 else e2)\<Colon>-T'"
  1168           by (cases "the_Bool b") simp+
  1169         have s0_s1: "dom (locals (store s0)) 
  1170                       \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1171         proof -
  1172           from eval_e0 
  1173           have eval_e0': "G\<turnstile>s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
  1174             by (rule evaln_eval)
  1175           hence
  1176             "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1177             by (rule dom_locals_eval_mono_elim)
  1178           moreover
  1179           from eval_e0' True wt_e0 
  1180           have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1181             by (rule assigns_if_good_approx') 
  1182           ultimately show ?thesis by (rule Un_least)
  1183         qed
  1184         obtain E' where
  1185           da_then_else:
  1186           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1187               \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>if the_Bool b then e1 else e2\<rangle>\<^sub>e\<guillemotright> E'"
  1188         proof (cases "the_Bool b")
  1189           case True
  1190           with that da_e1 s0_s1 show ?thesis
  1191             by simp (erule da_weakenE,auto)
  1192         next
  1193           case False
  1194           with that da_e2 s0_s1 show ?thesis
  1195             by simp (erule da_weakenE,auto)
  1196         qed
  1197         with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else
  1198         show ?thesis
  1199           by (rule validE)
  1200       next
  1201         case False
  1202         with valid_then_else P' valid_A conf_s1 eval_then_else
  1203         show ?thesis
  1204           by (cases rule: validE) iprover+
  1205       qed
  1206       moreover
  1207       from eval wt da conf_s0 wf
  1208       have "s2\<Colon>\<preceq>(G, L)"
  1209         by (rule evaln_type_sound [elim_format]) simp
  1210       ultimately show ?thesis ..
  1211     qed
  1212   qed
  1213 next
  1214   case (Call A P e Q args R mode statT mn pTs' S accC')
  1215   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
  1216   have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
  1217     using Call.hyps by simp
  1218   have valid_methd: "\<And> a vs invC declC l.
  1219         G,A|\<Turnstile>\<Colon>{ {R a\<leftarrow>In3 vs \<and>.
  1220                  (\<lambda>s. declC =
  1221                     invocation_declclass G mode (store s) a statT
  1222                      \<lparr>name = mn, parTs = pTs'\<rparr> \<and>
  1223                     invC = invocation_class mode (store s) a statT \<and>
  1224                     l = locals (store s)) ;.
  1225                  init_lvars G declC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs \<and>.
  1226                  (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
  1227             Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ> {set_lvars l .; S} }"
  1228     using Call.hyps by simp
  1229   show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ> {S} }"
  1230   proof (rule valid_expr_NormalI)
  1231     fix n s0 L accC T E v s5 Y Z
  1232     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1233     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1234     assume normal_s0: "normal s0"
  1235     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>{accC',statT,mode}e\<cdot>mn( {pTs'}args)\<Colon>-T"
  1236     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))
  1237                    \<guillemotright>\<langle>{accC',statT,mode}e\<cdot>mn( {pTs'}args)\<rangle>\<^sub>e\<guillemotright> E"
  1238     assume eval: "G\<turnstile>s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n\<rightarrow> s5"
  1239     assume P: "(Normal P) Y s0 Z"
  1240     show "S \<lfloor>v\<rfloor>\<^sub>e s5 Z \<and> s5\<Colon>\<preceq>(G, L)"
  1241     proof -
  1242       from wt obtain pTs statDeclT statM where
  1243                  wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  1244               wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  1245                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  1246                          = {((statDeclT,statM),pTs')}" and
  1247                  mode: "mode = invmode statM e" and
  1248                     T: "T =(resTy statM)" and
  1249         eq_accC_accC': "accC=accC'"
  1250         by cases fastsimp+
  1251       from da obtain C where
  1252         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s0)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
  1253         da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E" 
  1254         by cases simp
  1255       from eval eq_accC_accC' obtain a s1 vs s2 s3 s3' s4 invDeclC where
  1256         evaln_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
  1257         evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" and
  1258         invDeclC: "invDeclC = invocation_declclass 
  1259                 G mode (store s2) a statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1260         s3: "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a vs s2" and
  1261         check: "s3' = check_method_access G 
  1262                            accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" and
  1263         evaln_methd:
  1264            "G\<turnstile>s3' \<midarrow>Methd invDeclC  \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" and
  1265         s5: "s5=(set_lvars (locals (store s2))) s4"
  1266         using normal_s0 by (auto elim: evaln_elim_cases)
  1267 
  1268       from evaln_e
  1269       have eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
  1270         by (rule evaln_eval)
  1271       
  1272       from eval_e _ wt_e wf
  1273       have s1_no_return: "abrupt s1 \<noteq> Some (Jump Ret)"
  1274         by (rule eval_expression_no_jump 
  1275                  [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
  1276            (insert normal_s0,auto)
  1277 
  1278       from valid_e P valid_A conf_s0 evaln_e wt_e da_e
  1279       obtain "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  1280         by (rule validE)
  1281       hence Q: "\<And> v. (Q\<leftarrow>In1 a) v s1 Z"
  1282         by simp
  1283       obtain 
  1284         R: "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" and 
  1285         conf_s2: "s2\<Colon>\<preceq>(G,L)" and 
  1286         s2_no_return: "abrupt s2 \<noteq> Some (Jump Ret)"
  1287       proof (cases "normal s1")
  1288         case True
  1289         obtain E' where 
  1290           da_args':
  1291           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E'"
  1292         proof -
  1293           from evaln_e wt_e da_e wf True
  1294           have "nrm C \<subseteq>  dom (locals (store s1))"
  1295             by (cases rule: da_good_approx_evalnE) iprover
  1296           with da_args show thesis
  1297             by (rule da_weakenE) (rule that)
  1298         qed
  1299         with valid_args Q valid_A conf_s1 evaln_args wt_args 
  1300         obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
  1301           by (rule validE)
  1302         moreover
  1303         from evaln_args
  1304         have e: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
  1305           by (rule evaln_eval)
  1306         from this s1_no_return wt_args wf
  1307         have "abrupt s2 \<noteq> Some (Jump Ret)"
  1308           by (rule eval_expression_list_no_jump 
  1309                  [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
  1310         ultimately show ?thesis ..
  1311       next
  1312         case False
  1313         with valid_args Q valid_A conf_s1 evaln_args
  1314         obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
  1315           by (cases rule: validE) iprover+
  1316         moreover
  1317         from False evaln_args have "s2=s1"
  1318           by auto
  1319         with s1_no_return have "abrupt s2 \<noteq> Some (Jump Ret)"
  1320           by simp
  1321         ultimately show ?thesis ..
  1322       qed
  1323 
  1324       obtain invC where
  1325         invC: "invC = invocation_class mode (store s2) a statT"
  1326         by simp
  1327       with s3
  1328       have invC': "invC = (invocation_class mode (store s3) a statT)"
  1329         by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1330       obtain l where
  1331         l: "l = locals (store s2)"
  1332         by simp
  1333 
  1334       from eval wt da conf_s0 wf
  1335       have conf_s5: "s5\<Colon>\<preceq>(G, L)"
  1336         by (rule evaln_type_sound [elim_format]) simp
  1337       let "PROP ?R" = "\<And> v.
  1338              (R a\<leftarrow>In3 vs \<and>.
  1339                  (\<lambda>s. invDeclC = invocation_declclass G mode (store s) a statT
  1340                                   \<lparr>name = mn, parTs = pTs'\<rparr> \<and>
  1341                        invC = invocation_class mode (store s) a statT \<and>
  1342                           l = locals (store s)) ;.
  1343                   init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs \<and>.
  1344                   (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)
  1345                ) v s3' Z"
  1346       {
  1347         assume abrupt_s3: "\<not> normal s3"
  1348         have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
  1349         proof -
  1350           from abrupt_s3 check have eq_s3'_s3: "s3'=s3"
  1351             by (auto simp add: check_method_access_def Let_def)
  1352           with R s3 invDeclC invC l abrupt_s3
  1353           have R': "PROP ?R"
  1354             by auto
  1355           have conf_s3': "s3'\<Colon>\<preceq>(G, empty)"
  1356            (* we need an arbirary environment (here empty) that s2' conforms to
  1357               to apply validE *)
  1358           proof -
  1359             from s2_no_return s3
  1360             have "abrupt s3 \<noteq> Some (Jump Ret)"
  1361               by (cases s2) (auto simp add: init_lvars_def2 split: split_if_asm)
  1362             moreover
  1363             obtain abr2 str2 where s2: "s2=(abr2,str2)"
  1364               by (cases s2)
  1365             from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
  1366               by (auto simp add: init_lvars_def2 split: split_if_asm)
  1367             ultimately show ?thesis
  1368               using s3 s2 eq_s3'_s3
  1369               apply (simp add: init_lvars_def2)
  1370               apply (rule conforms_set_locals [OF _ wlconf_empty])
  1371               by auto
  1372           qed
  1373           from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3
  1374           have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
  1375             by (cases rule: validE) simp+
  1376           with s5 l show ?thesis
  1377             by simp
  1378         qed
  1379       } note abrupt_s3_lemma = this
  1380 
  1381       have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
  1382       proof (cases "normal s2")
  1383         case False
  1384         with s3 have abrupt_s3: "\<not> normal s3"
  1385           by (cases s2) (simp add: init_lvars_def2)
  1386         thus ?thesis
  1387           by (rule abrupt_s3_lemma)
  1388       next
  1389         case True
  1390         note normal_s2 = this
  1391         with evaln_args 
  1392         have normal_s1: "normal s1"
  1393           by (rule evaln_no_abrupt)
  1394         obtain E' where 
  1395           da_args':
  1396           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E'"
  1397         proof -
  1398           from evaln_e wt_e da_e wf normal_s1
  1399           have "nrm C \<subseteq>  dom (locals (store s1))"
  1400             by (cases rule: da_good_approx_evalnE) iprover
  1401           with da_args show thesis
  1402             by (rule da_weakenE) (rule that)
  1403         qed
  1404         from evaln_args
  1405         have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
  1406           by (rule evaln_eval)
  1407         from evaln_e wt_e da_e conf_s0 wf
  1408         have conf_a: "G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
  1409           by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
  1410         with normal_s1 normal_s2 eval_args 
  1411         have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1412           by (auto dest: eval_gext intro: conf_gext)
  1413         from evaln_args wt_args da_args' conf_s1 wf
  1414         have conf_args: "list_all2 (conf G (store s2)) vs pTs"
  1415           by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
  1416         from statM 
  1417         obtain
  1418           statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1419           and
  1420           pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1421           by (blast dest: max_spec2mheads)
  1422         show ?thesis
  1423         proof (cases "normal s3")
  1424           case False
  1425           thus ?thesis
  1426             by (rule abrupt_s3_lemma)
  1427         next
  1428           case True
  1429           note normal_s3 = this
  1430           with s3 have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  1431             by (cases s2) (auto simp add: init_lvars_def2)
  1432           from conf_s2 conf_a_s2 wf notNull invC
  1433           have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1434             by (cases s2) (auto intro: DynT_propI)
  1435 
  1436           with wt_e statM' invC mode wf 
  1437           obtain dynM where 
  1438             dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1439             acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1440                             in invC dyn_accessible_from accC"
  1441             by (force dest!: call_access_ok)
  1442           with invC' check eq_accC_accC'
  1443           have eq_s3'_s3: "s3'=s3"
  1444             by (auto simp add: check_method_access_def Let_def)
  1445           
  1446           with dynT_prop R s3 invDeclC invC l 
  1447           have R': "PROP ?R"
  1448             by auto
  1449 
  1450           from dynT_prop wf wt_e statM' mode invC invDeclC dynM
  1451           obtain 
  1452             dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1453             wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1454               dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1455             iscls_invDeclC: "is_class G invDeclC" and
  1456                  invDeclC': "invDeclC = declclass dynM" and
  1457               invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1458              resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1459             is_static_eq: "is_static dynM = is_static statM" and
  1460             involved_classes_prop:
  1461              "(if invmode statM e = IntVir
  1462                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1463                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1464                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1465                       statDeclT = ClassT invDeclC)"
  1466             by (cases rule: DynT_mheadsE) simp
  1467           obtain L' where 
  1468             L':"L'=(\<lambda> k. 
  1469                     (case k of
  1470                        EName e
  1471                        \<Rightarrow> (case e of 
  1472                              VNam v 
  1473                              \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  1474                                 (pars (mthd dynM)[\<mapsto>]pTs')) v
  1475                            | Res \<Rightarrow> Some (resTy dynM))
  1476                      | This \<Rightarrow> if is_static statM 
  1477                                then None else Some (Class invDeclC)))"
  1478             by simp
  1479           from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1480             wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  1481           have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1482             apply - 
  1483                (* FIXME confomrs_init_lvars should be 
  1484                   adjusted to be more directy applicable *)
  1485             apply (drule conforms_init_lvars [of G invDeclC 
  1486                     "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1487                     L statT invC a "(statDeclT,statM)" e])
  1488             apply (rule wf)
  1489             apply (rule conf_args)
  1490             apply (simp add: pTs_widen)
  1491             apply (cases s2,simp)
  1492             apply (rule dynM')
  1493             apply (force dest: ty_expr_is_type)
  1494             apply (rule invC_widen)
  1495             apply (force intro: conf_gext dest: eval_gext)
  1496             apply simp
  1497             apply simp
  1498             apply (simp add: invC)
  1499             apply (simp add: invDeclC)
  1500             apply (simp add: normal_s2)
  1501             apply (cases s2, simp add: L' init_lvars_def2 s3
  1502                              cong add: lname.case_cong ename.case_cong)
  1503             done
  1504           with eq_s3'_s3 have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  1505           from is_static_eq wf_dynM L'
  1506           obtain mthdT where
  1507             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1508                \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  1509             mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1510             by - (drule wf_mdecl_bodyD,
  1511                   auto simp add: callee_lcl_def  
  1512                        cong add: lname.case_cong ename.case_cong)
  1513           with dynM' iscls_invDeclC invDeclC'
  1514           have
  1515             wt_methd:
  1516             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1517                \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1518             by (auto intro: wt.Methd)
  1519           obtain M where 
  1520             da_methd:
  1521             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  1522                \<turnstile> dom (locals (store s3')) 
  1523                    \<guillemotright>\<langle>Methd invDeclC \<lparr>name=mn,parTs=pTs'\<rparr>\<rangle>\<^sub>e\<guillemotright> M"
  1524           proof -
  1525             from wf_dynM
  1526             obtain M' where
  1527               da_body: 
  1528               "\<lparr>prg=G, cls=invDeclC
  1529                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  1530                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  1531               res: "Result \<in> nrm M'"
  1532               by (rule wf_mdeclE) iprover
  1533             from da_body is_static_eq L' have
  1534               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1535                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  1536               by (simp add: callee_lcl_def  
  1537                   cong add: lname.case_cong ename.case_cong)
  1538             moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  1539             proof -
  1540               from is_static_eq 
  1541               have "(invmode (mthd dynM) e) = (invmode statM e)"
  1542                 by (simp add: invmode_def)
  1543               moreover
  1544               have "length (pars (mthd dynM)) = length vs" 
  1545               proof -
  1546                 from normal_s2 conf_args
  1547                 have "length vs = length pTs"
  1548                   by (simp add: list_all2_def)
  1549                 also from pTs_widen
  1550                 have "\<dots> = length pTs'"
  1551                   by (simp add: widens_def list_all2_def)
  1552                 also from wf_dynM
  1553                 have "\<dots> = length (pars (mthd dynM))"
  1554                   by (simp add: wf_mdecl_def wf_mhead_def)
  1555                 finally show ?thesis ..
  1556               qed
  1557               moreover note s3 dynM' is_static_eq normal_s2 mode 
  1558               ultimately
  1559               have "parameters (mthd dynM) = dom (locals (store s3))"
  1560                 using dom_locals_init_lvars 
  1561                   [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
  1562                 by simp
  1563               thus ?thesis using eq_s3'_s3 by simp
  1564             qed
  1565             ultimately obtain M2 where
  1566               da:
  1567               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1568                 \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  1569               M2: "nrm M' \<subseteq> nrm M2"
  1570               by (rule da_weakenE)
  1571             from res M2 have "Result \<in> nrm M2"
  1572               by blast
  1573             moreover from wf_dynM
  1574             have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  1575               by (rule wf_mdeclE)
  1576             ultimately
  1577             obtain M3 where
  1578               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  1579                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  1580               using da
  1581               by (iprover intro: da.Body assigned.select_convs)
  1582             from _ this [simplified]
  1583             show thesis
  1584               by (rule da.Methd [simplified,elim_format])
  1585                  (auto intro: dynM' that)
  1586           qed
  1587           from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd
  1588           have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
  1589             by (cases rule: validE) iprover+
  1590           with s5 l show ?thesis
  1591             by simp
  1592         qed
  1593       qed
  1594       with conf_s5 show ?thesis by iprover
  1595     qed
  1596   qed
  1597 next
  1598   case (Methd A P Q ms)
  1599   note valid_body = `G,A \<union> {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}`
  1600   show "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
  1601     by (rule Methd_sound) (rule Methd.hyps)
  1602 next
  1603   case (Body A P D Q c R)
  1604   note valid_init = `G,A|\<Turnstile>\<Colon>{ {Normal P} .Init D. {Q} }`
  1605   note valid_c = `G,A|\<Turnstile>\<Colon>{ {Q} .c.
  1606               {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))} }`
  1607   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Body D c-\<succ> {R} }"
  1608   proof (rule valid_expr_NormalI)
  1609     fix n s0 L accC T E v s4 Y Z
  1610     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1611     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1612     assume normal_s0: "normal s0"
  1613     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Body D c\<Colon>-T"
  1614     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright>E"
  1615     assume eval: "G\<turnstile>s0 \<midarrow>Body D c-\<succ>v\<midarrow>n\<rightarrow> s4"
  1616     assume P: "(Normal P) Y s0 Z"
  1617     show "R \<lfloor>v\<rfloor>\<^sub>e s4 Z \<and> s4\<Colon>\<preceq>(G, L)"
  1618     proof -
  1619       from wt obtain 
  1620         iscls_D: "is_class G D" and
  1621         wt_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Init D\<Colon>\<surd>" and
  1622         wt_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>" 
  1623         by cases auto
  1624       obtain I where 
  1625         da_init:"\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>Init D\<rangle>\<^sub>s\<guillemotright> I"
  1626         by (auto intro: da_Init [simplified] assigned.select_convs)
  1627       from da obtain C where
  1628         da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s0)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> C" and
  1629         jmpOk: "jumpNestingOkS {Ret} c" 
  1630         by cases simp
  1631       from eval obtain s1 s2 s3 where
  1632         eval_init: "G\<turnstile>s0 \<midarrow>Init D\<midarrow>n\<rightarrow> s1" and
  1633         eval_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2" and
  1634         v: "v = the (locals (store s2) Result)" and
  1635         s3: "s3 =(if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  1636                          abrupt s2 = Some (Jump (Cont l))
  1637                   then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"and
  1638         s4: "s4 = abupd (absorb Ret) s3"
  1639         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1640       obtain C' where 
  1641         da_c': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> C'"
  1642       proof -
  1643         from eval_init 
  1644         have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
  1645           by (rule dom_locals_evaln_mono_elim)
  1646         with da_c show thesis by (rule da_weakenE) (rule that)
  1647       qed
  1648       from valid_init P valid_A conf_s0 eval_init wt_init da_init
  1649       obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  1650         by (rule validE)
  1651       from valid_c Q valid_A conf_s1 eval_c wt_c da_c' 
  1652       have R: "(\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>In1 (the (locals s Result))) 
  1653                 \<diamondsuit> s2 Z"
  1654         by (rule validE)
  1655       have "s3=s2"
  1656       proof -
  1657         from eval_init [THEN evaln_eval] wf
  1658         have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  1659           by - (rule eval_statement_no_jump [OF _ _ _ wt_init],
  1660                 insert normal_s0,auto)
  1661         from eval_c [THEN evaln_eval] _ wt_c wf
  1662         have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  1663           by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  1664         moreover note s3
  1665         ultimately show ?thesis 
  1666           by (force split: split_if)
  1667       qed
  1668       with R v s4 
  1669       have "R \<lfloor>v\<rfloor>\<^sub>e s4 Z"
  1670         by simp
  1671       moreover
  1672       from eval wt da conf_s0 wf
  1673       have "s4\<Colon>\<preceq>(G, L)"
  1674         by (rule evaln_type_sound [elim_format]) simp
  1675       ultimately show ?thesis ..
  1676     qed
  1677   qed
  1678 next
  1679   case (Nil A P)
  1680   show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<lfloor>[]\<rfloor>\<^sub>l)} []\<doteq>\<succ> {P} }"
  1681   proof (rule valid_expr_list_NormalI)
  1682     fix s0 s1 vs n L Y Z
  1683     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1684     assume normal_s0: "normal s0"
  1685     assume eval: "G\<turnstile>s0 \<midarrow>[]\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s1"
  1686     assume P: "(Normal (P\<leftarrow>\<lfloor>[]\<rfloor>\<^sub>l)) Y s0 Z"
  1687     show "P \<lfloor>vs\<rfloor>\<^sub>l s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
  1688     proof -
  1689       from eval obtain "vs=[]" "s1=s0"
  1690         using normal_s0 by (auto elim: evaln_elim_cases)
  1691       with P conf_s0 show ?thesis
  1692         by simp
  1693     qed
  1694   qed
  1695 next
  1696   case (Cons A P e Q es R)
  1697   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }`
  1698   have valid_es: "\<And> v. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>\<lfloor>v\<rfloor>\<^sub>e} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>\<lfloor>(v # vs)\<rfloor>\<^sub>l} }"
  1699     using Cons.hyps by simp
  1700   show "G,A|\<Turnstile>\<Colon>{ {Normal P} e # es\<doteq>\<succ> {R} }"
  1701   proof (rule valid_expr_list_NormalI)
  1702     fix n s0 L accC T E v s2 Y Z
  1703     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1704     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1705     assume normal_s0: "normal s0"
  1706     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e # es\<Colon>\<doteq>T"
  1707     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>e # es\<rangle>\<^sub>l\<guillemotright> E"
  1708     assume eval: "G\<turnstile>s0 \<midarrow>e # es\<doteq>\<succ>v\<midarrow>n\<rightarrow> s2"
  1709     assume P: "(Normal P) Y s0 Z"
  1710     show "R \<lfloor>v\<rfloor>\<^sub>l s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
  1711     proof -
  1712       from wt obtain eT esT where
  1713         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT" and
  1714         wt_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>es\<Colon>\<doteq>esT"
  1715         by cases simp
  1716       from da obtain E1 where
  1717         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s0)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E1" and
  1718         da_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>\<langle>es\<rangle>\<^sub>l\<guillemotright> E" 
  1719         by cases simp
  1720       from eval obtain s1 ve vs where
  1721         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>ve\<midarrow>n\<rightarrow> s1" and
  1722         eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" and
  1723         v: "v=ve#vs"
  1724         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1725       from valid_e P valid_A conf_s0 eval_e wt_e da_e 
  1726       obtain Q: "Q \<lfloor>ve\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  1727         by (rule validE)
  1728       from Q have Q': "\<And> v. (Q\<leftarrow>\<lfloor>ve\<rfloor>\<^sub>e) v s1 Z"
  1729         by simp
  1730       have "(\<lambda>Vals:vs:. R\<leftarrow>\<lfloor>(ve # vs)\<rfloor>\<^sub>l) \<lfloor>vs\<rfloor>\<^sub>l s2 Z"
  1731       proof (cases "normal s1")
  1732         case True
  1733         obtain E' where 
  1734           da_es': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<^sub>l\<guillemotright> E'"
  1735         proof -
  1736           from eval_e wt_e da_e wf True
  1737           have "nrm E1 \<subseteq> dom (locals (store s1))"
  1738             by (cases rule: da_good_approx_evalnE) iprover
  1739           with da_es show thesis
  1740             by (rule da_weakenE) (rule that)
  1741         qed
  1742         from valid_es Q' valid_A conf_s1 eval_es wt_es da_es'
  1743         show ?thesis
  1744           by (rule validE)
  1745       next
  1746         case False
  1747         with valid_es Q' valid_A conf_s1 eval_es 
  1748         show ?thesis
  1749           by (cases rule: validE) iprover+
  1750       qed
  1751       with v have "R \<lfloor>v\<rfloor>\<^sub>l s2 Z"
  1752         by simp
  1753       moreover
  1754       from eval wt da conf_s0 wf
  1755       have "s2\<Colon>\<preceq>(G, L)"
  1756         by (rule evaln_type_sound [elim_format]) simp
  1757       ultimately show ?thesis ..
  1758     qed
  1759   qed
  1760 next
  1761   case (Skip A P)
  1762   show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P} }"
  1763   proof (rule valid_stmt_NormalI)
  1764     fix s0 s1 n L Y Z
  1765     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1766     assume normal_s0: "normal s0"
  1767     assume eval: "G\<turnstile>s0 \<midarrow>Skip\<midarrow>n\<rightarrow> s1"
  1768     assume P: "(Normal (P\<leftarrow>\<diamondsuit>)) Y s0 Z"
  1769     show "P \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
  1770     proof -
  1771       from eval obtain "s1=s0"
  1772         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1773       with P conf_s0 show ?thesis
  1774         by simp
  1775     qed
  1776   qed
  1777 next
  1778   case (Expr A P e Q)
  1779   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>} }`
  1780   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Expr e. {Q} }"
  1781   proof (rule valid_stmt_NormalI)
  1782     fix n s0 L accC C s1 Y Z
  1783     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1784     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1785     assume normal_s0: "normal s0"
  1786     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Expr e\<Colon>\<surd>"
  1787     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Expr e\<rangle>\<^sub>s\<guillemotright> C"
  1788     assume eval: "G\<turnstile>s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
  1789     assume P: "(Normal P) Y s0 Z"
  1790     show "Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
  1791     proof -
  1792       from wt obtain eT where 
  1793         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
  1794         by cases simp
  1795       from da obtain E where
  1796         da_e: "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E"
  1797         by cases simp
  1798       from eval obtain v where
  1799         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1800         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1801       from valid_e P valid_A conf_s0 eval_e wt_e da_e
  1802       obtain Q: "(Q\<leftarrow>\<diamondsuit>) \<lfloor>v\<rfloor>\<^sub>e s1 Z" and "s1\<Colon>\<preceq>(G,L)"
  1803         by (rule validE)
  1804       thus ?thesis by simp
  1805     qed
  1806   qed
  1807 next
  1808   case (Lab A P c l Q)
  1809   note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }`
  1810   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
  1811   proof (rule valid_stmt_NormalI)
  1812     fix n s0 L accC C s2 Y Z
  1813     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1814     assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1815     assume normal_s0: "normal s0"
  1816     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>l\<bullet> c\<Colon>\<surd>"
  1817     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>l\<bullet> c\<rangle>\<^sub>s\<guillemotright> C"
  1818     assume eval: "G\<turnstile>s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> s2"
  1819     assume P: "(Normal P) Y s0 Z"
  1820     show "Q \<diamondsuit> s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
  1821     proof -
  1822       from wt obtain 
  1823         wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1824         by cases simp
  1825       from da obtain E where
  1826         da_c: "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>E"
  1827         by cases simp
  1828       from eval obtain s1 where
  1829         eval_c: "G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1" and
  1830         s2: "s2 = abupd (absorb l) s1"
  1831         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1832       from valid_c P valid_A conf_s0 eval_c wt_c da_c
  1833       obtain Q: "(abupd (absorb l) .; Q) \<diamondsuit> s1 Z" 
  1834         by (rule validE)
  1835       with s2 have "Q \<diamondsuit> s2 Z"
  1836         by simp
  1837       moreover
  1838       from eval wt da conf_s0 wf
  1839       have "s2\<Colon>\<preceq>(G, L)"
  1840         by (rule evaln_type_sound [elim_format]) simp
  1841       ultimately show ?thesis ..
  1842     qed
  1843   qed
  1844 next
  1845   case (Comp A P c1 Q c2 R)
  1846   note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
  1847   note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q} .c2. {R} }`
  1848   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1;; c2. {R} }"
  1849   proof (rule valid_stmt_NormalI)
  1850     fix n s0 L accC C s2 Y Z
  1851     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1852     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  1853     assume normal_s0: "normal s0"
  1854     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(c1;; c2)\<Colon>\<surd>"
  1855     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c1;;c2\<rangle>\<^sub>s\<guillemotright>C"
  1856     assume eval: "G\<turnstile>s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
  1857     assume P: "(Normal P) Y s0 Z"
  1858     show "R \<diamondsuit> s2 Z \<and> s2\<Colon>\<preceq>(G,L)"
  1859     proof -
  1860       from eval  obtain s1 where
  1861         eval_c1: "G\<turnstile>s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1" and
  1862         eval_c2: "G\<turnstile>s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2"
  1863         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  1864       from wt obtain 
  1865         wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1866         wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1867         by cases simp
  1868       from da obtain C1 C2 where 
  1869         da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and 
  1870         da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>nrm C1 \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2" 
  1871         by cases simp
  1872       from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1  
  1873       obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
  1874         by (rule validE) 
  1875       have "R \<diamondsuit> s2 Z"
  1876       proof (cases "normal s1")
  1877         case True
  1878         obtain C2' where 
  1879           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  1880         proof -
  1881           from eval_c1 wt_c1 da_c1 wf True
  1882           have "nrm C1 \<subseteq> dom (locals (store s1))"
  1883             by (cases rule: da_good_approx_evalnE) iprover
  1884           with da_c2 show thesis
  1885             by (rule da_weakenE) (rule that)
  1886         qed
  1887         with valid_c2 Q valid_A conf_s1 eval_c2 wt_c2 
  1888         show ?thesis
  1889           by (rule validE)
  1890       next
  1891         case False
  1892         from valid_c2 Q valid_A conf_s1 eval_c2 False
  1893         show ?thesis
  1894           by (cases rule: validE) iprover+
  1895       qed
  1896       moreover
  1897       from eval wt da conf_s0 wf
  1898       have "s2\<Colon>\<preceq>(G, L)"
  1899         by (rule evaln_type_sound [elim_format]) simp
  1900       ultimately show ?thesis ..
  1901     qed
  1902   qed
  1903 next
  1904   case (If A P e P' c1 c2 Q)
  1905   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {P'} }`
  1906   have valid_then_else: "\<And> b. G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} .(if b then c1 else c2). {Q} }"
  1907     using If.hyps by simp
  1908   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .If(e) c1 Else c2. {Q} }"
  1909   proof (rule valid_stmt_NormalI)
  1910     fix n s0 L accC C s2 Y Z
  1911     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1912     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  1913     assume normal_s0: "normal s0"
  1914     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>If(e) c1 Else c2\<Colon>\<surd>"
  1915     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1916                     \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<guillemotright>C"
  1917     assume eval: "G\<turnstile>s0 \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
  1918     assume P: "(Normal P) Y s0 Z"
  1919     show "Q \<diamondsuit> s2 Z \<and> s2\<Colon>\<preceq>(G,L)"
  1920     proof -
  1921       from eval obtain b s1 where
  1922         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1" and
  1923         eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2"
  1924         using normal_s0 by (auto elim: evaln_elim_cases)
  1925       from wt obtain  
  1926         wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1927         wt_then_else: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1928         by cases (simp split: split_if)
  1929       from da obtain E S where
  1930         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  1931         da_then_else: 
  1932         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1933              (dom (locals (store s0)) \<union> assigns_if (the_Bool b) e)
  1934                \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> S"
  1935         by cases (cases "the_Bool b",auto)
  1936       from valid_e P valid_A conf_s0 eval_e wt_e da_e
  1937       obtain "P' \<lfloor>b\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  1938         by (rule validE)
  1939       hence P': "\<And>v. (P'\<leftarrow>=the_Bool b) v s1 Z"
  1940         by (cases "normal s1") auto
  1941       have "Q \<diamondsuit> s2 Z"
  1942       proof (cases "normal s1")
  1943         case True
  1944         have s0_s1: "dom (locals (store s0)) 
  1945                       \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1946         proof -
  1947           from eval_e 
  1948           have eval_e': "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
  1949             by (rule evaln_eval)
  1950           hence
  1951             "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1952             by (rule dom_locals_eval_mono_elim)
  1953           moreover
  1954           from eval_e' True wt_e
  1955           have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1956             by (rule assigns_if_good_approx') 
  1957           ultimately show ?thesis by (rule Un_least)
  1958         qed
  1959         with da_then_else
  1960         obtain S' where
  1961           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1962               \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> S'"
  1963           by (rule da_weakenE)
  1964         with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else
  1965         show ?thesis
  1966           by (rule validE)
  1967       next
  1968         case False
  1969         with valid_then_else P' valid_A conf_s1 eval_then_else
  1970         show ?thesis
  1971           by (cases rule: validE) iprover+
  1972       qed
  1973       moreover
  1974       from eval wt da conf_s0 wf
  1975       have "s2\<Colon>\<preceq>(G, L)"
  1976         by (rule evaln_type_sound [elim_format]) simp
  1977       ultimately show ?thesis ..
  1978     qed
  1979   qed
  1980 next
  1981   case (Loop A P e P' c l)
  1982   note valid_e = `G,A|\<Turnstile>\<Colon>{ {P} e-\<succ> {P'} }`
  1983   note valid_c = `G,A|\<Turnstile>\<Colon>{ {Normal (P'\<leftarrow>=True)}
  1984                          .c. 
  1985                          {abupd (absorb (Cont l)) .; P} }`
  1986   show "G,A|\<Turnstile>\<Colon>{ {P} .l\<bullet> While(e) c. {P'\<leftarrow>=False\<down>=\<diamondsuit>} }"
  1987   proof (rule valid_stmtI)
  1988     fix n s0 L accC C s3 Y Z
  1989     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  1990     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  1991     assume wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
  1992     assume da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1993                     \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright> C"
  1994     assume eval: "G\<turnstile>s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
  1995     assume P: "P Y s0 Z"
  1996     show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
  1997     proof -
  1998         --{* From the given hypothesises @{text valid_e} and @{text valid_c} 
  1999            we can only reach the state after unfolding the loop once, i.e. 
  2000            @{term "P \<diamondsuit> s2 Z"}, where @{term s2} is the state after executing
  2001            @{term c}. To gain validity of the further execution of while, to
  2002            finally get @{term "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z"} we have to get 
  2003            a hypothesis about the subsequent unfoldings (the whole loop again),
  2004            too. We can achieve this, by performing induction on the 
  2005            evaluation relation, with all
  2006            the necessary preconditions to apply @{text valid_e} and 
  2007            @{text valid_c} in the goal.
  2008         *}
  2009       {
  2010         fix t s s' v 
  2011         assume "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
  2012         hence "\<And> Y' T E. 
  2013                 \<lbrakk>t =  \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s; \<forall>t\<in>A. G\<Turnstile>n\<Colon>t; P Y' s Z; s\<Colon>\<preceq>(G, L);
  2014                  normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
  2015                  normal s \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>E
  2016                 \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
  2017           (is "PROP ?Hyp n t s v s'")
  2018         proof (induct)
  2019           case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
  2020           note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
  2021           hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
  2022           note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
  2023           note P = `P Y' (Norm s0') Z`
  2024           note conf_s0' = `Norm s0'\<Colon>\<preceq>(G, L)`
  2025           have wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
  2026             using Loop.prems eqs by simp
  2027           have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
  2028                     dom (locals (store ((Norm s0')::state)))\<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright>E"
  2029             using Loop.prems eqs by simp
  2030           have evaln_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<midarrow>n'\<rightarrow> s1'" 
  2031             using Loop.hyps eqs by simp
  2032           show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
  2033           proof -
  2034             from wt  obtain 
  2035               wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  2036               wt_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
  2037               by cases (simp add: eqs)
  2038             from da obtain E S where
  2039               da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2040                      \<turnstile> dom (locals (store ((Norm s0')::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  2041               da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2042                      \<turnstile> (dom (locals (store ((Norm s0')::state))) 
  2043                             \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S"
  2044               by cases (simp add: eqs)
  2045             from evaln_e 
  2046             have eval_e: "G\<turnstile>Norm s0' \<midarrow>e-\<succ>b\<rightarrow> s1'"
  2047               by (rule evaln_eval)
  2048             from valid_e P valid_A conf_s0' evaln_e wt_e da_e
  2049             obtain P': "P' \<lfloor>b\<rfloor>\<^sub>e s1' Z" and conf_s1': "s1'\<Colon>\<preceq>(G,L)"
  2050               by (rule validE)
  2051             show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z"
  2052             proof (cases "normal s1'")
  2053               case True
  2054               note normal_s1'=this
  2055               show ?thesis
  2056               proof (cases "the_Bool b")
  2057                 case True
  2058                 with P' normal_s1' have P'': "(Normal (P'\<leftarrow>=True)) \<lfloor>b\<rfloor>\<^sub>e s1' Z"
  2059                   by auto
  2060                 from True Loop.hyps obtain
  2061                   eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
  2062                   eval_while:  
  2063                      "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
  2064                   by (simp add: eqs)
  2065                 from True Loop.hyps have
  2066                   hyp: "PROP ?Hyp n' \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s 
  2067                           (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
  2068                   apply (simp only: True if_True eqs)
  2069                   apply (elim conjE)
  2070                   apply (tactic "smp_tac 3 1")
  2071                   apply fast
  2072                   done
  2073                 from eval_e
  2074                 have s0'_s1': "dom (locals (store ((Norm s0')::state))) 
  2075                                   \<subseteq> dom (locals (store s1'))"
  2076                   by (rule dom_locals_eval_mono_elim)
  2077                 obtain S' where
  2078                   da_c':
  2079                    "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(dom (locals (store s1')))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright> S'" 
  2080                 proof -
  2081                   note s0'_s1'
  2082                   moreover
  2083                   from eval_e normal_s1' wt_e 
  2084                   have "assigns_if True e \<subseteq> dom (locals (store s1'))"
  2085                     by (rule assigns_if_good_approx' [elim_format]) 
  2086                        (simp add: True)
  2087                   ultimately 
  2088                   have "dom (locals (store ((Norm s0')::state)))
  2089                            \<union> assigns_if True e \<subseteq> dom (locals (store s1'))"
  2090                     by (rule Un_least)
  2091                   with da_c show thesis
  2092                     by (rule da_weakenE) (rule that)
  2093                 qed
  2094                 with valid_c P'' valid_A conf_s1' eval_c wt_c
  2095                 obtain "(abupd (absorb (Cont l)) .; P) \<diamondsuit> s2' Z" and 
  2096                   conf_s2': "s2'\<Colon>\<preceq>(G,L)"
  2097                   by (rule validE)
  2098                 hence P_s2': "P \<diamondsuit> (abupd (absorb (Cont l)) s2') Z"
  2099                   by simp
  2100                 from conf_s2'
  2101                 have conf_absorb: "abupd (absorb (Cont l)) s2' \<Colon>\<preceq>(G, L)"
  2102                   by (cases s2') (auto intro: conforms_absorb)
  2103                 moreover
  2104                 obtain E' where 
  2105                   da_while':
  2106                    "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  2107                      dom (locals(store (abupd (absorb (Cont l)) s2')))
  2108                       \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<guillemotright> E'"
  2109                 proof -
  2110                   note s0'_s1'
  2111                   also 
  2112                   from eval_c 
  2113                   have "G\<turnstile>s1' \<midarrow>c\<rightarrow> s2'"
  2114                     by (rule evaln_eval)
  2115                   hence "dom (locals (store s1')) \<subseteq> dom (locals (store s2'))"
  2116                     by (rule dom_locals_eval_mono_elim)
  2117                   also 
  2118                   have "\<dots>\<subseteq>dom (locals (store (abupd (absorb (Cont l)) s2')))"
  2119                     by simp
  2120                   finally
  2121                   have "dom (locals (store ((Norm s0')::state))) \<subseteq> \<dots>" .
  2122                   with da show thesis
  2123                     by (rule da_weakenE) (rule that)
  2124                 qed
  2125                 from valid_A P_s2' conf_absorb wt da_while'
  2126                 show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3' Z" 
  2127                   using hyp by (simp add: eqs)
  2128               next
  2129                 case False
  2130                 with Loop.hyps obtain "s3'=s1'"
  2131                   by simp
  2132                 with P' False show ?thesis
  2133                   by auto
  2134               qed 
  2135             next
  2136               case False
  2137               note abnormal_s1'=this
  2138               have "s3'=s1'"
  2139               proof -
  2140                 from False obtain abr where abr: "abrupt s1' = Some abr"
  2141                   by (cases s1') auto
  2142                 from eval_e _ wt_e wf
  2143                 have no_jmp: "\<And> j. abrupt s1' \<noteq> Some (Jump j)"
  2144                   by (rule eval_expression_no_jump 
  2145                        [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
  2146                      simp
  2147                 show ?thesis
  2148                 proof (cases "the_Bool b")
  2149                   case True  
  2150                   with Loop.hyps obtain
  2151                     eval_c: "G\<turnstile>s1' \<midarrow>c\<midarrow>n'\<rightarrow> s2'" and 
  2152                     eval_while:  
  2153                      "G\<turnstile>abupd (absorb (Cont l)) s2' \<midarrow>l\<bullet> While(e) c\<midarrow>n'\<rightarrow> s3'"
  2154                     by (simp add: eqs)
  2155                   from eval_c abr have "s2'=s1'" by auto
  2156                   moreover from calculation no_jmp 
  2157                   have "abupd (absorb (Cont l)) s2'=s2'"
  2158                     by (cases s1') (simp add: absorb_def)
  2159                   ultimately show ?thesis
  2160                     using eval_while abr
  2161                     by auto
  2162                 next
  2163                   case False
  2164                   with Loop.hyps show ?thesis by simp
  2165                 qed
  2166               qed
  2167               with P' False show ?thesis
  2168                 by auto
  2169             qed
  2170           qed
  2171         next
  2172           case (Abrupt abr s t' n' Y' T E)
  2173           note t' = `t' = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
  2174           note conf = `(Some abr, s)\<Colon>\<preceq>(G, L)`
  2175           note P = `P Y' (Some abr, s) Z`
  2176           note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
  2177           show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
  2178           proof -
  2179             have eval_e: 
  2180               "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
  2181               by auto
  2182             from valid_e P valid_A conf eval_e 
  2183             have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
  2184               by (cases rule: validE [where ?P="P"]) simp+
  2185             with t' show ?thesis
  2186               by auto
  2187           qed
  2188         qed simp_all
  2189       } note generalized=this
  2190       from eval _ valid_A P conf_s0 wt da
  2191       have "(P'\<leftarrow>=False\<down>=\<diamondsuit>) \<diamondsuit> s3 Z"
  2192         by (rule generalized)  simp_all
  2193       moreover
  2194       have "s3\<Colon>\<preceq>(G, L)"
  2195       proof (cases "normal s0")
  2196         case True
  2197         from eval wt [OF True] da [OF True] conf_s0 wf
  2198         show ?thesis
  2199           by (rule evaln_type_sound [elim_format]) simp
  2200       next
  2201         case False
  2202         with eval have "s3=s0"
  2203           by auto
  2204         with conf_s0 show ?thesis 
  2205           by simp
  2206       qed
  2207       ultimately show ?thesis ..
  2208     qed
  2209   qed
  2210 next
  2211   case (Jmp A j P)
  2212   show "G,A|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
  2213   proof (rule valid_stmt_NormalI)
  2214     fix n s0 L accC C s1 Y Z
  2215     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2216     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2217     assume normal_s0: "normal s0"
  2218     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Jmp j\<Colon>\<surd>"
  2219     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2220                     \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Jmp j\<rangle>\<^sub>s\<guillemotright>C"
  2221     assume eval: "G\<turnstile>s0 \<midarrow>Jmp j\<midarrow>n\<rightarrow> s1"
  2222     assume P: "(Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)) Y s0 Z"
  2223     show "P \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
  2224     proof -
  2225       from eval obtain s where  
  2226         s: "s0=Norm s" "s1=(Some (Jump j), s)" 
  2227         using normal_s0 by (auto elim: evaln_elim_cases)
  2228       with P have "P \<diamondsuit> s1 Z"
  2229         by simp
  2230       moreover 
  2231       from eval wt da conf_s0 wf
  2232       have "s1\<Colon>\<preceq>(G,L)"
  2233         by (rule evaln_type_sound [elim_format]) simp
  2234       ultimately show ?thesis ..
  2235     qed
  2236   qed
  2237 next
  2238   case (Throw A P e Q)
  2239   note valid_e = `G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>} }`
  2240   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Throw e. {Q} }"
  2241   proof (rule valid_stmt_NormalI)
  2242     fix n s0 L accC C s2 Y Z
  2243     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2244     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2245     assume normal_s0: "normal s0"
  2246     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Throw e\<Colon>\<surd>"
  2247     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2248                     \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Throw e\<rangle>\<^sub>s\<guillemotright>C"
  2249     assume eval: "G\<turnstile>s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> s2"
  2250     assume P: "(Normal P) Y s0 Z"
  2251     show "Q \<diamondsuit> s2 Z \<and> s2\<Colon>\<preceq>(G,L)"
  2252     proof -
  2253       from eval obtain s1 a where
  2254         eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
  2255         s2: "s2 = abupd (throw a) s1"
  2256         using normal_s0 by (auto elim: evaln_elim_cases)
  2257       from wt obtain T where
  2258         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
  2259         by cases simp
  2260       from da obtain E where
  2261         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
  2262         by cases simp
  2263       from valid_e P valid_A conf_s0 eval_e wt_e da_e 
  2264       obtain "(\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>) \<lfloor>a\<rfloor>\<^sub>e s1 Z"
  2265         by (rule validE)
  2266       with s2 have "Q \<diamondsuit> s2 Z"
  2267         by simp
  2268       moreover 
  2269       from eval wt da conf_s0 wf
  2270       have "s2\<Colon>\<preceq>(G,L)"
  2271         by (rule evaln_type_sound [elim_format]) simp
  2272       ultimately show ?thesis ..
  2273     qed
  2274   qed
  2275 next
  2276   case (Try A P c1 Q C vn c2 R)
  2277   note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {SXAlloc G Q} }`
  2278   note valid_c2 = `G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} 
  2279                            .c2. 
  2280                           {R} }`
  2281   note Q_R = `(Q \<and>. (\<lambda>s. \<not> G,s\<turnstile>catch C)) \<Rightarrow> R`
  2282   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .Try c1 Catch(C vn) c2. {R} }"
  2283   proof (rule valid_stmt_NormalI)
  2284     fix n s0 L accC E s3 Y Z
  2285     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2286     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2287     assume normal_s0: "normal s0"
  2288     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Try c1 Catch(C vn) c2\<Colon>\<surd>"
  2289     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2290                     \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<^sub>s\<guillemotright> E"
  2291     assume eval: "G\<turnstile>s0 \<midarrow>Try c1 Catch(C vn) c2\<midarrow>n\<rightarrow> s3"
  2292     assume P: "(Normal P) Y s0 Z"
  2293     show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
  2294     proof -
  2295       from eval obtain s1 s2 where
  2296         eval_c1: "G\<turnstile>s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1" and
  2297         sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" and
  2298         s3: "if G,s2\<turnstile>catch C 
  2299                 then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 
  2300                 else s3 = s2"
  2301         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  2302       from wt obtain
  2303         wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2304         wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
  2305         by cases simp
  2306       from da obtain C1 C2 where
  2307         da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and
  2308         da_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>
  2309                    \<turnstile> (dom (locals (store s0)) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2"
  2310         by cases simp
  2311       from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1
  2312       obtain sxQ: "(SXAlloc G Q) \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  2313         by (rule validE)
  2314       from sxalloc sxQ
  2315       have Q: "Q \<diamondsuit> s2 Z"
  2316         by auto
  2317       have "R \<diamondsuit> s3 Z"
  2318       proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
  2319         case False
  2320         from sxalloc wf
  2321         have "s2=s1"
  2322           by (rule sxalloc_type_sound [elim_format])
  2323              (insert False, auto split: option.splits abrupt.splits )
  2324         with False 
  2325         have no_catch: "\<not>  G,s2\<turnstile>catch C"
  2326           by (simp add: catch_def)
  2327         moreover
  2328         from no_catch s3
  2329         have "s3=s2"
  2330           by simp
  2331         ultimately show ?thesis
  2332           using Q Q_R by simp
  2333       next
  2334         case True
  2335         note exception_s1 = this
  2336         show ?thesis
  2337         proof (cases "G,s2\<turnstile>catch C") 
  2338           case False
  2339           with s3
  2340           have "s3=s2"
  2341             by simp
  2342           with False Q Q_R show ?thesis
  2343             by simp
  2344         next
  2345           case True
  2346           with s3 have eval_c2: "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3"
  2347             by simp
  2348           from conf_s1 sxalloc wf 
  2349           have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  2350             by (auto dest: sxalloc_type_sound 
  2351                     split: option.splits abrupt.splits)
  2352           from exception_s1 sxalloc wf
  2353           obtain a 
  2354             where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  2355             by (auto dest!: sxalloc_type_sound 
  2356                             split: option.splits abrupt.splits)
  2357           with True
  2358           have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class C"
  2359             by (cases s2) simp
  2360           with xcpt_s2 conf_s2 wf
  2361           have conf_new_xcpt: "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class C))"
  2362             by (auto dest: Try_lemma)
  2363           obtain C2' where
  2364             da_c2':
  2365             "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class C)\<rparr>
  2366               \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  2367           proof -
  2368             have "(dom (locals (store s0)) \<union> {VName vn}) 
  2369                     \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  2370             proof -
  2371               from eval_c1 
  2372               have "dom (locals (store s0)) 
  2373                       \<subseteq> dom (locals (store s1))"
  2374                 by (rule dom_locals_evaln_mono_elim)
  2375               also
  2376               from sxalloc
  2377               have "\<dots> \<subseteq> dom (locals (store s2))"
  2378                 by (rule dom_locals_sxalloc_mono)
  2379               also 
  2380               have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  2381                 by (cases s2) (simp add: new_xcpt_var_def, blast) 
  2382               also
  2383               have "{VName vn} \<subseteq> \<dots>"
  2384                 by (cases s2) simp
  2385               ultimately show ?thesis
  2386                 by (rule Un_least)
  2387             qed
  2388             with da_c2 show thesis
  2389               by (rule da_weakenE) (rule that)
  2390           qed
  2391           from Q eval_c2 True 
  2392           have "(Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn) 
  2393                    \<diamondsuit> (new_xcpt_var vn s2) Z"
  2394             by auto
  2395           from valid_c2 this valid_A conf_new_xcpt eval_c2 wt_c2 da_c2'
  2396           show "R \<diamondsuit> s3 Z"
  2397             by (rule validE)
  2398         qed
  2399       qed
  2400       moreover 
  2401       from eval wt da conf_s0 wf
  2402       have "s3\<Colon>\<preceq>(G,L)"
  2403         by (rule evaln_type_sound [elim_format]) simp
  2404       ultimately show ?thesis ..
  2405     qed
  2406   qed
  2407 next
  2408   case (Fin A P c1 Q c2 R)
  2409   note valid_c1 = `G,A|\<Turnstile>\<Colon>{ {Normal P} .c1. {Q} }`
  2410   have valid_c2: "\<And> abr. G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. abr = fst s) ;. abupd (\<lambda>x. None)} 
  2411                                   .c2.
  2412                                   {abupd (abrupt_if (abr \<noteq> None) abr) .; R} }"
  2413     using Fin.hyps by simp
  2414   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .c1 Finally c2. {R} }"
  2415   proof (rule valid_stmt_NormalI)
  2416     fix n s0 L accC E s3 Y Z
  2417     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2418     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2419     assume normal_s0: "normal s0"
  2420     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1 Finally c2\<Colon>\<surd>"
  2421     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2422                     \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> E"
  2423     assume eval: "G\<turnstile>s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
  2424     assume P: "(Normal P) Y s0 Z"
  2425     show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
  2426     proof -
  2427       from eval obtain s1 abr1 s2 where
  2428         eval_c1: "G\<turnstile>s0 \<midarrow>c1\<midarrow>n\<rightarrow> (abr1, s1)" and
  2429         eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2" and
  2430         s3: "s3 = (if \<exists>err. abr1 = Some (Error err) 
  2431                       then (abr1, s1)
  2432                       else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
  2433         using normal_s0 by (fastsimp elim: evaln_elim_cases)
  2434       from wt obtain
  2435         wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2436         wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  2437         by cases simp
  2438       from da obtain C1 C2 where
  2439         da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and
  2440         da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2"
  2441         by cases simp
  2442       from valid_c1 P valid_A conf_s0 eval_c1 wt_c1 da_c1
  2443       obtain Q: "Q \<diamondsuit> (abr1,s1) Z" and conf_s1: "(abr1,s1)\<Colon>\<preceq>(G,L)" 
  2444         by (rule validE)
  2445       from Q 
  2446       have Q': "(Q \<and>. (\<lambda>s. abr1 = fst s) ;. abupd (\<lambda>x. None)) \<diamondsuit> (Norm s1) Z"
  2447         by auto
  2448       from eval_c1 wt_c1 da_c1 conf_s0 wf
  2449       have  "error_free (abr1,s1)"
  2450         by (rule evaln_type_sound  [elim_format]) (insert normal_s0,simp)
  2451       with s3 have s3': "s3 = abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
  2452         by (simp add: error_free_def)
  2453       from conf_s1 
  2454       have conf_Norm_s1: "Norm s1\<Colon>\<preceq>(G,L)"
  2455         by (rule conforms_NormI)
  2456       obtain C2' where 
  2457         da_c2': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2458                    \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  2459       proof -
  2460         from eval_c1 
  2461         have "dom (locals (store s0)) \<subseteq> dom (locals (store (abr1,s1)))"
  2462           by (rule dom_locals_evaln_mono_elim)
  2463         hence "dom (locals (store s0)) 
  2464                  \<subseteq> dom (locals (store ((Norm s1)::state)))"
  2465           by simp
  2466         with da_c2 show thesis
  2467           by (rule da_weakenE) (rule that)
  2468       qed
  2469       from valid_c2 Q' valid_A conf_Norm_s1 eval_c2 wt_c2 da_c2'
  2470       have "(abupd (abrupt_if (abr1 \<noteq> None) abr1) .; R) \<diamondsuit> s2 Z"
  2471         by (rule validE)
  2472       with s3' have "R \<diamondsuit> s3 Z"
  2473         by simp
  2474       moreover
  2475       from eval wt da conf_s0 wf
  2476       have "s3\<Colon>\<preceq>(G,L)"
  2477         by (rule evaln_type_sound [elim_format]) simp
  2478       ultimately show ?thesis ..
  2479     qed
  2480   qed
  2481 next
  2482   case (Done A P C)
  2483   show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }" 
  2484   proof (rule valid_stmt_NormalI)
  2485     fix n s0 L accC E s3 Y Z
  2486     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2487     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2488     assume normal_s0: "normal s0"
  2489     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>"
  2490     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2491                     \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> E"
  2492     assume eval: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
  2493     assume P: "(Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)) Y s0 Z"
  2494     show "P \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
  2495     proof -
  2496       from P have inited: "inited C (globs (store s0))"
  2497         by simp
  2498       with eval have "s3=s0"
  2499         using normal_s0 by (auto elim: evaln_elim_cases)
  2500       with P conf_s0 show ?thesis
  2501         by simp
  2502     qed
  2503   qed
  2504 next
  2505   case (Init C c A P Q R)
  2506   note c = `the (class G C) = c`
  2507   note valid_super =
  2508         `G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
  2509                  .(if C = Object then Skip else Init (super c)). 
  2510                  {Q} }`
  2511   have valid_init: 
  2512         "\<And> l.  G,A|\<Turnstile>\<Colon>{ {Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} 
  2513                         .init c.
  2514                         {set_lvars l .; R} }"
  2515     using Init.hyps by simp
  2516   show "G,A|\<Turnstile>\<Colon>{ {Normal (P \<and>. Not \<circ> initd C)} .Init C. {R} }"
  2517   proof (rule valid_stmt_NormalI)
  2518     fix n s0 L accC E s3 Y Z
  2519     assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
  2520     assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
  2521     assume normal_s0: "normal s0"
  2522     assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>"
  2523     assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2524                     \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> E"
  2525     assume eval: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
  2526     assume P: "(Normal (P \<and>. Not \<circ> initd C)) Y s0 Z"
  2527     show "R \<diamondsuit> s3 Z \<and> s3\<Colon>\<preceq>(G,L)"
  2528     proof -
  2529       from P have not_inited: "\<not> inited C (globs (store s0))" by simp
  2530       with eval c obtain s1 s2 where
  2531         eval_super: 
  2532         "G\<turnstile>Norm ((init_class_obj G C) (store s0)) 
  2533            \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1" and
  2534         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2" and
  2535         s3: "s3 = (set_lvars (locals (store s1))) s2"
  2536         using normal_s0 by (auto elim!: evaln_elim_cases)
  2537       from wt c have
  2538         cls_C: "class G C = Some c"
  2539         by cases auto
  2540       from wf cls_C have
  2541         wt_super: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2542                          \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  2543         by (cases "C=Object")
  2544            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  2545       obtain S where
  2546         da_super:
  2547         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2548           \<turnstile> dom (locals (store ((Norm 
  2549                             ((init_class_obj G C) (store s0)))::state))) 
  2550                \<guillemotright>\<langle>if C = Object then Skip else Init (super c)\<rangle>\<^sub>s\<guillemotright> S"
  2551       proof (cases "C=Object")
  2552         case True 
  2553         with da_Skip show ?thesis
  2554           using that by (auto intro: assigned.select_convs)
  2555       next
  2556         case False 
  2557         with da_Init show ?thesis
  2558           by - (rule that, auto intro: assigned.select_convs)
  2559       qed
  2560       from normal_s0 conf_s0 wf cls_C not_inited
  2561       have conf_init_cls: "(Norm ((init_class_obj G C) (store s0)))\<Colon>\<preceq>(G, L)"
  2562         by (auto intro: conforms_init_class_obj)        
  2563       from P 
  2564       have P': "(Normal (P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C)))
  2565                    Y (Norm ((init_class_obj G C) (store s0))) Z"
  2566         by auto
  2567 
  2568       from valid_super P' valid_A conf_init_cls eval_super wt_super da_super
  2569       obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
  2570         by (rule validE)
  2571       
  2572       from cls_C wf have wt_init: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
  2573         by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
  2574       from cls_C wf obtain I where 
  2575         "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I"
  2576         by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
  2577        (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
  2578       then obtain I' where
  2579         da_init:
  2580         "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
  2581             \<guillemotright>\<langle>init c\<rangle>\<^sub>s\<guillemotright> I'"
  2582         by (rule da_weakenE) simp
  2583       have conf_s1_empty: "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  2584       proof -
  2585         from eval_super have
  2586           "G\<turnstile>Norm ((init_class_obj G C) (store s0)) 
  2587              \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
  2588           by (rule evaln_eval)
  2589         from this wt_super wf
  2590         have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2591           by - (rule eval_statement_no_jump 
  2592                  [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], auto split: split_if)
  2593         with conf_s1
  2594         show ?thesis
  2595           by (cases s1) (auto intro: conforms_set_locals)
  2596       qed
  2597       
  2598       obtain l where l: "l = locals (store s1)"
  2599         by simp
  2600       with Q 
  2601       have Q': "(Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty)
  2602                   \<diamondsuit> ((set_lvars empty) s1) Z"
  2603         by auto
  2604       from valid_init Q' valid_A conf_s1_empty eval_init wt_init da_init
  2605       have "(set_lvars l .; R) \<diamondsuit> s2 Z"
  2606         by (rule validE)
  2607       with s3 l have "R \<diamondsuit> s3 Z"
  2608         by simp
  2609       moreover 
  2610       from eval wt da conf_s0 wf
  2611       have "s3\<Colon>\<preceq>(G,L)"
  2612         by (rule evaln_type_sound [elim_format]) simp
  2613       ultimately show ?thesis ..
  2614     qed
  2615   qed
  2616 next
  2617   case (InsInitV A P c v Q)
  2618   show "G,A|\<Turnstile>\<Colon>{ {Normal P} InsInitV c v=\<succ> {Q} }"
  2619   proof (rule valid_var_NormalI)
  2620     fix s0 vf n s1 L Z
  2621     assume "normal s0"
  2622     moreover
  2623     assume "G\<turnstile>s0 \<midarrow>InsInitV c v=\<succ>vf\<midarrow>n\<rightarrow> s1"
  2624     ultimately have "False" 
  2625       by (cases s0) (simp add: evaln_InsInitV) 
  2626     thus "Q \<lfloor>vf\<rfloor>\<^sub>v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  2627   qed
  2628 next
  2629   case (InsInitE A P c e Q)
  2630   show "G,A|\<Turnstile>\<Colon>{ {Normal P} InsInitE c e-\<succ> {Q} }"
  2631   proof (rule valid_expr_NormalI)
  2632     fix s0 v n s1 L Z
  2633     assume "normal s0"
  2634     moreover
  2635     assume "G\<turnstile>s0 \<midarrow>InsInitE c e-\<succ>v\<midarrow>n\<rightarrow> s1"
  2636     ultimately have "False" 
  2637       by (cases s0) (simp add: evaln_InsInitE) 
  2638     thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  2639   qed
  2640 next
  2641   case (Callee A P l e Q)
  2642   show "G,A|\<Turnstile>\<Colon>{ {Normal P} Callee l e-\<succ> {Q} }"
  2643   proof (rule valid_expr_NormalI)
  2644     fix s0 v n s1 L Z
  2645     assume "normal s0"
  2646     moreover
  2647     assume "G\<turnstile>s0 \<midarrow>Callee l e-\<succ>v\<midarrow>n\<rightarrow> s1"
  2648     ultimately have "False" 
  2649       by (cases s0) (simp add: evaln_Callee) 
  2650     thus "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  2651   qed
  2652 next
  2653   case (FinA A P a c Q)
  2654   show "G,A|\<Turnstile>\<Colon>{ {Normal P} .FinA a c. {Q} }"
  2655   proof (rule valid_stmt_NormalI)
  2656     fix s0 v n s1 L Z
  2657     assume "normal s0"
  2658     moreover
  2659     assume "G\<turnstile>s0 \<midarrow>FinA a c\<midarrow>n\<rightarrow> s1"
  2660     ultimately have "False" 
  2661       by (cases s0) (simp add: evaln_FinA) 
  2662     thus "Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G, L)"..
  2663   qed
  2664 qed
  2665 declare inj_term_simps [simp del]
  2666     
  2667 theorem ax_sound: 
  2668  "wf_prog G \<Longrightarrow> G,(A::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> G,A|\<Turnstile>ts"
  2669 apply (subst ax_valids2_eq [symmetric])
  2670 apply  assumption
  2671 apply (erule (1) ax_sound2)
  2672 done
  2673 
  2674 lemma sound_valid2_lemma: 
  2675 "\<lbrakk>\<forall>v n. Ball A (triple_valid2 G n) \<longrightarrow> P v n; Ball A (triple_valid2 G n)\<rbrakk>
  2676  \<Longrightarrow>P v n"
  2677 by blast
  2678 
  2679 end