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