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