src/HOL/Bali/AxSound.thy
author schirmer
Fri Nov 01 13:16:28 2002 +0100 (2002-11-01)
changeset 13690 ac335b2f4a39
parent 13688 a0b16d42d489
child 14030 cd928c0ac225
permissions -rw-r--r--
Inserted some extra paragraphs in large proofs to make tex run...
wenzelm@12857
     1
(*  Title:      HOL/Bali/AxSound.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@13688
     3
    Author:     David von Oheimb and Norbert Schirmer
wenzelm@12859
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Soundness proof for Axiomatic semantics of Java expressions and 
schirmer@12854
     7
          statements
schirmer@12854
     8
       *}
schirmer@12854
     9
schirmer@12854
    10
schirmer@12854
    11
schirmer@12854
    12
theory AxSound = AxSem:
schirmer@12854
    13
schirmer@12854
    14
section "validity"
schirmer@12854
    15
schirmer@12854
    16
consts
schirmer@12854
    17
schirmer@12854
    18
 triple_valid2:: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
schirmer@12854
    19
                                                (   "_\<Turnstile>_\<Colon>_"[61,0, 58] 57)
schirmer@12854
    20
    ax_valids2:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
schirmer@12854
    21
                                                ("_,_|\<Turnstile>\<Colon>_" [61,58,58] 57)
schirmer@12854
    22
schirmer@12854
    23
defs  triple_valid2_def: "G\<Turnstile>n\<Colon>t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
schirmer@12854
    24
 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>L. s\<Colon>\<preceq>(G,L) 
schirmer@13688
    25
 \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
schirmer@13688
    26
                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
schirmer@12854
    27
 (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L))))"
schirmer@12854
    28
schirmer@13688
    29
text {* This definition differs from the ordinary  @{text triple_valid_def} 
schirmer@13688
    30
manly in the conclusion: We also ensures conformance of the result state. So
schirmer@13688
    31
we don't have to apply the type soundness lemma all the time during
schirmer@13688
    32
induction. This definition is only introduced for the soundness
schirmer@13688
    33
proof of the axiomatic semantics, in the end we will conclude to 
schirmer@13688
    34
the ordinary definition.
schirmer@13688
    35
*}
schirmer@13688
    36
 
schirmer@12854
    37
defs  ax_valids2_def:    "G,A|\<Turnstile>\<Colon>ts \<equiv>  \<forall>n. (\<forall>t\<in>A. G\<Turnstile>n\<Colon>t) \<longrightarrow> (\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t)"
schirmer@12854
    38
schirmer@12854
    39
