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