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