lemma triple_valid2_def2: "G\<Turnstile>n\<Colon>{P} t\<succ> {Q} =  
schirmer@12854
    40
 (\<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow>  
schirmer@13688
    41
  (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
schirmer@13688
    42
                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<longrightarrow>
schirmer@12854
    43
  Q Y' s' Z \<and> s'\<Colon>\<preceq>(G,L)))))"
schirmer@12854
    44
apply (unfold triple_valid2_def)
schirmer@12854
    45
apply (simp (no_asm) add: split_paired_All)
schirmer@12854
    46
apply blast
schirmer@12854
    47
done
schirmer@12854
    48
schirmer@12854
    49
lemma triple_valid2_eq [rule_format (no_asm)]: 
schirmer@12854
    50
  "wf_prog G ==> triple_valid2 G = triple_valid G"
schirmer@12854
    51
apply (rule ext)
schirmer@12854
    52
apply (rule ext)
schirmer@12854
    53
apply (rule triple.induct)
schirmer@12854
    54
apply (simp (no_asm) add: triple_valid_def2 triple_valid2_def2)
schirmer@12854
    55
apply (rule iffI)
schirmer@12854
    56
apply  fast
schirmer@12854
    57
apply clarify
schirmer@12854
    58
apply (tactic "smp_tac 3 1")
schirmer@12854
    59
apply (case_tac "normal s")
schirmer@12854
    60
apply  clarsimp
schirmer@13688
    61
apply  (elim conjE impE)
schirmer@13688
    62
apply    blast
schirmer@13688
    63
schirmer@13688
    64
apply    (tactic "smp_tac 2 1")
schirmer@13688
    65
apply    (drule evaln_eval)
schirmer@13688
    66
apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
schirmer@13688
    67
apply    simp
schirmer@13688
    68
schirmer@13688
    69
apply    clarsimp
schirmer@12854
    70
done
schirmer@12854
    71
schirmer@13688
    72
schirmer@12854
    73
lemma ax_valids2_eq: "wf_prog G \<Longrightarrow> G,A|\<Turnstile>\<Colon>ts = G,A|\<Turnstile>ts"
schirmer@12854
    74
apply (unfold ax_valids_def ax_valids2_def)
schirmer@12854
    75
apply (force simp add: triple_valid2_eq)
schirmer@12854
    76
done
schirmer@12854
    77
schirmer@12854
    78
lemma triple_valid2_Suc [rule_format (no_asm)]: "G\<Turnstile>Suc n\<Colon>t \<longrightarrow> G\<Turnstile>n\<Colon>t"
schirmer@12854
    79
apply (induct_tac "t")
schirmer@12854
    80
apply (subst triple_valid2_def2)
schirmer@12854
    81
apply (subst triple_valid2_def2)
schirmer@12854
    82
apply (fast intro: evaln_nonstrict_Suc)
schirmer@12854
    83
done
schirmer@12854
    84
schirmer@12854
    85
lemma Methd_triple_valid2_0: "G\<Turnstile>0\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
schirmer@12854
    86
apply (clarsimp elim!: evaln_elim_cases simp add: triple_valid2_def2)
schirmer@12854
    87
done
schirmer@12854
    88
schirmer@12854
    89
lemma Methd_triple_valid2_SucI: 
schirmer@12854
    90
"\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
schirmer@12854
    91
  \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
schirmer@12854
    92
apply (simp (no_asm_use) add: triple_valid2_def2)
schirmer@12854
    93
apply (intro strip, tactic "smp_tac 3 1", clarify)
schirmer@13688
    94
apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
schirmer@12854
    95
apply (unfold body_def Let_def)
schirmer@13688
    96
apply (clarsimp simp add: inj_term_simps)
schirmer@12854
    97
apply blast
schirmer@12854
    98
done
schirmer@12854
    99
schirmer@12854
   100
lemma triples_valid2_Suc: 
schirmer@12854
   101
 "Ball ts (triple_valid2 G (Suc n)) \<Longrightarrow> Ball ts (triple_valid2 G n)"
schirmer@12854
   102
apply (fast intro: triple_valid2_Suc)
schirmer@12854
   103
done
schirmer@12854
   104
schirmer@12854
   105
lemma "G|\<Turnstile>n:insert t A = (G\<Turnstile>n:t \<and> G|\<Turnstile>n:A)";
schirmer@12854
   106
oops
schirmer@12854
   107
schirmer@12854
   108
schirmer@12854
   109
section "soundness"
schirmer@12854
   110
schirmer@12854
   111
lemma Methd_sound: 
schirmer@13688
   112
  assumes recursive: "G,A\<union>  {{P} Methd-\<succ> {Q} | ms}|\<Turnstile>\<Colon>{{P} body G-\<succ> {Q} | ms}"
schirmer@13688
   113
  shows "G,A|\<Turnstile>\<Colon>{{P} Methd-\<succ> {Q} | ms}"
schirmer@13688
   114
proof -
schirmer@13688
   115
  {
schirmer@13688
   116
    fix n
schirmer@13688
   117
    assume recursive: "\<And> n. \<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>n\<Colon>t
schirmer@13688
   118
                              \<Longrightarrow>  \<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
schirmer@13688
   119
    have "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>n\<Colon>t"
schirmer@13688
   120
    proof (induct n)
schirmer@13688
   121
      case 0
schirmer@13688
   122
      show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>0\<Colon>t"
schirmer@13688
   123
      proof -
schirmer@13688
   124
	{
schirmer@13688
   125
	  fix C sig
schirmer@13688
   126
	  assume "(C,sig) \<in> ms" 
schirmer@13688
   127
	  have "G\<Turnstile>0\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
schirmer@13688
   128
	    by (rule Methd_triple_valid2_0)
schirmer@13688
   129
	}
schirmer@13688
   130
	thus ?thesis
schirmer@13688
   131
	  by (simp add: mtriples_def split_def)
schirmer@13688
   132
      qed
schirmer@13688
   133
    next
schirmer@13688
   134
      case (Suc m)
schirmer@13688
   135
      have hyp: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t \<Longrightarrow> \<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t".
schirmer@13688
   136
      have prem: "\<forall>t\<in>A. G\<Turnstile>Suc m\<Colon>t" .
schirmer@13688
   137
      show "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>Suc m\<Colon>t"
schirmer@13688
   138
      proof -
schirmer@13688
   139
	{
schirmer@13688
   140
	  fix C sig
schirmer@13688
   141
	  assume m: "(C,sig) \<in> ms" 
schirmer@13688
   142
	  have "G\<Turnstile>Suc m\<Colon>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
schirmer@13688
   143
	  proof -
schirmer@13688
   144
	    from prem have prem_m: "\<forall>t\<in>A. G\<Turnstile>m\<Colon>t"
schirmer@13688
   145
	      by (rule triples_valid2_Suc)
schirmer@13688
   146
	    hence "\<forall>t\<in>{{P} Methd-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
schirmer@13688
   147
	      by (rule hyp)
schirmer@13688
   148
	    with prem_m
schirmer@13688
   149
	    have "\<forall>t\<in>(A \<union> {{P} Methd-\<succ> {Q} | ms}). G\<Turnstile>m\<Colon>t"
schirmer@13688
   150
	      by (simp add: ball_Un)
schirmer@13688
   151
	    hence "\<forall>t\<in>{{P} body G-\<succ> {Q} | ms}.  G\<Turnstile>m\<Colon>t"
schirmer@13688
   152
	      by (rule recursive)
schirmer@13688
   153
	    with m have "G\<Turnstile>m\<Colon>{Normal (P C sig)} body G C sig-\<succ> {Q C sig}"
schirmer@13688
   154
	      by (auto simp add: mtriples_def split_def)
schirmer@13688
   155
	    thus ?thesis
schirmer@13688
   156
	      by (rule Methd_triple_valid2_SucI)
schirmer@13688
   157
	  qed
schirmer@13688
   158
	}
schirmer@13688
   159
	thus ?thesis
schirmer@13688
   160
	  by (simp add: mtriples_def split_def)
schirmer@13688
   161
      qed
schirmer@13688
   162
    qed
schirmer@13688
   163
  }
schirmer@13688
   164
  with recursive show ?thesis
schirmer@13688
   165
    by (unfold ax_valids2_def) blast
schirmer@13688
   166
qed
schirmer@12854
   167
schirmer@12854
   168
schirmer@12854
   169
lemma valids2_inductI: "\<forall>s t n Y' s'. G\<turnstile>s\<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> t = c \<longrightarrow>    
schirmer@12854
   170
  Ball A (triple_valid2 G n) \<longrightarrow> (\<forall>Y Z. P Y s Z \<longrightarrow>  
schirmer@13688
   171
  (\<forall>L. s\<Colon>\<preceq>(G,L) \<longrightarrow> 
schirmer@13688
   172
    (\<forall>T C A. (normal s \<longrightarrow> (\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<and> 
schirmer@13688
   173
                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A) \<longrightarrow>
schirmer@13688
   174
    Q Y' s' Z \<and> s'\<Colon>\<preceq>(G, L)))) \<Longrightarrow>  
schirmer@12854
   175
  G,A|\<Turnstile>\<Colon>{ {P} c\<succ> {Q}}"
schirmer@12854
   176
apply (simp (no_asm) add: ax_valids2_def triple_valid2_def2)
schirmer@12854
   177
apply clarsimp
schirmer@12854
   178
done
schirmer@12854
   179
schirmer@13688
   180
lemma da_good_approx_evalnE [consumes 4]:
schirmer@13688
   181
  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
schirmer@13688
   182
     and     wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"
schirmer@13688
   183
     and     da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"
schirmer@13688
   184
     and     wf: "wf_prog G"
schirmer@13688
   185
     and   elim: "\<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
schirmer@13688
   186
                  \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
schirmer@13688
   187
                        \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
schirmer@13688
   188
                   \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
schirmer@13688
   189
                   \<Longrightarrow>Result \<in> dom (locals (store s1))
schirmer@13688
   190
                  \<rbrakk> \<Longrightarrow> P"
schirmer@13688
   191
  shows "P"
schirmer@13688
   192
proof -
schirmer@13688
   193
  from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
schirmer@13688
   194
    by (rule evaln_eval)
schirmer@13688
   195
  from this wt da wf elim show P
schirmer@13688
   196
    by (rule da_good_approxE') rules+
schirmer@13688
   197
qed
schirmer@12854
   198
schirmer@13688
   199
lemma validI: 
schirmer@13688
   200
   assumes I: "\<And> n s0 L accC T C v s1 Y Z.
schirmer@13688
   201
               \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); 
schirmer@13688
   202
               normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
schirmer@13688
   203
               normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C;
schirmer@13688
   204
               G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1); P Y s0 Z\<rbrakk> \<Longrightarrow> Q v s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
schirmer@13688
   205
  shows "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
schirmer@13688
   206
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   207
apply (intro allI impI)
schirmer@13688
   208
apply (case_tac "normal s")
schirmer@13688
   209
apply   clarsimp 
schirmer@13688
   210
apply   (rule I,(assumption|simp)+)
schirmer@13688
   211
schirmer@13688
   212
apply   (rule I,auto)
schirmer@13688
   213
done
schirmer@13688
   214
  
schirmer@13688
   215
schirmer@13688
   216
schirmer@13688
   217
schirmer@13688
   218
ML "Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]"
schirmer@13688
   219
schirmer@13688
   220
lemma valid_stmtI: 
schirmer@13688
   221
   assumes I: "\<And> n s0 L accC C s1 Y Z.
schirmer@13688
   222
             \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); 
schirmer@13688
   223
              normal s0\<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
schirmer@13688
   224
              normal s0\<Longrightarrow>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
schirmer@13688
   225
              G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1; P Y s0 Z\<rbrakk> \<Longrightarrow> Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
schirmer@13688
   226
  shows "G,A|\<Turnstile>\<Colon>{ {P} \<langle>c\<rangle>\<^sub>s\<succ> {Q} }"
schirmer@13688
   227
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   228
apply (intro allI impI)
schirmer@13688
   229
apply (case_tac "normal s")
schirmer@13688
   230
apply   clarsimp 
schirmer@13688
   231
apply   (rule I,(assumption|simp)+)
schirmer@13688
   232
schirmer@13688
   233
apply   (rule I,auto)
schirmer@12854
   234
done
schirmer@12854
   235
schirmer@13688
   236
lemma valid_stmt_NormalI: 
schirmer@13688
   237
   assumes I: "\<And> n s0 L accC C s1 Y Z.
schirmer@13688
   238
               \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
schirmer@13688
   239
               \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
schirmer@13688
   240
               G\<turnstile>s0 \<midarrow>c\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> \<Longrightarrow> Q \<diamondsuit> s1 Z \<and> s1\<Colon>\<preceq>(G,L)" 
schirmer@13688
   241
  shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>c\<rangle>\<^sub>s\<succ> {Q} }"
schirmer@13688
   242
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   243
apply (intro allI impI)
schirmer@13688
   244
apply (elim exE conjE)
schirmer@13688
   245
apply (rule I)
schirmer@13688
   246
by auto
schirmer@13688
   247
schirmer@13688
   248
lemma valid_var_NormalI: 
schirmer@13688
   249
   assumes I: "\<And> n s0 L accC T C vf s1 Y Z.
schirmer@13688
   250
               \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
schirmer@13688
   251
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>=T;
schirmer@13688
   252
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>v\<guillemotright>C;
schirmer@13688
   253
                G\<turnstile>s0 \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
schirmer@13688
   254
               \<Longrightarrow> Q (In2 vf) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
schirmer@13688
   255
   shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>v\<succ> {Q} }"
schirmer@13688
   256
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   257
apply (intro allI impI)
schirmer@13688
   258
apply (elim exE conjE)
schirmer@13688
   259
apply simp
schirmer@13688
   260
apply (rule I)
schirmer@13688
   261
by auto
schirmer@13688
   262
schirmer@13688
   263
lemma valid_expr_NormalI: 
schirmer@13688
   264
   assumes I: "\<And> n s0 L accC T C v s1 Y Z.
schirmer@13688
   265
               \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
schirmer@13688
   266
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>-T;
schirmer@13688
   267
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>e\<guillemotright>C;
schirmer@13688
   268
                G\<turnstile>s0 \<midarrow>t-\<succ>v\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
schirmer@13688
   269
               \<Longrightarrow> Q (In1 v) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
schirmer@13688
   270
   shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>e\<succ> {Q} }"
schirmer@13688
   271
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   272
apply (intro allI impI)
schirmer@13688
   273
apply (elim exE conjE)
schirmer@13688
   274
apply simp
schirmer@13688
   275
apply (rule I)
schirmer@13688
   276
by auto
schirmer@13688
   277
schirmer@13688
   278
lemma valid_expr_list_NormalI: 
schirmer@13688
   279
   assumes I: "\<And> n s0 L accC T C vs s1 Y Z.
schirmer@13688
   280
               \<lbrakk>\<forall>t\<in>A. G\<Turnstile>n\<Colon>t; s0\<Colon>\<preceq>(G,L); normal s0; 
schirmer@13688
   281
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>\<doteq>T;
schirmer@13688
   282
                \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>t\<rangle>\<^sub>l\<guillemotright>C;
schirmer@13688
   283
                G\<turnstile>s0 \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s1; (Normal P) Y s0 Z\<rbrakk> 
schirmer@13688
   284
                \<Longrightarrow> Q (In3 vs) s1 Z \<and> s1\<Colon>\<preceq>(G,L)"
schirmer@13688
   285
   shows "G,A|\<Turnstile>\<Colon>{ {Normal P} \<langle>t\<rangle>\<^sub>l\<succ> {Q} }"
schirmer@13688
   286
apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   287
apply (intro allI impI)
schirmer@13688
   288
apply (elim exE conjE)
schirmer@13688
   289
apply simp
schirmer@13688
   290
apply (rule I)
schirmer@13688
   291
by auto
schirmer@13688
   292
schirmer@13688
   293
lemma validE [consumes 5]: 
schirmer@13688
   294
  assumes valid: "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
schirmer@13688
   295
   and    P: "P Y s0 Z"
schirmer@13688
   296
   and    valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   297
   and    conf: "s0\<Colon>\<preceq>(G,L)"
schirmer@13688
   298
   and    eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
schirmer@13688
   299
   and    wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
schirmer@13688
   300
   and    da: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>C"
schirmer@13688
   301
   and    elim: "\<lbrakk>Q v s1 Z; s1\<Colon>\<preceq>(G,L)\<rbrakk> \<Longrightarrow> concl" 
schirmer@13688
   302
  shows "concl"
schirmer@13688
   303
using prems
schirmer@13688
   304
by (simp add: ax_valids2_def triple_valid2_def2) fast
schirmer@13688
   305
(* why consumes 5?. If I want to apply this lemma in a context wgere
schirmer@13688
   306
   \<not> normal s0 holds,
schirmer@13688
   307
   I can chain "\<not> normal s0" as fact number 6 and apply the rule with
schirmer@13688
   308
   cases. Auto will then solve premise 6 and 7.
schirmer@13688
   309
*)
schirmer@13688
   310
schirmer@12854
   311
lemma all_empty: "(!x. P) = P"
schirmer@12854
   312
by simp
schirmer@12854
   313
schirmer@12925
   314
corollary evaln_type_sound:
wenzelm@12937
   315
  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
wenzelm@12937
   316
             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
schirmer@13688
   317
             da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and
wenzelm@12937
   318
        conf_s0: "s0\<Colon>\<preceq>(G,L)" and
wenzelm@12937
   319
             wf: "wf_prog G"                         
wenzelm@12937
   320
  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
schirmer@12925
   321
         (error_free s0 = error_free s1)"
schirmer@12925
   322
proof -
schirmer@13688
   323
  from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
schirmer@13688
   324
    by (rule evaln_eval)
schirmer@13688
   325
  from this wt da wf conf_s0 show ?thesis
schirmer@13688
   326
    by (rule eval_type_sound)
schirmer@12925
   327
qed
schirmer@12925
   328
schirmer@13688
   329
corollary dom_locals_evaln_mono_elim [consumes 1]: 
schirmer@13688
   330
  assumes   
schirmer@13688
   331
  evaln: "G\<turnstile> s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
schirmer@13688
   332
    hyps: "\<lbrakk>dom (locals (store s0)) \<subseteq> dom (locals (store s1));
schirmer@13688
   333
           \<And> vv s val. \<lbrakk>v=In2 vv; normal s1\<rbrakk> 
schirmer@13688
   334
                        \<Longrightarrow> dom (locals (store s)) 
schirmer@13688
   335
                             \<subseteq> dom (locals (store ((snd vv) val s)))\<rbrakk> \<Longrightarrow> P"
schirmer@13688
   336
 shows "P"
schirmer@13688
   337
proof -
schirmer@13688
   338
  from evaln have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by (rule evaln_eval)
schirmer@13688
   339
  from this hyps show ?thesis
schirmer@13688
   340
    by (rule dom_locals_eval_mono_elim) rules+
schirmer@13688
   341
qed
schirmer@12854
   342
schirmer@12854
   343
schirmer@12854
   344
schirmer@13688
   345
lemma evaln_no_abrupt: 
schirmer@13688
   346
   "\<And>s s'. \<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s'); normal s'\<rbrakk> \<Longrightarrow> normal s"
schirmer@13688
   347
by (erule evaln_cases,auto)
schirmer@13688
   348
schirmer@13688
   349
declare inj_term_simps [simp]
schirmer@13688
   350
lemma ax_sound2: 
schirmer@13688
   351
  assumes    wf: "wf_prog G" 
schirmer@13688
   352
    and   deriv: "G,A|\<turnstile>ts"
schirmer@13688
   353
  shows "G,A|\<Turnstile>\<Colon>ts"
schirmer@13688
   354
using deriv
schirmer@13688
   355
proof (induct)
schirmer@13688
   356
  case (empty A)
schirmer@13688
   357
  show ?case
schirmer@13688
   358
    by (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   359
next
schirmer@13688
   360
  case (insert A t ts)
schirmer@13688
   361
  have valid_t: "G,A|\<Turnstile>\<Colon>{t}" . 
schirmer@13688
   362
  moreover have valid_ts: "G,A|\<Turnstile>\<Colon>ts" .
schirmer@13688
   363
  {
schirmer@13688
   364
    fix n assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   365
    have "G\<Turnstile>n\<Colon>t" and "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
schirmer@13688
   366
    proof -
schirmer@13688
   367
      from valid_A valid_t show "G\<Turnstile>n\<Colon>t"
schirmer@13688
   368
	by (simp add: ax_valids2_def)
schirmer@13688
   369
    next
schirmer@13688
   370
      from valid_A valid_ts show "\<forall>t\<in>ts. G\<Turnstile>n\<Colon>t"
schirmer@13688
   371
	by (unfold ax_valids2_def) blast
schirmer@13688
   372
    qed
schirmer@13688
   373
    hence "\<forall>t'\<in>insert t ts. G\<Turnstile>n\<Colon>t'"
schirmer@13688
   374
      by simp
schirmer@13688
   375
  }
schirmer@13688
   376
  thus ?case
schirmer@13688
   377
    by (unfold ax_valids2_def) blast
schirmer@13688
   378
next
schirmer@13688
   379
  case (asm A ts)
schirmer@13688
   380
  have "ts \<subseteq> A" .
schirmer@13688
   381
  then show "G,A|\<Turnstile>\<Colon>ts"
schirmer@13688
   382
    by (auto simp add: ax_valids2_def triple_valid2_def)
schirmer@13688
   383
next
schirmer@13688
   384
  case (weaken A ts ts')
schirmer@13688
   385
  have "G,A|\<Turnstile>\<Colon>ts'" .
schirmer@13688
   386
  moreover have "ts \<subseteq> ts'" .
schirmer@13688
   387
  ultimately show "G,A|\<Turnstile>\<Colon>ts"
schirmer@13688
   388
    by (unfold ax_valids2_def triple_valid2_def) blast
schirmer@13688
   389
next
schirmer@13688
   390
  case (conseq A P Q t)
schirmer@13688
   391
  have con: "\<forall>Y s Z. P Y s Z \<longrightarrow> 
schirmer@13688
   392
              (\<exists>P' Q'.
schirmer@13688
   393
                  (G,A\<turnstile>{P'} t\<succ> {Q'} \<and> G,A|\<Turnstile>\<Colon>{ {P'} t\<succ> {Q'} }) \<and>
schirmer@13688
   394
                  (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> Q Y' s' Z))".
schirmer@13688
   395
  show "G,A|\<Turnstile>\<Colon>{ {P} t\<succ> {Q} }"
schirmer@13688
   396
  proof (rule validI)
schirmer@13688
   397
    fix n s0 L accC T C v s1 Y Z
schirmer@13688
   398
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t" 
schirmer@13688
   399
    assume conf: "s0\<Colon>\<preceq>(G,L)"
schirmer@13688
   400
    assume wt: "normal s0 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T"
schirmer@13688
   401
    assume da: "normal s0 
schirmer@13688
   402
                 \<Longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>t\<guillemotright> C"
schirmer@13688
   403
    assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
schirmer@13688
   404
    assume P: "P Y s0 Z"
schirmer@13688
   405
    show "Q v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   406
    proof -
schirmer@13688
   407
      from valid_A conf wt da eval P con
schirmer@13688
   408
      have "Q v s1 Z"
schirmer@13688
   409
	apply (simp add: ax_valids2_def triple_valid2_def2)
schirmer@13688
   410
	apply (tactic "smp_tac 3 1")
schirmer@13688
   411
	apply clarify
schirmer@13688
   412
	apply (tactic "smp_tac 1 1")
schirmer@13688
   413
	apply (erule allE,erule allE, erule mp)
schirmer@13688
   414
	apply (intro strip)
schirmer@13688
   415
	apply (tactic "smp_tac 3 1")
schirmer@13688
   416
	apply (tactic "smp_tac 2 1")
schirmer@13688
   417
	apply (tactic "smp_tac 1 1")
schirmer@13688
   418
	by blast
schirmer@13688
   419
      moreover have "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   420
      proof (cases "normal s0")
schirmer@13688
   421
	case True
schirmer@13688
   422
	from eval wt [OF True] da [OF True] conf wf 
schirmer@13688
   423
	show ?thesis
schirmer@13688
   424
	  by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   425
      next
schirmer@13688
   426
	case False
schirmer@13688
   427
	with eval have "s1=s0"
schirmer@13688
   428
	  by auto
schirmer@13688
   429
	with conf show ?thesis by simp
schirmer@13688
   430
      qed
schirmer@13688
   431
      ultimately show ?thesis ..
schirmer@13688
   432
    qed
schirmer@13688
   433
  qed
schirmer@13688
   434
next
schirmer@13688
   435
  case (hazard A P Q t)
schirmer@13688
   436
  show "G,A|\<Turnstile>\<Colon>{ {P \<and>. Not \<circ> type_ok G t} t\<succ> {Q} }"
schirmer@13688
   437
    by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast
schirmer@13688
   438
next
schirmer@13688
   439
  case (Abrupt A P t)
schirmer@13688
   440
  show "G,A|\<Turnstile>\<Colon>{ {P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
schirmer@13688
   441
  proof (rule validI)
schirmer@13688
   442
    fix n s0 L accC T C v s1 Y Z 
schirmer@13688
   443
    assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   444
    assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
schirmer@13688
   445
    assume "(P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal) Y s0 Z"
schirmer@13688
   446
    then obtain P: "P (arbitrary3 t) s0 Z" and abrupt_s0: "\<not> normal s0"
schirmer@13688
   447
      by simp
schirmer@13688
   448
    from eval abrupt_s0 obtain "s1=s0" and "v=arbitrary3 t"
schirmer@13688
   449
      by auto
schirmer@13688
   450
    with P conf_s0
schirmer@13688
   451
    show "P v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   452
      by simp
schirmer@13688
   453
  qed
schirmer@13688
   454
next
schirmer@13688
   455
  case (LVar A P vn)
schirmer@13688
   456
  show "G,A|\<Turnstile>\<Colon>{ {Normal (\<lambda>s.. P\<leftarrow>In2 (lvar vn s))} LVar vn=\<succ> {P} }"
schirmer@13688
   457
  proof (rule valid_var_NormalI)
schirmer@13688
   458
    fix n s0 L accC T C vf s1 Y Z
schirmer@13688
   459
    assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   460
    assume normal_s0: "normal s0"
schirmer@13688
   461
    assume wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>LVar vn\<Colon>=T"
schirmer@13688
   462
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>LVar vn\<rangle>\<^sub>v\<guillemotright> C"
schirmer@13688
   463
    assume eval: "G\<turnstile>s0 \<midarrow>LVar vn=\<succ>vf\<midarrow>n\<rightarrow> s1" 
schirmer@13688
   464
    assume P: "(Normal (\<lambda>s.. P\<leftarrow>In2 (lvar vn s))) Y s0 Z"
schirmer@13688
   465
    show "P (In2 vf) s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   466
    proof 
schirmer@13688
   467
      from eval normal_s0 obtain "s1=s0" "vf=lvar vn (store s0)"
schirmer@13688
   468
	by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   469
      with P show "P (In2 vf) s1 Z"
schirmer@13688
   470
	by simp
schirmer@13688
   471
    next
schirmer@13688
   472
      from eval wt da conf_s0 wf
schirmer@13688
   473
      show "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   474
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   475
    qed
schirmer@13688
   476
  qed
schirmer@13688
   477
next
schirmer@13688
   478
  case (FVar A statDeclC P Q R accC e fn stat)
schirmer@13688
   479
  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init statDeclC. {Q} }" .
schirmer@13688
   480
  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; R} }" .
