src/HOL/Bali/AxCompl.thy
author wenzelm
Wed Jun 13 10:43:38 2007 +0200 (2007-06-13)
changeset 23366 a1e61b5c000f
parent 21669 c68717c16013
child 23894 1a4167d761ac
permissions -rw-r--r--
tuned proofs: avoid implicit prems;
wenzelm@12857
     1
(*  Title:      HOL/Bali/AxCompl.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@13688
     3
    Author:     David von Oheimb and Norbert Schirmer
schirmer@12854
     4
*)
schirmer@12854
     5
schirmer@12854
     6
header {*
schirmer@12854
     7
Completeness proof for Axiomatic semantics of Java expressions and statements
schirmer@12854
     8
*}
schirmer@12854
     9
haftmann@16417
    10
theory AxCompl imports AxSem begin
schirmer@12854
    11
schirmer@12854
    12
text {*
schirmer@12854
    13
design issues:
schirmer@12854
    14
\begin{itemize}
schirmer@12854
    15
\item proof structured by Most General Formulas (-> Thomas Kleymann)
schirmer@12854
    16
\end{itemize}
schirmer@12854
    17
*}
schirmer@12925
    18
schirmer@12925
    19
schirmer@12925
    20
schirmer@13688
    21
           
schirmer@12854
    22
section "set of not yet initialzed classes"
schirmer@12854
    23
schirmer@12854
    24
constdefs
schirmer@12854
    25
schirmer@12854
    26
  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
schirmer@12854
    27
 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
schirmer@12854
    28
schirmer@12854
    29
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
schirmer@12854
    30
apply (unfold nyinitcls_def)
schirmer@12854
    31
apply fast
schirmer@12854
    32
done
schirmer@12854
    33
schirmer@12854
    34
lemmas finite_nyinitcls [simp] =
schirmer@12854
    35
   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
schirmer@12854
    36
schirmer@12854
    37
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
schirmer@12854
    38
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
schirmer@12854
    39
done
schirmer@12854
    40
schirmer@12854
    41
lemma nyinitcls_set_locals_cong [simp]: 
schirmer@12854
    42
  "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
schirmer@12854
    43
apply (unfold nyinitcls_def)
schirmer@12854
    44
apply (simp (no_asm))
schirmer@12854
    45
done
schirmer@12854
    46
schirmer@12854
    47
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
schirmer@12854
    48
apply (unfold nyinitcls_def)
schirmer@12854
    49
apply (simp (no_asm))
schirmer@12854
    50
done
schirmer@12854
    51
schirmer@12854
    52
lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
schirmer@12854
    53
apply (unfold nyinitcls_def)
schirmer@12854
    54
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
    55
apply (simp (no_asm))
schirmer@12854
    56
done
schirmer@12854
    57
schirmer@12854
    58
lemma card_nyinitcls_abrupt_congE [elim!]: 
schirmer@12854
    59
        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
schirmer@12854
    60
apply (unfold nyinitcls_def)
schirmer@12854
    61
apply auto
schirmer@12854
    62
done
schirmer@12854
    63
schirmer@12854
    64
lemma nyinitcls_new_xcpt_var [simp]: 
schirmer@12854
    65
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
schirmer@12854
    66
apply (unfold nyinitcls_def)
schirmer@12854
    67
apply (induct_tac "s")
schirmer@12854
    68
apply (simp (no_asm))
schirmer@12854
    69
done
schirmer@12854
    70
schirmer@12854
    71
lemma nyinitcls_init_lvars [simp]: 
schirmer@12854
    72
  "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
schirmer@12854
    73
apply (induct_tac "s")
schirmer@12854
    74
apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
schirmer@12854
    75
done
schirmer@12854
    76
schirmer@12854
    77
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
schirmer@12854
    78
apply (unfold nyinitcls_def)
schirmer@12854
    79
apply fast
schirmer@12854
    80
done
schirmer@12854
    81
schirmer@13688
    82
lemma card_Suc_lemma: 
schirmer@13688
    83
  "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
schirmer@12854
    84
apply clarsimp
schirmer@12854
    85
done
schirmer@12854
    86
schirmer@12854
    87
lemma nyinitcls_le_SucD: 
schirmer@12854
    88
"\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
schirmer@12854
    89
  card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
schirmer@12854
    90
apply (subgoal_tac 
schirmer@12854
    91
        "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
schirmer@12854
    92
apply  clarsimp
berghofe@13601
    93
apply  (erule_tac V="nyinitcls G (x, s) = ?rhs" in thin_rl)
schirmer@12854
    94
apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
schirmer@12854
    95
apply   (auto dest!: not_initedD elim!: 
schirmer@12854
    96
              simp add: nyinitcls_def inited_def split add: split_if_asm)
schirmer@12854
    97
done
schirmer@12854
    98
schirmer@13688
    99
lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
schirmer@13688
   100
by (rule inited_gext)
schirmer@12854
   101
schirmer@12854
   102
lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
schirmer@12854
   103
apply (unfold nyinitcls_def)
schirmer@12854
   104
apply (force dest!: inited_gext')
schirmer@12854
   105
done
schirmer@12854
   106
schirmer@12854
   107
lemma card_nyinitcls_gext: 
schirmer@12854
   108
  "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
schirmer@12854
   109
apply (rule le_trans)
schirmer@12854
   110
apply  (rule card_mono)
schirmer@12854
   111
apply   (rule finite_nyinitcls)
schirmer@12854
   112
apply  (erule nyinitcls_gext)
schirmer@12854
   113
apply assumption
schirmer@12854
   114
done
schirmer@12854
   115
schirmer@12854
   116
schirmer@12854
   117
section "init-le"
schirmer@12854
   118
schirmer@12854
   119
constdefs
schirmer@12854
   120
  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
schirmer@12854
   121
 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
schirmer@12854
   122
  
schirmer@12854
   123
lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
schirmer@12854
   124
apply (unfold init_le_def)
schirmer@12854
   125
apply auto
schirmer@12854
   126
done
schirmer@12854
   127
schirmer@13688
   128
lemma All_init_leD: 
schirmer@13688
   129
 "\<forall>n::nat. G,(A::'a triple set)\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q::'a assn} 
schirmer@13688
   130
  \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
   131
apply (drule spec)
schirmer@12854
   132
apply (erule conseq1)
schirmer@12854
   133
apply clarsimp
schirmer@12854
   134
apply (rule card_nyinitcls_bound)
schirmer@12854
   135
done
schirmer@12854
   136
schirmer@12854
   137
section "Most General Triples and Formulas"
schirmer@12854
   138
schirmer@12854
   139
constdefs
schirmer@12854
   140
schirmer@12854
   141
  remember_init_state :: "state assn"                ("\<doteq>")
schirmer@12854
   142
  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
schirmer@12854
   143
schirmer@12854
   144
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
schirmer@12854
   145
apply (unfold remember_init_state_def)
schirmer@12854
   146
apply (simp (no_asm))
schirmer@12854
   147
done
schirmer@12854
   148
schirmer@12854
   149
consts
schirmer@12854
   150
  
schirmer@12854
   151
  MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
schirmer@12854
   152
  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
schirmer@12854
   153
schirmer@12854
   154
defs
schirmer@12854
   155
  
schirmer@12854
   156
schirmer@12854
   157
  MGF_def:
schirmer@12854
   158
  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
schirmer@12854
   159
schirmer@12854
   160
  MGFn_def:
schirmer@12854
   161
  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
schirmer@12854
   162
schirmer@12854
   163
(* unused *)
schirmer@12925
   164
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   165
apply (unfold MGF_def)
schirmer@12925
   166
apply (simp add:  ax_valids_def triple_valid_def2)
schirmer@12925
   167
apply (auto elim: evaln_eval)
schirmer@12854
   168
done
schirmer@12854
   169
schirmer@12925
   170
schirmer@12854
   171
lemma MGF_res_eq_lemma [simp]: 
schirmer@12854
   172
  "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
schirmer@12854
   173
apply auto
schirmer@12854
   174
done
schirmer@12854
   175
schirmer@12854
   176
lemma MGFn_def2: 
schirmer@12854
   177
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
schirmer@12854
   178
                    t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
schirmer@12854
   179
apply (unfold MGFn_def MGF_def)
schirmer@12854
   180
apply fast
schirmer@12854
   181
done
schirmer@12854
   182
schirmer@13688
   183
lemma MGF_MGFn_iff: 
schirmer@13688
   184
"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
schirmer@12854
   185
apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
schirmer@12854
   186
apply safe
schirmer@12854
   187
apply  (erule_tac [2] All_init_leD)
schirmer@12854
   188
apply (erule conseq1)
schirmer@12854
   189
apply clarsimp
schirmer@12854
   190
done
schirmer@12854
   191
schirmer@12854
   192
lemma MGFnD: 
schirmer@13688
   193
"G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854
   194
 G,A\<turnstile>{(\<lambda>Y' s' s. s' = s           \<and> P s) \<and>. G\<turnstile>init\<le>n}  
schirmer@12854
   195
 t\<succ>  {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}"
schirmer@12854
   196
apply (unfold init_le_def)
schirmer@12854
   197
apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854
   198
apply (erule conseq12)
schirmer@12854
   199
apply clarsimp
schirmer@12854
   200
apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
schirmer@12854
   201
done
schirmer@12854
   202
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
schirmer@12854
   203
schirmer@13688
   204
text {* To derive the most general formula, we can always assume a normal
schirmer@13688
   205
state in the precondition, since abrupt cases can be handled uniformally by
schirmer@13688
   206
the abrupt rule.
schirmer@13688
   207
*}
schirmer@12854
   208
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854
   209
  G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
schirmer@12854
   210
apply (unfold MGF_def)
schirmer@12854
   211
apply (rule ax_Normal_cases)
schirmer@12854
   212
apply  (erule conseq1)
schirmer@12854
   213
apply  clarsimp
schirmer@12854
   214
apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854
   215
apply (clarsimp simp add: Let_def)
schirmer@12854
   216
done
schirmer@12854
   217
schirmer@13688
   218
lemma MGFNormalD: 
schirmer@13688
   219
"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   220
apply (unfold MGF_def)
schirmer@12854
   221
apply (erule conseq1)
schirmer@12854
   222
apply clarsimp
schirmer@12854
   223
done
schirmer@12854
   224
schirmer@13688
   225
text {* Additionally to @{text MGFNormalI}, we also expand the definition of 
schirmer@13688
   226
the most general formula here *} 
schirmer@12854
   227
lemma MGFn_NormalI: 
schirmer@12854
   228
"G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ> 
schirmer@12854
   229
 {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12854
   230
apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854
   231
apply (rule ax_Normal_cases)
schirmer@12854
   232
apply  (erule conseq1)
schirmer@12854
   233
apply  clarsimp
schirmer@12854
   234
apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854
   235
apply (clarsimp simp add: Let_def)
schirmer@12854
   236
done
schirmer@12854
   237
schirmer@13688
   238
text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688
   239
welltyped terms, since all others can be uniformally handled by the hazard
schirmer@13688
   240
rule. *} 
schirmer@12854
   241
lemma MGFn_free_wt: 
schirmer@12854
   242
  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
schirmer@12854
   243
    \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
schirmer@12854
   244
   \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@12854
   245
apply (rule MGFn_NormalI)
schirmer@12854
   246
apply (rule ax_free_wt)
schirmer@12854
   247
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
schirmer@12854
   248
done
schirmer@12854
   249
schirmer@13688
   250
text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688
   251
welltyped terms and assume that the state in the precondition conforms to the
schirmer@13688
   252
environment. All type violations can be uniformally handled by the hazard
schirmer@13688
   253
rule. *} 
schirmer@12925
   254
lemma MGFn_free_wt_NormalConformI: 
schirmer@13688
   255
"(\<forall> T L C . \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T 
schirmer@12925
   256
  \<longrightarrow> G,(A::state triple set)
schirmer@12925
   257
      \<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n) \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))}
