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