schirmer@13688
   481
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC,statDeclC,stat}e..fn=\<succ> {R} }"
schirmer@13688
   482
  proof (rule valid_var_NormalI)
schirmer@13688
   483
    fix n s0 L accC' T V vf s3 Y Z
schirmer@13688
   484
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   485
    assume conf_s0:  "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   486
    assume normal_s0: "normal s0"
schirmer@13688
   487
    assume wt: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>{accC,statDeclC,stat}e..fn\<Colon>=T"
schirmer@13688
   488
    assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
schirmer@13688
   489
                  \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688
   490
    assume eval: "G\<turnstile>s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<midarrow>n\<rightarrow> s3"
schirmer@13688
   491
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   492
    show "R \<lfloor>vf\<rfloor>\<^sub>v s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
schirmer@13688
   493
    proof -
schirmer@13688
   494
      from wt obtain statC f where
schirmer@13688
   495
        wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@13688
   496
        accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
schirmer@13688
   497
	eq_accC: "accC=accC'" and
schirmer@13688
   498
        stat: "stat=is_static f" and
schirmer@13688
   499
	T: "T=(type f)"
schirmer@13688
   500
	by (cases) (auto simp add: member_is_static_simp)
schirmer@13688
   501
      from da eq_accC
schirmer@13688
   502
      have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> V"
schirmer@13688
   503
	by cases simp
schirmer@13688
   504
      from eval obtain a s1 s2 s2' where
schirmer@13688
   505
	eval_init: "G\<turnstile>s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" and 
schirmer@13688
   506
        eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" and 
schirmer@13688
   507
	fvar: "(vf,s2')=fvar statDeclC stat fn a s2" and
schirmer@13688
   508
	s3: "s3 = check_field_access G accC statDeclC fn stat a s2'"
schirmer@13688
   509
	using normal_s0 by (fastsimp elim: evaln_elim_cases) 
schirmer@13688
   510
      have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
schirmer@13688
   511
      proof -
schirmer@13688
   512
	from wf wt_e 
schirmer@13688
   513
	have iscls_statC: "is_class G statC"
schirmer@13688
   514
	  by (auto dest: ty_expr_is_type type_is_class)
schirmer@13688
   515
	with wf accfield 
schirmer@13688
   516
	have iscls_statDeclC: "is_class G statDeclC"
schirmer@13688
   517
	  by (auto dest!: accfield_fields dest: fields_declC)
schirmer@13688
   518
	thus ?thesis by simp
schirmer@13688
   519
      qed
schirmer@13688
   520
      obtain I where 
schirmer@13688
   521
	da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   522
                    \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
schirmer@13688
   523
	by (auto intro: da_Init [simplified] assigned.select_convs)
schirmer@13688
   524
      from valid_init P valid_A conf_s0 eval_init wt_init da_init
schirmer@13688
   525
      obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   526
	by (rule validE)
schirmer@13688
   527
      obtain 
schirmer@13688
   528
	R: "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and 
schirmer@13688
   529
        conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@13688
   530
	conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@13688
   531
      proof (cases "normal s1")
schirmer@13688
   532
	case True
schirmer@13688
   533
	obtain V' where 
schirmer@13688
   534
	  da_e':
schirmer@13688
   535
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> V'"
schirmer@13688
   536
	proof -
schirmer@13688
   537
	  from eval_init 
schirmer@13688
   538
	  have "(dom (locals (store s0))) \<subseteq> (dom (locals (store s1)))"
schirmer@13688
   539
	    by (rule dom_locals_evaln_mono_elim)
schirmer@13688
   540
	  with da_e show ?thesis
schirmer@13688
   541
	    by (rule da_weakenE)
schirmer@13688
   542
	qed
schirmer@13688
   543
	with valid_e Q valid_A conf_s1 eval_e wt_e
schirmer@13688
   544
	obtain "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   545
	  by (rule validE) (simp add: fvar [symmetric])
schirmer@13688
   546
	moreover
schirmer@13688
   547
	from eval_e wt_e da_e' conf_s1 wf
schirmer@13688
   548
	have "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@13688
   549
	  by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   550
	ultimately show ?thesis ..
schirmer@13688
   551
      next
schirmer@13688
   552
	case False
schirmer@13688
   553
	with valid_e Q valid_A conf_s1 eval_e
schirmer@13688
   554
	obtain  "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z" and "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   555
	  by (cases rule: validE) (simp add: fvar [symmetric])+
schirmer@13688
   556
	moreover from False eval_e have "\<not> normal s2"
schirmer@13688
   557
	  by auto
schirmer@13688
   558
	hence "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@13688
   559
	  by auto
schirmer@13688
   560
	ultimately show ?thesis ..
schirmer@13688
   561
      qed
schirmer@13688
   562
      from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat s3 wf
schirmer@13688
   563
      have eq_s3_s2': "s3=s2'"  
schirmer@13688
   564
	using normal_s0 by (auto dest!: error_free_field_access evaln_eval)
schirmer@13688
   565
      moreover
