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