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