schirmer@13688
   566
      from eval wt da conf_s0 wf
schirmer@13688
   567
      have "s3\<Colon>\<preceq>(G, L)"
schirmer@13688
   568
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   569
      ultimately show ?thesis using Q by simp
schirmer@13688
   570
    qed
schirmer@13688
   571
  qed
schirmer@13690
   572
next
schirmer@13690
   573
-- {* 
schirmer@13690
   574
\par
schirmer@13690
   575
*} (* dummy text command to break paragraph for latex;
schirmer@13690
   576
              large paragraphs exhaust memory of debian pdflatex *)   
schirmer@13688
   577
  case (AVar A P Q R e1 e2)
schirmer@13688
   578
  have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
schirmer@13688
   579
  have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
schirmer@13688
   580
    using AVar.hyps by simp
schirmer@13688
   581
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} e1.[e2]=\<succ> {R} }"
schirmer@13688
   582
  proof (rule valid_var_NormalI)
schirmer@13688
   583
    fix n s0 L accC T V vf s2' Y Z
schirmer@13688
   584
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   585
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   586
    assume normal_s0: "normal s0"
schirmer@13688
   587
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1.[e2]\<Colon>=T"
schirmer@13688
   588
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   589
                  \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1.[e2]\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688
   590
    assume eval: "G\<turnstile>s0 \<midarrow>e1.[e2]=\<succ>vf\<midarrow>n\<rightarrow> s2'"
schirmer@13688
   591
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   592
    show "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z \<and> s2'\<Colon>\<preceq>(G, L)"
schirmer@13688
   593
    proof -
schirmer@13688
   594
      from wt obtain 
schirmer@13688
   595
	wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-T.[]" and
schirmer@13688
   596
        wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" 
schirmer@13688
   597
	by (rule wt_elim_cases) simp
schirmer@13688
   598
      from da obtain E1 where
schirmer@13688
   599
	da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1" and
schirmer@13688
   600
	da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> V"
schirmer@13688
   601
	by (rule da_elim_cases) simp
schirmer@13688
   602
      from eval obtain s1 a i s2 where
schirmer@13688
   603
	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1" and
schirmer@13688
   604
	eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2" and
schirmer@13688
   605
	avar: "avar G i a s2 =(vf, s2')"
schirmer@13688
   606
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   607
      from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
schirmer@13688
   608
      obtain Q: "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   609
	by (rule validE)
schirmer@13688
   610
      from Q have Q': "\<And> v. (Q\<leftarrow>In1 a) v s1 Z"
schirmer@13688
   611
	by simp
schirmer@13688
   612
      have "R \<lfloor>vf\<rfloor>\<^sub>v s2' Z"
schirmer@13688
   613
      proof (cases "normal s1")
schirmer@13688
   614
	case True
schirmer@13688
   615
	obtain V' where 
schirmer@13688
   616
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> V'"
schirmer@13688
   617
	proof -
schirmer@13688
   618
	  from eval_e1  wt_e1 da_e1 wf True
schirmer@13688
   619
	  have "nrm E1 \<subseteq> dom (locals (store s1))"
schirmer@13688
   620
	    by (cases rule: da_good_approx_evalnE) rules
schirmer@13688
   621
	  with da_e2 show ?thesis
schirmer@13688
   622
	    by (rule da_weakenE)
schirmer@13688
   623
	qed
schirmer@13688
   624
	with valid_e2 Q' valid_A conf_s1 eval_e2 wt_e2 
schirmer@13688
   625
	show ?thesis
schirmer@13688
   626
	  by (rule validE) (simp add: avar)
schirmer@13688
   627
      next
schirmer@13688
   628
	case False
schirmer@13688
   629
	with valid_e2 Q' valid_A conf_s1 eval_e2
schirmer@13688
   630
	show ?thesis
schirmer@13688
   631
	  by (cases rule: validE) (simp add: avar)+
schirmer@13688
   632
      qed
schirmer@13688
   633
      moreover
schirmer@13688
   634
      from eval wt da conf_s0 wf
schirmer@13688
   635
      have "s2'\<Colon>\<preceq>(G, L)"
schirmer@13688
   636
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   637
      ultimately show ?thesis ..
schirmer@13688
   638
    qed
schirmer@13688
   639
  qed
schirmer@13688
   640
next
schirmer@13688
   641
  case (NewC A C P Q)
schirmer@13688
   642
  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .Init C. {Alloc G (CInst C) Q} }".
schirmer@13688
   643
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} NewC C-\<succ> {Q} }"
schirmer@13688
   644
  proof (rule valid_expr_NormalI)
schirmer@13688
   645
    fix n s0 L accC T E v s2 Y Z
schirmer@13688
   646
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   647
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   648
    assume normal_s0: "normal s0"
schirmer@13688
   649
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>NewC C\<Colon>-T"
schirmer@13688
   650
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   651
                  \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>NewC C\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   652
    assume eval: "G\<turnstile>s0 \<midarrow>NewC C-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
   653
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   654
    show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   655
    proof -
schirmer@13688
   656
      from wt obtain is_cls_C: "is_class G C" 
schirmer@13688
   657
	by (rule wt_elim_cases) (auto dest: is_acc_classD)
schirmer@13688
   658
      hence wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" 
schirmer@13688
   659
	by auto
schirmer@13688
   660
      obtain I where 
schirmer@13688
   661
	da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>Init C\<rangle>\<^sub>s\<guillemotright> I"
schirmer@13688
   662
	by (auto intro: da_Init [simplified] assigned.select_convs)
schirmer@13688
   663
      from eval obtain s1 a where
schirmer@13688
   664
	eval_init: "G\<turnstile>s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1" and 
schirmer@13688
   665
        alloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" and
schirmer@13688
   666
	v: "v=Addr a"
schirmer@13688
   667
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   668
      from valid_init P valid_A conf_s0 eval_init wt_init da_init
schirmer@13688
   669
      obtain "(Alloc G (CInst C) Q) \<diamondsuit> s1 Z" 
schirmer@13688
   670
	by (rule validE)
schirmer@13688
   671
      with alloc v have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
   672
	by simp
schirmer@13688
   673
      moreover
schirmer@13688
   674
      from eval wt da conf_s0 wf
schirmer@13688
   675
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   676
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   677
      ultimately show ?thesis ..
schirmer@13688
   678
    qed
schirmer@13688
   679
  qed
schirmer@13688
   680
next
schirmer@13688
   681
  case (NewA A P Q R T e)
schirmer@13688
   682
  have valid_init: "G,A|\<Turnstile>\<Colon>{ {Normal P} .init_comp_ty T. {Q} }" .
schirmer@13688
   683
  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Q} e-\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; 
schirmer@13688
   684
                                            Alloc G (Arr T (the_Intg i)) R}}" .
schirmer@13688
   685
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} New T[e]-\<succ> {R} }"
schirmer@13688
   686
  proof (rule valid_expr_NormalI)
schirmer@13688
   687
    fix n s0 L accC arrT E v s3 Y Z
schirmer@13688
   688
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   689
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   690
    assume normal_s0: "normal s0"
schirmer@13688
   691
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>New T[e]\<Colon>-arrT"
schirmer@13688
   692
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>New T[e]\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   693
    assume eval: "G\<turnstile>s0 \<midarrow>New T[e]-\<succ>v\<midarrow>n\<rightarrow> s3"
schirmer@13688
   694
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   695
    show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
schirmer@13688
   696
    proof -
schirmer@13688
   697
      from wt obtain
schirmer@13688
   698
	wt_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and 
schirmer@13688
   699
	wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" 
schirmer@13688
   700
	by (rule wt_elim_cases) (auto intro: wt_init_comp_ty )
schirmer@13688
   701
      from da obtain
schirmer@13688
   702
	da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   703
	by cases simp
schirmer@13688
   704
      from eval obtain s1 i s2 a where
schirmer@13688
   705
	eval_init: "G\<turnstile>s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1" and 
schirmer@13688
   706
        eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n\<rightarrow> s2" and
schirmer@13688
   707
        alloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" and
schirmer@13688
   708
        v: "v=Addr a"
schirmer@13688
   709
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   710
      obtain I where
schirmer@13688
   711
	da_init:
schirmer@13688
   712
	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>init_comp_ty T\<rangle>\<^sub>s\<guillemotright> I"
schirmer@13688
   713
      proof (cases "\<exists>C. T = Class C")
schirmer@13688
   714
	case True
schirmer@13688
   715
	thus ?thesis
schirmer@13688
   716
	  by - (rule that, (auto intro: da_Init [simplified] 
schirmer@13688
   717
                                        assigned.select_convs
schirmer@13688
   718
                              simp add: init_comp_ty_def))
schirmer@13688
   719
	 (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
schirmer@13688
   720
      next
schirmer@13688
   721
	case False
schirmer@13688
   722
	thus ?thesis
schirmer@13688
   723
	  by - (rule that, (auto intro: da_Skip [simplified] 
schirmer@13688
   724
                                      assigned.select_convs
schirmer@13688
   725
                           simp add: init_comp_ty_def))
schirmer@13688
   726
         (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
schirmer@13688
   727
      qed
schirmer@13688
   728
      with valid_init P valid_A conf_s0 eval_init wt_init 
schirmer@13688
   729
      obtain Q: "Q \<diamondsuit> s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   730
	by (rule validE)
schirmer@13688
   731
      obtain E' where
schirmer@13688
   732
       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
schirmer@13688
   733
      proof -
schirmer@13688
   734
	from eval_init 
schirmer@13688
   735
	have "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
schirmer@13688
   736
	  by (rule dom_locals_evaln_mono_elim)
schirmer@13688
   737
	with da_e show ?thesis
schirmer@13688
   738
	  by (rule da_weakenE)
schirmer@13688
   739
      qed
schirmer@13688
   740
      with valid_e Q valid_A conf_s1 eval_e wt_e
schirmer@13688
   741
      have "(\<lambda>Val:i:. abupd (check_neg i) .; 
schirmer@13688
   742
                      Alloc G (Arr T (the_Intg i)) R) \<lfloor>i\<rfloor>\<^sub>e s2 Z"
schirmer@13688
   743
	by (rule validE)
schirmer@13688
   744
      with alloc v have "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
schirmer@13688
   745
	by simp
schirmer@13688
   746
      moreover 
schirmer@13688
   747
      from eval wt da conf_s0 wf
schirmer@13688
   748
      have "s3\<Colon>\<preceq>(G, L)"
schirmer@13688
   749
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   750
      ultimately show ?thesis ..
schirmer@13688
   751
    qed
schirmer@13688
   752
  qed
schirmer@13688
   753
next
schirmer@13688
   754
  case (Cast A P Q T e)
schirmer@13688
   755
  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> 
schirmer@13688
   756
                 {\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
schirmer@13688
   757
                  Q\<leftarrow>In1 v} }" .
schirmer@13688
   758
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} Cast T e-\<succ> {Q} }"
schirmer@13688
   759
  proof (rule valid_expr_NormalI)
schirmer@13688
   760
    fix n s0 L accC castT E v s2 Y Z
schirmer@13688
   761
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   762
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   763
    assume normal_s0: "normal s0"
schirmer@13688
   764
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Cast T e\<Colon>-castT"
schirmer@13688
   765
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>Cast T e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   766
    assume eval: "G\<turnstile>s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
   767
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   768
    show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   769
    proof -
schirmer@13688
   770
      from wt obtain eT where 
schirmer@13688
   771
	wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
schirmer@13688
   772
	by cases simp
schirmer@13688
   773
      from da obtain
schirmer@13688
   774
	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   775
	by cases simp
schirmer@13688
   776
      from eval obtain s1 where
schirmer@13688
   777
	eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1" and
schirmer@13688
   778
        s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits T) ClassCast) s1"
