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