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