schirmer@13688
   779
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   780
      from valid_e P valid_A conf_s0 eval_e wt_e da_e
schirmer@13688
   781
      have "(\<lambda>Val:v:. \<lambda>s.. abupd (raise_if (\<not> G,s\<turnstile>v fits T) ClassCast) .;
schirmer@13688
   782
                  Q\<leftarrow>In1 v) \<lfloor>v\<rfloor>\<^sub>e s1 Z"
schirmer@13688
   783
	by (rule validE)
schirmer@13688
   784
      with s2 have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
   785
	by simp
schirmer@13688
   786
      moreover
schirmer@13688
   787
      from eval wt da conf_s0 wf
schirmer@13688
   788
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   789
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   790
      ultimately show ?thesis ..
schirmer@13688
   791
    qed
schirmer@13688
   792
  qed
schirmer@13688
   793
next
schirmer@13688
   794
  case (Inst A P Q T e)
schirmer@13688
   795
  assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ>
schirmer@13688
   796
               {\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T))} }"
schirmer@13688
   797
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} e InstOf T-\<succ> {Q} }"
schirmer@13688
   798
  proof (rule valid_expr_NormalI)
schirmer@13688
   799
    fix n s0 L accC instT E v s1 Y Z
schirmer@13688
   800
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   801
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   802
    assume normal_s0: "normal s0"
schirmer@13688
   803
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e InstOf T\<Colon>-instT"
schirmer@13688
   804
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e InstOf T\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   805
    assume eval: "G\<turnstile>s0 \<midarrow>e InstOf T-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   806
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   807
    show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   808
    proof -
schirmer@13688
   809
      from wt obtain eT where 
schirmer@13688
   810
	wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
schirmer@13688
   811
	by cases simp
schirmer@13688
   812
      from da obtain
schirmer@13688
   813
	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   814
	by cases simp
schirmer@13688
   815
      from eval obtain a where
schirmer@13688
   816
	eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
schirmer@13688
   817
        v: "v = Bool (a \<noteq> Null \<and> G,store s1\<turnstile>a fits RefT T)"
schirmer@13688
   818
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   819
      from valid_e P valid_A conf_s0 eval_e wt_e da_e
schirmer@13688
   820
      have "(\<lambda>Val:v:. \<lambda>s.. Q\<leftarrow>In1 (Bool (v \<noteq> Null \<and> G,s\<turnstile>v fits RefT T))) 
schirmer@13688
   821
              \<lfloor>a\<rfloor>\<^sub>e s1 Z"
schirmer@13688
   822
	by (rule validE)
schirmer@13688
   823
      with v have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
schirmer@13688
   824
	by simp
schirmer@13688
   825
      moreover
schirmer@13688
   826
      from eval wt da conf_s0 wf
schirmer@13688
   827
      have "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   828
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   829
      ultimately show ?thesis ..
schirmer@13688
   830
    qed
schirmer@13688
   831
  qed
schirmer@13688
   832
next
schirmer@13688
   833
  case (Lit A P v)
schirmer@13688
   834
  show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>In1 v)} Lit v-\<succ> {P} }"
schirmer@13688
   835
  proof (rule valid_expr_NormalI)
schirmer@13688
   836
    fix n L s0 s1 v'  Y Z
schirmer@13688
   837
    assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   838
    assume normal_s0: " normal s0"
schirmer@13688
   839
    assume eval: "G\<turnstile>s0 \<midarrow>Lit v-\<succ>v'\<midarrow>n\<rightarrow> s1"
schirmer@13688
   840
    assume P: "(Normal (P\<leftarrow>In1 v)) Y s0 Z"
schirmer@13688
   841
    show "P \<lfloor>v'\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   842
    proof -
schirmer@13688
   843
      from eval have "s1=s0" and  "v'=v"
schirmer@13688
   844
	using normal_s0 by (auto elim: evaln_elim_cases)
schirmer@13688
   845
      with P conf_s0 show ?thesis by simp
schirmer@13688
   846
    qed
schirmer@13688
   847
  qed
schirmer@13688
   848
next
schirmer@13688
   849
  case (UnOp A P Q e unop)
schirmer@13688
   850
  assume valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P}e-\<succ>{\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)} }"
schirmer@13688
   851
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} UnOp unop e-\<succ> {Q} }"
schirmer@13688
   852
  proof (rule valid_expr_NormalI)
schirmer@13688
   853
    fix n s0 L accC T E v s1 Y Z
schirmer@13688
   854
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   855
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   856
    assume normal_s0: "normal s0"
schirmer@13688
   857
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>UnOp unop e\<Colon>-T"
schirmer@13688
   858
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>UnOp unop e\<rangle>\<^sub>e\<guillemotright>E"
schirmer@13688
   859
    assume eval: "G\<turnstile>s0 \<midarrow>UnOp unop e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   860
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   861
    show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   862
    proof -
schirmer@13688
   863
      from wt obtain eT where 
schirmer@13688
   864
	wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
schirmer@13688
   865
	by cases simp
schirmer@13688
   866
      from da obtain
schirmer@13688
   867
	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   868
	by cases simp
schirmer@13688
   869
      from eval obtain ve where
schirmer@13688
   870
	eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>ve\<midarrow>n\<rightarrow> s1" and
schirmer@13688
   871
        v: "v = eval_unop unop ve"
schirmer@13688
   872
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   873
      from valid_e P valid_A conf_s0 eval_e wt_e da_e
schirmer@13688
   874
      have "(\<lambda>Val:v:. Q\<leftarrow>In1 (eval_unop unop v)) \<lfloor>ve\<rfloor>\<^sub>e s1 Z"
schirmer@13688
   875
	by (rule validE)
schirmer@13688
   876
      with v have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
schirmer@13688
   877
	by simp
schirmer@13688
   878
      moreover
schirmer@13688
   879
      from eval wt da conf_s0 wf
schirmer@13688
   880
      have "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   881
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   882
      ultimately show ?thesis ..
schirmer@13688
   883
    qed
schirmer@13688
   884
  qed
schirmer@13688
   885
next
schirmer@13690
   886
-- {* 
schirmer@13690
   887
\par
schirmer@13690
   888
*} (* dummy text command to break paragraph for latex;
schirmer@13690
   889
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@13688
   890
  case (BinOp A P Q R binop e1 e2)
schirmer@13688
   891
  assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" 
schirmer@13688
   892
  have valid_e2: "\<And> v1.  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
schirmer@13688
   893
              (if need_second_arg binop v1 then In1l e2 else In1r Skip)\<succ>
schirmer@13688
   894
              {\<lambda>Val:v2:. R\<leftarrow>In1 (eval_binop binop v1 v2)} }"
schirmer@13688
   895
    using BinOp.hyps by simp
schirmer@13688
   896
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} BinOp binop e1 e2-\<succ> {R} }"
schirmer@13688
   897
  proof (rule valid_expr_NormalI)
schirmer@13688
   898
    fix n s0 L accC T E v s2 Y Z
schirmer@13688
   899
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   900
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   901
    assume normal_s0: "normal s0"
schirmer@13688
   902
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>BinOp binop e1 e2\<Colon>-T"
schirmer@13688
   903
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   904
                  \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   905
    assume eval: "G\<turnstile>s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
   906
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
   907
    show "R \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   908
    proof -
schirmer@13688
   909
      from wt obtain e1T e2T where
schirmer@13688
   910
        wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T" and
schirmer@13688
   911
        wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" and
schirmer@13688
   912
	wt_binop: "wt_binop G binop e1T e2T" 
schirmer@13688
   913
	by cases simp
schirmer@13688
   914
      have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
schirmer@13688
   915
	by simp
schirmer@13688
   916
      (*
schirmer@13688
   917
      obtain S where
schirmer@13688
   918
	daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   919
                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
schirmer@13688
   920
	by (auto intro: da_Skip [simplified] assigned.select_convs) *)
schirmer@13688
   921
      from da obtain E1 where
schirmer@13688
   922
	da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
schirmer@13688
   923
	by cases simp+
schirmer@13688
   924
      from eval obtain v1 s1 v2 where
schirmer@13688
   925
	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1" and
schirmer@13688
   926
	eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)
schirmer@13688
   927
                        \<succ>\<midarrow>n\<rightarrow> (\<lfloor>v2\<rfloor>\<^sub>e, s2)" and
schirmer@13688
   928
        v: "v=eval_binop binop v1 v2"
schirmer@13688
   929
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
   930
      from valid_e1 P valid_A conf_s0 eval_e1 wt_e1 da_e1
schirmer@13688
   931
      obtain Q: "Q \<lfloor>v1\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
schirmer@13688
   932
	by (rule validE)
schirmer@13688
   933
      from Q have Q': "\<And> v. (Q\<leftarrow>In1 v1) v s1 Z"
schirmer@13688
   934
	by simp
schirmer@13688
   935
      have "(\<lambda>Val:v2:. R\<leftarrow>In1 (eval_binop binop v1 v2)) \<lfloor>v2\<rfloor>\<^sub>e s2 Z"
schirmer@13688
   936
      proof (cases "normal s1")
schirmer@13688
   937
	case True
schirmer@13688
   938
	from eval_e1 wt_e1 da_e1 conf_s0 wf
schirmer@13688
   939
	have conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" 
schirmer@13688
   940
	  by (rule evaln_type_sound [elim_format]) (insert True,simp)
schirmer@13688
   941
	from eval_e1 
schirmer@13688
   942
	have "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
schirmer@13688
   943
	  by (rule evaln_eval)
schirmer@13688
   944
	from da wt_e1 wt_e2 wt_binop conf_s0 True this conf_v1 wf
schirmer@13688
   945
	obtain E2 where
schirmer@13688
   946
	  da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
schirmer@13688
   947
                   \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
schirmer@13688
   948
	  by (rule da_e2_BinOp [elim_format]) rules
schirmer@13688
   949
	from wt_e2 wt_Skip obtain T2 
schirmer@13688
   950
	  where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   951
                  \<turnstile>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<Colon>T2"
schirmer@13688
   952
	  by (cases "need_second_arg binop v1") auto
schirmer@13688
   953
	note ve=validE [OF valid_e2,OF  Q' valid_A conf_s1 eval_e2 this da_e2]
schirmer@13688
   954
	(* chaining Q', without extra OF causes unification error *)
schirmer@13688
   955
	thus ?thesis
schirmer@13688
   956
	  by (rule ve)
schirmer@13688
   957
      next
schirmer@13688
   958
	case False
schirmer@13688
   959
	note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2]
schirmer@13688
   960
	with False show ?thesis
schirmer@13688
   961
	  by rules
schirmer@13688
   962
      qed
schirmer@13688
   963
      with v have "R \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
   964
	by simp
schirmer@13688
   965
      moreover
schirmer@13688
   966
      from eval wt da conf_s0 wf
schirmer@13688
   967
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   968
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
   969
      ultimately show ?thesis ..
schirmer@13688
   970
    qed
schirmer@13688
   971
  qed
schirmer@13688
   972
next
schirmer@13688
   973
  case (Super A P)
schirmer@13688
   974
  show "G,A|\<Turnstile>\<Colon>{ {Normal (\<lambda>s.. P\<leftarrow>In1 (val_this s))} Super-\<succ> {P} }"
schirmer@13688
   975
  proof (rule valid_expr_NormalI)
schirmer@13688
   976
    fix n L s0 s1 v  Y Z
schirmer@13688
   977
    assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   978
    assume normal_s0: " normal s0"
schirmer@13688
   979
    assume eval: "G\<turnstile>s0 \<midarrow>Super-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
   980
    assume P: "(Normal (\<lambda>s.. P\<leftarrow>In1 (val_this s))) Y s0 Z"
schirmer@13688
   981
    show "P \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   982
    proof -
schirmer@13688
   983
      from eval have "s1=s0" and  "v=val_this (store s0)"
schirmer@13688
   984
	using normal_s0 by (auto elim: evaln_elim_cases)
schirmer@13688
   985
      with P conf_s0 show ?thesis by simp
schirmer@13688
   986
    qed
schirmer@13688
   987
  qed
schirmer@13688
   988
next
schirmer@13688
   989
  case (Acc A P Q var)
schirmer@13688
   990
  have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {\<lambda>Var:(v, f):. Q\<leftarrow>In1 v} }" .
