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