src/HOL/Bali/AxCompl.thy
author schirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13384 a34e38154413
permissions -rw-r--r--
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
wenzelm@12857
     1
(*  Title:      HOL/Bali/AxCompl.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
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@12854
    22
section "set of not yet initialzed classes"
schirmer@12854
    23
schirmer@12854
    24
constdefs
schirmer@12854
    25
schirmer@12854
    26
  nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
schirmer@12854
    27
 "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
schirmer@12854
    28
schirmer@12854
    29
lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
schirmer@12854
    30
apply (unfold nyinitcls_def)
schirmer@12854
    31
apply fast
schirmer@12854
    32
done
schirmer@12854
    33
schirmer@12854
    34
lemmas finite_nyinitcls [simp] =
schirmer@12854
    35
   finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
schirmer@12854
    36
schirmer@12854
    37
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
schirmer@12854
    38
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
schirmer@12854
    39
done
schirmer@12854
    40
schirmer@12854
    41
lemma nyinitcls_set_locals_cong [simp]: 
schirmer@12854
    42
  "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
schirmer@12854
    43
apply (unfold nyinitcls_def)
schirmer@12854
    44
apply (simp (no_asm))
schirmer@12854
    45
done
schirmer@12854
    46
schirmer@12854
    47
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
schirmer@12854
    48
apply (unfold nyinitcls_def)
schirmer@12854
    49
apply (simp (no_asm))
schirmer@12854
    50
done
schirmer@12854
    51
schirmer@12854
    52
lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
schirmer@12854
    53
apply (unfold nyinitcls_def)
schirmer@12854
    54
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
    55
apply (simp (no_asm))
schirmer@12854
    56
done
schirmer@12854
    57
schirmer@12854
    58
lemma card_nyinitcls_abrupt_congE [elim!]: 
schirmer@12854
    59
        "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
schirmer@12854
    60
apply (unfold nyinitcls_def)
schirmer@12854
    61
apply auto
schirmer@12854
    62
done
schirmer@12854
    63
schirmer@12854
    64
lemma nyinitcls_new_xcpt_var [simp]: 
schirmer@12854
    65
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
schirmer@12854
    66
apply (unfold nyinitcls_def)
schirmer@12854
    67
apply (induct_tac "s")
schirmer@12854
    68
apply (simp (no_asm))
schirmer@12854
    69
done
schirmer@12854
    70
schirmer@12854
    71
lemma nyinitcls_init_lvars [simp]: 
schirmer@12854
    72
  "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
schirmer@12854
    73
apply (induct_tac "s")
schirmer@12854
    74
apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
schirmer@12854
    75
done
schirmer@12854
    76
schirmer@12854
    77
lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
schirmer@12854
    78
apply (unfold nyinitcls_def)
schirmer@12854
    79
apply fast
schirmer@12854
    80
done
schirmer@12854
    81
schirmer@12854
    82
lemma card_Suc_lemma: "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
schirmer@12854
    83
apply (rotate_tac 1)
schirmer@12854
    84
apply clarsimp
schirmer@12854
    85
done
schirmer@12854
    86
schirmer@12854
    87
lemma nyinitcls_le_SucD: 
schirmer@12854
    88
"\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
schirmer@12854
    89
  card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
schirmer@12854
    90
apply (subgoal_tac 
schirmer@12854
    91
        "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
schirmer@12854
    92
apply  clarsimp
schirmer@12854
    93
apply  (erule thin_rl)
schirmer@12854
    94
apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
schirmer@12854
    95
apply   (auto dest!: not_initedD elim!: 
schirmer@12854
    96
              simp add: nyinitcls_def inited_def split add: split_if_asm)
schirmer@12854
    97
done
schirmer@12854
    98
schirmer@12854
    99
ML {* bind_thm("inited_gext'",permute_prems 0 1 (thm "inited_gext")) *}
schirmer@12854
   100
schirmer@12854
   101
lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
schirmer@12854
   102
apply (unfold nyinitcls_def)
schirmer@12854
   103
apply (force dest!: inited_gext')
schirmer@12854
   104
done
schirmer@12854
   105
schirmer@12854
   106
lemma card_nyinitcls_gext: 
schirmer@12854
   107
  "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
schirmer@12854
   108
apply (rule le_trans)
schirmer@12854
   109
apply  (rule card_mono)
schirmer@12854
   110
apply   (rule finite_nyinitcls)
schirmer@12854
   111
apply  (erule nyinitcls_gext)
schirmer@12854
   112
apply assumption
schirmer@12854
   113
done
schirmer@12854
   114
schirmer@12854
   115
schirmer@12854
   116
section "init-le"
schirmer@12854
   117
schirmer@12854
   118
constdefs
schirmer@12854
   119
  init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
schirmer@12854
   120
 "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
schirmer@12854
   121
  
schirmer@12854
   122
lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
schirmer@12854
   123
apply (unfold init_le_def)
schirmer@12854
   124
apply auto
schirmer@12854
   125
done
schirmer@12854
   126
schirmer@12854
   127
lemma All_init_leD: "\<forall>n::nat. G,A\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
   128
apply (drule spec)
schirmer@12854
   129
apply (erule conseq1)
schirmer@12854
   130
apply clarsimp
schirmer@12854
   131
apply (rule card_nyinitcls_bound)
schirmer@12854
   132
done
schirmer@12854
   133
schirmer@12854
   134
section "Most General Triples and Formulas"
schirmer@12854
   135
schirmer@12854
   136
constdefs
schirmer@12854
   137
schirmer@12854
   138
  remember_init_state :: "state assn"                ("\<doteq>")
schirmer@12854
   139
  "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
schirmer@12854
   140
schirmer@12854
   141
lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
schirmer@12854
   142
apply (unfold remember_init_state_def)
schirmer@12854
   143
apply (simp (no_asm))
schirmer@12854
   144
done
schirmer@12854
   145
schirmer@12854
   146
consts
schirmer@12854
   147
  
schirmer@12854
   148
  MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
schirmer@12854
   149
  MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
schirmer@12854
   150
schirmer@12854
   151
defs
schirmer@12854
   152
  
schirmer@12854
   153
schirmer@12854
   154
  MGF_def:
schirmer@12854
   155
  "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
schirmer@12854
   156
schirmer@12854
   157
  MGFn_def:
schirmer@12854
   158
  "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
schirmer@12854
   159
schirmer@12854
   160
(* unused *)
schirmer@12925
   161
schirmer@12925
   162
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   163
apply (unfold MGF_def)
schirmer@12925
   164
apply (simp add:  ax_valids_def triple_valid_def2)
schirmer@12925
   165
apply (auto elim: evaln_eval)
schirmer@12854
   166
done
schirmer@12854
   167
schirmer@12925
   168
schirmer@12854
   169
lemma MGF_res_eq_lemma [simp]: 
schirmer@12854
   170
  "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
schirmer@12854
   171
apply auto
schirmer@12854
   172
done
schirmer@12854
   173
schirmer@12854
   174
lemma MGFn_def2: 
schirmer@12854
   175
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
schirmer@12854
   176
                    t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
schirmer@12854
   177
apply (unfold MGFn_def MGF_def)
schirmer@12854
   178
apply fast
schirmer@12854
   179
done
schirmer@12854
   180
schirmer@12854
   181
lemma MGF_MGFn_iff: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
schirmer@12854
   182
apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
schirmer@12854
   183
apply safe
schirmer@12854
   184
apply  (erule_tac [2] All_init_leD)
schirmer@12854
   185
apply (erule conseq1)
schirmer@12854
   186
apply clarsimp
schirmer@12854
   187
done
schirmer@12854
   188
schirmer@12854
   189
lemma MGFnD: 
schirmer@12854
   190
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854
   191
 G,A\<turnstile>{(\<lambda>Y' s' s. s' = s           \<and> P s) \<and>. G\<turnstile>init\<le>n}  
schirmer@12854
   192
 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
   193
apply (unfold init_le_def)
schirmer@12854
   194
apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854
   195
apply (erule conseq12)
schirmer@12854
   196
apply clarsimp
schirmer@12854
   197
apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
schirmer@12854
   198
done
schirmer@12854
   199
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
schirmer@12854
   200
schirmer@12854
   201
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854
   202
  G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
schirmer@12854
   203
apply (unfold MGF_def)
schirmer@12854
   204
apply (rule ax_Normal_cases)
schirmer@12854
   205
apply  (erule conseq1)
schirmer@12854
   206
apply  clarsimp
schirmer@12854
   207
apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854
   208
apply (clarsimp simp add: Let_def)
schirmer@12854
   209
done
schirmer@12854
   210
schirmer@12854
   211
lemma MGFNormalD: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   212
apply (unfold MGF_def)
schirmer@12854
   213
apply (erule conseq1)
schirmer@12854
   214
apply clarsimp
schirmer@12854
   215
done
schirmer@12854
   216
schirmer@12854
   217
lemma MGFn_NormalI: 
schirmer@12854
   218
"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
   219
 {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12854
   220
apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854
   221
apply (rule ax_Normal_cases)
schirmer@12854
   222
apply  (erule conseq1)
schirmer@12854
   223
apply  clarsimp
schirmer@12854
   224
apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854
   225
apply (clarsimp simp add: Let_def)
schirmer@12854
   226
done
schirmer@12854
   227
schirmer@12854
   228
lemma MGFn_free_wt: 
schirmer@12854
   229
  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
schirmer@12854
   230
    \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
schirmer@12854
   231
   \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@12854
   232
apply (rule MGFn_NormalI)
schirmer@12854
   233
apply (rule ax_free_wt)
schirmer@12854
   234
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
schirmer@12854
   235
done
schirmer@12854
   236
schirmer@12925
   237
lemma MGFn_free_wt_NormalConformI: 
schirmer@12925
   238
"(\<forall> T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T 
schirmer@12925
   239
  \<longrightarrow> G,(A::state triple set)
schirmer@12925
   240
      \<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
   241
      t\<succ> 
schirmer@12925
   242
      {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
schirmer@12925
   243
 \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12925
   244
apply (rule MGFn_NormalI)
schirmer@12925
   245
apply (rule ax_no_hazard)
schirmer@12925
   246
apply (rule ax_escape)
schirmer@12925
   247
apply (intro strip)
schirmer@12925
   248
apply (simp only: type_ok_def peek_and_def)
schirmer@12925
   249
apply (erule conjE)+
schirmer@12925
   250
apply (erule exE,erule exE, erule exE,erule conjE,drule (1) mp)
schirmer@12925
   251
apply (drule spec,drule spec, drule spec, drule (1) mp)
schirmer@12925
   252
apply (erule conseq12)
schirmer@12925
   253
apply blast
schirmer@12925
   254
done
schirmer@12925
   255
schirmer@12854
   256
schirmer@12854
   257
section "main lemmas"
schirmer@12854
   258
schirmer@12854
   259
declare fun_upd_apply [simp del]
schirmer@12854
   260
declare splitI2 [rule del] (*prevents ugly renaming of state variables*)
schirmer@12854
   261
schirmer@12854
   262
ML_setup {* 
schirmer@12854
   263
Delsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
schirmer@12854
   264
*} (*prevents modifying rhs of MGF*)
schirmer@12854
   265
ML {*
schirmer@12854
   266
val eval_css = (claset() delrules [thm "eval.Abrupt"] addSIs (thms "eval.intros") 
schirmer@12854
   267
                delrules[thm "eval.Expr", thm "eval.Init", thm "eval.Try"] 
schirmer@12854
   268
                addIs   [thm "eval.Expr", thm "eval.Init"]
schirmer@12854
   269
                addSEs[thm "eval.Try"] delrules[equalityCE],
schirmer@12854
   270
                simpset() addsimps [split_paired_all,Let_def]
schirmer@12854
   271
 addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]);
schirmer@12854
   272
val eval_Force_tac = force_tac eval_css;
schirmer@12854
   273
schirmer@12854
   274
val wt_prepare_tac = EVERY'[
schirmer@12854
   275
    rtac (thm "MGFn_free_wt"),
schirmer@12854
   276
    clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
schirmer@12854
   277
val compl_prepare_tac = EVERY'[rtac (thm "MGFn_NormalI"), Simp_tac]
schirmer@12925
   278
val wt_conf_prepare_tac = EVERY'[
schirmer@12925
   279
    rtac (thm "MGFn_free_wt_NormalConformI"),
schirmer@12925
   280
    clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
schirmer@12854
   281
val forw_hyp_tac = EVERY'[etac (thm "MGFnD'" RS thm "conseq12"), Clarsimp_tac]
schirmer@12854
   282
val forw_hyp_eval_Force_tac = 
schirmer@12854
   283
         EVERY'[TRY o rtac allI, forw_hyp_tac, eval_Force_tac]
schirmer@12854
   284
*}
schirmer@12854
   285
schirmer@12854
   286
lemma MGFn_Init: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow>  
schirmer@12854
   287
  G,(A::state triple set)\<turnstile>{=:n} In1r (Init C)\<succ> {G\<rightarrow>}"
schirmer@12854
   288
apply (tactic "wt_prepare_tac 1")
schirmer@12854
   289
(* requires is_class G C two times for nyinitcls *)
schirmer@12854
   290
apply (tactic "compl_prepare_tac 1")
schirmer@12854
   291
apply (rule_tac C = "initd C" in ax_cases)
schirmer@12854
   292
apply  (rule ax_derivs.Done [THEN conseq1])
schirmer@12854
   293
apply  (clarsimp intro!: init_done)
schirmer@12854
   294
apply (rule_tac y = n in nat.exhaust, clarsimp)
schirmer@12854
   295
apply  (rule ax_impossible [THEN conseq1])
schirmer@12854
   296
apply  (force dest!: nyinitcls_emptyD)
schirmer@12854
   297
apply clarsimp
schirmer@12854
   298
apply (drule_tac x = "nat" in spec)
schirmer@12854
   299
apply clarsimp
schirmer@12854
   300
apply (rule_tac Q = " (\<lambda>Y s' (x,s) . G\<turnstile> (x,init_class_obj G C s) \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s' \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>nat" in ax_derivs.Init)
schirmer@12854
   301
apply   simp
schirmer@12854
   302
apply  (rule_tac P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>nat) " in conseq1)
schirmer@12854
   303
prefer 2
schirmer@12854
   304
apply   (force elim!: nyinitcls_le_SucD)
schirmer@12854
   305
apply  (simp split add: split_if, rule conjI, clarify)
schirmer@12854
   306
apply   (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   307
apply  clarify
schirmer@12854
   308
apply  (drule spec)
schirmer@12854
   309
apply  (erule MGFnD' [THEN conseq12])
schirmer@12854
   310
apply  (tactic "force_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
schirmer@12854
   311
apply (rule allI)
schirmer@12854
   312
apply (drule spec)
schirmer@12854
   313
apply (erule MGFnD' [THEN conseq12])
schirmer@12854
   314
apply clarsimp
schirmer@12854
   315
apply (tactic {* pair_tac "sa" 1 *})
schirmer@12854
   316
apply (tactic"clarsimp_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
schirmer@12854
   317
apply (rule eval_Init, force+)
schirmer@12854
   318
done
schirmer@12854
   319
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
schirmer@12854
   320
schirmer@12925
   321
text {* For @{text MGFn_Call} we need the wellformedness of the program to
schirmer@12925
   322
switch from the evaln-semantics to the eval-semantics *}
schirmer@12854
   323
lemma MGFn_Call: 
schirmer@12854
   324
"\<lbrakk>\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};  
schirmer@12925
   325
  G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>};wf_prog G\<rbrakk> \<Longrightarrow>  
schirmer@12925
   326
  G,A\<turnstile>{=:n} In1l ({accC,statT,mode}e\<cdot>mn({pTs'}ps))\<succ> {G\<rightarrow>}"
schirmer@12925
   327
apply (tactic "wt_conf_prepare_tac 1")
schirmer@12925
   328
apply (rule_tac  
schirmer@12925
   329
  Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@12925
   330
        (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
schirmer@12925
   331
         \<and> Y = In1 a)) 
schirmer@12925
   332
    \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" and 
schirmer@12925
   333
 R = "\<lambda>a'. (\<lambda>Y (x2,s2) (x,s) . x = None \<and> 
schirmer@12925
   334
             (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a'\<rightarrow> s1 \<and> 
schirmer@12925
   335
                       (normal s1 \<longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT)\<and> 
schirmer@12925
   336
                       Y = In3 pvs \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) 
schirmer@12925
   337
            \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" in ax_derivs.Call)
schirmer@12925
   338
apply   (tactic "forw_hyp_tac 1")
schirmer@12925
   339
apply   (tactic "clarsimp_tac eval_css 1")
schirmer@12925
   340
apply   (frule (3) eval_type_sound)
schirmer@12925
   341
apply   force
schirmer@12925
   342
schirmer@12925
   343
apply   safe
schirmer@12925
   344
apply   (tactic "forw_hyp_tac 1")
schirmer@12925
   345
apply   (tactic "clarsimp_tac eval_css 1")
schirmer@12925
   346
apply   (frule (3) eval_type_sound)
schirmer@12925
   347
apply     (rule conjI)
schirmer@12925
   348
apply       (rule exI,rule conjI)
schirmer@12925
   349
apply         (assumption)
schirmer@12925
   350
schirmer@12925
   351
apply         (rule conjI)
schirmer@12925
   352
apply           simp
schirmer@12925
   353
apply           assumption
schirmer@12925
   354
apply      blast
schirmer@12925
   355
schirmer@12854
   356
apply (drule spec, drule spec)
schirmer@12854
   357
apply (erule MGFnD' [THEN conseq12])
schirmer@12854
   358
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   359
apply (erule (1) eval_Call)
schirmer@12925
   360
apply   (rule HOL.refl)+
schirmer@12925
   361
apply   (subgoal_tac "check_method_access G C statT (invmode m e)
schirmer@12925
   362
             \<lparr>name = mn, parTs = pTs'\<rparr> a
schirmer@12925
   363
             (init_lvars G
schirmer@12925
   364
               (invocation_declclass G (invmode m e) (snd (ab, ba)) a statT
schirmer@12925
   365
                 \<lparr>name = mn, parTs = pTs'\<rparr>)
schirmer@12925
   366
               \<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs
schirmer@12925
   367
               (ab,
schirmer@12925
   368
                ba)) = (init_lvars G
schirmer@12925
   369
               (invocation_declclass G (invmode m e) (snd (ab, ba)) a statT
schirmer@12925
   370
                 \<lparr>name = mn, parTs = pTs'\<rparr>)
schirmer@12925
   371
               \<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs
schirmer@12925
   372
               (ab,
schirmer@12925
   373
                ba))")
schirmer@12925
   374
apply    simp
schirmer@12925
   375
defer 
schirmer@12925
   376
apply simp
schirmer@12925
   377
apply (erule (3) error_free_call_access) (* now showing the subgoal *)
schirmer@12925
   378
apply auto
schirmer@12854
   379
done
schirmer@12854
   380
schirmer@12854
   381
lemma MGF_altern: "G,A\<turnstile>{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} =  
schirmer@12854
   382
 G,A\<turnstile>{Normal ((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) \<and>. p)} 
schirmer@12854
   383
  t\<succ> {\<lambda>Y s Z. (Y,s) = Z}"
schirmer@12854
   384
apply (unfold MGF_def)
schirmer@12854
   385
apply (auto del: conjI elim!: conseq12)
schirmer@12854
   386
apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
schirmer@12854
   387
apply  (fast dest: unique_eval)
schirmer@12854
   388
apply clarsimp
schirmer@12854
   389
apply (erule thin_rl)
schirmer@12854
   390
apply (erule thin_rl)
schirmer@12854
   391
apply (drule split_paired_All [THEN subst])
schirmer@12854
   392
apply (clarsimp elim!: state_not_single)
schirmer@12854
   393
done
schirmer@12854
   394
schirmer@12854
   395
schirmer@12854
   396
lemma MGFn_Loop: 
schirmer@12854
   397
"\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk> 
schirmer@12854
   398
\<Longrightarrow> 
schirmer@12854
   399
  G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}"
schirmer@12854
   400
apply (rule MGFn_NormalI, simp)
schirmer@12854
   401
apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in 
schirmer@12854
   402
          MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1])
schirmer@12854
   403
prefer 2
schirmer@12854
   404
apply  clarsimp
schirmer@12854
   405
apply (rule_tac P' = 
schirmer@12854
   406
"((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>In1r (l\<bullet>  While(expr) stmnt) \<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) 
schirmer@12854
   407
  \<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12)
schirmer@12854
   408
prefer 2
schirmer@12854
   409
apply  clarsimp
schirmer@12854
   410
apply  (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl)
schirmer@12854
   411
apply  (rule_tac [2] P' = " (\<lambda>b s (Y',s') . (\<exists>s0. G\<turnstile>s0 \<midarrow>In1l expr\<succ>\<rightarrow> (b,s)) \<and> (if normal s \<and> the_Bool (the_In1 b) then (\<forall>s'' w s0. G\<turnstile>s \<midarrow>stmnt\<rightarrow> s'' \<and> G\<turnstile>(abupd (absorb (Cont l)) s'') \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s0) \<longrightarrow> (w,s0) = (Y',s')) else (\<diamondsuit>,s) = (Y',s'))) \<and>. G\<turnstile>init\<le>n" in polymorphic_Loop)
schirmer@12854
   412
apply   (force dest!: eval.Loop split add: split_if_asm)
schirmer@12854
   413
prefer 2
schirmer@12854
   414
apply  (erule MGFnD' [THEN conseq12])
schirmer@12854
   415
apply  clarsimp
schirmer@12854
   416
apply  (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl)
schirmer@12854
   417
apply  (tactic "eval_Force_tac 1")
schirmer@12854
   418
apply (erule MGFnD' [THEN conseq12] , clarsimp)
schirmer@12854
   419
apply (rule conjI, erule exI)
schirmer@12854
   420
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   421
apply (case_tac "a")
schirmer@12854
   422
prefer 2
schirmer@12854
   423
apply  (clarsimp)
schirmer@12854
   424
apply (clarsimp split add: split_if)
schirmer@12854
   425
apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"],
schirmer@12854
   426
  simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+)
schirmer@12854
   427
done
schirmer@12854
   428
schirmer@12925
   429
text {* For @{text MGFn_FVar} we need the wellformedness of the program to
schirmer@12925
   430
switch from the evaln-semantics to the eval-semantics *}
schirmer@12925
   431
lemma MGFn_FVar:
schirmer@12925
   432
 "\<lbrakk>G,A\<turnstile>{=:n} In1r (Init statDeclC)\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk>
schirmer@12925
   433
   \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In2 ({accC,statDeclC,stat}e..fn)\<succ> {G\<rightarrow>}"
schirmer@12925
   434
apply (tactic "wt_conf_prepare_tac 1")
schirmer@12925
   435
apply (rule_tac  
schirmer@12925
   436
  Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@12925
   437
        (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1 
schirmer@12925
   438
         )) \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"  
schirmer@12925
   439
 in ax_derivs.FVar)
schirmer@12925
   440
apply (tactic "forw_hyp_tac 1")
schirmer@12925
   441
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12925
   442
apply (subgoal_tac "is_class G statDeclC")
schirmer@12925
   443
apply   (force dest: eval_type_sound)
schirmer@12925
   444
apply   (force dest: ty_expr_is_type [THEN type_is_class] 
schirmer@12925
   445
                      accfield_fields [THEN fields_declC])
schirmer@12925
   446
apply (tactic "forw_hyp_tac 1")
schirmer@12925
   447
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12925
   448
apply (subgoal_tac "(\<exists> v' s2' s3.   
schirmer@12925
   449
        ( fvar statDeclC (is_static f) fn v (aa, ba) = (v',s2') ) \<and>
schirmer@12925
   450
            (s3  = check_field_access G C statDeclC fn (is_static f) v s2') \<and>
schirmer@12925
   451
            (s3 = s2'))")
schirmer@12925
   452
apply   (erule exE)+
schirmer@12925
   453
apply   (erule conjE)+
schirmer@12925
   454
apply   (erule (1) eval.FVar)
schirmer@12925
   455
apply     simp
schirmer@12925
   456
apply     simp
schirmer@12925
   457
schirmer@12925
   458
apply   (case_tac "fvar statDeclC (is_static f) fn v (aa, ba)")
schirmer@12925
   459
apply   (rule exI)+
schirmer@12925
   460
apply   (rule context_conjI)
schirmer@12925
   461
apply      force
schirmer@12925
   462
schirmer@12925
   463
apply   (rule context_conjI)
schirmer@12925
   464
apply     simp
schirmer@12925
   465
schirmer@12925
   466
apply     (erule (3) error_free_field_access)
schirmer@12925
   467
apply       (auto dest: eval_type_sound)
schirmer@12925
   468
done
schirmer@12925
   469
schirmer@13337
   470
(* FIXME To TypeSafe *)
schirmer@13337
   471
lemma wf_eval_Fin: 
schirmer@13337
   472
  assumes wf:    "wf_prog G" and
schirmer@13337
   473
          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
schirmer@13337
   474
        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
schirmer@13337
   475
        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
schirmer@13337
   476
        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
schirmer@13337
   477
            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
schirmer@13337
   478
  shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
schirmer@13337
   479
proof -
schirmer@13337
   480
  from eval_c1 wt_c1 wf conf_s0
schirmer@13337
   481
  have "error_free (x1,s1)"
schirmer@13337
   482
    by (auto dest: eval_type_sound)
schirmer@13337
   483
  with eval_c1 eval_c2 s3
schirmer@13337
   484
  show ?thesis
schirmer@13337
   485
    by - (rule eval.Fin, auto simp add: error_free_def)
schirmer@13337
   486
qed
schirmer@13337
   487
schirmer@13337
   488
text {* For @{text MGFn_Fin} we need the wellformedness of the program to
schirmer@13337
   489
switch from the evaln-semantics to the eval-semantics *}
schirmer@13337
   490
lemma MGFn_Fin: 
schirmer@13337
   491
"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk>
schirmer@13337
   492
 \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}"
schirmer@13337
   493
apply (tactic "wt_conf_prepare_tac 1")
schirmer@13337
   494
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L)) 
schirmer@13337
   495
\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
schirmer@13337
   496
apply (tactic "forw_hyp_tac 1")
schirmer@13337
   497
apply (tactic "clarsimp_tac eval_css 1")
schirmer@13337
   498
apply (rule allI)
schirmer@13337
   499
apply (tactic "clarsimp_tac eval_css 1")
schirmer@13337
   500
apply (tactic "forw_hyp_tac 1")
schirmer@13337
   501
apply (tactic {* pair_tac "sb" 1 *})
schirmer@13337
   502
apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
schirmer@13337
   503
apply (rule wf_eval_Fin)
schirmer@13337
   504
apply auto
schirmer@13337
   505
done
schirmer@13337
   506
schirmer@12925
   507
text {* For @{text MGFn_lemma} we need the wellformedness of the program to
schirmer@12925
   508
switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call}, 
schirmer@12925
   509
@{text MGFn_FVar}*}
schirmer@12854
   510
lemma MGFn_lemma [rule_format (no_asm)]: 
schirmer@12925
   511
 "\<lbrakk>\<forall>n C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};
schirmer@12925
   512
   wf_prog G\<rbrakk> 
schirmer@12925
   513
  \<Longrightarrow>  \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@12854
   514
apply (rule full_nat_induct)
schirmer@12854
   515
apply (rule allI)
schirmer@12854
   516
apply (drule_tac x = n in spec)
schirmer@12854
   517
apply (drule_tac psi = "All ?P" in asm_rl)
schirmer@12854
   518
apply (subgoal_tac "\<forall>v e c es. G,A\<turnstile>{=:n} In2 v\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In3 es\<succ> {G\<rightarrow>}")
schirmer@12854
   519
apply  (tactic "Clarify_tac 2")
schirmer@12854
   520
apply  (induct_tac "t")
schirmer@12854
   521
apply    (induct_tac "a")
schirmer@12854
   522
apply     fast+
schirmer@13337
   523
apply (rule var_expr_stmt.induct) 
schirmer@13337
   524
(* 34 subgoals *)
schirmer@13337
   525
prefer 17 apply fast (* Methd *)
schirmer@13337
   526
prefer 16 apply (erule (3) MGFn_Call)
schirmer@12925
   527
prefer 2  apply (drule MGFn_Init,erule (2) MGFn_FVar)
schirmer@12854
   528
apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
schirmer@13337
   529
apply (erule_tac [29] MGFn_Init)
schirmer@13337
   530
prefer 23 apply (erule (1) MGFn_Loop)
schirmer@13337
   531
prefer 26 apply (erule (2) MGFn_Fin)
schirmer@12854
   532
apply (tactic "ALLGOALS compl_prepare_tac")
schirmer@12854
   533
schirmer@12854
   534
apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   535
schirmer@12854
   536
apply (rule ax_derivs.AVar)
schirmer@12854
   537
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   538
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   539
schirmer@13337
   540
apply (rule ax_derivs.InstInitV)
schirmer@13337
   541
schirmer@12854
   542
apply (rule ax_derivs.NewC)
schirmer@12854
   543
apply (erule MGFn_InitD [THEN conseq2])
schirmer@12854
   544
apply (tactic "eval_Force_tac 1")
schirmer@12854
   545
schirmer@12854
   546
apply (rule_tac Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty ty) \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.NewA)
schirmer@12854
   547
apply  (simp add: init_comp_ty_def split add: split_if)
schirmer@12854
   548
apply   (rule conjI, clarsimp)
schirmer@12854
   549
apply   (erule MGFn_InitD [THEN conseq2])
schirmer@12854
   550
apply   (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   551
apply  clarsimp
schirmer@12854
   552
apply  (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   553
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   554
schirmer@12854
   555
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1")
schirmer@12854
   556
schirmer@12854
   557
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
schirmer@12854
   558
apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@13337
   559
apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
schirmer@13337
   560
schirmer@13337
   561
apply (rule ax_derivs.BinOp)
schirmer@13337
   562
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@13337
   563
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@13337
   564
schirmer@12854
   565
apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   566
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
schirmer@12854
   567
schirmer@12854
   568
apply (rule ax_derivs.Ass)
schirmer@12854
   569
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   570
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   571
schirmer@12854
   572
apply (rule ax_derivs.Cond)
schirmer@12854
   573
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   574
apply (rule allI)
schirmer@12854
   575
apply (rule ax_Normal_cases)
schirmer@12854
   576
prefer 2
schirmer@12854
   577
apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
schirmer@12854
   578
apply  (tactic "eval_Force_tac 1")
schirmer@12854
   579
apply (case_tac "b")
schirmer@12854
   580
apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   581
apply (simp, tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   582
schirmer@12854
   583
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init pid_field_type\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Body)
schirmer@12854
   584
 apply (erule MGFn_InitD [THEN conseq2])
schirmer@12854
   585
 apply (tactic "eval_Force_tac 1")
schirmer@12854
   586
apply (tactic "forw_hyp_tac 1")
schirmer@12854
   587
apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
schirmer@12854
   588
apply (erule (1) eval.Body)
schirmer@12854
   589
schirmer@13337
   590
apply (rule ax_derivs.InstInitE)
schirmer@13337
   591
schirmer@13337
   592
apply (rule ax_derivs.Callee)
schirmer@13337
   593
schirmer@12854
   594
apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   595
schirmer@12854
   596
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
schirmer@12854
   597
schirmer@12854
   598
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
schirmer@12854
   599
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   600
schirmer@12854
   601
apply (rule ax_derivs.Comp)
schirmer@12854
   602
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   603
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   604
schirmer@12854
   605
apply (rule ax_derivs.If)
schirmer@12854
   606
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   607
apply (rule allI)
schirmer@12854
   608
apply (rule ax_Normal_cases)
schirmer@12854
   609
prefer 2
schirmer@12854
   610
apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
schirmer@12854
   611
apply  (tactic "eval_Force_tac 1")
schirmer@12854
   612
apply (case_tac "b")
schirmer@12854
   613
apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   614
apply (simp, tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   615
schirmer@12854
   616
apply (rule ax_derivs.Do [THEN conseq1])
schirmer@12854
   617
apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *})
schirmer@12854
   618
schirmer@12854
   619
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
schirmer@12854
   620
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   621
schirmer@12854
   622
apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>In1r stmt1\<succ>\<rightarrow> (Y',s'') \<and> G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Try)
schirmer@12854
   623
apply   (tactic "eval_Force_tac 3")
schirmer@12854
   624
apply  (tactic "forw_hyp_eval_Force_tac 2")
schirmer@12854
   625
apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
schirmer@12854
   626
apply (tactic "clarsimp_tac eval_css 1")
schirmer@12854
   627
apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
schirmer@12854
   628
schirmer@13337
   629
apply (rule ax_derivs.FinA)
schirmer@12854
   630
schirmer@12854
   631
apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
schirmer@12854
   632
schirmer@12854
   633
apply (rule ax_derivs.Cons)
schirmer@12854
   634
apply  (erule MGFnD [THEN ax_NormalD])
schirmer@12854
   635
apply (tactic "forw_hyp_eval_Force_tac 1")
schirmer@12854
   636
done
schirmer@12854
   637
schirmer@12925
   638
lemma MGF_asm: 
schirmer@12925
   639
"\<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
   640
 \<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   641
apply (simp (no_asm_use) add: MGF_MGFn_iff)
schirmer@12854
   642
apply (rule allI)
schirmer@12854
   643
apply (rule MGFn_lemma)
schirmer@12854
   644
apply (intro strip)
schirmer@12854
   645
apply (rule MGFn_free_wt)
schirmer@12854
   646
apply (force dest: wt_Methd_is_methd)
schirmer@12925
   647
apply assumption (* wf_prog G *)
schirmer@12854
   648
done
schirmer@12854
   649
schirmer@12854
   650
declare splitI2 [intro!]
schirmer@12854
   651
ML_setup {*
schirmer@12854
   652
Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
schirmer@12854
   653
*}
schirmer@12854
   654
schirmer@12854
   655
schirmer@12854
   656
section "nested version"
schirmer@12854
   657
schirmer@12854
   658
lemma nesting_lemma' [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
schirmer@12854
   659
  !!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn}; 
schirmer@12854
   660
  !!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t};  
schirmer@12854
   661
          finite U; uA = mgf_call`U |] ==>  
schirmer@12854
   662
  !A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})"
schirmer@12854
   663
proof -
schirmer@12854
   664
  assume ax_derivs_asm:    "!!A ts. ts <= A ==> P A ts"
schirmer@12854
   665
  assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) 
schirmer@12854
   666
                                                  {mgf b} ==> P A {mgf_call pn}"
schirmer@12854
   667
  assume MGF_asm:          "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}"
schirmer@12854
   668
  assume "finite U" "uA = mgf_call`U"
schirmer@12854
   669
  then show ?thesis
schirmer@12854
   670
    apply -
schirmer@12854
   671
    apply (induct_tac "n")
schirmer@12854
   672
    apply  (tactic "ALLGOALS Clarsimp_tac")
schirmer@12854
   673
    apply  (tactic "dtac (permute_prems 0 1 card_seteq) 1")
schirmer@12854
   674
    apply    simp
schirmer@12854
   675
    apply   (erule finite_imageI)
schirmer@12854
   676
    apply  (simp add: MGF_asm ax_derivs_asm)
schirmer@12854
   677
    apply (rule MGF_asm)
schirmer@12854
   678
    apply (rule ballI)
schirmer@12854
   679
    apply (case_tac "mgf_call pn : A")
schirmer@12854
   680
    apply  (fast intro: ax_derivs_asm)
schirmer@12854
   681
    apply (rule MGF_nested_Methd)
schirmer@12854
   682
    apply (rule ballI)
schirmer@12854
   683
    apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, 
schirmer@12854
   684
           erule_tac [4] spec)
schirmer@12854
   685
    apply   fast
schirmer@12854
   686
    apply  (erule Suc_leD)
schirmer@12854
   687
    apply (drule finite_subset)
schirmer@12854
   688
    apply (erule finite_imageI)
schirmer@12854
   689
    apply auto
schirmer@12854
   690
    apply arith
schirmer@12854
   691
  done
schirmer@12854
   692
qed
schirmer@12854
   693
schirmer@12854
   694
lemma nesting_lemma [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
schirmer@12854
   695
  !!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}; 
schirmer@12854
   696
          !!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}; 
schirmer@12854
   697
          finite U |] ==> P {} {mgf t}"
schirmer@12854
   698
proof -
schirmer@12854
   699
  assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}"
schirmer@12854
   700
  assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}"
schirmer@12854
   701
  assume "!!A ts. ts <= A ==> P A ts" "finite U"
schirmer@12854
   702
  then show ?thesis
schirmer@12854
   703
    apply -
schirmer@12854
   704
    apply (rule_tac mgf = "mgf" in nesting_lemma')
schirmer@12854
   705
    apply (erule_tac [2] 2)
schirmer@12854
   706
    apply (rule_tac [2] 3)
schirmer@12854
   707
    apply (rule_tac [6] le_refl)
schirmer@12854
   708
    apply auto
schirmer@12854
   709
  done
schirmer@12854
   710
qed
schirmer@12854
   711
schirmer@12854
   712
lemma MGF_nested_Methd: "\<lbrakk>  
schirmer@12854
   713
  G,insert ({Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}) A\<turnstile>  
schirmer@12854
   714
            {Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>}  
schirmer@12854
   715
 \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}"
schirmer@12854
   716
apply (unfold MGF_def)
schirmer@12854
   717
apply (rule ax_MethdN)
schirmer@12854
   718
apply (erule conseq2)
schirmer@12854
   719
apply clarsimp
schirmer@12854
   720
apply (erule MethdI)
schirmer@12854
   721
done
schirmer@12854
   722
schirmer@12925
   723
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   724
apply (rule MGFNormalI)
schirmer@12854
   725
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 
schirmer@12854
   726
                bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and 
schirmer@12854
   727
                f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma)
schirmer@12854
   728
apply    (erule ax_derivs.asm)
schirmer@12854
   729
apply   (clarsimp simp add: split_tupled_all)
schirmer@12854
   730
apply   (erule MGF_nested_Methd)
schirmer@12925
   731
apply  (erule_tac [2] finite_is_methd [OF wf_ws_prog])
schirmer@12854
   732
apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925
   733
apply (auto intro: MGFNormalI)
schirmer@12854
   734
done
schirmer@12854
   735
schirmer@12854
   736
schirmer@12854
   737
section "simultaneous version"
schirmer@12854
   738
schirmer@12854
   739
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
schirmer@12854
   740
  G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms  
schirmer@12854
   741
     |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>  
schirmer@12854
   742
  G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms"
schirmer@12854
   743
apply (unfold MGF_def)
schirmer@12854
   744
apply (rule ax_derivs.Methd [unfolded mtriples_def])
schirmer@12854
   745
apply (erule ax_finite_pointwise)
schirmer@12854
   746
prefer 2
schirmer@12854
   747
apply  (rule ax_derivs.asm)
schirmer@12854
   748
apply  fast
schirmer@12854
   749
apply clarsimp
schirmer@12854
   750
apply (rule conseq2)
schirmer@12854
   751
apply  (erule (1) ax_methods_spec)
schirmer@12854
   752
apply clarsimp
schirmer@12854
   753
apply (erule eval_Methd)
schirmer@12854
   754
done
schirmer@12854
   755
schirmer@12925
   756
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> 
schirmer@12854
   757
   G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) 
schirmer@12854
   758
   ` Collect (split (is_methd G)) "
schirmer@12925
   759
apply (frule finite_is_methd [OF wf_ws_prog])
schirmer@12854
   760
apply (rule MGF_simult_Methd_lemma)
schirmer@12854
   761
apply  assumption
schirmer@12854
   762
apply (erule ax_finite_pointwise)
schirmer@12854
   763
prefer 2
schirmer@12854
   764
apply  (rule ax_derivs.asm)
schirmer@12854
   765
apply  blast
schirmer@12854
   766
apply clarsimp
schirmer@12854
   767
apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925
   768
apply   (auto intro: MGFNormalI)
schirmer@12854
   769
done
schirmer@12854
   770
schirmer@12925
   771
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854
   772
apply (rule MGF_asm)
schirmer@12854
   773
apply (intro strip)
schirmer@12854
   774
apply (rule MGFNormalI)
schirmer@12854
   775
apply (rule ax_derivs.weaken)
schirmer@12854
   776
apply  (erule MGF_simult_Methd)
schirmer@12925
   777
apply auto
schirmer@12854
   778
done
schirmer@12854
   779
schirmer@12854
   780
schirmer@12854
   781
section "corollaries"
schirmer@12854
   782
schirmer@12925
   783
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
   784
 \<Longrightarrow>   \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
schirmer@12925
   785
apply (cases "normal s")
schirmer@12925
   786
apply   (force simp add: type_ok_def intro: eval_evaln)
schirmer@12925
   787
apply   (force intro: evaln.Abrupt)
schirmer@12925
   788
done
schirmer@12925
   789
schirmer@12925
   790
lemma MGF_complete: 
schirmer@12925
   791
 "\<lbrakk>G,{}\<Turnstile>{P} t\<succ> {Q}; G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk> 
schirmer@12925
   792
  \<Longrightarrow> G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
schirmer@12854
   793
apply (rule ax_no_hazard)
schirmer@12854
   794
apply (unfold MGF_def)
schirmer@12854
   795
apply (erule conseq12)
schirmer@12854
   796
apply (simp (no_asm_use) add: ax_valids_def triple_valid_def)
schirmer@12925
   797
apply (blast dest: eval_to_evaln)
schirmer@12854
   798
done
schirmer@12854
   799
schirmer@12925
   800
theorem ax_complete: "wf_prog G \<Longrightarrow>  
schirmer@12854
   801
  G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
schirmer@12854
   802
apply (erule MGF_complete)
schirmer@12925
   803
apply (erule (1) MGF_deriv)
schirmer@12854
   804
done
schirmer@12854
   805
schirmer@12854
   806
end