schirmer@13688
   991
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} Acc var-\<succ> {Q} }"
schirmer@13688
   992
  proof (rule valid_expr_NormalI)
schirmer@13688
   993
    fix n s0 L accC T E v s1 Y Z
schirmer@13688
   994
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
   995
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
   996
    assume normal_s0: "normal s0"
schirmer@13688
   997
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>Acc var\<Colon>-T"
schirmer@13688
   998
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>Acc var\<rangle>\<^sub>e\<guillemotright>E"
schirmer@13688
   999
    assume eval: "G\<turnstile>s0 \<midarrow>Acc var-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13688
  1000
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
  1001
    show "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
  1002
    proof -
schirmer@13688
  1003
      from wt obtain 
schirmer@13688
  1004
	wt_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var\<Colon>=T" 
schirmer@13688
  1005
	by cases simp
schirmer@13688
  1006
      from da obtain V where 
schirmer@13688
  1007
	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688
  1008
	by (cases "\<exists> n. var=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
schirmer@13688
  1009
      from eval obtain w upd where
schirmer@13688
  1010
	eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(v, upd)\<midarrow>n\<rightarrow> s1"
schirmer@13688
  1011
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
  1012
      from valid_var P valid_A conf_s0 eval_var wt_var da_var
schirmer@13688
  1013
      have "(\<lambda>Var:(v, f):. Q\<leftarrow>In1 v) \<lfloor>(v, upd)\<rfloor>\<^sub>v s1 Z"
schirmer@13688
  1014
	by (rule validE)
schirmer@13688
  1015
      then have "Q \<lfloor>v\<rfloor>\<^sub>e s1 Z"
schirmer@13688
  1016
	by simp
schirmer@13688
  1017
      moreover
schirmer@13688
  1018
      from eval wt da conf_s0 wf
schirmer@13688
  1019
      have "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
  1020
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
  1021
      ultimately show ?thesis ..
schirmer@13688
  1022
    qed
schirmer@13688
  1023
  qed
schirmer@13688
  1024
next
schirmer@13688
  1025
  case (Ass A P Q R e var)
schirmer@13688
  1026
  have valid_var: "G,A|\<Turnstile>\<Colon>{ {Normal P} var=\<succ> {Q} }" .
schirmer@13688
  1027
  have valid_e: "\<And> vf. 
schirmer@13688
  1028
                  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In2 vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R} }"
schirmer@13688
  1029
    using Ass.hyps by simp
schirmer@13688
  1030
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} var:=e-\<succ> {R} }"
schirmer@13688
  1031
  proof (rule valid_expr_NormalI)
schirmer@13688
  1032
    fix n s0 L accC T E v s3 Y Z
schirmer@13688
  1033
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
  1034
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1035
    assume normal_s0: "normal s0"
schirmer@13688
  1036
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var:=e\<Colon>-T"
schirmer@13688
  1037
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>var:=e\<rangle>\<^sub>e\<guillemotright>E"
schirmer@13688
  1038
    assume eval: "G\<turnstile>s0 \<midarrow>var:=e-\<succ>v\<midarrow>n\<rightarrow> s3"
schirmer@13688
  1039
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
  1040
    show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z \<and> s3\<Colon>\<preceq>(G, L)"
schirmer@13688
  1041
    proof -
schirmer@13688
  1042
      from wt obtain varT  where
schirmer@13688
  1043
	wt_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>var\<Colon>=varT" and
schirmer@13688
  1044
	wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-T" 
schirmer@13688
  1045
	by cases simp
schirmer@13688
  1046
      from eval obtain w upd s1 s2 where
schirmer@13688
  1047
	eval_var: "G\<turnstile>s0 \<midarrow>var=\<succ>(w, upd)\<midarrow>n\<rightarrow> s1" and
schirmer@13688
  1048
        eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s2" and
schirmer@13688
  1049
	s3: "s3=assign upd v s2"
schirmer@13688
  1050
	using normal_s0 by (auto elim: evaln_elim_cases)
schirmer@13688
  1051
      have "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
schirmer@13688
  1052
      proof (cases "\<exists> vn. var = LVar vn")
schirmer@13688
  1053
	case False
schirmer@13688
  1054
	with da obtain V where
schirmer@13688
  1055
	  da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1056
                      \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V" and
schirmer@13688
  1057
	  da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
  1058
	  by cases simp+
schirmer@13688
  1059
	from valid_var P valid_A conf_s0 eval_var wt_var da_var
schirmer@13688
  1060
	obtain Q: "Q \<lfloor>(w,upd)\<rfloor>\<^sub>v s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1061
	  by (rule validE) 
schirmer@13688
  1062
	hence Q': "\<And> v. (Q\<leftarrow>In2 (w,upd)) v s1 Z"
schirmer@13688
  1063
	  by simp
schirmer@13688
  1064
	have "(\<lambda>Val:v:. assign (snd (w,upd)) v .; R) \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
  1065
	proof (cases "normal s1")
schirmer@13688
  1066
	  case True
schirmer@13688
  1067
	  obtain E' where 
schirmer@13688
  1068
	    da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
schirmer@13688
  1069
	  proof -
schirmer@13688
  1070
	    from eval_var wt_var da_var wf True
schirmer@13688
  1071
	    have "nrm V \<subseteq>  dom (locals (store s1))"
schirmer@13688
  1072
	      by (cases rule: da_good_approx_evalnE) rules
schirmer@13688
  1073
	    with da_e show ?thesis
schirmer@13688
  1074
	      by (rule da_weakenE) 
schirmer@13688
  1075
	  qed
schirmer@13688
  1076
	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
schirmer@13688
  1077
	  show ?thesis
schirmer@13688
  1078
	    by (rule ve)
schirmer@13688
  1079
	next
schirmer@13688
  1080
	  case False
schirmer@13688
  1081
	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
schirmer@13688
  1082
	  with False show ?thesis
schirmer@13688
  1083
	    by rules
schirmer@13688
  1084
	qed
schirmer@13688
  1085
	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
schirmer@13688
  1086
	  by simp
schirmer@13688
  1087
      next
schirmer@13688
  1088
	case True
schirmer@13688
  1089
	then obtain vn where 
schirmer@13688
  1090
	  vn: "var = LVar vn" 
schirmer@13688
  1091
	  by auto
schirmer@13688
  1092
	with da obtain E where
schirmer@13688
  1093
	    da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
  1094
	  by cases simp+
schirmer@13688
  1095
	from da.LVar vn obtain  V where
schirmer@13688
  1096
	  da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1097
                      \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>var\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688
  1098
	  by auto
schirmer@13688
  1099
	from valid_var P valid_A conf_s0 eval_var wt_var da_var
schirmer@13688
  1100
	obtain Q: "Q \<lfloor>(w,upd)\<rfloor>\<^sub>v s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1101
	  by (rule validE) 
schirmer@13688
  1102
	hence Q': "\<And> v. (Q\<leftarrow>In2 (w,upd)) v s1 Z"
schirmer@13688
  1103
	  by simp
schirmer@13688
  1104
	have "(\<lambda>Val:v:. assign (snd (w,upd)) v .; R) \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
  1105
	proof (cases "normal s1")
schirmer@13688
  1106
	  case True
schirmer@13688
  1107
	  obtain E' where
schirmer@13688
  1108
	    da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1109
                       \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
schirmer@13688
  1110
	  proof -
schirmer@13688
  1111
	    from eval_var
schirmer@13688
  1112
	    have "dom (locals (store s0)) \<subseteq> dom (locals (store (s1)))"
schirmer@13688
  1113
	      by (rule dom_locals_evaln_mono_elim)
schirmer@13688
  1114
	    with da_e show ?thesis
schirmer@13688
  1115
	      by (rule da_weakenE)
schirmer@13688
  1116
	  qed
schirmer@13688
  1117
	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e wt_e da_e']
schirmer@13688
  1118
	  show ?thesis
schirmer@13688
  1119
	    by (rule ve)
schirmer@13688
  1120
	next
schirmer@13688
  1121
	  case False
schirmer@13688
  1122
	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
schirmer@13688
  1123
	  with False show ?thesis
schirmer@13688
  1124
	    by rules
schirmer@13688
  1125
	qed
schirmer@13688
  1126
	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
schirmer@13688
  1127
	  by simp
schirmer@13688
  1128
      qed
schirmer@13688
  1129
      moreover
schirmer@13688
  1130
      from eval wt da conf_s0 wf
schirmer@13688
  1131
      have "s3\<Colon>\<preceq>(G, L)"
schirmer@13688
  1132
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
  1133
      ultimately show ?thesis ..
schirmer@13688
  1134
    qed
schirmer@13688
  1135
  qed
schirmer@13688
  1136
next
schirmer@13688
  1137
  case (Cond A P P' Q e0 e1 e2)
schirmer@13688
  1138
  have valid_e0: "G,A|\<Turnstile>\<Colon>{ {Normal P} e0-\<succ> {P'} }" .
schirmer@13688
  1139
  have valid_then_else:"\<And> b.  G,A|\<Turnstile>\<Colon>{ {P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q} }"
schirmer@13688
  1140
    using Cond.hyps by simp
schirmer@13688
  1141
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} e0 ? e1 : e2-\<succ> {Q} }"
schirmer@13688
  1142
  proof (rule valid_expr_NormalI)
schirmer@13688
  1143
    fix n s0 L accC T E v s2 Y Z
schirmer@13688
  1144
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
  1145
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1146
    assume normal_s0: "normal s0"
schirmer@13688
  1147
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e0 ? e1 : e2\<Colon>-T"
schirmer@13688
  1148
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>\<langle>e0 ? e1:e2\<rangle>\<^sub>e\<guillemotright>E"
schirmer@13688
  1149
    assume eval: "G\<turnstile>s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
  1150
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
  1151
    show "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z \<and> s2\<Colon>\<preceq>(G, L)"
schirmer@13688
  1152
    proof -
schirmer@13688
  1153
      from wt obtain T1 T2 where
schirmer@13688
  1154
	wt_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
schirmer@13688
  1155
	wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-T1" and
schirmer@13688
  1156
	wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-T2" 
schirmer@13688
  1157
	by cases simp
schirmer@13688
  1158
      from da obtain E0 E1 E2 where
schirmer@13688
  1159
        da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e0\<rangle>\<^sub>e\<guillemotright> E0" and
schirmer@13688
  1160
        da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1161
                 \<turnstile>(dom (locals (store s0)) \<union> assigns_if True e0)\<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1" and
schirmer@13688
  1162
        da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1163
                 \<turnstile>(dom (locals (store s0)) \<union> assigns_if False e0)\<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2"
schirmer@13688
  1164
	by cases simp+
schirmer@13688
  1165
      from eval obtain b s1 where
schirmer@13688
  1166
	eval_e0: "G\<turnstile>s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1" and
schirmer@13688
  1167
        eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@13688
  1168
	using normal_s0 by (fastsimp elim: evaln_elim_cases)
schirmer@13688
  1169
      from valid_e0 P valid_A conf_s0 eval_e0 wt_e0 da_e0
schirmer@13688
  1170
      obtain "P' \<lfloor>b\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1171
	by (rule validE)
schirmer@13688
  1172
      hence P': "\<And> v. (P'\<leftarrow>=(the_Bool b)) v s1 Z"
schirmer@13688
  1173
	by (cases "normal s1") auto
