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