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