schirmer@13688
  1174
      have "Q \<lfloor>v\<rfloor>\<^sub>e s2 Z"
schirmer@13688
  1175
      proof (cases "normal s1")
schirmer@13688
  1176
	case True
schirmer@13688
  1177
	note normal_s1=this
schirmer@13688
  1178
	from wt_e1 wt_e2 obtain T' where
schirmer@13688
  1179
	  wt_then_else: 
schirmer@13688
  1180
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(if the_Bool b then e1 else e2)\<Colon>-T'"
schirmer@13688
  1181
	  by (cases "the_Bool b") simp+
schirmer@13688
  1182
	have s0_s1: "dom (locals (store s0)) 
schirmer@13688
  1183
                      \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1184
	proof -
schirmer@13688
  1185
	  from eval_e0 
schirmer@13688
  1186
	  have eval_e0': "G\<turnstile>s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
schirmer@13688
  1187
	    by (rule evaln_eval)
schirmer@13688
  1188
	  hence
schirmer@13688
  1189
	    "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
schirmer@13688
  1190
	    by (rule dom_locals_eval_mono_elim)
schirmer@13688
  1191
          moreover
schirmer@13688
  1192
	  from eval_e0' True wt_e0 
schirmer@13688
  1193
	  have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
schirmer@13688
  1194
	    by (rule assigns_if_good_approx') 
schirmer@13688
  1195
	  ultimately show ?thesis by (rule Un_least)
schirmer@13688
  1196
	qed
schirmer@13688
  1197
	obtain E' where
schirmer@13688
  1198
	  da_then_else:
schirmer@13688
  1199
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1200
              \<turnstile>dom (locals (store s1))\<guillemotright>\<langle>if the_Bool b then e1 else e2\<rangle>\<^sub>e\<guillemotright> E'"
schirmer@13688
  1201
	proof (cases "the_Bool b")
schirmer@13688
  1202
	  case True
schirmer@13688
  1203
	  with that da_e1 s0_s1 show ?thesis
schirmer@13688
  1204
	    by simp (erule da_weakenE,auto)
schirmer@13688
  1205
	next
schirmer@13688
  1206
	  case False
schirmer@13688
  1207
	  with that da_e2 s0_s1 show ?thesis
schirmer@13688
  1208
	    by simp (erule da_weakenE,auto)
schirmer@13688
  1209
	qed
schirmer@13688
  1210
	with valid_then_else P' valid_A conf_s1 eval_then_else wt_then_else
schirmer@13688
  1211
	show ?thesis
schirmer@13688
  1212
	  by (rule validE)
schirmer@13688
  1213
      next
schirmer@13688
  1214
	case False
schirmer@13688
  1215
	with valid_then_else P' valid_A conf_s1 eval_then_else
schirmer@13688
  1216
	show ?thesis
schirmer@13688
  1217
	  by (cases rule: validE) rules+
schirmer@13688
  1218
      qed
schirmer@13688
  1219
      moreover
schirmer@13688
  1220
      from eval wt da conf_s0 wf
schirmer@13688
  1221
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
  1222
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
  1223
      ultimately show ?thesis ..
schirmer@13688
  1224
    qed
schirmer@13688
  1225
  qed
schirmer@13688
  1226
next
schirmer@13690
  1227
-- {* 
schirmer@13690
  1228
\par
schirmer@13690
  1229
*} (* dummy text command to break paragraph for latex;
schirmer@13690
  1230
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@13688
  1231
  case (Call A P Q R S accC' args e mn mode pTs' statT)
schirmer@13688
  1232
  have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
schirmer@13688
  1233
  have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
schirmer@13688
  1234
    using Call.hyps by simp
schirmer@13688
  1235
  have valid_methd: "\<And> a vs invC declC l.
schirmer@13688
  1236
        G,A|\<Turnstile>\<Colon>{ {R a\<leftarrow>In3 vs \<and>.
schirmer@13688
  1237
                 (\<lambda>s. declC =
schirmer@13688
  1238
                    invocation_declclass G mode (store s) a statT
schirmer@13688
  1239
                     \<lparr>name = mn, parTs = pTs'\<rparr> \<and>
schirmer@13688
  1240
                    invC = invocation_class mode (store s) a statT \<and>
schirmer@13688
  1241
                    l = locals (store s)) ;.
schirmer@13688
  1242
                 init_lvars G declC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs \<and>.
schirmer@13688
  1243
                 (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
schirmer@13688
  1244
            Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ> {set_lvars l .; S} }"
schirmer@13688
  1245
    using Call.hyps by simp
schirmer@13688
  1246
  show "G,A|\<Turnstile>\<Colon>{ {Normal P} {accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ> {S} }"
schirmer@13688
  1247
  proof (rule valid_expr_NormalI)
schirmer@13688
  1248
    fix n s0 L accC T E v s5 Y Z
schirmer@13688
  1249
    assume valid_A: "\<forall>t\<in>A. G\<Turnstile>n\<Colon>t"
schirmer@13688
  1250
    assume conf_s0: "s0\<Colon>\<preceq>(G,L)"  
schirmer@13688
  1251
    assume normal_s0: "normal s0"
schirmer@13688
  1252
    assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>{accC',statT,mode}e\<cdot>mn( {pTs'}args)\<Colon>-T"
schirmer@13688
  1253
    assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))
schirmer@13688
  1254
                   \<guillemotright>\<langle>{accC',statT,mode}e\<cdot>mn( {pTs'}args)\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
  1255
    assume eval: "G\<turnstile>s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n\<rightarrow> s5"
schirmer@13688
  1256
    assume P: "(Normal P) Y s0 Z"
schirmer@13688
  1257
    show "S \<lfloor>v\<rfloor>\<^sub>e s5 Z \<and> s5\<Colon>\<preceq>(G, L)"
schirmer@13688
  1258
    proof -
schirmer@13688
  1259
      from wt obtain pTs statDeclT statM where
schirmer@13688
  1260
                 wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
schirmer@13688
  1261
              wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
