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