schirmer@12925
   258
      t\<succ> 
schirmer@12925
   259
      {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
schirmer@12925
   260
 \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12925
   261
apply (rule MGFn_NormalI)
schirmer@12925
   262
apply (rule ax_no_hazard)
schirmer@12925
   263
apply (rule ax_escape)
schirmer@12925
   264
apply (intro strip)
schirmer@12925
   265
apply (simp only: type_ok_def peek_and_def)
schirmer@12925
   266
apply (erule conjE)+
schirmer@13688
   267
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
schirmer@13688
   268
       erule conjE)
schirmer@12925
   269
apply (drule spec,drule spec, drule spec, drule (1) mp)
schirmer@12925
   270
apply (erule conseq12)
schirmer@12925
   271
apply blast
schirmer@12925
   272
done
schirmer@12925
   273
schirmer@13688
   274
text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688
   275
welltyped terms and assume that the state in the precondition conforms to the
schirmer@13688
   276
environment and that the term is definetly assigned with respect to this state.
schirmer@13688
   277
All type violations can be uniformally handled by the hazard rule. *} 
schirmer@13688
   278
lemma MGFn_free_wt_da_NormalConformI: 
schirmer@13688
   279
"(\<forall> T L C B. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
schirmer@13688
   280
  \<longrightarrow> G,(A::state triple set)
schirmer@13688
   281
      \<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n) \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))
schirmer@13688
   282
        \<and>. (\<lambda> s. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>B)}
schirmer@13688
   283
      t\<succ> 
schirmer@13688
   284
      {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
schirmer@13688
   285
 \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@13688
   286
apply (rule MGFn_NormalI)
schirmer@13688
   287
apply (rule ax_no_hazard)
schirmer@13688
   288
apply (rule ax_escape)
schirmer@13688
   289
apply (intro strip)
schirmer@13688
   290
apply (simp only: type_ok_def peek_and_def)
schirmer@13688
   291
apply (erule conjE)+
schirmer@13688
   292
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
schirmer@13688
   293
       erule conjE)
schirmer@13688
   294
apply (drule spec,drule spec, drule spec,drule spec, drule (1) mp)
schirmer@13688
   295
apply (erule conseq12)
schirmer@13688
   296
apply blast
schirmer@13688
   297
done
schirmer@12854
   298
schirmer@12854
   299
section "main lemmas"
schirmer@12854
   300
schirmer@13688
   301
lemma MGFn_Init: 
schirmer@13688
   302
 assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
schirmer@13688
   303
 shows "G,(A::state triple set)\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   304
proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI)
schirmer@13688
   305
  fix T L accC
schirmer@13688
   306
  assume "\<lparr>prg=G, cls=accC, lcl= L\<rparr>\<turnstile>\<langle>Init C\<rangle>\<^sub>s\<Colon>T"
schirmer@13688
   307
  hence is_cls: "is_class G C"
schirmer@13688
   308
    by cases simp
schirmer@13688
   309
  show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)} 
schirmer@13688
   310
            .Init C.
schirmer@13688
   311
            {\<lambda>Y s' s. G\<turnstile>s \<midarrow>\<langle>Init C\<rangle>\<^sub>s\<succ>\<rightarrow> (Y, s')}"
schirmer@13688
   312
       (is "G,A\<turnstile>{Normal ?P} .Init C. {?R}")
schirmer@13688
   313
  proof (rule ax_cases [where ?C="initd C"])
schirmer@13688
   314
    show "G,A\<turnstile>{Normal ?P  \<and>. initd C} .Init C. {?R}"
schirmer@13688
   315
      by (rule ax_derivs.Done [THEN conseq1]) (fastsimp intro: init_done)
schirmer@13688
   316
  next
schirmer@13688
   317
    have "G,A\<turnstile>{Normal (?P  \<and>. Not \<circ> initd C)} .Init C. {?R}" 
schirmer@13688
   318
    proof (cases n)
schirmer@13688
   319
      case 0
schirmer@13688
   320
      with is_cls
schirmer@13688
   321
      show ?thesis
schirmer@13688
   322
	by - (rule ax_impossible [THEN conseq1],fastsimp dest: nyinitcls_emptyD)
schirmer@13688
   323
    next
schirmer@13688
   324
      case (Suc m)
schirmer@13688
   325
      with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
schirmer@13688
   326
	by simp
schirmer@13688
   327
      from is_cls obtain c where c: "the (class G C) = c"
schirmer@13688
   328
	by auto
schirmer@13688
   329
      let ?Q= "(\<lambda>Y s' (x,s) . 
schirmer@13688
   330
          G\<turnstile> (x,init_class_obj G C s) 
schirmer@13688
   331
             \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s'
schirmer@13688
   332
          \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>m"
schirmer@13688
   333
      from c
schirmer@13688
   334
      show ?thesis
schirmer@13688
   335
      proof (rule ax_derivs.Init [where ?Q="?Q"])
schirmer@13688
   336
	let ?P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s 
schirmer@13688
   337
                           \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>m)" 
schirmer@13688
   338
	show "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
schirmer@13688
   339
                  .(if C = Object then Skip else Init (super c)). 
schirmer@13688
   340
                  {?Q}"
schirmer@13688
   341
	proof (rule conseq1 [where ?P'="?P'"])
schirmer@13688
   342
	  show "G,A\<turnstile>{?P'} .(if C = Object then Skip else Init (super c)). {?Q}"
schirmer@13688
   343
	  proof (cases "C=Object")
schirmer@13688
   344
	    case True
schirmer@13688
   345
	    have "G,A\<turnstile>{?P'} .Skip. {?Q}"
schirmer@13688
   346
	      by (rule ax_derivs.Skip [THEN conseq1])
schirmer@13688
   347
	         (auto simp add: True intro: eval.Skip)
schirmer@13688
   348
            with True show ?thesis 
schirmer@13688
   349
	      by simp
schirmer@13688
   350
	  next
schirmer@13688
   351
	    case False
schirmer@13688
   352
	    from mgf_hyp'
schirmer@13688
   353
	    have "G,A\<turnstile>{?P'} .Init (super c). {?Q}"
schirmer@13688
   354
	      by (rule MGFnD' [THEN conseq12]) (fastsimp simp add: False c)
schirmer@13688
   355
	    with False show ?thesis
schirmer@13688
   356
	      by simp
schirmer@13688
   357
	  qed
schirmer@13688
   358
	next
schirmer@13688
   359
	  from Suc is_cls
schirmer@13688
   360
	  show "Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))
schirmer@13688
   361
                \<Rightarrow> ?P'"
schirmer@13688
   362
	    by (fastsimp elim: nyinitcls_le_SucD)
schirmer@13688
   363
	qed
schirmer@13688
   364
      next
schirmer@13688
   365
	from mgf_hyp'
schirmer@13688
   366
	show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} 
schirmer@13688
   367
                      .init c.
schirmer@13688
   368
                      {set_lvars l .; ?R}"
schirmer@13688
   369
	  apply (rule MGFnD' [THEN conseq12, THEN allI])
schirmer@13688
   370
	  apply (clarsimp simp add: split_paired_all)
schirmer@13688
   371
	  apply (rule eval.Init [OF c])
schirmer@13688
   372
	  apply (insert c)
schirmer@13688
   373
	  apply auto
schirmer@13688
   374
	  done
schirmer@13688
   375
      qed
schirmer@13688
   376
    qed
schirmer@13688
   377
    thus "G,A\<turnstile>{Normal ?P  \<and>. Not \<circ> initd C} .Init C. {?R}"
schirmer@13688
   378
      by clarsimp
schirmer@13688
   379
  qed
schirmer@13688
   380
qed
schirmer@12854
   381
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
schirmer@12854
   382
schirmer@12854
   383
lemma MGFn_Call: 
schirmer@13688
   384
  assumes mgf_methds: 
schirmer@13688
   385
           "\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>(Methd C sig)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   386
  and mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   387
  and mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
schirmer@13688
   388
  and wf: "wf_prog G"
schirmer@13688
   389
  shows "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   390
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
schirmer@13688
   391
  note inj_term_simps [simp]
schirmer@13688
   392
  fix T L accC' E
schirmer@13688
   393
  assume wt: "\<lparr>prg=G,cls=accC',lcl = L\<rparr>\<turnstile>\<langle>({accC,statT,mode}e\<cdot>mn( {pTs'}ps))\<rangle>\<^sub>e\<Colon>T"
schirmer@13688
   394
  then obtain pTs statDeclT statM where
schirmer@13688
   395
                 wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
schirmer@13688
   396
              wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>ps\<Colon>\<doteq>pTs" and
schirmer@13688
   397
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@13688
   398
                         = {((statDeclT,statM),pTs')}" and
schirmer@13688
   399
                 mode: "mode = invmode statM e" and
schirmer@13688
   400
                    T: "T =Inl (resTy statM)" and
schirmer@13688
   401
        eq_accC_accC': "accC=accC'"
schirmer@13688
   402
	by cases fastsimp+
schirmer@13688
   403
  let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@13688
   404
              (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> 
schirmer@13688
   405
                   (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
schirmer@13688
   406
                   \<and> Y = In1 a) \<and> 
schirmer@13688
   407
              (\<exists> P. normal s1
schirmer@13688
   408
                  \<longrightarrow> \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright>P)) 
schirmer@13688
   409
          \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))::state assn"
schirmer@13688
   410
  let ?R="\<lambda>a. ((\<lambda>Y (x2,s2) (x,s) . x = None \<and> 
schirmer@13688
   411
                (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> 
schirmer@13688
   412
                          (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)\<and> 
schirmer@13688
   413
                          Y = \<lfloor>pvs\<rfloor>\<^sub>l \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) 
schirmer@13688
   414
               \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L)))::state assn"
schirmer@12925
   415
schirmer@13688
   416
  show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688
   417
                     (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688
   418
                     (\<lambda>s. \<lparr>prg=G, cls=accC',lcl=L\<rparr> \<turnstile> dom (locals (store s)) 
schirmer@13688
   419
                           \<guillemotright> \<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E))}