schirmer@13688
  1262
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@13688
  1263
                         = {((statDeclT,statM),pTs')}" and
schirmer@13688
  1264
                 mode: "mode = invmode statM e" and
schirmer@13688
  1265
                    T: "T =(resTy statM)" and
schirmer@13688
  1266
        eq_accC_accC': "accC=accC'"
schirmer@13688
  1267
	by cases fastsimp+
schirmer@13688
  1268
      from da obtain C where
schirmer@13688
  1269
	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s0)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
schirmer@13688
  1270
	da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E" 
schirmer@13688
  1271
	by cases simp
schirmer@13688
  1272
      from eval eq_accC_accC' obtain a s1 vs s2 s3 s3' s4 invDeclC where
schirmer@13688
  1273
	evaln_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1" and
schirmer@13688
  1274
        evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" and
schirmer@13688
  1275
	invDeclC: "invDeclC = invocation_declclass 
schirmer@13688
  1276
                G mode (store s2) a statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
schirmer@13688
  1277
        s3: "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a vs s2" and
schirmer@13688
  1278
        check: "s3' = check_method_access G 
schirmer@13688
  1279
                           accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" and
schirmer@13688
  1280
	evaln_methd:
schirmer@13688
  1281
           "G\<turnstile>s3' \<midarrow>Methd invDeclC  \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" and
schirmer@13688
  1282
        s5: "s5=(set_lvars (locals (store s2))) s4"
schirmer@13688
  1283
	using normal_s0 by (auto elim: evaln_elim_cases)
schirmer@13688
  1284
schirmer@13688
  1285
      from evaln_e
schirmer@13688
  1286
      have eval_e: "G\<turnstile>s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
schirmer@13688
  1287
	by (rule evaln_eval)
schirmer@13688
  1288
      
schirmer@13688
  1289
      from eval_e _ wt_e wf
schirmer@13688
  1290
      have s1_no_return: "abrupt s1 \<noteq> Some (Jump Ret)"
schirmer@13688
  1291
	by (rule eval_expression_no_jump 
schirmer@13688
  1292
                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
schirmer@13688
  1293
	   (insert normal_s0,auto)
schirmer@13688
  1294
schirmer@13688
  1295
      from valid_e P valid_A conf_s0 evaln_e wt_e da_e
schirmer@13688
  1296
      obtain "Q \<lfloor>a\<rfloor>\<^sub>e s1 Z" and conf_s1: "s1\<Colon>\<preceq>(G,L)"
schirmer@13688
  1297
	by (rule validE)
schirmer@13688
  1298
      hence Q: "\<And> v. (Q\<leftarrow>In1 a) v s1 Z"
schirmer@13688
  1299
	by simp
schirmer@13688
  1300
      obtain 
schirmer@13688
  1301
	R: "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" and 
schirmer@13688
  1302
	conf_s2: "s2\<Colon>\<preceq>(G,L)" and 
schirmer@13688
  1303
	s2_no_return: "abrupt s2 \<noteq> Some (Jump Ret)"
schirmer@13688
  1304
      proof (cases "normal s1")
schirmer@13688
  1305
	case True
schirmer@13688
  1306
	obtain E' where 
schirmer@13688
  1307
	  da_args':
schirmer@13688
  1308
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E'"
schirmer@13688
  1309
	proof -
schirmer@13688
  1310
	  from evaln_e wt_e da_e wf True
schirmer@13688
  1311
	  have "nrm C \<subseteq>  dom (locals (store s1))"
schirmer@13688
  1312
	    by (cases rule: da_good_approx_evalnE) rules
schirmer@13688
  1313
	  with da_args show ?thesis
schirmer@13688
  1314
	    by (rule da_weakenE) 
schirmer@13688
  1315
	qed
schirmer@13688
  1316
	with valid_args Q valid_A conf_s1 evaln_args wt_args 
schirmer@13688
  1317
	obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
schirmer@13688
  1318
	  by (rule validE)
schirmer@13688
  1319
	moreover
schirmer@13688
  1320
	from evaln_args
schirmer@13688
  1321
	have e: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
schirmer@13688
  1322
	  by (rule evaln_eval)
schirmer@13688
  1323
	from this s1_no_return wt_args wf
schirmer@13688
  1324
	have "abrupt s2 \<noteq> Some (Jump Ret)"
schirmer@13688
  1325
	  by (rule eval_expression_list_no_jump 
schirmer@13688
  1326
                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified])
schirmer@13688
  1327
	ultimately show ?thesis ..
schirmer@13688
  1328
      next
schirmer@13688
  1329
	case False
schirmer@13688
  1330
	with valid_args Q valid_A conf_s1 evaln_args
schirmer@13688
  1331
	obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
schirmer@13688
  1332
	  by (cases rule: validE) rules+
schirmer@13688
  1333
	moreover
schirmer@13688
  1334
	from False evaln_args have "s2=s1"
schirmer@13688
  1335
	  by auto
schirmer@13688
  1336
	with s1_no_return have "abrupt s2 \<noteq> Some (Jump Ret)"
schirmer@13688
  1337
	  by simp
schirmer@13688
  1338
	ultimately show ?thesis ..
schirmer@13688
  1339
      qed
schirmer@13688
  1340
schirmer@13688
  1341
      obtain invC where
schirmer@13688
  1342
	invC: "invC = invocation_class mode (store s2) a statT"
schirmer@13688
  1343
	by simp
schirmer@13688
  1344
      with s3
schirmer@13688
  1345
      have invC': "invC = (invocation_class mode (store s3) a statT)"
schirmer@13688
  1346
	by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
schirmer@13688
  1347
      obtain l where
schirmer@13688
  1348
	l: "l = locals (store s2)"
schirmer@13688
  1349
	by simp
schirmer@13688
  1350
schirmer@13688
  1351
      from eval wt da conf_s0 wf
schirmer@13688
  1352
      have conf_s5: "s5\<Colon>\<preceq>(G, L)"
schirmer@13688
  1353
	by (rule evaln_type_sound [elim_format]) simp
schirmer@13688
  1354
      let "PROP ?R" = "\<And> v.
schirmer@13688
  1355
             (R a\<leftarrow>In3 vs \<and>.
schirmer@13688
  1356
                 (\<lambda>s. invDeclC = invocation_declclass G mode (store s) a statT
schirmer@13688
  1357
                                  \<lparr>name = mn, parTs = pTs'\<rparr> \<and>
schirmer@13688
  1358
                       invC = invocation_class mode (store s) a statT \<and>
schirmer@13688
  1359
                          l = locals (store s)) ;.
schirmer@13688
  1360
                  init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs \<and>.
schirmer@13688
  1361
                  (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)
schirmer@13688
  1362
               ) v s3' Z"
schirmer@13688
  1363
      {
schirmer@13688
  1364
	assume abrupt_s3: "\<not> normal s3"
schirmer@13688
  1365
	have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
schirmer@13688
  1366
	proof -
schirmer@13688
  1367
	  from abrupt_s3 check have eq_s3'_s3: "s3'=s3"
schirmer@13688
  1368
	    by (auto simp add: check_method_access_def Let_def)
schirmer@13688
  1369
	  with R s3 invDeclC invC l abrupt_s3
schirmer@13688
  1370
	  have R': "PROP ?R"
schirmer@13688
  1371
	    by auto
schirmer@13688
  1372
	  have conf_s3': "s3'\<Colon>\<preceq>(G, empty)"
schirmer@13688
  1373
	   (* we need an arbirary environment (here empty) that s2' conforms to
schirmer@13688
  1374
              to apply validE *)
schirmer@13688
  1375
	  proof -
schirmer@13688
  1376
	    from s2_no_return s3
schirmer@13688
  1377
	    have "abrupt s3 \<noteq> Some (Jump Ret)"
schirmer@13688
  1378
	      by (cases s2) (auto simp add: init_lvars_def2 split: split_if_asm)
schirmer@13688
  1379
	    moreover
schirmer@13688
  1380
	    obtain abr2 str2 where s2: "s2=(abr2,str2)"
schirmer@13688
  1381
	      by (cases s2) simp
schirmer@13688
  1382
	    from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
schirmer@13688
  1383
	      by (auto simp add: init_lvars_def2 split: split_if_asm)
schirmer@13688
  1384
	    ultimately show ?thesis
schirmer@13688
  1385
	      using s3 s2 eq_s3'_s3
schirmer@13688
  1386
	      apply (simp add: init_lvars_def2)
schirmer@13688
  1387
	      apply (rule conforms_set_locals [OF _ wlconf_empty])
schirmer@13688
  1388
	      by auto
schirmer@13688
  1389
	  qed
schirmer@13688
  1390
	  from valid_methd R' valid_A conf_s3' evaln_methd abrupt_s3 eq_s3'_s3
schirmer@13688
  1391
	  have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
schirmer@13688
  1392
	    by (cases rule: validE) simp+
schirmer@13688
  1393
	  with s5 l show ?thesis
schirmer@13688
  1394
	    by simp
schirmer@13688
  1395
	qed
schirmer@13688
  1396
      } note abrupt_s3_lemma = this
schirmer@13688
  1397
schirmer@13688
  1398
      have "S \<lfloor>v\<rfloor>\<^sub>e s5 Z"
schirmer@13688
  1399
      proof (cases "normal s2")
schirmer@13688
  1400
	case False
schirmer@13688
  1401
	with s3 have abrupt_s3: "\<not> normal s3"
schirmer@13688
  1402
	  by (cases s2) (simp add: init_lvars_def2)
schirmer@13688
  1403
	thus ?thesis
schirmer@13688
  1404
	  by (rule abrupt_s3_lemma)
schirmer@13688
  1405
      next
schirmer@13688
  1406
	case True
schirmer@13688
  1407
	note normal_s2 = this
schirmer@13688
  1408
	with evaln_args 
schirmer@13688
  1409
	have normal_s1: "normal s1"
schirmer@13688
  1410
	  by (rule evaln_no_abrupt)
schirmer@13688
  1411
	obtain E' where 
schirmer@13688
  1412
	  da_args':
schirmer@13688
  1413
	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<^sub>l\<guillemotright> E'"
schirmer@13688
  1414
	proof -
schirmer@13688
  1415
	  from evaln_e wt_e da_e wf normal_s1
schirmer@13688
  1416
	  have "nrm C \<subseteq>  dom (locals (store s1))"
schirmer@13688
  1417
	    by (cases rule: da_good_approx_evalnE) rules
schirmer@13688
  1418
	  with da_args show ?thesis
schirmer@13688
  1419
	    by (rule da_weakenE) 
schirmer@13688
  1420
	qed
schirmer@13688
  1421
	from evaln_args
schirmer@13688
  1422
	have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
schirmer@13688
  1423
	  by (rule evaln_eval)
schirmer@13688
  1424
	from evaln_e wt_e da_e conf_s0 wf
schirmer@13688
  1425
	have conf_a: "G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
schirmer@13688
  1426
	  by (rule evaln_type_sound [elim_format]) (insert normal_s1,simp)
schirmer@13688
  1427
	with normal_s1 normal_s2 eval_args 
schirmer@13688
  1428
	have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
schirmer@13688
  1429
	  by (auto dest: eval_gext intro: conf_gext)
schirmer@13688
  1430
	from evaln_args wt_args da_args' conf_s1 wf
schirmer@13688
  1431
	have conf_args: "list_all2 (conf G (store s2)) vs pTs"
schirmer@13688
  1432
	  by (rule evaln_type_sound [elim_format]) (insert normal_s2,simp)
schirmer@13688
  1433
	from statM 
schirmer@13688
  1434
	obtain
schirmer@13688
  1435
	  statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
schirmer@13688
  1436
	  and
schirmer@13688
  1437
	  pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@13688
  1438
	  by (blast dest: max_spec2mheads)
schirmer@13688
  1439
	show ?thesis
schirmer@13688
  1440
	proof (cases "normal s3")
schirmer@13688
  1441
	  case False
schirmer@13688
  1442
	  thus ?thesis
schirmer@13688
  1443
	    by (rule abrupt_s3_lemma)
schirmer@13688
  1444
	next
schirmer@13688
  1445
	  case True
schirmer@13688
  1446
	  note normal_s3 = this
schirmer@13688
  1447
	  with s3 have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
schirmer@13688
  1448
	    by (cases s2) (auto simp add: init_lvars_def2)
schirmer@13688
  1449
	  from conf_s2 conf_a_s2 wf notNull invC
schirmer@13688
  1450
	  have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
schirmer@13688
  1451
	    by (cases s2) (auto intro: DynT_propI)
schirmer@13688
  1452
schirmer@13688
  1453
	  with wt_e statM' invC mode wf 
schirmer@13688
  1454
	  obtain dynM where 
schirmer@13688
  1455
            dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@13688
  1456
            acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
schirmer@13688
  1457
                            in invC dyn_accessible_from accC"
schirmer@13688
  1458
	    by (force dest!: call_access_ok)
schirmer@13688
  1459
	  with invC' check eq_accC_accC'
schirmer@13688
  1460
	  have eq_s3'_s3: "s3'=s3"
schirmer@13688
  1461
	    by (auto simp add: check_method_access_def Let_def)
schirmer@13688
  1462
	  
schirmer@13688
  1463
	  with dynT_prop R s3 invDeclC invC l 
schirmer@13688
  1464
	  have R': "PROP ?R"
schirmer@13688
  1465
	    by auto
schirmer@12854
  1466
schirmer@13688
  1467
	  from dynT_prop wf wt_e statM' mode invC invDeclC dynM
schirmer@13688
  1468
	  obtain 
schirmer@13688
  1469
            dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@13688
  1470
	    wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
schirmer@13688
  1471
	      dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@13688
  1472
            iscls_invDeclC: "is_class G invDeclC" and
schirmer@13688
  1473
	         invDeclC': "invDeclC = declclass dynM" and
schirmer@13688
  1474
	      invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
schirmer@13688
  1475
	     resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
schirmer@13688
  1476
	    is_static_eq: "is_static dynM = is_static statM" and
schirmer@13688
  1477
	    involved_classes_prop:
schirmer@13688
  1478
             "(if invmode statM e = IntVir
schirmer@13688
  1479
               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
schirmer@13688
  1480
               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
schirmer@13688
  1481
                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
schirmer@13688
  1482
                      statDeclT = ClassT invDeclC)"
schirmer@13688
  1483
	    by (cases rule: DynT_mheadsE) simp
schirmer@13688
  1484
	  obtain L' where 
schirmer@13688
  1485
	    L':"L'=(\<lambda> k. 
schirmer@13688
  1486
                    (case k of
schirmer@13688
  1487
                       EName e
schirmer@13688
  1488
                       \<Rightarrow> (case e of 
schirmer@13688
  1489
                             VNam v 
schirmer@13688
  1490
                             \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
schirmer@13688
  1491
                                (pars (mthd dynM)[\<mapsto>]pTs')) v
schirmer@13688
  1492
                           | Res \<Rightarrow> Some (resTy dynM))
schirmer@13688
  1493
                     | This \<Rightarrow> if is_static statM 
schirmer@13688
  1494
                               then None else Some (Class invDeclC)))"
schirmer@13688
  1495
	    by simp
schirmer@13688
  1496
	  from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
schirmer@13688
  1497
            wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
schirmer@13688
  1498
	  have conf_s3: "s3\<Colon>\<preceq>(G,L')"
schirmer@13688
  1499
	    apply - 
schirmer@13688
  1500
               (* FIXME confomrs_init_lvars should be 
schirmer@13688
  1501
                  adjusted to be more directy applicable *)
schirmer@13688
  1502
	    apply (drule conforms_init_lvars [of G invDeclC 
schirmer@13688
  1503
                    "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
schirmer@13688
  1504
                    L statT invC a "(statDeclT,statM)" e])
schirmer@13688
  1505
	    apply (rule wf)
schirmer@13688
  1506
	    apply (rule conf_args)
schirmer@13688
  1507
	    apply (simp add: pTs_widen)
schirmer@13688
  1508
	    apply (cases s2,simp)
schirmer@13688
  1509
	    apply (rule dynM')
schirmer@13688
  1510
	    apply (force dest: ty_expr_is_type)
schirmer@13688
  1511
	    apply (rule invC_widen)
schirmer@13688
  1512
	    apply (force intro: conf_gext dest: eval_gext)
schirmer@13688
  1513
	    apply simp
schirmer@13688
  1514
	    apply simp
schirmer@13688
  1515
	    apply (simp add: invC)
schirmer@13688
  1516
	    apply (simp add: invDeclC)
schirmer@13688
  1517
	    apply (simp add: normal_s2)
schirmer@13688
  1518
	    apply (cases s2, simp add: L' init_lvars_def2 s3
schirmer@13688
  1519
	                     cong add: lname.case_cong ename.case_cong)
schirmer@13688
  1520
	    done
schirmer@13688
  1521
	  with eq_s3'_s3 have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
schirmer@13688
  1522
	  from is_static_eq wf_dynM L'
schirmer@13688
  1523
	  obtain mthdT where
schirmer@13688
  1524
	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
schirmer@13688
  1525
               \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
schirmer@13688
  1526
	    mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
schirmer@13688
  1527
	    by - (drule wf_mdecl_bodyD,
schirmer@13688
  1528
                  auto simp add: callee_lcl_def  
schirmer@13688
  1529
                       cong add: lname.case_cong ename.case_cong)
schirmer@13688
  1530
	  with dynM' iscls_invDeclC invDeclC'
schirmer@13688
  1531
	  have
schirmer@13688
  1532
	    wt_methd:
schirmer@13688
  1533
	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>