src/HOL/Bali/AxCompl.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/AxCompl.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {*
     8 Completeness proof for Axiomatic semantics of Java expressions and statements
     9 *}
    10 
    11 theory AxCompl = AxSem:
    12 
    13 text {*
    14 design issues:
    15 \begin{itemize}
    16 \item proof structured by Most General Formulas (-> Thomas Kleymann)
    17 \end{itemize}
    18 *}
    19 section "set of not yet initialzed classes"
    20 
    21 constdefs
    22 
    23   nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
    24  "nyinitcls G s \<equiv> {C. is_class G C \<and> \<not> initd C s}"
    25 
    26 lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
    27 apply (unfold nyinitcls_def)
    28 apply fast
    29 done
    30 
    31 lemmas finite_nyinitcls [simp] =
    32    finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
    33 
    34 lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
    35 apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
    36 done
    37 
    38 lemma nyinitcls_set_locals_cong [simp]: 
    39   "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
    40 apply (unfold nyinitcls_def)
    41 apply (simp (no_asm))
    42 done
    43 
    44 lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
    45 apply (unfold nyinitcls_def)
    46 apply (simp (no_asm))
    47 done
    48 
    49 lemma nyinitcls_abupd_cong [simp]:"!!s. nyinitcls G (abupd f s) = nyinitcls G s"
    50 apply (unfold nyinitcls_def)
    51 apply (simp (no_asm_simp) only: split_tupled_all)
    52 apply (simp (no_asm))
    53 done
    54 
    55 lemma card_nyinitcls_abrupt_congE [elim!]: 
    56         "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
    57 apply (unfold nyinitcls_def)
    58 apply auto
    59 done
    60 
    61 lemma nyinitcls_new_xcpt_var [simp]: 
    62 "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
    63 apply (unfold nyinitcls_def)
    64 apply (induct_tac "s")
    65 apply (simp (no_asm))
    66 done
    67 
    68 lemma nyinitcls_init_lvars [simp]: 
    69   "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
    70 apply (induct_tac "s")
    71 apply (simp (no_asm) add: init_lvars_def2 split add: split_if)
    72 done
    73 
    74 lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
    75 apply (unfold nyinitcls_def)
    76 apply fast
    77 done
    78 
    79 lemma card_Suc_lemma: "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
    80 apply (rotate_tac 1)
    81 apply clarsimp
    82 done
    83 
    84 lemma nyinitcls_le_SucD: 
    85 "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
    86   card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
    87 apply (subgoal_tac 
    88         "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
    89 apply  clarsimp
    90 apply  (erule thin_rl)
    91 apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
    92 apply   (auto dest!: not_initedD elim!: 
    93               simp add: nyinitcls_def inited_def split add: split_if_asm)
    94 done
    95 
    96 ML {* bind_thm("inited_gext'",permute_prems 0 1 (thm "inited_gext")) *}
    97 
    98 lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
    99 apply (unfold nyinitcls_def)
   100 apply (force dest!: inited_gext')
   101 done
   102 
   103 lemma card_nyinitcls_gext: 
   104   "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
   105 apply (rule le_trans)
   106 apply  (rule card_mono)
   107 apply   (rule finite_nyinitcls)
   108 apply  (erule nyinitcls_gext)
   109 apply assumption
   110 done
   111 
   112 
   113 section "init-le"
   114 
   115 constdefs
   116   init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"            ("_\<turnstile>init\<le>_"  [51,51] 50)
   117  "G\<turnstile>init\<le>n \<equiv> \<lambda>s. card (nyinitcls G s) \<le> n"
   118   
   119 lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
   120 apply (unfold init_le_def)
   121 apply auto
   122 done
   123 
   124 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}"
   125 apply (drule spec)
   126 apply (erule conseq1)
   127 apply clarsimp
   128 apply (rule card_nyinitcls_bound)
   129 done
   130 
   131 section "Most General Triples and Formulas"
   132 
   133 constdefs
   134 
   135   remember_init_state :: "state assn"                ("\<doteq>")
   136   "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
   137 
   138 lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
   139 apply (unfold remember_init_state_def)
   140 apply (simp (no_asm))
   141 done
   142 
   143 consts
   144   
   145   MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
   146   MGFn::"[nat       , term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
   147 
   148 defs
   149   
   150 
   151   MGF_def:
   152   "{P} t\<succ> {G\<rightarrow>} \<equiv> {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
   153 
   154   MGFn_def:
   155   "{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
   156 
   157 (* unused *)
   158 lemma MGF_valid: "G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
   159 apply (unfold MGF_def)
   160 apply (force dest!: evaln_eval simp add: ax_valids_def triple_valid_def2)
   161 done
   162 
   163 lemma MGF_res_eq_lemma [simp]: 
   164   "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
   165 apply auto
   166 done
   167 
   168 lemma MGFn_def2: 
   169 "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
   170                     t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
   171 apply (unfold MGFn_def MGF_def)
   172 apply fast
   173 done
   174 
   175 lemma MGF_MGFn_iff: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
   176 apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
   177 apply safe
   178 apply  (erule_tac [2] All_init_leD)
   179 apply (erule conseq1)
   180 apply clarsimp
   181 done
   182 
   183 lemma MGFnD: 
   184 "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
   185  G,A\<turnstile>{(\<lambda>Y' s' s. s' = s           \<and> P s) \<and>. G\<turnstile>init\<le>n}  
   186  t\<succ>  {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}"
   187 apply (unfold init_le_def)
   188 apply (simp (no_asm_use) add: MGFn_def2)
   189 apply (erule conseq12)
   190 apply clarsimp
   191 apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
   192 done
   193 lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
   194 
   195 lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
   196   G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
   197 apply (unfold MGF_def)
   198 apply (rule ax_Normal_cases)
   199 apply  (erule conseq1)
   200 apply  clarsimp
   201 apply (rule ax_derivs.Abrupt [THEN conseq1])
   202 apply (clarsimp simp add: Let_def)
   203 done
   204 
   205 lemma MGFNormalD: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
   206 apply (unfold MGF_def)
   207 apply (erule conseq1)
   208 apply clarsimp
   209 done
   210 
   211 lemma MGFn_NormalI: 
   212 "G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ> 
   213  {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
   214 apply (simp (no_asm_use) add: MGFn_def2)
   215 apply (rule ax_Normal_cases)
   216 apply  (erule conseq1)
   217 apply  clarsimp
   218 apply (rule ax_derivs.Abrupt [THEN conseq1])
   219 apply (clarsimp simp add: Let_def)
   220 done
   221 
   222 lemma MGFn_free_wt: 
   223   "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
   224     \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
   225    \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
   226 apply (rule MGFn_NormalI)
   227 apply (rule ax_free_wt)
   228 apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
   229 done
   230 
   231 
   232 section "main lemmas"
   233 
   234 declare fun_upd_apply [simp del]
   235 declare splitI2 [rule del] (*prevents ugly renaming of state variables*)
   236 
   237 ML_setup {* 
   238 Delsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
   239 *} (*prevents modifying rhs of MGF*)
   240 ML {*
   241 val eval_css = (claset() delrules [thm "eval.Abrupt"] addSIs (thms "eval.intros") 
   242                 delrules[thm "eval.Expr", thm "eval.Init", thm "eval.Try"] 
   243                 addIs   [thm "eval.Expr", thm "eval.Init"]
   244                 addSEs[thm "eval.Try"] delrules[equalityCE],
   245                 simpset() addsimps [split_paired_all,Let_def]
   246  addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]);
   247 val eval_Force_tac = force_tac eval_css;
   248 
   249 val wt_prepare_tac = EVERY'[
   250     rtac (thm "MGFn_free_wt"),
   251     clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
   252 val compl_prepare_tac = EVERY'[rtac (thm "MGFn_NormalI"), Simp_tac]
   253 val forw_hyp_tac = EVERY'[etac (thm "MGFnD'" RS thm "conseq12"), Clarsimp_tac]
   254 val forw_hyp_eval_Force_tac = 
   255          EVERY'[TRY o rtac allI, forw_hyp_tac, eval_Force_tac]
   256 *}
   257 
   258 lemma MGFn_Init: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow>  
   259   G,(A::state triple set)\<turnstile>{=:n} In1r (Init C)\<succ> {G\<rightarrow>}"
   260 apply (tactic "wt_prepare_tac 1")
   261 (* requires is_class G C two times for nyinitcls *)
   262 apply (tactic "compl_prepare_tac 1")
   263 apply (rule_tac C = "initd C" in ax_cases)
   264 apply  (rule ax_derivs.Done [THEN conseq1])
   265 apply  (clarsimp intro!: init_done)
   266 apply (rule_tac y = n in nat.exhaust, clarsimp)
   267 apply  (rule ax_impossible [THEN conseq1])
   268 apply  (force dest!: nyinitcls_emptyD)
   269 apply clarsimp
   270 apply (drule_tac x = "nat" in spec)
   271 apply clarsimp
   272 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)
   273 apply   simp
   274 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)
   275 prefer 2
   276 apply   (force elim!: nyinitcls_le_SucD)
   277 apply  (simp split add: split_if, rule conjI, clarify)
   278 apply   (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
   279 apply  clarify
   280 apply  (drule spec)
   281 apply  (erule MGFnD' [THEN conseq12])
   282 apply  (tactic "force_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
   283 apply (rule allI)
   284 apply (drule spec)
   285 apply (erule MGFnD' [THEN conseq12])
   286 apply clarsimp
   287 apply (tactic {* pair_tac "sa" 1 *})
   288 apply (tactic"clarsimp_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
   289 apply (rule eval_Init, force+)
   290 done
   291 lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
   292 
   293 lemma MGFn_Call: 
   294 "\<lbrakk>\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};  
   295   G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>}\<rbrakk> \<Longrightarrow>  
   296   G,A\<turnstile>{=:n} In1l ({statT,mode}e\<cdot>mn({pTs'}ps))\<succ> {G\<rightarrow>}"
   297 apply (tactic "wt_prepare_tac 1") (* required for equating mode = invmode m e *)
   298 apply (tactic "compl_prepare_tac 1")
   299 apply (rule_tac R = "\<lambda>a'. (\<lambda>Y (x2,s2) (x,s) . x = None \<and> (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a'\<rightarrow> s1 \<and> Y = In3 pvs \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Call)
   300 apply  (erule MGFnD [THEN ax_NormalD])
   301 apply safe
   302 apply  (erule_tac V = "All ?P" in thin_rl, tactic "forw_hyp_eval_Force_tac 1")
   303 apply (drule spec, drule spec)
   304 apply (erule MGFnD' [THEN conseq12])
   305 apply (tactic "clarsimp_tac eval_css 1")
   306 apply (erule (1) eval_Call)
   307 apply   (rule HOL.refl)
   308 apply  (simp (no_asm_simp))+
   309 done
   310 
   311 lemma MGF_altern: "G,A\<turnstile>{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} =  
   312  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)} 
   313   t\<succ> {\<lambda>Y s Z. (Y,s) = Z}"
   314 apply (unfold MGF_def)
   315 apply (auto del: conjI elim!: conseq12)
   316 apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
   317 apply  (fast dest: unique_eval)
   318 apply clarsimp
   319 apply (erule thin_rl)
   320 apply (erule thin_rl)
   321 apply (drule split_paired_All [THEN subst])
   322 apply (clarsimp elim!: state_not_single)
   323 done
   324 
   325 
   326 lemma MGFn_Loop: 
   327 "\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk> 
   328 \<Longrightarrow> 
   329   G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}"
   330 apply (rule MGFn_NormalI, simp)
   331 apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in 
   332           MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1])
   333 prefer 2
   334 apply  clarsimp
   335 apply (rule_tac P' = 
   336 "((\<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) 
   337   \<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12)
   338 prefer 2
   339 apply  clarsimp
   340 apply  (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl)
   341 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)
   342 apply   (force dest!: eval.Loop split add: split_if_asm)
   343 prefer 2
   344 apply  (erule MGFnD' [THEN conseq12])
   345 apply  clarsimp
   346 apply  (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl)
   347 apply  (tactic "eval_Force_tac 1")
   348 apply (erule MGFnD' [THEN conseq12] , clarsimp)
   349 apply (rule conjI, erule exI)
   350 apply (tactic "clarsimp_tac eval_css 1")
   351 apply (case_tac "a")
   352 prefer 2
   353 apply  (clarsimp)
   354 apply (clarsimp split add: split_if)
   355 apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"],
   356   simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+)
   357 done
   358 
   359 lemma MGFn_lemma [rule_format (no_asm)]: 
   360  "\<forall>n C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow>  
   361   \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
   362 apply (rule full_nat_induct)
   363 apply (rule allI)
   364 apply (drule_tac x = n in spec)
   365 apply (drule_tac psi = "All ?P" in asm_rl)
   366 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>}")
   367 apply  (tactic "Clarify_tac 2")
   368 apply  (induct_tac "t")
   369 apply    (induct_tac "a")
   370 apply     fast+
   371 apply (rule var_expr_stmt.induct)
   372 (* 28 subgoals *)
   373 prefer 14 apply fast (* Methd *)
   374 prefer 13 apply (erule (2) MGFn_Call)
   375 apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
   376 apply (erule_tac [24] MGFn_Init)
   377 prefer 19 apply (erule (1) MGFn_Loop)
   378 apply (tactic "ALLGOALS compl_prepare_tac")
   379 
   380 apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
   381 
   382 apply (rule ax_derivs.FVar)
   383 apply  (erule MGFn_InitD)
   384 apply (tactic "forw_hyp_eval_Force_tac 1")
   385 
   386 apply (rule ax_derivs.AVar)
   387 apply  (erule MGFnD [THEN ax_NormalD])
   388 apply (tactic "forw_hyp_eval_Force_tac 1")
   389 
   390 apply (rule ax_derivs.NewC)
   391 apply (erule MGFn_InitD [THEN conseq2])
   392 apply (tactic "eval_Force_tac 1")
   393 
   394 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)
   395 apply  (simp add: init_comp_ty_def split add: split_if)
   396 apply   (rule conjI, clarsimp)
   397 apply   (erule MGFn_InitD [THEN conseq2])
   398 apply   (tactic "clarsimp_tac eval_css 1")
   399 apply  clarsimp
   400 apply  (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
   401 apply (tactic "forw_hyp_eval_Force_tac 1")
   402 
   403 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1")
   404 
   405 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
   406 apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
   407 apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
   408 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
   409 
   410 apply (rule ax_derivs.Ass)
   411 apply  (erule MGFnD [THEN ax_NormalD])
   412 apply (tactic "forw_hyp_eval_Force_tac 1")
   413 
   414 apply (rule ax_derivs.Cond)
   415 apply  (erule MGFnD [THEN ax_NormalD])
   416 apply (rule allI)
   417 apply (rule ax_Normal_cases)
   418 prefer 2
   419 apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
   420 apply  (tactic "eval_Force_tac 1")
   421 apply (case_tac "b")
   422 apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
   423 apply (simp, tactic "forw_hyp_eval_Force_tac 1")
   424 
   425 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)
   426  apply (erule MGFn_InitD [THEN conseq2])
   427  apply (tactic "eval_Force_tac 1")
   428 apply (tactic "forw_hyp_tac 1")
   429 apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
   430 apply (erule (1) eval.Body)
   431 
   432 apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
   433 
   434 apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
   435 
   436 apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
   437 apply (tactic "clarsimp_tac eval_css 1")
   438 
   439 apply (rule ax_derivs.Comp)
   440 apply  (erule MGFnD [THEN ax_NormalD])
   441 apply (tactic "forw_hyp_eval_Force_tac 1")
   442 
   443 apply (rule ax_derivs.If)
   444 apply  (erule MGFnD [THEN ax_NormalD])
   445 apply (rule allI)
   446 apply (rule ax_Normal_cases)
   447 prefer 2
   448 apply  (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
   449 apply  (tactic "eval_Force_tac 1")
   450 apply (case_tac "b")
   451 apply  (simp, tactic "forw_hyp_eval_Force_tac 1")
   452 apply (simp, tactic "forw_hyp_eval_Force_tac 1")
   453 
   454 apply (rule ax_derivs.Do [THEN conseq1])
   455 apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *})
   456 
   457 apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
   458 apply (tactic "clarsimp_tac eval_css 1")
   459 
   460 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)
   461 apply   (tactic "eval_Force_tac 3")
   462 apply  (tactic "forw_hyp_eval_Force_tac 2")
   463 apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
   464 apply (tactic "clarsimp_tac eval_css 1")
   465 apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
   466 
   467 apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
   468 apply  (tactic "forw_hyp_eval_Force_tac 1")
   469 apply (rule allI)
   470 apply (tactic "forw_hyp_tac 1")
   471 apply (tactic {* pair_tac "sb" 1 *})
   472 apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
   473 apply (drule (1) eval.Fin)
   474 apply clarsimp
   475 
   476 apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
   477 
   478 apply (rule ax_derivs.Cons)
   479 apply  (erule MGFnD [THEN ax_NormalD])
   480 apply (tactic "forw_hyp_eval_Force_tac 1")
   481 done
   482 
   483 lemma MGF_asm: "\<forall>C sig. is_methd G C sig \<longrightarrow> G,A\<turnstile>{\<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow>
   484   G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
   485 apply (simp (no_asm_use) add: MGF_MGFn_iff)
   486 apply (rule allI)
   487 apply (rule MGFn_lemma)
   488 apply (intro strip)
   489 apply (rule MGFn_free_wt)
   490 apply (force dest: wt_Methd_is_methd)
   491 done
   492 
   493 declare splitI2 [intro!]
   494 ML_setup {*
   495 Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
   496 *}
   497 
   498 
   499 section "nested version"
   500 
   501 lemma nesting_lemma' [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
   502   !!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn}; 
   503   !!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t};  
   504           finite U; uA = mgf_call`U |] ==>  
   505   !A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})"
   506 proof -
   507   assume ax_derivs_asm:    "!!A ts. ts <= A ==> P A ts"
   508   assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A) 
   509                                                   {mgf b} ==> P A {mgf_call pn}"
   510   assume MGF_asm:          "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}"
   511   assume "finite U" "uA = mgf_call`U"
   512   then show ?thesis
   513     apply -
   514     apply (induct_tac "n")
   515     apply  (tactic "ALLGOALS Clarsimp_tac")
   516     apply  (tactic "dtac (permute_prems 0 1 card_seteq) 1")
   517     apply    simp
   518     apply   (erule finite_imageI)
   519     apply  (simp add: MGF_asm ax_derivs_asm)
   520     apply (rule MGF_asm)
   521     apply (rule ballI)
   522     apply (case_tac "mgf_call pn : A")
   523     apply  (fast intro: ax_derivs_asm)
   524     apply (rule MGF_nested_Methd)
   525     apply (rule ballI)
   526     apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] impE, 
   527            erule_tac [4] spec)
   528     apply   fast
   529     apply  (erule Suc_leD)
   530     apply (drule finite_subset)
   531     apply (erule finite_imageI)
   532     apply auto
   533     apply arith
   534   done
   535 qed
   536 
   537 lemma nesting_lemma [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts; 
   538   !!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}; 
   539           !!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}; 
   540           finite U |] ==> P {} {mgf t}"
   541 proof -
   542   assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}"
   543   assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}"
   544   assume "!!A ts. ts <= A ==> P A ts" "finite U"
   545   then show ?thesis
   546     apply -
   547     apply (rule_tac mgf = "mgf" in nesting_lemma')
   548     apply (erule_tac [2] 2)
   549     apply (rule_tac [2] 3)
   550     apply (rule_tac [6] le_refl)
   551     apply auto
   552   done
   553 qed
   554 
   555 lemma MGF_nested_Methd: "\<lbrakk>  
   556   G,insert ({Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}) A\<turnstile>  
   557             {Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>}  
   558  \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal \<doteq>} In1l (Methd  C sig) \<succ>{G\<rightarrow>}"
   559 apply (unfold MGF_def)
   560 apply (rule ax_MethdN)
   561 apply (erule conseq2)
   562 apply clarsimp
   563 apply (erule MethdI)
   564 done
   565 
   566 lemma MGF_deriv: "ws_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
   567 apply (rule MGFNormalI)
   568 apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 
   569                 bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and 
   570                 f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma)
   571 apply    (erule ax_derivs.asm)
   572 apply   (clarsimp simp add: split_tupled_all)
   573 apply   (erule MGF_nested_Methd)
   574 apply  (erule_tac [2] finite_is_methd)
   575 apply (rule MGF_asm [THEN MGFNormalD])
   576 apply clarify
   577 apply (rule MGFNormalI)
   578 apply force
   579 done
   580 
   581 
   582 section "simultaneous version"
   583 
   584 lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
   585   G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms  
   586      |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>  
   587   G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) ` ms"
   588 apply (unfold MGF_def)
   589 apply (rule ax_derivs.Methd [unfolded mtriples_def])
   590 apply (erule ax_finite_pointwise)
   591 prefer 2
   592 apply  (rule ax_derivs.asm)
   593 apply  fast
   594 apply clarsimp
   595 apply (rule conseq2)
   596 apply  (erule (1) ax_methods_spec)
   597 apply clarsimp
   598 apply (erule eval_Methd)
   599 done
   600 
   601 lemma MGF_simult_Methd: "ws_prog G \<Longrightarrow> 
   602    G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) 
   603    ` Collect (split (is_methd G)) "
   604 apply (frule finite_is_methd)
   605 apply (rule MGF_simult_Methd_lemma)
   606 apply  assumption
   607 apply (erule ax_finite_pointwise)
   608 prefer 2
   609 apply  (rule ax_derivs.asm)
   610 apply  blast
   611 apply clarsimp
   612 apply (rule MGF_asm [THEN MGFNormalD])
   613 apply clarify
   614 apply (rule MGFNormalI)
   615 apply force
   616 done
   617 
   618 lemma MGF_deriv: "ws_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
   619 apply (rule MGF_asm)
   620 apply (intro strip)
   621 apply (rule MGFNormalI)
   622 apply (rule ax_derivs.weaken)
   623 apply  (erule MGF_simult_Methd)
   624 apply force
   625 done
   626 
   627 
   628 section "corollaries"
   629 
   630 lemma MGF_complete: "G,{}\<Turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>
   631   G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
   632 apply (rule ax_no_hazard)
   633 apply (unfold MGF_def)
   634 apply (erule conseq12)
   635 apply (simp (no_asm_use) add: ax_valids_def triple_valid_def)
   636 apply (fast dest!: eval_evaln)
   637 done
   638 
   639 theorem ax_complete: "ws_prog G \<Longrightarrow>  
   640   G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
   641 apply (erule MGF_complete)
   642 apply (erule MGF_deriv)
   643 done
   644 
   645 end