schirmer@13688
   420
             {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>
schirmer@13688
   421
             {\<lambda>Y s' s. \<exists>v. Y = \<lfloor>v\<rfloor>\<^sub>e \<and> 
schirmer@13688
   422
                           G\<turnstile>s \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v\<rightarrow> s'}"
schirmer@13688
   423
    (is "G,A\<turnstile>{Normal ?P} {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ> {?S}")
schirmer@13688
   424
  proof (rule ax_derivs.Call [where ?Q="?Q" and ?R="?R"])
schirmer@13688
   425
    from mgf_e
schirmer@13688
   426
    show "G,A\<turnstile>{Normal ?P} e-\<succ> {?Q}"
schirmer@13688
   427
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   428
      fix s0 s1 a
schirmer@13688
   429
      assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   430
      assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> 
schirmer@13688
   431
                     dom (locals s0) \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   432
      assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
schirmer@13688
   433
      show "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
schirmer@13688
   434
            (abrupt s1 = None \<longrightarrow>
schirmer@13688
   435
              (\<exists>P. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P))
schirmer@13688
   436
            \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   437
      proof -
schirmer@13688
   438
	from da obtain C where
schirmer@13688
   439
	  da_e:  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
schirmer@13688
   440
                    dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
schirmer@13688
   441
	  da_ps: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> E" 
schirmer@13688
   442
	  by cases (simp add: eq_accC_accC')
schirmer@13688
   443
	from eval_e conf_s0 wt_e da_e wf
schirmer@13688
   444
	obtain "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT)"
schirmer@13688
   445
	  and  "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   446
	  by (rule eval_type_soundE) simp
schirmer@13688
   447
	moreover
schirmer@13688
   448
	{
schirmer@13688
   449
	  assume normal_s1: "normal s1"
schirmer@13688
   450
	  have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
schirmer@13688
   451
	  proof -
schirmer@13688
   452
	    from eval_e wt_e da_e wf normal_s1
schirmer@13688
   453
	    have "nrm C \<subseteq>  dom (locals (store s1))"
nipkow@17589
   454
	      by (cases rule: da_good_approxE') iprover
schirmer@13688
   455
	    with da_ps show ?thesis
nipkow@17589
   456
	      by (rule da_weakenE) iprover
schirmer@13688
   457
	  qed
schirmer@13688
   458
	}
schirmer@13688
   459
	ultimately show ?thesis
schirmer@13688
   460
	  using eq_accC_accC' by simp
schirmer@13688
   461
      qed
schirmer@13688
   462
    qed
schirmer@13688
   463
  next
schirmer@13688
   464
    show "\<forall>a. G,A\<turnstile>{?Q\<leftarrow>In1 a} ps\<doteq>\<succ> {?R a}" (is "\<forall> a. ?PS a")
schirmer@13688
   465
    proof 
schirmer@13688
   466
      fix a  
schirmer@13688
   467
      show "?PS a"
schirmer@13688
   468
      proof (rule MGFnD' [OF mgf_ps, THEN conseq12],
schirmer@13688
   469
             clarsimp simp add: eq_accC_accC' [symmetric])
schirmer@13688
   470
	fix s0 s1 s2 vs
schirmer@13688
   471
	assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   472
	assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
schirmer@13688
   473
	assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
schirmer@13688
   474
	assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
schirmer@13688
   475
	assume da_ps: "abrupt s1 = None \<longrightarrow> 
schirmer@13688
   476
                       (\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
schirmer@13688
   477
                               dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P)"
schirmer@13688
   478
	show "(\<exists>s1. G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
schirmer@13688
   479
                (abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
schirmer@13688
   480
                G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2) \<and>
schirmer@13688
   481
              s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   482
	proof (cases "normal s1")
schirmer@13688
   483
	  case True
schirmer@13688
   484
	  with da_ps obtain P where
schirmer@13688
   485
	   "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
schirmer@13688
   486
	    by auto
schirmer@13688
   487
	  from eval_ps conf_s1 wt_args this wf
schirmer@13688
   488
	  have "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   489
	    by (rule eval_type_soundE)
schirmer@13688
   490
	  with eval_e conf_a eval_ps 
schirmer@13688
   491
	  show ?thesis 
schirmer@13688
   492
	    by auto
schirmer@13688
   493
	next
schirmer@13688
   494
	  case False
schirmer@13688
   495
	  with eval_ps have "s2=s1" by auto
schirmer@13688
   496
	  with eval_e conf_a eval_ps conf_s1 
schirmer@13688
   497
	  show ?thesis 
schirmer@13688
   498
	    by auto
schirmer@13688
   499
	qed
schirmer@13688
   500
      qed
schirmer@13688
   501
    qed
schirmer@13688
   502
  next
schirmer@13688
   503
    show "\<forall>a vs invC declC l.
schirmer@13688
   504
      G,A\<turnstile>{?R a\<leftarrow>\<lfloor>vs\<rfloor>\<^sub>l \<and>.
schirmer@13688
   505
             (\<lambda>s. declC =
schirmer@13688
   506
                  invocation_declclass G mode (store s) a statT
schirmer@13688
   507
                      \<lparr>name=mn, parTs=pTs'\<rparr> \<and>
schirmer@13688
   508
                  invC = invocation_class mode (store s) a statT \<and>
schirmer@13688
   509
                  l = locals (store s)) ;.
schirmer@13688
   510
             init_lvars G declC \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs \<and>.
schirmer@13688
   511
             (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
schirmer@13688
   512
          Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ> 
schirmer@13688
   513
          {set_lvars l .; ?S}" 
schirmer@13688
   514
      (is "\<forall> a vs invC declC l. ?METHD a vs invC declC l")
schirmer@13688
   515
    proof (intro allI)
schirmer@13688
   516
      fix a vs invC declC l
schirmer@13688
   517
      from mgf_methds [rule_format]
schirmer@13688
   518
      show "?METHD a vs invC declC l"
schirmer@13688
   519
      proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   520
	fix s4 s2 s1::state
schirmer@13688
   521
	fix s0 v
schirmer@13688
   522
	let ?D= "invocation_declclass G mode (store s2) a statT 
schirmer@13688
   523
                    \<lparr>name=mn,parTs=pTs'\<rparr>"
schirmer@13688
   524
	let ?s3= "init_lvars G ?D \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs s2"
schirmer@13688
   525
	assume inv_prop: "abrupt ?s3=None 
schirmer@13688
   526
             \<longrightarrow> G\<turnstile>mode\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
schirmer@13688
   527
	assume conf_s2: "s2\<Colon>\<preceq>(G, L)"
schirmer@13688
   528
	assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
schirmer@13688
   529
	assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
schirmer@13688
   530
	assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
schirmer@13688
   531
	assume eval_mthd: "G\<turnstile>?s3 \<midarrow>Methd ?D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
schirmer@13688
   532
	show "G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v
schirmer@13688
   533
                        \<rightarrow> (set_lvars (locals (store s2))) s4"
schirmer@13688
   534
	proof -
schirmer@13688
   535
	  obtain D where D: "D=?D" by simp
schirmer@13688
   536
	  obtain s3 where s3: "s3=?s3" by simp
schirmer@13688
   537
	  obtain s3' where 
schirmer@13688
   538
	    s3': "s3' = check_method_access G accC statT mode 
schirmer@13688
   539
                           \<lparr>name=mn,parTs=pTs'\<rparr> a s3"
schirmer@13688
   540
	    by simp
schirmer@13688
   541
	  have eq_s3'_s3: "s3'=s3"
schirmer@13688
   542
	  proof -
schirmer@13688
   543
	    from inv_prop s3 mode
schirmer@13688
   544
	    have "normal s3 \<Longrightarrow> 
schirmer@13688
   545
             G\<turnstile>invmode statM e\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
schirmer@13688
   546
	      by auto
schirmer@13688
   547
	    with eval_ps wt_e statM conf_s2 conf_a [rule_format] 
schirmer@13688
   548
	    have "check_method_access G accC statT (invmode statM e)
schirmer@13688
   549
                      \<lparr>name=mn,parTs=pTs'\<rparr> a s3 = s3"
schirmer@13688
   550
	      by (rule error_free_call_access) (auto simp add: s3 mode wf)
schirmer@13688
   551
	    thus ?thesis 
schirmer@13688
   552
	      by (simp add: s3' mode)
schirmer@13688
   553
	  qed
schirmer@13688
   554
	  with eval_mthd D s3
schirmer@13688
   555
	  have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
schirmer@13688
   556
	    by simp
schirmer@13688
   557
	  with eval_e eval_ps D _ s3' 
schirmer@13688
   558
	  show ?thesis
schirmer@13688
   559
	    by (rule eval_Call) (auto simp add: s3 mode D)
schirmer@13688
   560
	qed
schirmer@13688
   561
      qed
schirmer@13688
   562
    qed
schirmer@13688
   563
  qed
schirmer@13688
   564
qed
schirmer@13688
   565
	  	  
schirmer@13688
   566
lemma eval_expression_no_jump':
schirmer@13688
   567
  assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1"
schirmer@13688
   568
  and   no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688
   569
  and      wt: "\<lparr>prg=G, cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T" 
schirmer@13688
   570
  and      wf: "wf_prog G"
schirmer@13688
   571
shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
   572
using eval no_jmp wt wf
schirmer@13688
   573
by - (rule eval_expression_no_jump 
schirmer@13688
   574
            [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
schirmer@12854
   575
schirmer@13688
   576
schirmer@13688
   577
text {* To derive the most general formula for the loop statement, we need to
schirmer@13688
   578
come up with a proper loop invariant, which intuitively states that we are 
schirmer@13688
   579
currently inside the evaluation of the loop. To define such an invariant, we
schirmer@13688
   580
unroll the loop in iterated evaluations of the expression and evaluations of
schirmer@13688
   581
the loop body. *}
schirmer@13688
   582
schirmer@13688
   583
constdefs
schirmer@13688
   584
 unroll:: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set"
schirmer@13688
   585
schirmer@13688
   586
 "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
schirmer@13688
   587
                             G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
schirmer@13688
   588
                             G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
schirmer@13688
   589
schirmer@13688
   590
schirmer@13688
   591
lemma unroll_while:
schirmer@13688
   592
  assumes unroll: "(s, t) \<in> (unroll G l e c)\<^sup>*"
schirmer@13688
   593
  and     eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" 
schirmer@13688
   594
  and     normal_termination: "normal s'  \<longrightarrow> \<not> the_Bool v"
schirmer@13688
   595
  and     wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
schirmer@13688
   596
  and     wf: "wf_prog G" 
schirmer@13688
   597
  shows "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   598
using unroll (* normal_s *)
schirmer@13688
   599
proof (induct rule: converse_rtrancl_induct) 
schirmer@13688
   600
  show "G\<turnstile>t \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   601
  proof (cases "normal t")
schirmer@13688
   602
    case False
schirmer@13688
   603
    with eval_e have "s'=t" by auto
schirmer@13688
   604
    with False show ?thesis by auto
schirmer@13688
   605
  next
schirmer@13688
   606
    case True
schirmer@13688
   607
    note normal_t = this
schirmer@13688
   608
    show ?thesis
schirmer@13688
   609
    proof (cases "normal s'")
schirmer@13688
   610
      case True
schirmer@13688
   611
      with normal_t eval_e normal_termination
schirmer@13688
   612
      show ?thesis
schirmer@13688
   613
	by (auto intro: eval.Loop)
schirmer@13688
   614
    next
schirmer@13688
   615
      case False
schirmer@13688
   616
      note abrupt_s' = this
schirmer@13688
   617
      from eval_e _ wt wf
schirmer@13688
   618
      have no_cont: "abrupt s' \<noteq> Some (Jump (Cont l))"
schirmer@13688
   619
	by (rule eval_expression_no_jump') (insert normal_t,simp)
schirmer@13688
   620
      have
schirmer@13688
   621
	"if the_Bool v 
schirmer@13688
   622
             then (G\<turnstile>s' \<midarrow>c\<rightarrow> s' \<and> 
schirmer@13688
   623
                   G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s')
schirmer@13688
   624
	     else s' = s'"
schirmer@13688
   625
      proof (cases "the_Bool v")
schirmer@13688
   626
	case False thus ?thesis by simp
schirmer@13688
   627
      next
schirmer@13688
   628
	case True
schirmer@13688
   629
	with abrupt_s' have "G\<turnstile>s' \<midarrow>c\<rightarrow> s'" by auto
schirmer@13688
   630
	moreover from abrupt_s' no_cont 
schirmer@13688
   631
	have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
schirmer@13688
   632
	  by (cases s') (simp add: absorb_def split: split_if)
schirmer@13688
   633
	moreover
schirmer@13688
   634
	from no_absorb abrupt_s'
schirmer@13688
   635
	have "G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   636
	  by auto
schirmer@13688
   637
	ultimately show ?thesis
schirmer@13688
   638
	  using True by simp
schirmer@13688
   639
      qed
schirmer@13688
   640
      with eval_e 
schirmer@13688
   641
      show ?thesis
schirmer@13688
   642
	using normal_t by (auto intro: eval.Loop)
schirmer@13688
   643
    qed
schirmer@13688
   644
  qed
schirmer@13688
   645
next
schirmer@13688
   646
  fix s s3
schirmer@13688
   647
  assume unroll: "(s,s3) \<in> unroll G l e c"
schirmer@13688
   648
  assume while: "G\<turnstile>s3 \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   649
  show "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   650
  proof -
schirmer@13688
   651
    from unroll obtain v s1 s2 where
schirmer@13688
   652
      normal_s1: "normal s1" and
schirmer@13688
   653
      eval_e: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1" and
schirmer@13688
   654
      continue: "the_Bool v" and
schirmer@13688
   655
      eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and
schirmer@13688
   656
      s3: "s3=(abupd (absorb (Cont l)) s2)"
schirmer@13688
   657
      by  (unfold unroll_def) fast 
schirmer@13688
   658
    from eval_e normal_s1 have
schirmer@13688
   659
      "normal s"
schirmer@13688
   660
      by (rule eval_no_abrupt_lemma [rule_format])
schirmer@13688
   661
    with while eval_e continue eval_c s3 show ?thesis
schirmer@13688
   662
      by (auto intro!: eval.Loop)
schirmer@13688
   663
  qed
schirmer@13688
   664
qed
schirmer@12854
   665
schirmer@12854
   666
schirmer@13688
   667
ML"Addsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]"
schirmer@13688
   668
  
schirmer@13688
   669
lemma MGFn_Loop:
schirmer@13688
   670
  assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   671
  and     mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   672
  and     wf: "wf_prog G" 
schirmer@13688
   673
shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   674
proof (rule MGFn_free_wt [rule_format],elim exE)
schirmer@13688
   675
  fix T L C
schirmer@13688
   676
  assume wt: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
schirmer@13688
   677
  then obtain eT where
schirmer@13688
   678
    wt_e: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
schirmer@13688
   679
    by cases simp
schirmer@13688
   680
  show ?thesis
schirmer@13688
   681
  proof (rule MGFn_NormalI)
schirmer@13688
   682
    show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)} 
schirmer@13688
   683
              .l\<bullet> While(e) c.
schirmer@13688
   684
              {\<lambda>Y s' s. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(e) c)\<succ>\<rightarrow> (Y, s')}"
schirmer@13688
   685
    proof (rule conseq12 
schirmer@13688
   686
           [where ?P'="(\<lambda> Y s' s. (s,s') \<in> (unroll G l e c)\<^sup>* ) \<and>. G\<turnstile>init\<le>n"
schirmer@13688
   687
             and  ?Q'="((\<lambda> Y s' s. (\<exists> t b. (s,t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688
   688
                          Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688
   689
                        \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>"])
schirmer@13688
   690
      show  "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n} 
schirmer@13688
   691
                  .l\<bullet> While(e) c.
schirmer@13688
   692
                 {((\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688
   693
                                  Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688
   694
                              \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>}"
schirmer@13688
   695
      proof (rule ax_derivs.Loop)
schirmer@13688
   696
	from mfg_e
schirmer@13688
   697
	show "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n} 
schirmer@13688
   698
                   e-\<succ>
schirmer@13688
   699
                  {(\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688
   700
                                     Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688
   701
                   \<and>. G\<turnstile>init\<le>n}"
schirmer@13688
   702
	proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   703
	  fix s Z s' v
schirmer@13688
   704
	  assume "(Z, s) \<in> (unroll G l e c)\<^sup>*"
schirmer@13688
   705
	  moreover
schirmer@13688
   706
	  assume "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s'"
schirmer@13688
   707
	  ultimately
schirmer@13688
   708
	  show "\<exists>t. (Z, t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'"
schirmer@13688
   709
	    by blast
schirmer@13688
   710
	qed
schirmer@13688
   711
      next
schirmer@13688
   712
	from mfg_c
schirmer@13688
   713
	show "G,A\<turnstile>{Normal (((\<lambda>Y s' s. \<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
schirmer@13688
   714
                                       Y = \<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
schirmer@13688
   715
                          \<and>. G\<turnstile>init\<le>n)\<leftarrow>=True)}
schirmer@13688
   716
                  .c.
schirmer@13688
   717
                  {abupd (absorb (Cont l)) .;
schirmer@13688
   718
                   ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n)}"
schirmer@13688
   719
	proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   720
	  fix Z s' s v t
schirmer@13688
   721
	  assume unroll: "(Z, t) \<in> (unroll G l e c)\<^sup>*"
schirmer@13688
   722
	  assume eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> Norm s" 
schirmer@13688
   723
	  assume true: "the_Bool v"
schirmer@13688
   724
	  assume eval_c: "G\<turnstile>Norm s \<midarrow>c\<rightarrow> s'"
schirmer@13688
   725
	  show "(Z, abupd (absorb (Cont l)) s') \<in> (unroll G l e c)\<^sup>*"
schirmer@13688
   726
	  proof -
schirmer@13688
   727
	    note unroll
schirmer@13688
   728
	    also
schirmer@13688
   729
	    from eval_e true eval_c
schirmer@13688
   730
	    have "(t,abupd (absorb (Cont l)) s') \<in> unroll G l e c" 
schirmer@13688
   731
	      by (unfold unroll_def) force
schirmer@13688
   732
	    ultimately show ?thesis ..
schirmer@13688
   733
	  qed
schirmer@13688
   734
	qed
schirmer@13688
   735
      qed
schirmer@13688
   736
    next
schirmer@13688
   737
      show 
schirmer@13688
   738
	"\<forall>Y s Z.
schirmer@13688
   739
         (Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)) Y s Z 
schirmer@13688
   740
         \<longrightarrow> (\<forall>Y' s'.
schirmer@13688
   741
               (\<forall>Y Z'. 
schirmer@13688
   742
                 ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n) Y s Z' 
schirmer@13688
   743
                 \<longrightarrow> (((\<lambda>Y s' s. \<exists>t b. (s,t) \<in> (unroll G l e c)\<^sup>* 
schirmer@13688
   744
                                       \<and> Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
schirmer@13688
   745
                     \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>) Y' s' Z') 
schirmer@13688
   746
               \<longrightarrow> G\<turnstile>Z \<midarrow>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ>\<rightarrow> (Y', s'))"
schirmer@13688
   747
      proof (clarsimp)
schirmer@13688
   748
	fix Y' s' s
schirmer@13688
   749
	assume asm:
schirmer@13688
   750
	  "\<forall>Z'. (Z', Norm s) \<in> (unroll G l e c)\<^sup>* 
schirmer@13688
   751
                 \<longrightarrow> card (nyinitcls G s') \<le> n \<and>
schirmer@13688
   752
                     (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<and>
schirmer@13688
   753
                     (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>"
schirmer@13688
   754
	show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   755
	proof -
schirmer@13688
   756
	  from asm obtain v t where 
schirmer@13688
   757
	    -- {* @{term "Z'"} gets instantiated with @{term "Norm s"} *}  
schirmer@13688
   758
	    unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and
schirmer@13688
   759
            eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and
schirmer@13688
   760
            normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and
schirmer@13688
   761
	     Y': "Y' = \<diamondsuit>"
schirmer@13688
   762
	    by auto
schirmer@13688
   763
	  from unroll eval_e normal_termination wt_e wf
schirmer@13688
   764
	  have "G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688
   765
	    by (rule unroll_while)
schirmer@13688
   766
	  with Y' 
schirmer@13688
   767
	  show ?thesis
schirmer@13688
   768
	    by simp
schirmer@13688
   769
	qed
schirmer@13688
   770
      qed
schirmer@13688
   771
    qed
schirmer@13688
   772
  qed
schirmer@13688
   773
qed
schirmer@12854
   774
schirmer@12925
   775
lemma MGFn_FVar:
schirmer@13688
   776
  fixes A :: "state triple set"
schirmer@13688
   777
 assumes mgf_init: "G,A\<turnstile>{=:n} \<langle>Init statDeclC\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" 
schirmer@13688
   778
  and    mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   779
  and    wf: "wf_prog G"
schirmer@13688
   780
  shows "G,A\<turnstile>{=:n} \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
schirmer@13688
   781
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
schirmer@13688
   782
  note inj_term_simps [simp]
schirmer@13688
   783
  fix T L accC' V
schirmer@13688
   784
  assume wt: "\<lparr>prg = G, cls = accC', lcl = L\<rparr>\<turnstile>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<Colon>T"
schirmer@13688
   785
  then obtain statC f where
schirmer@13688
   786
    wt_e: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@13688
   787
    accfield: "accfield G accC' statC fn = Some (statDeclC,f )" and
schirmer@13688
   788
    eq_accC: "accC=accC'" and
schirmer@13688
   789
    stat: "stat=is_static  f"
schirmer@13688
   790
    by (cases) (auto simp add: member_is_static_simp)
schirmer@13688
   791
  let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@13688
   792
                (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1) \<and>
schirmer@13688
   793
                (\<exists> E. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E))
schirmer@13688
   794
                \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"
schirmer@13688
   795
  show "G,A\<turnstile>{Normal
schirmer@13688
   796
             ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688
   797
              (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688
   798
              (\<lambda>s. \<lparr>prg=G,cls=accC',lcl=L\<rparr>
schirmer@13688
   799
                 \<turnstile> dom (locals (store s)) \<guillemotright> \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V))
schirmer@13688
   800
             } {accC,statDeclC,stat}e..fn=\<succ>
schirmer@13688
   801
             {\<lambda>Y s' s. \<exists>vf. Y = \<lfloor>vf\<rfloor>\<^sub>v \<and> 
schirmer@13688
   802
                        G\<turnstile>s \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<rightarrow> s'}"
schirmer@13688
   803
    (is "G,A\<turnstile>{Normal ?P} {accC,statDeclC,stat}e..fn=\<succ> {?R}")
schirmer@13688
   804
  proof (rule ax_derivs.FVar [where ?Q="?Q" ])
schirmer@13688
   805
    from mgf_init
schirmer@13688
   806
    show "G,A\<turnstile>{Normal ?P} .Init statDeclC. {?Q}"
schirmer@13688
   807
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   808
      fix s s'
schirmer@13688
   809
      assume conf_s: "Norm s\<Colon>\<preceq>(G, L)"
schirmer@13688
   810
      assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
schirmer@13688
   811
                    \<turnstile> dom (locals s) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688
   812
      assume eval_init: "G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s'"
schirmer@13688
   813
      show "(\<exists>E. \<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E) \<and>
schirmer@13688
   814
            s'\<Colon>\<preceq>(G, L)"
schirmer@13688
   815
      proof -
schirmer@13688
   816
	from da 
schirmer@13688
   817
	obtain E where
schirmer@13688
   818
	  "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals s) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   819
	  by cases simp
schirmer@13688
   820
	moreover
schirmer@13688
   821
	from eval_init
schirmer@13688
   822
	have "dom (locals s) \<subseteq> dom (locals (store s'))"
schirmer@13688
   823
	  by (rule dom_locals_eval_mono [elim_format]) simp
schirmer@13688
   824
	ultimately obtain E' where
schirmer@13688
   825
	  "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
schirmer@13688
   826
	  by (rule da_weakenE)
schirmer@13688
   827
	moreover
schirmer@13688
   828
	have "s'\<Colon>\<preceq>(G, L)"
schirmer@13688
   829
	proof -
schirmer@13688
   830
	  have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
schirmer@13688
   831
	  proof -
schirmer@13688
   832
	    from wf wt_e 
schirmer@13688
   833
	    have iscls_statC: "is_class G statC"
schirmer@13688
   834
	      by (auto dest: ty_expr_is_type type_is_class)
schirmer@13688
   835
	    with wf accfield 
schirmer@13688
   836
	    have iscls_statDeclC: "is_class G statDeclC"
schirmer@13688
   837
	      by (auto dest!: accfield_fields dest: fields_declC)
schirmer@13688
   838
	    thus ?thesis by simp
schirmer@13688
   839
	  qed
schirmer@13688
   840
	  obtain I where 
schirmer@13688
   841
	    da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
   842
               \<turnstile> dom (locals (store ((Norm s)::state))) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
schirmer@13688
   843
	    by (auto intro: da_Init [simplified] assigned.select_convs)
schirmer@13688
   844
	  from eval_init conf_s wt_init da_init  wf
schirmer@13688
   845
	  show ?thesis
schirmer@13688
   846
	    by (rule eval_type_soundE)
schirmer@13688
   847
	qed
nipkow@17589
   848
	ultimately show ?thesis by iprover
schirmer@13688
   849
      qed
schirmer@13688
   850
    qed
schirmer@13688
   851
  next
schirmer@13688
   852
    from mgf_e
schirmer@13688
   853
    show "G,A\<turnstile>{?Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; ?R}"
schirmer@13688
   854
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   855
      fix s0 s1 s2 E a
schirmer@13688
   856
      let ?fvar = "fvar statDeclC stat fn a s2"
schirmer@13688
   857
      assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
schirmer@13688
   858
      assume eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
schirmer@13688
   859
      assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688
   860
      assume da_e: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
   861
      show "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>fst ?fvar\<rightarrow> snd ?fvar"
schirmer@13688
   862
      proof -
schirmer@13688
   863
	obtain v s2' where
schirmer@13688
   864
	  v: "v=fst ?fvar" and s2': "s2'=snd ?fvar"
schirmer@13688
   865
	  by simp
schirmer@13688
   866
	obtain s3 where
schirmer@13688
   867
	  s3: "s3= check_field_access G accC' statDeclC fn stat a s2'"
schirmer@13688
   868
	  by simp
schirmer@13688
   869
	have eq_s3_s2': "s3=s2'"
schirmer@13688
   870
	proof -
schirmer@13688
   871
	  from eval_e conf_s1 wt_e da_e wf obtain
schirmer@13688
   872
	    conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
schirmer@13688
   873
	    conf_a: "normal s2 \<Longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@13688
   874
	    by (rule eval_type_soundE) simp
schirmer@13688
   875
	  from accfield wt_e eval_init eval_e conf_s2 conf_a _ wf
schirmer@13688
   876
	  show ?thesis
schirmer@13688
   877
	    by (rule  error_free_field_access 
schirmer@13688
   878
                      [where ?v=v and ?s2'=s2',elim_format])
schirmer@13688
   879
	       (simp add: s3 v s2' stat)+
schirmer@13688
   880
        qed
schirmer@13688
   881
	from eval_init eval_e 
schirmer@13688
   882
	show ?thesis
schirmer@13688
   883
	  apply (rule eval.FVar [where ?s2'=s2'])
schirmer@13688
   884
	  apply  (simp add: s2')
schirmer@13688
   885
	  apply  (simp add: s3 [symmetric]   eq_s3_s2' eq_accC s2' [symmetric])
schirmer@13688
   886
	  done
schirmer@13688
   887
      qed
schirmer@13688
   888
    qed
schirmer@13688
   889
  qed
schirmer@13688
   890
qed
schirmer@12925
   891
schirmer@13337
   892
schirmer@13688
   893
lemma MGFn_Fin:
schirmer@13688
   894
  assumes wf: "wf_prog G" 
schirmer@13688
   895
  and     mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   896
  and     mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   897
  shows "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   898
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
schirmer@13688
   899
  fix T L accC C 
schirmer@13688
   900
  assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T"
schirmer@13688
   901
  then obtain
schirmer@13688
   902
    wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@13688
   903
    wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@13688
   904
    by cases simp
schirmer@13688
   905
  let  ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>c1\<rightarrow> s' \<and> 
schirmer@13688
   906
               (\<exists> C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1)
schirmer@13688
   907
               \<and> s\<Colon>\<preceq>(G, L)) 
schirmer@13688
   908
             \<and>. G\<turnstile>init\<le>n"
schirmer@13688
   909
  show "G,A\<turnstile>{Normal
schirmer@13688
   910
              ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688
   911
              (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688
   912
              (\<lambda>s. \<lparr>prg=G,cls=accC,lcl =L\<rparr>  
schirmer@13688
   913
                     \<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C))}
schirmer@13688
   914
             .c1 Finally c2. 
schirmer@13688
   915
             {\<lambda>Y s' s. Y = \<diamondsuit> \<and> G\<turnstile>s \<midarrow>c1 Finally c2\<rightarrow> s'}"
schirmer@13688
   916
    (is "G,A\<turnstile>{Normal ?P} .c1 Finally c2. {?R}")
schirmer@13688
   917
  proof (rule ax_derivs.Fin [where ?Q="?Q"])
schirmer@13688
   918
    from mgf_c1
schirmer@13688
   919
    show "G,A\<turnstile>{Normal ?P} .c1. {?Q}"
schirmer@13688
   920
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
   921
      fix s0
schirmer@13688
   922
      assume "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C"
schirmer@13688
   923
      thus "\<exists>C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
schirmer@13688
   924
	by cases (auto simp add: inj_term_simps)
schirmer@13688
   925
    qed
schirmer@13688
   926
  next
schirmer@13688
   927
    from mgf_c2
schirmer@13688
   928
    show "\<forall>abr. G,A\<turnstile>{?Q \<and>. (\<lambda>s. abr = abrupt s) ;. abupd (\<lambda>abr. None)} .c2.
schirmer@13688
   929
          {abupd (abrupt_if (abr \<noteq> None) abr) .; ?R}"
schirmer@13688
   930
    proof (rule MGFnD' [THEN conseq12, THEN allI],clarsimp)
schirmer@13688
   931
      fix s0 s1 s2 C1
schirmer@13688
   932
      assume da_c1:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
schirmer@13688
   933
      assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
schirmer@13688
   934
      assume eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
schirmer@13688
   935
      assume eval_c2: "G\<turnstile>abupd (\<lambda>abr. None) s1 \<midarrow>c2\<rightarrow> s2"
schirmer@13688
   936
      show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2
schirmer@13688
   937
               \<rightarrow> abupd (abrupt_if (\<exists>y. abrupt s1 = Some y) (abrupt s1)) s2"
schirmer@13688
   938
      proof -
schirmer@13688
   939
	obtain abr1 str1 where s1: "s1=(abr1,str1)"
wenzelm@23366
   940
	  by (cases s1)
schirmer@13688
   941
	with eval_c1 eval_c2 obtain
schirmer@13688
   942
	  eval_c1': "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (abr1,str1)" and
schirmer@13688
   943
	  eval_c2': "G\<turnstile>Norm str1 \<midarrow>c2\<rightarrow> s2"
schirmer@13688
   944
	  by simp
schirmer@13688
   945
	obtain s3 where 
schirmer@13688
   946
	  s3: "s3 = (if \<exists>err. abr1 = Some (Error err) 
schirmer@13688
   947
	                then (abr1, str1)
schirmer@13688
   948
                        else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
schirmer@13688
   949
	  by simp
schirmer@13688
   950
	from eval_c1' conf_s0 wt_c1 _ wf 
schirmer@13688
   951
	have "error_free (abr1,str1)"
schirmer@13688
   952
	  by (rule eval_type_soundE) (insert da_c1,auto)
schirmer@13688
   953
	with s3 have eq_s3: "s3=abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
schirmer@13688
   954
	  by (simp add: error_free_def)
schirmer@13688
   955
	from eval_c1' eval_c2' s3
schirmer@13688
   956
	show ?thesis
schirmer@13688
   957
	  by (rule eval.Fin [elim_format]) (simp add: s1 eq_s3)
schirmer@13688
   958
      qed
schirmer@13688
   959
    qed 
schirmer@13688
   960
  qed
schirmer@13688
   961
qed
schirmer@13688
   962
      
schirmer@13688
   963
lemma Body_no_break:
schirmer@13688
   964
 assumes eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" 
schirmer@13688
   965
   and      eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" 
schirmer@13688
   966
   and       jmpOk: "jumpNestingOkS {Ret} c"
schirmer@13688
   967
   and        wt_c: "\<lparr>prg=G, cls=C, lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@13688
   968
   and        clsD: "class G D=Some d"
schirmer@13688
   969
   and          wf: "wf_prog G" 
schirmer@13688
   970
  shows "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l)) \<and> 
schirmer@13688
   971
              abrupt s2 \<noteq> Some (Jump (Cont l))"
schirmer@13688
   972
proof
schirmer@13688
   973
  fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<and>  
schirmer@13688
   974
              abrupt s2 \<noteq> Some (Jump (Cont l))"
schirmer@13688
   975
  proof -
schirmer@13688
   976
    from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
schirmer@13688
   977
      by auto
schirmer@13688
   978
    from eval_init wf
schirmer@13688
   979
    have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688
   980
      by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
schirmer@13688
   981
    from eval_c _ wt_c wf
schirmer@13688
   982
    show ?thesis
schirmer@13688
   983
      apply (rule jumpNestingOk_eval [THEN conjE, elim_format])
schirmer@13688
   984
      using jmpOk s1_no_jmp
schirmer@13688
   985
      apply auto
schirmer@13688
   986
      done
schirmer@13688
   987
  qed
schirmer@13688
   988
qed
schirmer@12854
   989
schirmer@13688
   990
lemma MGFn_Body:
schirmer@13688
   991
  assumes wf: "wf_prog G"
schirmer@13688
   992
  and     mgf_init: "G,A\<turnstile>{=:n} \<langle>Init D\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   993
  and     mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
   994
  shows  "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
   995
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
schirmer@13688
   996
  fix T L accC E
schirmer@13688
   997
  assume wt: "\<lparr>prg=G, cls=accC,lcl=L\<rparr>\<turnstile>\<langle>Body D c\<rangle>\<^sub>e\<Colon>T"
schirmer@13688
   998
  let ?Q="(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init D\<rightarrow> s' \<and> jumpNestingOkS {Ret} c) 
schirmer@13688
   999
          \<and>. G\<turnstile>init\<le>n" 
schirmer@13688
  1000
  show "G,A\<turnstile>{Normal
schirmer@13688
  1001
               ((\<lambda>Y' s' s. s' = s \<and> fst s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688
  1002
                (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688
  1003
                (\<lambda>s. \<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688
  1004
                       \<turnstile> dom (locals (store s)) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E))}
schirmer@13688
  1005
             Body D c-\<succ> 
schirmer@13688
  1006
             {\<lambda>Y s' s. \<exists>v. Y = In1 v \<and> G\<turnstile>s \<midarrow>Body D c-\<succ>v\<rightarrow> s'}"
schirmer@13688
  1007
    (is "G,A\<turnstile>{Normal ?P} Body D c-\<succ> {?R}")
schirmer@13688
  1008
  proof (rule ax_derivs.Body [where ?Q="?Q"])
schirmer@13688
  1009
    from mgf_init
schirmer@13688
  1010
    show "G,A\<turnstile>{Normal ?P} .Init D. {?Q}"
schirmer@13688
  1011
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
  1012
      fix s0
schirmer@13688
  1013
      assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688
  1014
      thus "jumpNestingOkS {Ret} c"
schirmer@13688
  1015
	by cases simp
schirmer@13688
  1016
    qed
schirmer@13688
  1017
  next
schirmer@13688
  1018
    from mgf_c
schirmer@13688
  1019
    show "G,A\<turnstile>{?Q}.c.{\<lambda>s.. abupd (absorb Ret) .; ?R\<leftarrow>\<lfloor>the (locals s Result)\<rfloor>\<^sub>e}"
schirmer@13688
  1020
    proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688
  1021
      fix s0 s1 s2
schirmer@13688
  1022
      assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1"
schirmer@13688
  1023
      assume eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
schirmer@13688
  1024
      assume nestingOk: "jumpNestingOkS {Ret} c"
schirmer@13688
  1025
      show "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
schirmer@13688
  1026
              \<rightarrow> abupd (absorb Ret) s2"
schirmer@13688
  1027
      proof -
schirmer@13688
  1028
	from wt obtain d where 
schirmer@13688
  1029
          d: "class G D=Some d" and
schirmer@13688
  1030
          wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@13688
  1031
	  by cases auto
schirmer@13688
  1032
	obtain s3 where 
schirmer@13688
  1033
	  s3: "s3= (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
schirmer@13688
  1034
                           fst s2 = Some (Jump (Cont l))
schirmer@13688
  1035
                       then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
schirmer@13688
  1036
                       else s2)"
schirmer@13688
  1037
	  by simp
schirmer@13688
  1038
	from eval_init eval_c nestingOk wt_c d wf
schirmer@13688
  1039
	have eq_s3_s2: "s3=s2"
schirmer@13688
  1040
	  by (rule Body_no_break [elim_format]) (simp add: s3)
schirmer@13688
  1041
	from eval_init eval_c s3
schirmer@13688
  1042
	show ?thesis
schirmer@13688
  1043
	  by (rule eval.Body [elim_format]) (simp add: eq_s3_s2)
schirmer@13688
  1044
      qed
schirmer@13688
  1045
    qed
schirmer@13688
  1046
  qed
schirmer@13688
  1047
qed
schirmer@13337
  1048
schirmer@13688
  1049
lemma MGFn_lemma:
schirmer@13688
  1050
  assumes mgf_methds: 
schirmer@13688
  1051
           "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1052
  and wf: "wf_prog G"
schirmer@13688
  1053
  shows "\<And> t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@13688
  1054
proof (induct rule: full_nat_induct)
schirmer@13688
  1055
  fix n t
schirmer@13688
  1056
  assume hyp: "\<forall> m. Suc m \<le> n \<longrightarrow> (\<forall> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
schirmer@13688
  1057
  show "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@13688
  1058
  proof -
schirmer@13688
  1059
  { 
schirmer@13688
  1060
    fix v e c es
schirmer@13688
  1061
    have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" and 
schirmer@13688
  1062
      "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
schirmer@13688
  1063
      "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and  
schirmer@13688
  1064
      "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
wenzelm@18459
  1065
    proof (induct rule: var_expr_stmt.inducts)
schirmer@13688
  1066
      case (LVar v)
schirmer@13688
  1067
      show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
schirmer@13688
  1068
	apply (rule MGFn_NormalI)
schirmer@13688
  1069
	apply (rule ax_derivs.LVar [THEN conseq1])
schirmer@13688
  1070
	apply (clarsimp)
schirmer@13688
  1071
	apply (rule eval.LVar)
schirmer@13688
  1072
	done
schirmer@13688
  1073
    next
schirmer@13688
  1074
      case (FVar accC statDeclC stat e fn)
wenzelm@23366
  1075
      from MGFn_Init [OF hyp] and `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}` and wf
schirmer@13688
  1076
      show ?case
schirmer@13688
  1077
	by (rule MGFn_FVar)
schirmer@13688
  1078
    next
schirmer@13688
  1079
      case (AVar e1 e2)
wenzelm@23366
  1080
      note mgf_e1 = `G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366
  1081
      note mgf_e2 = `G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
schirmer@13688
  1082
      show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
schirmer@13688
  1083
	apply (rule MGFn_NormalI)
schirmer@13688
  1084
	apply (rule ax_derivs.AVar)
schirmer@13688
  1085
	apply  (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
schirmer@13688
  1086
	apply (rule allI)
schirmer@13688
  1087
	apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
schirmer@13688
  1088
	apply (fastsimp intro: eval.AVar)
schirmer@13688
  1089
	done
schirmer@13688
  1090
    next
schirmer@13688
  1091
      case (InsInitV c v)
schirmer@13688
  1092
      show ?case
schirmer@13688
  1093
	by (rule MGFn_NormalI) (rule ax_derivs.InsInitV)
schirmer@13688
  1094
    next
schirmer@13688
  1095
      case (NewC C)
schirmer@13688
  1096
      show ?case
schirmer@13688
  1097
	apply (rule MGFn_NormalI)
schirmer@13688
  1098
	apply (rule ax_derivs.NewC)
schirmer@13688
  1099
	apply (rule MGFn_InitD [OF hyp, THEN conseq2])
schirmer@13688
  1100
	apply (fastsimp intro: eval.NewC)
schirmer@13688
  1101
	done
schirmer@13688
  1102
    next
schirmer@13688
  1103
      case (NewA T e)
schirmer@13688
  1104
      thus ?case
schirmer@13688
  1105
	apply -
schirmer@13688
  1106
	apply (rule MGFn_NormalI) 
schirmer@13688
  1107
	apply (rule ax_derivs.NewA 
schirmer@13688
  1108
               [where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T) 
schirmer@13688
  1109
                              \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
schirmer@13688
  1110
	apply  (simp add: init_comp_ty_def split add: split_if)
schirmer@13688
  1111
	apply  (rule conjI, clarsimp)
schirmer@13688
  1112
	apply   (rule MGFn_InitD [OF hyp, THEN conseq2])
schirmer@13688
  1113
	apply   (clarsimp intro: eval.Init)
schirmer@13688
  1114
	apply  clarsimp
schirmer@13688
  1115
	apply  (rule ax_derivs.Skip [THEN conseq1])
schirmer@13688
  1116
	apply  (clarsimp intro: eval.Skip)
schirmer@13688
  1117
	apply (erule MGFnD' [THEN conseq12])
schirmer@13688
  1118
	apply (fastsimp intro: eval.NewA)
schirmer@13688
  1119
	done
schirmer@13688
  1120
    next
schirmer@13688
  1121
      case (Cast C e)
schirmer@13688
  1122
      thus ?case
schirmer@13688
  1123
	apply -
schirmer@13688
  1124
	apply (rule MGFn_NormalI)
schirmer@13688
  1125
	apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast])
schirmer@13688
  1126
	apply (fastsimp intro: eval.Cast)
schirmer@13688
  1127
	done
schirmer@13688
  1128
    next
schirmer@13688
  1129
      case (Inst e C)
schirmer@13688
  1130
      thus ?case
schirmer@13688
  1131
	apply -
schirmer@13688
  1132
	apply (rule MGFn_NormalI)
schirmer@13688
  1133
	apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst])
schirmer@13688
  1134
	apply (fastsimp intro: eval.Inst)
schirmer@13688
  1135
	done
schirmer@13688
  1136
    next
schirmer@13688
  1137
      case (Lit v)
schirmer@13688
  1138
      show ?case
schirmer@13688
  1139
	apply -
schirmer@13688
  1140
	apply (rule MGFn_NormalI)
schirmer@13688
  1141
	apply (rule ax_derivs.Lit [THEN conseq1])
schirmer@13688
  1142
	apply (fastsimp intro: eval.Lit)
schirmer@13688
  1143
	done
schirmer@13688
  1144
    next
schirmer@13688
  1145
      case (UnOp unop e)
schirmer@13688
  1146
      thus ?case
schirmer@13688
  1147
	apply -
schirmer@13688
  1148
	apply (rule MGFn_NormalI)
schirmer@13688
  1149
	apply (rule ax_derivs.UnOp)
schirmer@13688
  1150
	apply (erule MGFnD' [THEN conseq12])
schirmer@13688
  1151
	apply (fastsimp intro: eval.UnOp)
schirmer@13688
  1152
	done
schirmer@13688
  1153
    next
schirmer@13688
  1154
      case (BinOp binop e1 e2)
schirmer@13688
  1155
      thus ?case
schirmer@13688
  1156
	apply -
schirmer@13688
  1157
	apply (rule MGFn_NormalI)
schirmer@13688
  1158
	apply (rule ax_derivs.BinOp)
schirmer@13688
  1159
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1160
	apply (rule allI)
wenzelm@20103
  1161
	apply (case_tac "need_second_arg binop v1")
schirmer@13688
  1162
	apply  simp
schirmer@13688
  1163
	apply  (erule MGFnD' [THEN conseq12])
schirmer@13688
  1164
	apply  (fastsimp intro: eval.BinOp)
schirmer@13688
  1165
	apply simp
schirmer@13688
  1166
	apply (rule ax_Normal_cases)
schirmer@13688
  1167
	apply  (rule ax_derivs.Skip [THEN conseq1])
schirmer@13688
  1168
	apply  clarsimp
schirmer@13688
  1169
	apply  (rule eval_BinOp_arg2_indepI)
schirmer@13688
  1170
	apply   simp
schirmer@13688
  1171
	apply  simp
schirmer@13688
  1172
	apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
schirmer@13688
  1173
	apply (fastsimp intro: eval.BinOp)
schirmer@13688
  1174
	done
schirmer@13688
  1175
    next
schirmer@13688
  1176
      case Super
schirmer@13688
  1177
      show ?case
schirmer@13688
  1178
	apply -
schirmer@13688
  1179
	apply (rule MGFn_NormalI)
schirmer@13688
  1180
	apply (rule ax_derivs.Super [THEN conseq1])
schirmer@13688
  1181
	apply (fastsimp intro: eval.Super)
schirmer@13688
  1182
	done
schirmer@13688
  1183
    next
schirmer@13688
  1184
      case (Acc v)
schirmer@13688
  1185
      thus ?case
schirmer@13688
  1186
	apply -
schirmer@13688
  1187
	apply (rule MGFn_NormalI)
schirmer@13688
  1188
	apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc])
schirmer@13688
  1189
	apply (fastsimp intro: eval.Acc simp add: split_paired_all)
schirmer@13688
  1190
	done
schirmer@13688
  1191
    next
schirmer@13688
  1192
      case (Ass v e)
schirmer@13688
  1193
      thus "G,A\<turnstile>{=:n} \<langle>v:=e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1194
	apply -
schirmer@13688
  1195
	apply (rule MGFn_NormalI)
schirmer@13688
  1196
	apply (rule ax_derivs.Ass)
schirmer@13688
  1197
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1198
	apply (rule allI)
schirmer@13688
  1199
	apply (erule MGFnD'[THEN conseq12])
schirmer@13688
  1200
	apply (fastsimp intro: eval.Ass simp add: split_paired_all)
schirmer@13688
  1201
	done
schirmer@13688
  1202
    next
schirmer@13688
  1203
      case (Cond e1 e2 e3)
schirmer@13688
  1204
      thus "G,A\<turnstile>{=:n} \<langle>e1 ? e2 : e3\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1205
	apply -
schirmer@13688
  1206
	apply (rule MGFn_NormalI)
schirmer@13688
  1207
	apply (rule ax_derivs.Cond)
schirmer@13688
  1208
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1209
	apply (rule allI)
schirmer@13688
  1210
	apply (rule ax_Normal_cases)
schirmer@13688
  1211
	prefer 2
schirmer@13688
  1212
	apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
schirmer@13688
  1213
	apply  (fastsimp intro: eval.Cond)
schirmer@13688
  1214
	apply (case_tac "b")
schirmer@13688
  1215
	apply  simp
schirmer@13688
  1216
	apply  (erule MGFnD'[THEN conseq12])
schirmer@13688
  1217
	apply  (fastsimp intro: eval.Cond)
schirmer@13688
  1218
	apply simp
schirmer@13688
  1219
	apply (erule MGFnD'[THEN conseq12])
schirmer@13688
  1220
	apply (fastsimp intro: eval.Cond)
schirmer@13688
  1221
	done
schirmer@13688
  1222
    next
schirmer@13688
  1223
      case (Call accC statT mode e mn pTs' ps)
wenzelm@23366
  1224
      note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366
  1225
      note mgf_ps = `G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}`
schirmer@13688
  1226
      from mgf_methds mgf_e mgf_ps wf
schirmer@13688
  1227
      show "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1228
	by (rule MGFn_Call)
schirmer@13688
  1229
    next
schirmer@13688
  1230
      case (Methd D mn)
schirmer@13688
  1231
      from mgf_methds
schirmer@13688
  1232
      show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1233
	by simp
schirmer@13688
  1234
    next
schirmer@13688
  1235
      case (Body D c)
wenzelm@23366
  1236
      note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688
  1237
      from wf MGFn_Init [OF hyp] mgf_c
schirmer@13688
  1238
      show "G,A\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688
  1239
	by (rule MGFn_Body)
schirmer@13688
  1240
    next
schirmer@13688
  1241
      case (InsInitE c e)
schirmer@13688
  1242
      show ?case
schirmer@13688
  1243
	by (rule MGFn_NormalI) (rule ax_derivs.InsInitE)
schirmer@13688
  1244
    next
schirmer@13688
  1245
      case (Callee l e)
schirmer@13688
  1246
      show ?case
schirmer@13688
  1247
	by (rule MGFn_NormalI) (rule ax_derivs.Callee)
schirmer@13688
  1248
    next
schirmer@13688
  1249
      case Skip
schirmer@13688
  1250
      show ?case
schirmer@13688
  1251
	apply -
schirmer@13688
  1252
	apply (rule MGFn_NormalI)
schirmer@13688
  1253
	apply (rule ax_derivs.Skip [THEN conseq1])
schirmer@13688
  1254
	apply (fastsimp intro: eval.Skip)
schirmer@13688
  1255
	done
schirmer@13688
  1256
    next
schirmer@13688
  1257
      case (Expr e)
schirmer@13688
  1258
      thus ?case
schirmer@13688
  1259
	apply -
schirmer@13688
  1260
	apply (rule MGFn_NormalI)
schirmer@13688
  1261
	apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr])
schirmer@13688
  1262
	apply (fastsimp intro: eval.Expr)
schirmer@13688
  1263
	done
schirmer@13688
  1264
    next
schirmer@13688
  1265
      case (Lab l c)
schirmer@13688
  1266
      thus "G,A\<turnstile>{=:n} \<langle>l\<bullet> c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1267
	apply -
schirmer@13688
  1268
	apply (rule MGFn_NormalI)
schirmer@13688
  1269
	apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
schirmer@13688
  1270
	apply (fastsimp intro: eval.Lab)
schirmer@13688
  1271
	done
schirmer@13688
  1272
    next
schirmer@13688
  1273
      case (Comp c1 c2)
schirmer@13688
  1274
      thus "G,A\<turnstile>{=:n} \<langle>c1;; c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1275
	apply -
schirmer@13688
  1276
	apply (rule MGFn_NormalI)
schirmer@13688
  1277
	apply (rule ax_derivs.Comp)
schirmer@13688
  1278
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1279
	apply (erule MGFnD' [THEN conseq12])
schirmer@13688
  1280
	apply (fastsimp intro: eval.Comp) 
schirmer@13688
  1281
	done
schirmer@13688
  1282
    next
schirmer@13688
  1283
      case (If_ e c1 c2)
schirmer@13688
  1284
      thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1285
	apply -
schirmer@13688
  1286
	apply (rule MGFn_NormalI)
schirmer@13688
  1287
	apply (rule ax_derivs.If)
schirmer@13688
  1288
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1289
	apply (rule allI)
schirmer@13688
  1290
	apply (rule ax_Normal_cases)
schirmer@13688
  1291
	prefer 2
schirmer@13688
  1292
	apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
schirmer@13688
  1293
	apply  (fastsimp intro: eval.If)
schirmer@13688
  1294
	apply (case_tac "b")
schirmer@13688
  1295
	apply  simp
schirmer@13688
  1296
	apply  (erule MGFnD' [THEN conseq12])
schirmer@13688
  1297
	apply  (fastsimp intro: eval.If)
schirmer@13688
  1298
	apply simp
schirmer@13688
  1299
	apply (erule MGFnD' [THEN conseq12])
schirmer@13688
  1300
	apply (fastsimp intro: eval.If)
schirmer@13688
  1301
	done
schirmer@13688
  1302
    next
schirmer@13688
  1303
      case (Loop l e c)
wenzelm@23366
  1304
      note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366
  1305
      note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688
  1306
      from mgf_e mgf_c wf
schirmer@13688
  1307
      show "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1308
	by (rule MGFn_Loop)
schirmer@13688
  1309
    next
schirmer@13688
  1310
      case (Jmp j)
schirmer@13688
  1311
      thus ?case
schirmer@13688
  1312
	apply -
schirmer@13688
  1313
	apply (rule MGFn_NormalI)
schirmer@13688
  1314
	apply (rule ax_derivs.Jmp [THEN conseq1])
schirmer@13688
  1315
	apply (auto intro: eval.Jmp simp add: abupd_def2)
schirmer@13688
  1316
	done
schirmer@13688
  1317
    next
schirmer@13688
  1318
      case (Throw e)
schirmer@13688
  1319
      thus ?case
schirmer@13688
  1320
	apply -
schirmer@13688
  1321
	apply (rule MGFn_NormalI)
schirmer@13688
  1322
	apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
schirmer@13688
  1323
	apply (fastsimp intro: eval.Throw)
schirmer@13688
  1324
	done
schirmer@13688
  1325
    next
schirmer@13688
  1326
      case (TryC c1 C vn c2)
schirmer@13688
  1327
      thus "G,A\<turnstile>{=:n} \<langle>Try c1 Catch(C vn) c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1328
	apply -
schirmer@13688
  1329
	apply (rule MGFn_NormalI)
schirmer@13688
  1330
	apply (rule ax_derivs.Try [where 
schirmer@13688
  1331
          ?Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>\<langle>c1\<rangle>\<^sub>s\<succ>\<rightarrow> (Y',s'') \<and> 
schirmer@13688
  1332
                            G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n"])
schirmer@13688
  1333
	apply   (erule MGFnD [THEN ax_NormalD, THEN conseq2])
schirmer@13688
  1334
	apply   (fastsimp elim: sxalloc_gext [THEN card_nyinitcls_gext])
schirmer@13688
  1335
	apply  (erule MGFnD'[THEN conseq12])
schirmer@13688
  1336
	apply  (fastsimp intro: eval.Try)
schirmer@13688
  1337
	apply (fastsimp intro: eval.Try)
schirmer@13688
  1338
	done
schirmer@13688
  1339
    next
schirmer@13688
  1340
      case (Fin c1 c2)
wenzelm@23366
  1341
      note mgf_c1 = `G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
wenzelm@23366
  1342
      note mgf_c2 = `G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688
  1343
      from wf mgf_c1 mgf_c2
schirmer@13688
  1344
      show "G,A\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1345
	by (rule MGFn_Fin)
schirmer@13688
  1346
    next
schirmer@13688
  1347
      case (FinA abr c)
schirmer@13688
  1348
      show ?case
schirmer@13688
  1349
	by (rule MGFn_NormalI) (rule ax_derivs.FinA)
schirmer@13688
  1350
    next
schirmer@13688
  1351
      case (Init C)
schirmer@13688
  1352
      from hyp
schirmer@13688
  1353
      show "G,A\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688
  1354
	by (rule MGFn_Init)
schirmer@13688
  1355
    next
schirmer@13688
  1356
      case Nil_expr
schirmer@13688
  1357
      show "G,A\<turnstile>{=:n} \<langle>[]\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
schirmer@13688
  1358
	apply -
schirmer@13688
  1359
	apply (rule MGFn_NormalI)
schirmer@13688
  1360
	apply (rule ax_derivs.Nil [THEN conseq1])
schirmer@13688
  1361
	apply (fastsimp intro: eval.Nil)
schirmer@13688
  1362
	done
schirmer@13688
  1363
    next
schirmer@13688
  1364
      case (Cons_expr e es)
schirmer@13688
  1365
      thus "G,A\<turnstile>{=:n} \<langle>e# es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
schirmer@13688
  1366
	apply -
schirmer@13688
  1367
	apply (rule MGFn_NormalI)
schirmer@13688
  1368
	apply (rule ax_derivs.Cons)
schirmer@13688
  1369
	apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13688
  1370
	apply (rule allI)
schirmer@13688
  1371
	apply (erule MGFnD'[THEN conseq12])
schirmer@13688
  1372
	apply (fastsimp intro: eval.Cons)
schirmer@13688
  1373
	done
schirmer@13688
  1374
    qed
schirmer@13688
  1375
  }
schirmer@13688
  1376
  thus ?thesis
schirmer@13688
  1377
    by (cases rule: term_cases) auto
schirmer@13688
  1378
  qed
schirmer@13688
  1379
qed
schirmer@12854
  1380
schirmer@12925
  1381
lemma MGF_asm: 
schirmer@12925
  1382
"\<lbrakk>\<forall>C sig. is_methd G C sig \<longrightarrow> G,A\<turnstile>{\<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk>
schirmer@12925
  1383
 \<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
  1384
apply (simp (no_asm_use) add: MGF_MGFn_iff)
schirmer@12854
  1385
apply (rule allI)
schirmer@12854
  1386
apply (rule MGFn_lemma)
schirmer@12854
  1387
apply (intro strip)
schirmer@12854
  1388
apply (rule MGFn_free_wt)
schirmer@12854
  1389
apply (force dest: wt_Methd_is_methd)
schirmer@12925
  1390
apply assumption (* wf_prog G *)
schirmer@12854
  1391
done
schirmer@12854
  1392
schirmer@12854
  1393
section "nested version"
schirmer@12854
  1394
schirmer@13688
  1395
lemma nesting_lemma' [rule_format (no_asm)]: 
schirmer@13688
  1396
  assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts" 
schirmer@13688
  1397
  and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf_call pn) A) {mgf b}
schirmer@13688
  1398
                                  \<Longrightarrow> P A {mgf_call pn}"
schirmer@13688
  1399
  and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf_call pn} \<Longrightarrow> P A {mgf t}"
schirmer@13688
  1400
  and finU: "finite U"
schirmer@13688
  1401
  and uA: "uA = mgf_call`U"
schirmer@13688
  1402
  shows "\<forall>A. A \<subseteq> uA \<longrightarrow> n \<le> card uA \<longrightarrow> card A = card uA - n 
schirmer@13688
  1403
             \<longrightarrow> (\<forall>t. P A {mgf t})"
schirmer@13688
  1404
using finU uA
schirmer@13688
  1405
apply -
schirmer@13688
  1406
apply (induct_tac "n")
schirmer@13688
  1407
apply  (tactic "ALLGOALS Clarsimp_tac")
wenzelm@21669
  1408
apply  (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
schirmer@13688
  1409
apply    simp
schirmer@13688
  1410
apply   (erule finite_imageI)
schirmer@13688
  1411
apply  (simp add: MGF_asm ax_derivs_asm)
schirmer@13688
  1412
apply (rule MGF_asm)
schirmer@13688
  1413
apply (rule ballI)
schirmer@13688
  1414
apply (case_tac "mgf_call pn : A")
schirmer@13688
  1415
apply  (fast intro: ax_derivs_asm)
schirmer@13688
  1416
apply (rule MGF_nested_Methd)
schirmer@13688
  1417
apply (rule ballI)
schirmer@13688
  1418
apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
schirmer@13688
  1419
apply   fast
schirmer@13688
  1420
apply (drule finite_subset)
schirmer@13688
  1421
apply (erule finite_imageI)
schirmer@13688
  1422
apply auto
schirmer@13688
  1423
done
schirmer@12854
  1424
schirmer@13688
  1425
schirmer@13688
  1426
lemma nesting_lemma [rule_format (no_asm)]:
schirmer@13688
  1427
  assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts"
schirmer@13688
  1428
  and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf (f pn)) A) {mgf b}
schirmer@13688
  1429
                                  \<Longrightarrow> P A {mgf (f pn)}"
schirmer@13688
  1430
  and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf (f pn)} \<Longrightarrow> P A {mgf t}"
schirmer@13688
  1431
  and finU: "finite U"
schirmer@13688
  1432
shows "P {} {mgf t}"
schirmer@13688
  1433
using ax_derivs_asm MGF_nested_Methd MGF_asm finU
schirmer@13688
  1434
by (rule nesting_lemma') (auto intro!: le_refl)
schirmer@13688
  1435
schirmer@12854
  1436
schirmer@12854
  1437
lemma MGF_nested_Methd: "\<lbrakk>  
schirmer@13688
  1438
 G,insert ({Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}) A
schirmer@13688
  1439
    \<turnstile>{Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}  
schirmer@13688
  1440
 \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal \<doteq>}  \<langle>Methd  C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}"
schirmer@12854
  1441
apply (unfold MGF_def)
schirmer@12854
  1442
apply (rule ax_MethdN)
schirmer@12854
  1443
apply (erule conseq2)
schirmer@12854
  1444
apply clarsimp
schirmer@12854
  1445
apply (erule MethdI)
schirmer@12854
  1446
done
schirmer@12854
  1447
schirmer@12925
  1448
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
  1449
apply (rule MGFNormalI)
schirmer@12854
  1450
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 
schirmer@13688
  1451
                bdy = "\<lambda> (C,sig) .{\<langle>body G C sig\<rangle>\<^sub>e }" and 
schirmer@13688
  1452
                f = "\<lambda> (C,sig) . \<langle>Methd C sig\<rangle>\<^sub>e " in nesting_lemma)
schirmer@12854
  1453
apply    (erule ax_derivs.asm)
schirmer@12854
  1454
apply   (clarsimp simp add: split_tupled_all)
schirmer@12854
  1455
apply   (erule MGF_nested_Methd)
schirmer@12925
  1456
apply  (erule_tac [2] finite_is_methd [OF wf_ws_prog])
schirmer@12854
  1457
apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925
  1458
apply (auto intro: MGFNormalI)
schirmer@12854
  1459
done
schirmer@12854
  1460
schirmer@12854
  1461
schirmer@12854
  1462
section "simultaneous version"
schirmer@12854
  1463
schirmer@12854
  1464
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
schirmer@13688
  1465
  G,A \<union> (\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms  
schirmer@13688
  1466
      |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>  
schirmer@13688
  1467
  G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms"
schirmer@12854
  1468
apply (unfold MGF_def)
schirmer@12854
  1469
apply (rule ax_derivs.Methd [unfolded mtriples_def])
schirmer@12854
  1470
apply (erule ax_finite_pointwise)
schirmer@12854
  1471
prefer 2
schirmer@12854
  1472
apply  (rule ax_derivs.asm)
schirmer@12854
  1473
apply  fast
schirmer@12854
  1474
apply clarsimp
schirmer@12854
  1475
apply (rule conseq2)
schirmer@12854
  1476
apply  (erule (1) ax_methods_spec)
schirmer@12854
  1477
apply clarsimp
schirmer@12854
  1478
apply (erule eval_Methd)
schirmer@12854
  1479
done
schirmer@12854
  1480
schirmer@12925
  1481
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> 
schirmer@13688
  1482
   G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) 
schirmer@12854
  1483
   ` Collect (split (is_methd G)) "
schirmer@12925
  1484
apply (frule finite_is_methd [OF wf_ws_prog])
schirmer@12854
  1485
apply (rule MGF_simult_Methd_lemma)
schirmer@12854
  1486
apply  assumption
schirmer@12854
  1487
apply (erule ax_finite_pointwise)
schirmer@12854
  1488
prefer 2
schirmer@12854
  1489
apply  (rule ax_derivs.asm)
schirmer@12854
  1490
apply  blast
schirmer@12854
  1491
apply clarsimp
schirmer@12854
  1492
apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925
  1493
apply   (auto intro: MGFNormalI)
schirmer@12854
  1494
done
schirmer@12854
  1495
schirmer@12854
  1496
schirmer@12854
  1497
section "corollaries"
schirmer@12854
  1498
schirmer@12925
  1499
lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk>
schirmer@12925
  1500
 \<Longrightarrow>   \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
schirmer@12925
  1501
apply (cases "normal s")
schirmer@12925
  1502
apply   (force simp add: type_ok_def intro: eval_evaln)
schirmer@12925
  1503
apply   (force intro: evaln.Abrupt)
schirmer@12925
  1504
done
schirmer@12925
  1505
schirmer@13688
  1506
lemma MGF_complete:
schirmer@13688
  1507
  assumes valid: "G,{}\<Turnstile>{P} t\<succ> {Q}"
schirmer@13688
  1508
  and     mgf: "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@13688
  1509
  and      wf: "wf_prog G"
schirmer@13688
  1510
  shows "G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
schirmer@13688
  1511
proof (rule ax_no_hazard)
schirmer@13688
  1512
  from mgf
schirmer@13688
  1513
  have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y, s')}"  
schirmer@13688
  1514
    by  (unfold MGF_def) 
schirmer@13688
  1515
  thus "G,({}::state triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q}"
schirmer@13688
  1516
  proof (rule conseq12,clarsimp)
schirmer@13688
  1517
    fix Y s Z Y' s'
schirmer@13688
  1518
    assume P: "P Y s Z"
schirmer@13688
  1519
    assume type_ok: "type_ok G t s"
schirmer@13688
  1520
    assume eval_t: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s')"
schirmer@13688
  1521
    show "Q Y' s' Z"
schirmer@13688
  1522
    proof -
schirmer@13688
  1523
      from eval_t type_ok wf 
schirmer@13688
  1524
      obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
nipkow@17589
  1525
	by (rule eval_to_evaln [elim_format]) iprover
schirmer@13688
  1526
      from valid have 
schirmer@13688
  1527
	valid_expanded:
schirmer@13688
  1528
	"\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s 
schirmer@13688
  1529
                   \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s') \<longrightarrow> Q Y' s' Z)"
schirmer@13688
  1530
	by (simp add: ax_valids_def triple_valid_def)
schirmer@13688
  1531
      from P type_ok evaln
schirmer@13688
  1532
      show "Q Y' s' Z"
schirmer@13688
  1533
	by (rule valid_expanded [rule_format])
schirmer@13688
  1534
    qed
schirmer@13688
  1535
  qed 
schirmer@13688
  1536
qed
schirmer@13688
  1537
   
schirmer@13688
  1538
theorem ax_complete: 
schirmer@13688
  1539
  assumes wf: "wf_prog G" 
schirmer@13688
  1540
  and valid: "G,{}\<Turnstile>{P::state assn} t\<succ> {Q}"
schirmer@13688
  1541
  shows "G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
schirmer@13688
  1542
proof -
schirmer@13688
  1543
  from wf have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@13688
  1544
    by (rule MGF_deriv)
schirmer@13688
  1545
  from valid this wf
schirmer@13688
  1546
  show ?thesis
schirmer@13688
  1547
    by (rule MGF_complete)
schirmer@13688
  1548
qed
schirmer@13688
  1549
 
schirmer@12854
  1550
end