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