--- a/src/HOL/Bali/AxCompl.thy Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/AxCompl.thy Thu Oct 31 18:27:10 2002 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Bali/AxCompl.thy
ID: $Id$
- Author: David von Oheimb
+ Author: David von Oheimb and Norbert Schirmer
License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
@@ -19,6 +19,7 @@
+
section "set of not yet initialzed classes"
constdefs
@@ -79,8 +80,8 @@
apply fast
done
-lemma card_Suc_lemma: "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
-apply (rotate_tac 1)
+lemma card_Suc_lemma:
+ "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
apply clarsimp
done
@@ -96,7 +97,8 @@
simp add: nyinitcls_def inited_def split add: split_if_asm)
done
-ML {* bind_thm("inited_gext'",permute_prems 0 1 (thm "inited_gext")) *}
+lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
+by (rule inited_gext)
lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
apply (unfold nyinitcls_def)
@@ -124,7 +126,9 @@
apply auto
done
-lemma All_init_leD: "\<forall>n::nat. G,A\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
+lemma All_init_leD:
+ "\<forall>n::nat. G,(A::'a triple set)\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q::'a assn}
+ \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
apply (drule spec)
apply (erule conseq1)
apply clarsimp
@@ -158,7 +162,6 @@
"{=:n} t\<succ> {G\<rightarrow>} \<equiv> {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
(* unused *)
-
lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
apply (unfold MGF_def)
apply (simp add: ax_valids_def triple_valid_def2)
@@ -178,7 +181,8 @@
apply fast
done
-lemma MGF_MGFn_iff: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
+lemma MGF_MGFn_iff:
+"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
apply (simp (no_asm_use) add: MGFn_def2 MGF_def)
apply safe
apply (erule_tac [2] All_init_leD)
@@ -187,7 +191,7 @@
done
lemma MGFnD:
-"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>
+"G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>
G,A\<turnstile>{(\<lambda>Y' s' s. s' = s \<and> P s) \<and>. G\<turnstile>init\<le>n}
t\<succ> {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}"
apply (unfold init_le_def)
@@ -198,6 +202,10 @@
done
lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"]
+text {* To derive the most general formula, we can always assume a normal
+state in the precondition, since abrupt cases can be handled uniformally by
+the abrupt rule.
+*}
lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>
G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
apply (unfold MGF_def)
@@ -208,12 +216,15 @@
apply (clarsimp simp add: Let_def)
done
-lemma MGFNormalD: "G,A\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
+lemma MGFNormalD:
+"G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
apply (unfold MGF_def)
apply (erule conseq1)
apply clarsimp
done
+text {* Additionally to @{text MGFNormalI}, we also expand the definition of
+the most general formula here *}
lemma MGFn_NormalI:
"G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ>
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
@@ -225,6 +236,9 @@
apply (clarsimp simp add: Let_def)
done
+text {* To derive the most general formula, we can restrict ourselves to
+welltyped terms, since all others can be uniformally handled by the hazard
+rule. *}
lemma MGFn_free_wt:
"(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T)
\<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>}
@@ -234,8 +248,12 @@
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
done
+text {* To derive the most general formula, we can restrict ourselves to
+welltyped terms and assume that the state in the precondition conforms to the
+environment. All type violations can be uniformally handled by the hazard
+rule. *}
lemma MGFn_free_wt_NormalConformI:
-"(\<forall> T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
+"(\<forall> T L C . \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
\<longrightarrow> G,(A::state triple set)
\<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))}
t\<succ>
@@ -247,389 +265,1129 @@
apply (intro strip)
apply (simp only: type_ok_def peek_and_def)
apply (erule conjE)+
-apply (erule exE,erule exE, erule exE,erule conjE,drule (1) mp)
+apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
+ erule conjE)
apply (drule spec,drule spec, drule spec, drule (1) mp)
apply (erule conseq12)
apply blast
done
+text {* To derive the most general formula, we can restrict ourselves to
+welltyped terms and assume that the state in the precondition conforms to the
+environment and that the term is definetly assigned with respect to this state.
+All type violations can be uniformally handled by the hazard rule. *}
+lemma MGFn_free_wt_da_NormalConformI:
+"(\<forall> T L C B. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
+ \<longrightarrow> G,(A::state triple set)
+ \<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))
+ \<and>. (\<lambda> s. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>B)}
+ t\<succ>
+ {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')})
+ \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
+apply (rule MGFn_NormalI)
+apply (rule ax_no_hazard)
+apply (rule ax_escape)
+apply (intro strip)
+apply (simp only: type_ok_def peek_and_def)
+apply (erule conjE)+
+apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
+ erule conjE)
+apply (drule spec,drule spec, drule spec,drule spec, drule (1) mp)
+apply (erule conseq12)
+apply blast
+done
section "main lemmas"
-declare fun_upd_apply [simp del]
-declare splitI2 [rule del] (*prevents ugly renaming of state variables*)
-
-ML_setup {*
-Delsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
-*} (*prevents modifying rhs of MGF*)
-ML {*
-val eval_css = (claset() delrules [thm "eval.Abrupt"] addSIs (thms "eval.intros")
- delrules[thm "eval.Expr", thm "eval.Init", thm "eval.Try"]
- addIs [thm "eval.Expr", thm "eval.Init"]
- addSEs[thm "eval.Try"] delrules[equalityCE],
- simpset() addsimps [split_paired_all,Let_def]
- addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]);
-val eval_Force_tac = force_tac eval_css;
-
-val wt_prepare_tac = EVERY'[
- rtac (thm "MGFn_free_wt"),
- clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
-val compl_prepare_tac = EVERY'[rtac (thm "MGFn_NormalI"), Simp_tac]
-val wt_conf_prepare_tac = EVERY'[
- rtac (thm "MGFn_free_wt_NormalConformI"),
- clarsimp_tac (claset() addSEs (thms "wt_elim_cases"), simpset())]
-val forw_hyp_tac = EVERY'[etac (thm "MGFnD'" RS thm "conseq12"), Clarsimp_tac]
-val forw_hyp_eval_Force_tac =
- EVERY'[TRY o rtac allI, forw_hyp_tac, eval_Force_tac]
-*}
-
-lemma MGFn_Init: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow>
- G,(A::state triple set)\<turnstile>{=:n} In1r (Init C)\<succ> {G\<rightarrow>}"
-apply (tactic "wt_prepare_tac 1")
-(* requires is_class G C two times for nyinitcls *)
-apply (tactic "compl_prepare_tac 1")
-apply (rule_tac C = "initd C" in ax_cases)
-apply (rule ax_derivs.Done [THEN conseq1])
-apply (clarsimp intro!: init_done)
-apply (rule_tac y = n in nat.exhaust, clarsimp)
-apply (rule ax_impossible [THEN conseq1])
-apply (force dest!: nyinitcls_emptyD)
-apply clarsimp
-apply (drule_tac x = "nat" in spec)
-apply clarsimp
-apply (rule_tac Q = " (\<lambda>Y s' (x,s) . G\<turnstile> (x,init_class_obj G C s) \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s' \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>nat" in ax_derivs.Init)
-apply simp
-apply (rule_tac P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>nat) " in conseq1)
-prefer 2
-apply (force elim!: nyinitcls_le_SucD)
-apply (simp split add: split_if, rule conjI, clarify)
-apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
-apply clarify
-apply (drule spec)
-apply (erule MGFnD' [THEN conseq12])
-apply (tactic "force_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
-apply (rule allI)
-apply (drule spec)
-apply (erule MGFnD' [THEN conseq12])
-apply clarsimp
-apply (tactic {* pair_tac "sa" 1 *})
-apply (tactic"clarsimp_tac (claset(), simpset() addsimprocs[eval_stmt_proc]) 1")
-apply (rule eval_Init, force+)
-done
+lemma MGFn_Init:
+ assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
+ shows "G,(A::state triple set)\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI)
+ fix T L accC
+ assume "\<lparr>prg=G, cls=accC, lcl= L\<rparr>\<turnstile>\<langle>Init C\<rangle>\<^sub>s\<Colon>T"
+ hence is_cls: "is_class G C"
+ by cases simp
+ show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}
+ .Init C.
+ {\<lambda>Y s' s. G\<turnstile>s \<midarrow>\<langle>Init C\<rangle>\<^sub>s\<succ>\<rightarrow> (Y, s')}"
+ (is "G,A\<turnstile>{Normal ?P} .Init C. {?R}")
+ proof (rule ax_cases [where ?C="initd C"])
+ show "G,A\<turnstile>{Normal ?P \<and>. initd C} .Init C. {?R}"
+ by (rule ax_derivs.Done [THEN conseq1]) (fastsimp intro: init_done)
+ next
+ have "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C)} .Init C. {?R}"
+ proof (cases n)
+ case 0
+ with is_cls
+ show ?thesis
+ by - (rule ax_impossible [THEN conseq1],fastsimp dest: nyinitcls_emptyD)
+ next
+ case (Suc m)
+ with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
+ by simp
+ from is_cls obtain c where c: "the (class G C) = c"
+ by auto
+ let ?Q= "(\<lambda>Y s' (x,s) .
+ G\<turnstile> (x,init_class_obj G C s)
+ \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s'
+ \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>m"
+ from c
+ show ?thesis
+ proof (rule ax_derivs.Init [where ?Q="?Q"])
+ let ?P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s
+ \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>m)"
+ show "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
+ .(if C = Object then Skip else Init (super c)).
+ {?Q}"
+ proof (rule conseq1 [where ?P'="?P'"])
+ show "G,A\<turnstile>{?P'} .(if C = Object then Skip else Init (super c)). {?Q}"
+ proof (cases "C=Object")
+ case True
+ have "G,A\<turnstile>{?P'} .Skip. {?Q}"
+ by (rule ax_derivs.Skip [THEN conseq1])
+ (auto simp add: True intro: eval.Skip)
+ with True show ?thesis
+ by simp
+ next
+ case False
+ from mgf_hyp'
+ have "G,A\<turnstile>{?P'} .Init (super c). {?Q}"
+ by (rule MGFnD' [THEN conseq12]) (fastsimp simp add: False c)
+ with False show ?thesis
+ by simp
+ qed
+ next
+ from Suc is_cls
+ show "Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))
+ \<Rightarrow> ?P'"
+ by (fastsimp elim: nyinitcls_le_SucD)
+ qed
+ next
+ from mgf_hyp'
+ show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
+ .init c.
+ {set_lvars l .; ?R}"
+ apply (rule MGFnD' [THEN conseq12, THEN allI])
+ apply (clarsimp simp add: split_paired_all)
+ apply (rule eval.Init [OF c])
+ apply (insert c)
+ apply auto
+ done
+ qed
+ qed
+ thus "G,A\<turnstile>{Normal ?P \<and>. Not \<circ> initd C} .Init C. {?R}"
+ by clarsimp
+ qed
+qed
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
-text {* For @{text MGFn_Call} we need the wellformedness of the program to
-switch from the evaln-semantics to the eval-semantics *}
lemma MGFn_Call:
-"\<lbrakk>\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};
- G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>};wf_prog G\<rbrakk> \<Longrightarrow>
- G,A\<turnstile>{=:n} In1l ({accC,statT,mode}e\<cdot>mn({pTs'}ps))\<succ> {G\<rightarrow>}"
-apply (tactic "wt_conf_prepare_tac 1")
-apply (rule_tac
- Q="(\<lambda>Y s1 (x,s) . x = None \<and>
- (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
- \<and> Y = In1 a))
- \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" and
- R = "\<lambda>a'. (\<lambda>Y (x2,s2) (x,s) . x = None \<and>
- (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a'\<rightarrow> s1 \<and>
- (normal s1 \<longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT)\<and>
- Y = In3 pvs \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2)))
- \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))" in ax_derivs.Call)
-apply (tactic "forw_hyp_tac 1")
-apply (tactic "clarsimp_tac eval_css 1")
-apply (frule (3) eval_type_sound)
-apply force
-
-apply safe
-apply (tactic "forw_hyp_tac 1")
-apply (tactic "clarsimp_tac eval_css 1")
-apply (frule (3) eval_type_sound)
-apply (rule conjI)
-apply (rule exI,rule conjI)
-apply (assumption)
-
-apply (rule conjI)
-apply simp
-apply assumption
-apply blast
+ assumes mgf_methds:
+ "\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>(Methd C sig)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ and mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ and mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
+ and wf: "wf_prog G"
+ shows "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
+ note inj_term_simps [simp]
+ fix T L accC' E
+ 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"
+ then obtain pTs statDeclT statM where
+ wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
+ wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>ps\<Colon>\<doteq>pTs" and
+ statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr>
+ = {((statDeclT,statM),pTs')}" and
+ mode: "mode = invmode statM e" and
+ T: "T =Inl (resTy statM)" and
+ eq_accC_accC': "accC=accC'"
+ by cases fastsimp+
+ let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and>
+ (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
+ (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
+ \<and> Y = In1 a) \<and>
+ (\<exists> P. normal s1
+ \<longrightarrow> \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright>P))
+ \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))::state assn"
+ let ?R="\<lambda>a. ((\<lambda>Y (x2,s2) (x,s) . x = None \<and>
+ (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
+ (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)\<and>
+ Y = \<lfloor>pvs\<rfloor>\<^sub>l \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2)))
+ \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L)))::state assn"
-apply (drule spec, drule spec)
-apply (erule MGFnD' [THEN conseq12])
-apply (tactic "clarsimp_tac eval_css 1")
-apply (erule (1) eval_Call)
-apply (rule HOL.refl)+
-apply (subgoal_tac "check_method_access G C statT (invmode m e)
- \<lparr>name = mn, parTs = pTs'\<rparr> a
- (init_lvars G
- (invocation_declclass G (invmode m e) (snd (ab, ba)) a statT
- \<lparr>name = mn, parTs = pTs'\<rparr>)
- \<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs
- (ab,
- ba)) = (init_lvars G
- (invocation_declclass G (invmode m e) (snd (ab, ba)) a statT
- \<lparr>name = mn, parTs = pTs'\<rparr>)
- \<lparr>name = mn, parTs = pTs'\<rparr> (invmode m e) a vs
- (ab,
- ba))")
-apply simp
-defer
-apply simp
-apply (erule (3) error_free_call_access) (* now showing the subgoal *)
-apply auto
-done
+ show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
+ (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
+ (\<lambda>s. \<lparr>prg=G, cls=accC',lcl=L\<rparr> \<turnstile> dom (locals (store s))
+ \<guillemotright> \<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E))}
+ {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>
+ {\<lambda>Y s' s. \<exists>v. Y = \<lfloor>v\<rfloor>\<^sub>e \<and>
+ G\<turnstile>s \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v\<rightarrow> s'}"
+ (is "G,A\<turnstile>{Normal ?P} {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ> {?S}")
+ proof (rule ax_derivs.Call [where ?Q="?Q" and ?R="?R"])
+ from mgf_e
+ show "G,A\<turnstile>{Normal ?P} e-\<succ> {?Q}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s0 s1 a
+ assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
+ assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>
+ dom (locals s0) \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E"
+ assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
+ show "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
+ (abrupt s1 = None \<longrightarrow>
+ (\<exists>P. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P))
+ \<and> s1\<Colon>\<preceq>(G, L)"
+ proof -
+ from da obtain C where
+ da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
+ dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
+ da_ps: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> E"
+ by cases (simp add: eq_accC_accC')
+ from eval_e conf_s0 wt_e da_e wf
+ obtain "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT)"
+ and "s1\<Colon>\<preceq>(G, L)"
+ by (rule eval_type_soundE) simp
+ moreover
+ {
+ assume normal_s1: "normal s1"
+ have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
+ proof -
+ from eval_e wt_e da_e wf normal_s1
+ have "nrm C \<subseteq> dom (locals (store s1))"
+ by (cases rule: da_good_approxE') rules
+ with da_ps show ?thesis
+ by (rule da_weakenE) rules
+ qed
+ }
+ ultimately show ?thesis
+ using eq_accC_accC' by simp
+ qed
+ qed
+ next
+ show "\<forall>a. G,A\<turnstile>{?Q\<leftarrow>In1 a} ps\<doteq>\<succ> {?R a}" (is "\<forall> a. ?PS a")
+ proof
+ fix a
+ show "?PS a"
+ proof (rule MGFnD' [OF mgf_ps, THEN conseq12],
+ clarsimp simp add: eq_accC_accC' [symmetric])
+ fix s0 s1 s2 vs
+ assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
+ assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
+ assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
+ assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
+ assume da_ps: "abrupt s1 = None \<longrightarrow>
+ (\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
+ dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P)"
+ show "(\<exists>s1. G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
+ (abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
+ G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2) \<and>
+ s2\<Colon>\<preceq>(G, L)"
+ proof (cases "normal s1")
+ case True
+ with da_ps obtain P where
+ "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
+ by auto
+ from eval_ps conf_s1 wt_args this wf
+ have "s2\<Colon>\<preceq>(G, L)"
+ by (rule eval_type_soundE)
+ with eval_e conf_a eval_ps
+ show ?thesis
+ by auto
+ next
+ case False
+ with eval_ps have "s2=s1" by auto
+ with eval_e conf_a eval_ps conf_s1
+ show ?thesis
+ by auto
+ qed
+ qed
+ qed
+ next
+ show "\<forall>a vs invC declC l.
+ G,A\<turnstile>{?R a\<leftarrow>\<lfloor>vs\<rfloor>\<^sub>l \<and>.
+ (\<lambda>s. declC =
+ invocation_declclass G mode (store s) a statT
+ \<lparr>name=mn, parTs=pTs'\<rparr> \<and>
+ invC = invocation_class mode (store s) a statT \<and>
+ l = locals (store s)) ;.
+ init_lvars G declC \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs \<and>.
+ (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
+ Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>
+ {set_lvars l .; ?S}"
+ (is "\<forall> a vs invC declC l. ?METHD a vs invC declC l")
+ proof (intro allI)
+ fix a vs invC declC l
+ from mgf_methds [rule_format]
+ show "?METHD a vs invC declC l"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s4 s2 s1::state
+ fix s0 v
+ let ?D= "invocation_declclass G mode (store s2) a statT
+ \<lparr>name=mn,parTs=pTs'\<rparr>"
+ let ?s3= "init_lvars G ?D \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs s2"
+ assume inv_prop: "abrupt ?s3=None
+ \<longrightarrow> G\<turnstile>mode\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
+ assume conf_s2: "s2\<Colon>\<preceq>(G, L)"
+ assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
+ assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
+ assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
+ assume eval_mthd: "G\<turnstile>?s3 \<midarrow>Methd ?D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
+ show "G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v
+ \<rightarrow> (set_lvars (locals (store s2))) s4"
+ proof -
+ obtain D where D: "D=?D" by simp
+ obtain s3 where s3: "s3=?s3" by simp
+ obtain s3' where
+ s3': "s3' = check_method_access G accC statT mode
+ \<lparr>name=mn,parTs=pTs'\<rparr> a s3"
+ by simp
+ have eq_s3'_s3: "s3'=s3"
+ proof -
+ from inv_prop s3 mode
+ have "normal s3 \<Longrightarrow>
+ G\<turnstile>invmode statM e\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
+ by auto
+ with eval_ps wt_e statM conf_s2 conf_a [rule_format]
+ have "check_method_access G accC statT (invmode statM e)
+ \<lparr>name=mn,parTs=pTs'\<rparr> a s3 = s3"
+ by (rule error_free_call_access) (auto simp add: s3 mode wf)
+ thus ?thesis
+ by (simp add: s3' mode)
+ qed
+ with eval_mthd D s3
+ have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
+ by simp
+ with eval_e eval_ps D _ s3'
+ show ?thesis
+ by (rule eval_Call) (auto simp add: s3 mode D)
+ qed
+ qed
+ qed
+ qed
+qed
+
+lemma eval_expression_no_jump':
+ assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1"
+ and no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
+ and wt: "\<lparr>prg=G, cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
+ and wf: "wf_prog G"
+shows "abrupt s1 \<noteq> Some (Jump j)"
+using eval no_jmp wt wf
+by - (rule eval_expression_no_jump
+ [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
-lemma MGF_altern: "G,A\<turnstile>{Normal (\<doteq> \<and>. p)} t\<succ> {G\<rightarrow>} =
- G,A\<turnstile>{Normal ((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z) \<and>. p)}
- t\<succ> {\<lambda>Y s Z. (Y,s) = Z}"
-apply (unfold MGF_def)
-apply (auto del: conjI elim!: conseq12)
-apply (case_tac "\<exists>w s. G\<turnstile>Norm sa \<midarrow>t\<succ>\<rightarrow> (w,s) ")
-apply (fast dest: unique_eval)
-apply clarsimp
-apply (drule split_paired_All [THEN subst])
-apply (clarsimp elim!: state_not_single)
-done
+
+text {* To derive the most general formula for the loop statement, we need to
+come up with a proper loop invariant, which intuitively states that we are
+currently inside the evaluation of the loop. To define such an invariant, we
+unroll the loop in iterated evaluations of the expression and evaluations of
+the loop body. *}
+
+constdefs
+ unroll:: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times> state) set"
+
+ "unroll G l e c \<equiv> {(s,t). \<exists> v s1 s2.
+ G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
+ G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
+
+
+lemma unroll_while:
+ assumes unroll: "(s, t) \<in> (unroll G l e c)\<^sup>*"
+ and eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'"
+ and normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v"
+ and wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
+ and wf: "wf_prog G"
+ shows "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+using unroll (* normal_s *)
+proof (induct rule: converse_rtrancl_induct)
+ show "G\<turnstile>t \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ proof (cases "normal t")
+ case False
+ with eval_e have "s'=t" by auto
+ with False show ?thesis by auto
+ next
+ case True
+ note normal_t = this
+ show ?thesis
+ proof (cases "normal s'")
+ case True
+ with normal_t eval_e normal_termination
+ show ?thesis
+ by (auto intro: eval.Loop)
+ next
+ case False
+ note abrupt_s' = this
+ from eval_e _ wt wf
+ have no_cont: "abrupt s' \<noteq> Some (Jump (Cont l))"
+ by (rule eval_expression_no_jump') (insert normal_t,simp)
+ have
+ "if the_Bool v
+ then (G\<turnstile>s' \<midarrow>c\<rightarrow> s' \<and>
+ G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s')
+ else s' = s'"
+ proof (cases "the_Bool v")
+ case False thus ?thesis by simp
+ next
+ case True
+ with abrupt_s' have "G\<turnstile>s' \<midarrow>c\<rightarrow> s'" by auto
+ moreover from abrupt_s' no_cont
+ have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
+ by (cases s') (simp add: absorb_def split: split_if)
+ moreover
+ from no_absorb abrupt_s'
+ have "G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ by auto
+ ultimately show ?thesis
+ using True by simp
+ qed
+ with eval_e
+ show ?thesis
+ using normal_t by (auto intro: eval.Loop)
+ qed
+ qed
+next
+ fix s s3
+ assume unroll: "(s,s3) \<in> unroll G l e c"
+ assume while: "G\<turnstile>s3 \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ show "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ proof -
+ from unroll obtain v s1 s2 where
+ normal_s1: "normal s1" and
+ eval_e: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1" and
+ continue: "the_Bool v" and
+ eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and
+ s3: "s3=(abupd (absorb (Cont l)) s2)"
+ by (unfold unroll_def) fast
+ from eval_e normal_s1 have
+ "normal s"
+ by (rule eval_no_abrupt_lemma [rule_format])
+ with while eval_e continue eval_c s3 show ?thesis
+ by (auto intro!: eval.Loop)
+ qed
+qed
-lemma MGFn_Loop:
-"\<lbrakk>G,(A::state triple set)\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>};G,A\<turnstile>{=:n} In1r stmnt\<succ> {G\<rightarrow>} \<rbrakk>
-\<Longrightarrow>
- G,A\<turnstile>{=:n} In1r (l\<bullet> While(expr) stmnt)\<succ> {G\<rightarrow>}"
-apply (rule MGFn_NormalI, simp)
-apply (rule_tac p2 = "\<lambda>s. card (nyinitcls G s) \<le> n" in
- MGF_altern [unfolded MGF_def, THEN iffD2, THEN conseq1])
-prefer 2
-apply clarsimp
-apply (rule_tac P' =
-"((\<lambda>Y s Z. \<forall>w s'. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s') \<longrightarrow> (w,s') = Z)
- \<and>. (\<lambda>s. card (nyinitcls G s) \<le> n))" in conseq12)
-prefer 2
-apply clarsimp
-apply (tactic "smp_tac 1 1", erule_tac V = "All ?P" in thin_rl)
-apply (rule_tac [2] P' = " (\<lambda>b s (Y',s') . (\<exists>s0. G\<turnstile>s0 \<midarrow>In1l expr\<succ>\<rightarrow> (b,s)) \<and> (if normal s \<and> the_Bool (the_In1 b) then (\<forall>s'' w s0. G\<turnstile>s \<midarrow>stmnt\<rightarrow> s'' \<and> G\<turnstile>(abupd (absorb (Cont l)) s'') \<midarrow>In1r (l\<bullet> While(expr) stmnt) \<succ>\<rightarrow> (w,s0) \<longrightarrow> (w,s0) = (Y',s')) else (\<diamondsuit>,s) = (Y',s'))) \<and>. G\<turnstile>init\<le>n" in polymorphic_Loop)
-apply (force dest!: eval.Loop split add: split_if_asm)
-prefer 2
-apply (erule MGFnD' [THEN conseq12])
-apply clarsimp
-apply (erule_tac V = "card (nyinitcls G s') \<le> n" in thin_rl)
-apply (tactic "eval_Force_tac 1")
-apply (erule MGFnD' [THEN conseq12] , clarsimp)
-apply (rule conjI, erule exI)
-apply (tactic "clarsimp_tac eval_css 1")
-apply (case_tac "a")
-prefer 2
-apply (clarsimp)
-apply (clarsimp split add: split_if)
-apply (rule conjI, (tactic {* force_tac (claset() addSDs [thm "eval.Loop"],
- simpset() addsimps [split_paired_all] addsimprocs [eval_stmt_proc]) 1*})+)
-done
+ML"Addsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]"
+
+lemma MGFn_Loop:
+ assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ and mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ and wf: "wf_prog G"
+shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt [rule_format],elim exE)
+ fix T L C
+ assume wt: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
+ then obtain eT where
+ wt_e: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
+ by cases simp
+ show ?thesis
+ proof (rule MGFn_NormalI)
+ show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}
+ .l\<bullet> While(e) c.
+ {\<lambda>Y s' s. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(e) c)\<succ>\<rightarrow> (Y, s')}"
+ proof (rule conseq12
+ [where ?P'="(\<lambda> Y s' s. (s,s') \<in> (unroll G l e c)\<^sup>* ) \<and>. G\<turnstile>init\<le>n"
+ and ?Q'="((\<lambda> Y s' s. (\<exists> t b. (s,t) \<in> (unroll G l e c)\<^sup>* \<and>
+ Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s'))
+ \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>"])
+ show "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n}
+ .l\<bullet> While(e) c.
+ {((\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
+ Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s'))
+ \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>}"
+ proof (rule ax_derivs.Loop)
+ from mfg_e
+ show "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n}
+ e-\<succ>
+ {(\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
+ Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s'))
+ \<and>. G\<turnstile>init\<le>n}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s Z s' v
+ assume "(Z, s) \<in> (unroll G l e c)\<^sup>*"
+ moreover
+ assume "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s'"
+ ultimately
+ show "\<exists>t. (Z, t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'"
+ by blast
+ qed
+ next
+ from mfg_c
+ show "G,A\<turnstile>{Normal (((\<lambda>Y s' s. \<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
+ Y = \<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')
+ \<and>. G\<turnstile>init\<le>n)\<leftarrow>=True)}
+ .c.
+ {abupd (absorb (Cont l)) .;
+ ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n)}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix Z s' s v t
+ assume unroll: "(Z, t) \<in> (unroll G l e c)\<^sup>*"
+ assume eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> Norm s"
+ assume true: "the_Bool v"
+ assume eval_c: "G\<turnstile>Norm s \<midarrow>c\<rightarrow> s'"
+ show "(Z, abupd (absorb (Cont l)) s') \<in> (unroll G l e c)\<^sup>*"
+ proof -
+ note unroll
+ also
+ from eval_e true eval_c
+ have "(t,abupd (absorb (Cont l)) s') \<in> unroll G l e c"
+ by (unfold unroll_def) force
+ ultimately show ?thesis ..
+ qed
+ qed
+ qed
+ next
+ show
+ "\<forall>Y s Z.
+ (Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)) Y s Z
+ \<longrightarrow> (\<forall>Y' s'.
+ (\<forall>Y Z'.
+ ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n) Y s Z'
+ \<longrightarrow> (((\<lambda>Y s' s. \<exists>t b. (s,t) \<in> (unroll G l e c)\<^sup>*
+ \<and> Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')
+ \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>) Y' s' Z')
+ \<longrightarrow> G\<turnstile>Z \<midarrow>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ>\<rightarrow> (Y', s'))"
+ proof (clarsimp)
+ fix Y' s' s
+ assume asm:
+ "\<forall>Z'. (Z', Norm s) \<in> (unroll G l e c)\<^sup>*
+ \<longrightarrow> card (nyinitcls G s') \<le> n \<and>
+ (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<and>
+ (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>"
+ show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ proof -
+ from asm obtain v t where
+ -- {* @{term "Z'"} gets instantiated with @{term "Norm s"} *}
+ unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and
+ eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and
+ normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and
+ Y': "Y' = \<diamondsuit>"
+ by auto
+ from unroll eval_e normal_termination wt_e wf
+ have "G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
+ by (rule unroll_while)
+ with Y'
+ show ?thesis
+ by simp
+ qed
+ qed
+ qed
+ qed
+qed
-text {* For @{text MGFn_FVar} we need the wellformedness of the program to
-switch from the evaln-semantics to the eval-semantics *}
lemma MGFn_FVar:
- "\<lbrakk>G,A\<turnstile>{=:n} In1r (Init statDeclC)\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk>
- \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In2 ({accC,statDeclC,stat}e..fn)\<succ> {G\<rightarrow>}"
-apply (tactic "wt_conf_prepare_tac 1")
-apply (rule_tac
- Q="(\<lambda>Y s1 (x,s) . x = None \<and>
- (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1
- )) \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"
- in ax_derivs.FVar)
-apply (tactic "forw_hyp_tac 1")
-apply (tactic "clarsimp_tac eval_css 1")
-apply (subgoal_tac "is_class G statDeclC")
-apply (force dest: eval_type_sound)
-apply (force dest: ty_expr_is_type [THEN type_is_class]
- accfield_fields [THEN fields_declC])
-apply (tactic "forw_hyp_tac 1")
-apply (tactic "clarsimp_tac eval_css 1")
-apply (subgoal_tac "(\<exists> v' s2' s3.
- ( fvar statDeclC (is_static f) fn v (aa, ba) = (v',s2') ) \<and>
- (s3 = check_field_access G C statDeclC fn (is_static f) v s2') \<and>
- (s3 = s2'))")
-apply (erule exE)+
-apply (erule conjE)+
-apply (erule (1) eval.FVar)
-apply simp
-apply simp
-
-apply (case_tac "fvar statDeclC (is_static f) fn v (aa, ba)")
-apply (rule exI)+
-apply (rule context_conjI)
-apply force
-
-apply (rule context_conjI)
-apply simp
-
-apply (erule (3) error_free_field_access)
-apply (auto dest: eval_type_sound)
-done
+ fixes A :: "state triple set"
+ assumes mgf_init: "G,A\<turnstile>{=:n} \<langle>Init statDeclC\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ and mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ and wf: "wf_prog G"
+ shows "G,A\<turnstile>{=:n} \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
+ note inj_term_simps [simp]
+ fix T L accC' V
+ assume wt: "\<lparr>prg = G, cls = accC', lcl = L\<rparr>\<turnstile>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<Colon>T"
+ then obtain statC f where
+ wt_e: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
+ accfield: "accfield G accC' statC fn = Some (statDeclC,f )" and
+ eq_accC: "accC=accC'" and
+ stat: "stat=is_static f"
+ by (cases) (auto simp add: member_is_static_simp)
+ let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and>
+ (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1) \<and>
+ (\<exists> E. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E))
+ \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"
+ show "G,A\<turnstile>{Normal
+ ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
+ (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
+ (\<lambda>s. \<lparr>prg=G,cls=accC',lcl=L\<rparr>
+ \<turnstile> dom (locals (store s)) \<guillemotright> \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V))
+ } {accC,statDeclC,stat}e..fn=\<succ>
+ {\<lambda>Y s' s. \<exists>vf. Y = \<lfloor>vf\<rfloor>\<^sub>v \<and>
+ G\<turnstile>s \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<rightarrow> s'}"
+ (is "G,A\<turnstile>{Normal ?P} {accC,statDeclC,stat}e..fn=\<succ> {?R}")
+ proof (rule ax_derivs.FVar [where ?Q="?Q" ])
+ from mgf_init
+ show "G,A\<turnstile>{Normal ?P} .Init statDeclC. {?Q}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s s'
+ assume conf_s: "Norm s\<Colon>\<preceq>(G, L)"
+ assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
+ \<turnstile> dom (locals s) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
+ assume eval_init: "G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s'"
+ 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>
+ s'\<Colon>\<preceq>(G, L)"
+ proof -
+ from da
+ obtain E where
+ "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals s) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
+ by cases simp
+ moreover
+ from eval_init
+ have "dom (locals s) \<subseteq> dom (locals (store s'))"
+ by (rule dom_locals_eval_mono [elim_format]) simp
+ ultimately obtain E' where
+ "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
+ by (rule da_weakenE)
+ moreover
+ have "s'\<Colon>\<preceq>(G, L)"
+ proof -
+ have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
+ proof -
+ from wf wt_e
+ have iscls_statC: "is_class G statC"
+ by (auto dest: ty_expr_is_type type_is_class)
+ with wf accfield
+ have iscls_statDeclC: "is_class G statDeclC"
+ by (auto dest!: accfield_fields dest: fields_declC)
+ thus ?thesis by simp
+ qed
+ obtain I where
+ da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
+ \<turnstile> dom (locals (store ((Norm s)::state))) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
+ by (auto intro: da_Init [simplified] assigned.select_convs)
+ from eval_init conf_s wt_init da_init wf
+ show ?thesis
+ by (rule eval_type_soundE)
+ qed
+ ultimately show ?thesis by rules
+ qed
+ qed
+ next
+ from mgf_e
+ show "G,A\<turnstile>{?Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; ?R}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s0 s1 s2 E a
+ let ?fvar = "fvar statDeclC stat fn a s2"
+ assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
+ assume eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
+ assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
+ assume da_e: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
+ show "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>fst ?fvar\<rightarrow> snd ?fvar"
+ proof -
+ obtain v s2' where
+ v: "v=fst ?fvar" and s2': "s2'=snd ?fvar"
+ by simp
+ obtain s3 where
+ s3: "s3= check_field_access G accC' statDeclC fn stat a s2'"
+ by simp
+ have eq_s3_s2': "s3=s2'"
+ proof -
+ from eval_e conf_s1 wt_e da_e wf obtain
+ conf_s2: "s2\<Colon>\<preceq>(G, L)" and
+ conf_a: "normal s2 \<Longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
+ by (rule eval_type_soundE) simp
+ from accfield wt_e eval_init eval_e conf_s2 conf_a _ wf
+ show ?thesis
+ by (rule error_free_field_access
+ [where ?v=v and ?s2'=s2',elim_format])
+ (simp add: s3 v s2' stat)+
+ qed
+ from eval_init eval_e
+ show ?thesis
+ apply (rule eval.FVar [where ?s2'=s2'])
+ apply (simp add: s2')
+ apply (simp add: s3 [symmetric] eq_s3_s2' eq_accC s2' [symmetric])
+ done
+ qed
+ qed
+ qed
+qed
-text {* For @{text MGFn_Fin} we need the wellformedness of the program to
-switch from the evaln-semantics to the eval-semantics *}
-lemma MGFn_Fin:
-"\<lbrakk>wf_prog G; G,A\<turnstile>{=:n} In1r stmt1\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt2\<succ> {G\<rightarrow>}\<rbrakk>
- \<Longrightarrow> G,(A\<Colon>state triple set)\<turnstile>{=:n} In1r (stmt1 Finally stmt2)\<succ> {G\<rightarrow>}"
-apply (tactic "wt_conf_prepare_tac 1")
-apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> s' \<and> s\<Colon>\<preceq>(G, L))
-\<and>. G\<turnstile>init\<le>n" in ax_derivs.Fin)
-apply (tactic "forw_hyp_tac 1")
-apply (tactic "clarsimp_tac eval_css 1")
-apply (rule allI)
-apply (tactic "clarsimp_tac eval_css 1")
-apply (tactic "forw_hyp_tac 1")
-apply (tactic {* pair_tac "sb" 1 *})
-apply (tactic"clarsimp_tac (claset(),simpset() addsimprocs [eval_stmt_proc]) 1")
-apply (rule wf_eval_Fin)
-apply auto
-done
-text {* For @{text MGFn_lemma} we need the wellformedness of the program to
-switch from the evaln-semantics to the eval-semantics cf. @{text MGFn_call},
-@{text MGFn_FVar}*}
-lemma MGFn_lemma [rule_format (no_asm)]:
- "\<lbrakk>\<forall>n C sig. G,(A::state triple set)\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>};
- wf_prog G\<rbrakk>
- \<Longrightarrow> \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
-apply (rule full_nat_induct)
-apply (rule allI)
-apply (drule_tac x = n in spec)
-apply (drule_tac psi = "All ?P" in asm_rl)
-apply (subgoal_tac "\<forall>v e c es. G,A\<turnstile>{=:n} In2 v\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<and> G,A\<turnstile>{=:n} In3 es\<succ> {G\<rightarrow>}")
-apply (tactic "Clarify_tac 2")
-apply (induct_tac "t")
-apply (induct_tac "a")
-apply fast+
-apply (rule var_expr_stmt.induct)
-(* 34 subgoals *)
-prefer 17 apply fast (* Methd *)
-prefer 16 apply (erule (3) MGFn_Call)
-prefer 2 apply (drule MGFn_Init,erule (2) MGFn_FVar)
-apply (erule_tac [!] V = "All ?P" in thin_rl) (* assumptions on Methd *)
-apply (erule_tac [29] MGFn_Init)
-prefer 23 apply (erule (1) MGFn_Loop)
-prefer 26 apply (erule (2) MGFn_Fin)
-apply (tactic "ALLGOALS compl_prepare_tac")
+lemma MGFn_Fin:
+ assumes wf: "wf_prog G"
+ and mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ and mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ shows "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
+ fix T L accC C
+ assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T"
+ then obtain
+ wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
+ wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
+ by cases simp
+ let ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>c1\<rightarrow> s' \<and>
+ (\<exists> C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1)
+ \<and> s\<Colon>\<preceq>(G, L))
+ \<and>. G\<turnstile>init\<le>n"
+ show "G,A\<turnstile>{Normal
+ ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
+ (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
+ (\<lambda>s. \<lparr>prg=G,cls=accC,lcl =L\<rparr>
+ \<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C))}
+ .c1 Finally c2.
+ {\<lambda>Y s' s. Y = \<diamondsuit> \<and> G\<turnstile>s \<midarrow>c1 Finally c2\<rightarrow> s'}"
+ (is "G,A\<turnstile>{Normal ?P} .c1 Finally c2. {?R}")
+ proof (rule ax_derivs.Fin [where ?Q="?Q"])
+ from mgf_c1
+ show "G,A\<turnstile>{Normal ?P} .c1. {?Q}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s0
+ assume "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C"
+ thus "\<exists>C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
+ by cases (auto simp add: inj_term_simps)
+ qed
+ next
+ from mgf_c2
+ show "\<forall>abr. G,A\<turnstile>{?Q \<and>. (\<lambda>s. abr = abrupt s) ;. abupd (\<lambda>abr. None)} .c2.
+ {abupd (abrupt_if (abr \<noteq> None) abr) .; ?R}"
+ proof (rule MGFnD' [THEN conseq12, THEN allI],clarsimp)
+ fix s0 s1 s2 C1
+ assume da_c1:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
+ assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
+ assume eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
+ assume eval_c2: "G\<turnstile>abupd (\<lambda>abr. None) s1 \<midarrow>c2\<rightarrow> s2"
+ show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2
+ \<rightarrow> abupd (abrupt_if (\<exists>y. abrupt s1 = Some y) (abrupt s1)) s2"
+ proof -
+ obtain abr1 str1 where s1: "s1=(abr1,str1)"
+ by (cases s1) simp
+ with eval_c1 eval_c2 obtain
+ eval_c1': "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (abr1,str1)" and
+ eval_c2': "G\<turnstile>Norm str1 \<midarrow>c2\<rightarrow> s2"
+ by simp
+ obtain s3 where
+ s3: "s3 = (if \<exists>err. abr1 = Some (Error err)
+ then (abr1, str1)
+ else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
+ by simp
+ from eval_c1' conf_s0 wt_c1 _ wf
+ have "error_free (abr1,str1)"
+ by (rule eval_type_soundE) (insert da_c1,auto)
+ with s3 have eq_s3: "s3=abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
+ by (simp add: error_free_def)
+ from eval_c1' eval_c2' s3
+ show ?thesis
+ by (rule eval.Fin [elim_format]) (simp add: s1 eq_s3)
+ qed
+ qed
+ qed
+qed
+
+lemma Body_no_break:
+ assumes eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1"
+ and eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
+ and jmpOk: "jumpNestingOkS {Ret} c"
+ and wt_c: "\<lparr>prg=G, cls=C, lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
+ and clsD: "class G D=Some d"
+ and wf: "wf_prog G"
+ shows "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l)) \<and>
+ abrupt s2 \<noteq> Some (Jump (Cont l))"
+proof
+ fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<and>
+ abrupt s2 \<noteq> Some (Jump (Cont l))"
+ proof -
+ from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
+ by auto
+ from eval_init wf
+ have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
+ by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
+ from eval_c _ wt_c wf
+ show ?thesis
+ apply (rule jumpNestingOk_eval [THEN conjE, elim_format])
+ using jmpOk s1_no_jmp
+ apply auto
+ done
+ qed
+qed
-apply (rule ax_derivs.LVar [THEN conseq1], tactic "eval_Force_tac 1")
-
-apply (rule ax_derivs.AVar)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
-
-apply (rule ax_derivs.InstInitV)
-
-apply (rule ax_derivs.NewC)
-apply (erule MGFn_InitD [THEN conseq2])
-apply (tactic "eval_Force_tac 1")
-
-apply (rule_tac Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty ty) \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.NewA)
-apply (simp add: init_comp_ty_def split add: split_if)
-apply (rule conjI, clarsimp)
-apply (erule MGFn_InitD [THEN conseq2])
-apply (tactic "clarsimp_tac eval_css 1")
-apply clarsimp
-apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
-apply (tactic "forw_hyp_eval_Force_tac 1")
-
-apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast],tactic"eval_Force_tac 1")
-
-apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst],tactic"eval_Force_tac 1")
-apply (rule ax_derivs.Lit [THEN conseq1], tactic "eval_Force_tac 1")
-apply (rule ax_derivs.UnOp, tactic "forw_hyp_eval_Force_tac 1")
+lemma MGFn_Body:
+ assumes wf: "wf_prog G"
+ and mgf_init: "G,A\<turnstile>{=:n} \<langle>Init D\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ and mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ shows "G,(A\<Colon>state triple set)\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
+ fix T L accC E
+ assume wt: "\<lparr>prg=G, cls=accC,lcl=L\<rparr>\<turnstile>\<langle>Body D c\<rangle>\<^sub>e\<Colon>T"
+ let ?Q="(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init D\<rightarrow> s' \<and> jumpNestingOkS {Ret} c)
+ \<and>. G\<turnstile>init\<le>n"
+ show "G,A\<turnstile>{Normal
+ ((\<lambda>Y' s' s. s' = s \<and> fst s = None) \<and>. G\<turnstile>init\<le>n \<and>.
+ (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
+ (\<lambda>s. \<lparr>prg=G,cls=accC,lcl=L\<rparr>
+ \<turnstile> dom (locals (store s)) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E))}
+ Body D c-\<succ>
+ {\<lambda>Y s' s. \<exists>v. Y = In1 v \<and> G\<turnstile>s \<midarrow>Body D c-\<succ>v\<rightarrow> s'}"
+ (is "G,A\<turnstile>{Normal ?P} Body D c-\<succ> {?R}")
+ proof (rule ax_derivs.Body [where ?Q="?Q"])
+ from mgf_init
+ show "G,A\<turnstile>{Normal ?P} .Init D. {?Q}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s0
+ assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E"
+ thus "jumpNestingOkS {Ret} c"
+ by cases simp
+ qed
+ next
+ from mgf_c
+ show "G,A\<turnstile>{?Q}.c.{\<lambda>s.. abupd (absorb Ret) .; ?R\<leftarrow>\<lfloor>the (locals s Result)\<rfloor>\<^sub>e}"
+ proof (rule MGFnD' [THEN conseq12],clarsimp)
+ fix s0 s1 s2
+ assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1"
+ assume eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
+ assume nestingOk: "jumpNestingOkS {Ret} c"
+ show "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
+ \<rightarrow> abupd (absorb Ret) s2"
+ proof -
+ from wt obtain d where
+ d: "class G D=Some d" and
+ wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
+ by cases auto
+ obtain s3 where
+ s3: "s3= (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
+ fst s2 = Some (Jump (Cont l))
+ then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
+ else s2)"
+ by simp
+ from eval_init eval_c nestingOk wt_c d wf
+ have eq_s3_s2: "s3=s2"
+ by (rule Body_no_break [elim_format]) (simp add: s3)
+ from eval_init eval_c s3
+ show ?thesis
+ by (rule eval.Body [elim_format]) (simp add: eq_s3_s2)
+ qed
+ qed
+ qed
+qed
-apply (rule ax_derivs.BinOp)
-apply (erule MGFnD [THEN ax_NormalD])
-
-apply (rule allI)
-apply (case_tac "need_second_arg binop v1")
-apply simp
-apply (tactic "forw_hyp_eval_Force_tac 1")
-
-apply simp
-apply (rule ax_Normal_cases)
-apply (rule ax_derivs.Skip [THEN conseq1])
-apply clarsimp
-
-apply (rule eval_BinOp_arg2_indepI)
-apply simp
-apply simp
-
-apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
-apply (tactic "eval_Force_tac 1")
-
-apply (rule ax_derivs.Super [THEN conseq1], tactic "eval_Force_tac 1")
-apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc],tactic"eval_Force_tac 1")
-
-apply (rule ax_derivs.Ass)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
+(* To term *)
+lemma term_cases: "
+ \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
+ \<Longrightarrow> P t"
+ apply (cases t)
+ apply (case_tac a)
+ apply auto
+ done
-apply (rule ax_derivs.Cond)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (rule allI)
-apply (rule ax_Normal_cases)
-prefer 2
-apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
-apply (tactic "eval_Force_tac 1")
-apply (case_tac "b")
-apply (simp, tactic "forw_hyp_eval_Force_tac 1")
-apply (simp, tactic "forw_hyp_eval_Force_tac 1")
-
-apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init pid_field_type\<rightarrow> s') \<and>. G\<turnstile>init\<le>n" in ax_derivs.Body)
- apply (erule MGFn_InitD [THEN conseq2])
- apply (tactic "eval_Force_tac 1")
-apply (tactic "forw_hyp_tac 1")
-apply (tactic {* clarsimp_tac (eval_css delsimps2 [split_paired_all]) 1 *})
-apply (erule (1) eval.Body)
-
-apply (rule ax_derivs.InstInitE)
-
-apply (rule ax_derivs.Callee)
-
-apply (rule ax_derivs.Skip [THEN conseq1], tactic "eval_Force_tac 1")
-
-apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr],tactic"eval_Force_tac 1")
-
-apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
-apply (tactic "clarsimp_tac eval_css 1")
-
-apply (rule ax_derivs.Comp)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
-
-apply (rule ax_derivs.If)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (rule allI)
-apply (rule ax_Normal_cases)
-prefer 2
-apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
-apply (tactic "eval_Force_tac 1")
-apply (case_tac "b")
-apply (simp, tactic "forw_hyp_eval_Force_tac 1")
-apply (simp, tactic "forw_hyp_eval_Force_tac 1")
-
-apply (rule ax_derivs.Do [THEN conseq1])
-apply (tactic {* force_tac (eval_css addsimps2 [thm "abupd_def2"]) 1 *})
-
-apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
-apply (tactic "clarsimp_tac eval_css 1")
-
-apply (rule_tac Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>In1r stmt1\<succ>\<rightarrow> (Y',s'') \<and> G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n" in ax_derivs.Try)
-apply (tactic "eval_Force_tac 3")
-apply (tactic "forw_hyp_eval_Force_tac 2")
-apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
-apply (tactic "clarsimp_tac eval_css 1")
-apply (force elim: sxalloc_gext [THEN card_nyinitcls_gext])
-
-apply (rule ax_derivs.FinA)
-
-apply (rule ax_derivs.Nil [THEN conseq1], tactic "eval_Force_tac 1")
-
-apply (rule ax_derivs.Cons)
-apply (erule MGFnD [THEN ax_NormalD])
-apply (tactic "forw_hyp_eval_Force_tac 1")
-done
+lemma MGFn_lemma:
+ assumes mgf_methds:
+ "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ and wf: "wf_prog G"
+ shows "\<And> t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
+proof (induct rule: full_nat_induct)
+ fix n t
+ assume hyp: "\<forall> m. Suc m \<le> n \<longrightarrow> (\<forall> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
+ show "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
+ proof -
+ {
+ fix v e c es
+ have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" and
+ "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
+ "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and
+ "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
+ proof (induct rule: var_expr_stmt.induct)
+ case (LVar v)
+ show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.LVar [THEN conseq1])
+ apply (clarsimp)
+ apply (rule eval.LVar)
+ done
+ next
+ case (FVar accC statDeclC stat e fn)
+ have "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
+ from MGFn_Init [OF hyp] this wf
+ show ?case
+ by (rule MGFn_FVar)
+ next
+ case (AVar e1 e2)
+ have mgf_e1: "G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
+ have mgf_e2: "G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
+ show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.AVar)
+ apply (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
+ apply (rule allI)
+ apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
+ apply (fastsimp intro: eval.AVar)
+ done
+ next
+ case (InsInitV c v)
+ show ?case
+ by (rule MGFn_NormalI) (rule ax_derivs.InsInitV)
+ next
+ case (NewC C)
+ show ?case
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.NewC)
+ apply (rule MGFn_InitD [OF hyp, THEN conseq2])
+ apply (fastsimp intro: eval.NewC)
+ done
+ next
+ case (NewA T e)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.NewA
+ [where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T)
+ \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
+ apply (simp add: init_comp_ty_def split add: split_if)
+ apply (rule conjI, clarsimp)
+ apply (rule MGFn_InitD [OF hyp, THEN conseq2])
+ apply (clarsimp intro: eval.Init)
+ apply clarsimp
+ apply (rule ax_derivs.Skip [THEN conseq1])
+ apply (clarsimp intro: eval.Skip)
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.NewA)
+ done
+ next
+ case (Cast C e)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast])
+ apply (fastsimp intro: eval.Cast)
+ done
+ next
+ case (Inst e C)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst])
+ apply (fastsimp intro: eval.Inst)
+ done
+ next
+ case (Lit v)
+ show ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Lit [THEN conseq1])
+ apply (fastsimp intro: eval.Lit)
+ done
+ next
+ case (UnOp unop e)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.UnOp)
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.UnOp)
+ done
+ next
+ case (BinOp binop e1 e2)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.BinOp)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (rule allI)
+ apply (case_tac "need_second_arg binop__ v1")
+ apply simp
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.BinOp)
+ apply simp
+ apply (rule ax_Normal_cases)
+ apply (rule ax_derivs.Skip [THEN conseq1])
+ apply clarsimp
+ apply (rule eval_BinOp_arg2_indepI)
+ apply simp
+ apply simp
+ apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
+ apply (fastsimp intro: eval.BinOp)
+ done
+ next
+ case Super
+ show ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Super [THEN conseq1])
+ apply (fastsimp intro: eval.Super)
+ done
+ next
+ case (Acc v)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc])
+ apply (fastsimp intro: eval.Acc simp add: split_paired_all)
+ done
+ next
+ case (Ass v e)
+ thus "G,A\<turnstile>{=:n} \<langle>v:=e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Ass)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (rule allI)
+ apply (erule MGFnD'[THEN conseq12])
+ apply (fastsimp intro: eval.Ass simp add: split_paired_all)
+ done
+ next
+ case (Cond e1 e2 e3)
+ thus "G,A\<turnstile>{=:n} \<langle>e1 ? e2 : e3\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Cond)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (rule allI)
+ apply (rule ax_Normal_cases)
+ prefer 2
+ apply (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
+ apply (fastsimp intro: eval.Cond)
+ apply (case_tac "b")
+ apply simp
+ apply (erule MGFnD'[THEN conseq12])
+ apply (fastsimp intro: eval.Cond)
+ apply simp
+ apply (erule MGFnD'[THEN conseq12])
+ apply (fastsimp intro: eval.Cond)
+ done
+ next
+ case (Call accC statT mode e mn pTs' ps)
+ have mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
+ have mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}".
+ from mgf_methds mgf_e mgf_ps wf
+ show "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ by (rule MGFn_Call)
+ next
+ case (Methd D mn)
+ from mgf_methds
+ show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ by simp
+ next
+ case (Body D c)
+ have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" .
+ from wf MGFn_Init [OF hyp] mgf_c
+ show "G,A\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
+ by (rule MGFn_Body)
+ next
+ case (InsInitE c e)
+ show ?case
+ by (rule MGFn_NormalI) (rule ax_derivs.InsInitE)
+ next
+ case (Callee l e)
+ show ?case
+ by (rule MGFn_NormalI) (rule ax_derivs.Callee)
+ next
+ case Skip
+ show ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Skip [THEN conseq1])
+ apply (fastsimp intro: eval.Skip)
+ done
+ next
+ case (Expr e)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr])
+ apply (fastsimp intro: eval.Expr)
+ done
+ next
+ case (Lab l c)
+ thus "G,A\<turnstile>{=:n} \<langle>l\<bullet> c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
+ apply (fastsimp intro: eval.Lab)
+ done
+ next
+ case (Comp c1 c2)
+ thus "G,A\<turnstile>{=:n} \<langle>c1;; c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Comp)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.Comp)
+ done
+ next
+ case (If_ e c1 c2)
+ thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.If)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (rule allI)
+ apply (rule ax_Normal_cases)
+ prefer 2
+ apply (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
+ apply (fastsimp intro: eval.If)
+ apply (case_tac "b")
+ apply simp
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.If)
+ apply simp
+ apply (erule MGFnD' [THEN conseq12])
+ apply (fastsimp intro: eval.If)
+ done
+ next
+ case (Loop l e c)
+ have mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}".
+ have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
+ from mgf_e mgf_c wf
+ show "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ by (rule MGFn_Loop)
+ next
+ case (Jmp j)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Jmp [THEN conseq1])
+ apply (auto intro: eval.Jmp simp add: abupd_def2)
+ done
+ next
+ case (Throw e)
+ thus ?case
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
+ apply (fastsimp intro: eval.Throw)
+ done
+ next
+ case (TryC c1 C vn c2)
+ thus "G,A\<turnstile>{=:n} \<langle>Try c1 Catch(C vn) c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Try [where
+ ?Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>\<langle>c1\<rangle>\<^sub>s\<succ>\<rightarrow> (Y',s'') \<and>
+ G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n"])
+ apply (erule MGFnD [THEN ax_NormalD, THEN conseq2])
+ apply (fastsimp elim: sxalloc_gext [THEN card_nyinitcls_gext])
+ apply (erule MGFnD'[THEN conseq12])
+ apply (fastsimp intro: eval.Try)
+ apply (fastsimp intro: eval.Try)
+ done
+ next
+ case (Fin c1 c2)
+ have mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
+ have mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}".
+ from wf mgf_c1 mgf_c2
+ show "G,A\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ by (rule MGFn_Fin)
+ next
+ case (FinA abr c)
+ show ?case
+ by (rule MGFn_NormalI) (rule ax_derivs.FinA)
+ next
+ case (Init C)
+ from hyp
+ show "G,A\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
+ by (rule MGFn_Init)
+ next
+ case Nil_expr
+ show "G,A\<turnstile>{=:n} \<langle>[]\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Nil [THEN conseq1])
+ apply (fastsimp intro: eval.Nil)
+ done
+ next
+ case (Cons_expr e es)
+ thus "G,A\<turnstile>{=:n} \<langle>e# es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
+ apply -
+ apply (rule MGFn_NormalI)
+ apply (rule ax_derivs.Cons)
+ apply (erule MGFnD [THEN ax_NormalD])
+ apply (rule allI)
+ apply (erule MGFnD'[THEN conseq12])
+ apply (fastsimp intro: eval.Cons)
+ done
+ qed
+ }
+ thus ?thesis
+ by (cases rule: term_cases) auto
+ qed
+qed
lemma MGF_asm:
"\<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>
@@ -643,70 +1401,55 @@
apply assumption (* wf_prog G *)
done
-declare splitI2 [intro!]
-ML_setup {*
-Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]
-*}
-
-
section "nested version"
-lemma nesting_lemma' [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts;
- !!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn};
- !!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t};
- finite U; uA = mgf_call`U |] ==>
- !A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})"
-proof -
- assume ax_derivs_asm: "!!A ts. ts <= A ==> P A ts"
- assume MGF_nested_Methd: "!!A pn. !b:bdy pn. P (insert (mgf_call pn) A)
- {mgf b} ==> P A {mgf_call pn}"
- assume MGF_asm: "!!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}"
- assume "finite U" "uA = mgf_call`U"
- then show ?thesis
- apply -
- apply (induct_tac "n")
- apply (tactic "ALLGOALS Clarsimp_tac")
- apply (tactic "dtac (permute_prems 0 1 card_seteq) 1")
- apply simp
- apply (erule finite_imageI)
- apply (simp add: MGF_asm ax_derivs_asm)
- apply (rule MGF_asm)
- apply (rule ballI)
- apply (case_tac "mgf_call pn : A")
- apply (fast intro: ax_derivs_asm)
- apply (rule MGF_nested_Methd)
- apply (rule ballI)
- apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
- apply fast
- apply (drule finite_subset)
- apply (erule finite_imageI)
- apply auto
- apply arith
- done
-qed
+lemma nesting_lemma' [rule_format (no_asm)]:
+ assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts"
+ and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf_call pn) A) {mgf b}
+ \<Longrightarrow> P A {mgf_call pn}"
+ and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf_call pn} \<Longrightarrow> P A {mgf t}"
+ and finU: "finite U"
+ and uA: "uA = mgf_call`U"
+ shows "\<forall>A. A \<subseteq> uA \<longrightarrow> n \<le> card uA \<longrightarrow> card A = card uA - n
+ \<longrightarrow> (\<forall>t. P A {mgf t})"
+using finU uA
+apply -
+apply (induct_tac "n")
+apply (tactic "ALLGOALS Clarsimp_tac")
+apply (tactic "dtac (permute_prems 0 1 card_seteq) 1")
+apply simp
+apply (erule finite_imageI)
+apply (simp add: MGF_asm ax_derivs_asm)
+apply (rule MGF_asm)
+apply (rule ballI)
+apply (case_tac "mgf_call pn : A")
+apply (fast intro: ax_derivs_asm)
+apply (rule MGF_nested_Methd)
+apply (rule ballI)
+apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
+apply fast
+apply (drule finite_subset)
+apply (erule finite_imageI)
+apply auto
+apply arith
+done
-lemma nesting_lemma [rule_format (no_asm)]: "[| !!A ts. ts <= A ==> P A ts;
- !!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)};
- !!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t};
- finite U |] ==> P {} {mgf t}"
-proof -
- assume 2: "!!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)}"
- assume 3: "!!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t}"
- assume "!!A ts. ts <= A ==> P A ts" "finite U"
- then show ?thesis
- apply -
- apply (rule_tac mgf = "mgf" in nesting_lemma')
- apply (erule_tac [2] 2)
- apply (rule_tac [2] 3)
- apply (rule_tac [6] le_refl)
- apply auto
- done
-qed
+
+lemma nesting_lemma [rule_format (no_asm)]:
+ assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts"
+ and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf (f pn)) A) {mgf b}
+ \<Longrightarrow> P A {mgf (f pn)}"
+ and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf (f pn)} \<Longrightarrow> P A {mgf t}"
+ and finU: "finite U"
+shows "P {} {mgf t}"
+using ax_derivs_asm MGF_nested_Methd MGF_asm finU
+by (rule nesting_lemma') (auto intro!: le_refl)
+
lemma MGF_nested_Methd: "\<lbrakk>
- G,insert ({Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}) A\<turnstile>
- {Normal \<doteq>} In1l (body G C sig) \<succ>{G\<rightarrow>}
- \<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} In1l (Methd C sig) \<succ>{G\<rightarrow>}"
+ G,insert ({Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}) A
+ \<turnstile>{Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}
+ \<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}"
apply (unfold MGF_def)
apply (rule ax_MethdN)
apply (erule conseq2)
@@ -717,8 +1460,8 @@
lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
apply (rule MGFNormalI)
apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and
- bdy = "\<lambda> (C,sig) .{In1l (body G C sig) }" and
- f = "\<lambda> (C,sig) . In1l (Methd C sig) " in nesting_lemma)
+ bdy = "\<lambda> (C,sig) .{\<langle>body G C sig\<rangle>\<^sub>e }" and
+ f = "\<lambda> (C,sig) . \<langle>Methd C sig\<rangle>\<^sub>e " in nesting_lemma)
apply (erule ax_derivs.asm)
apply (clarsimp simp add: split_tupled_all)
apply (erule MGF_nested_Methd)
@@ -731,9 +1474,9 @@
section "simultaneous version"
lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>
- G,A\<union> (\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms
- |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (body G C sig)\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>
- G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>}) ` ms"
+ G,A \<union> (\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms
+ |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>
+ G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms"
apply (unfold MGF_def)
apply (rule ax_derivs.Methd [unfolded mtriples_def])
apply (erule ax_finite_pointwise)
@@ -748,7 +1491,7 @@
done
lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow>
- G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} In1l (Methd C sig)\<succ> {G\<rightarrow>})
+ G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>})
` Collect (split (is_methd G)) "
apply (frule finite_is_methd [OF wf_ws_prog])
apply (rule MGF_simult_Methd_lemma)
@@ -772,20 +1515,48 @@
apply (force intro: evaln.Abrupt)
done
-lemma MGF_complete:
- "\<lbrakk>G,{}\<Turnstile>{P} t\<succ> {Q}; G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}; wf_prog G\<rbrakk>
- \<Longrightarrow> G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
-apply (rule ax_no_hazard)
-apply (unfold MGF_def)
-apply (erule conseq12)
-apply (simp (no_asm_use) add: ax_valids_def triple_valid_def)
-apply (blast dest: eval_to_evaln)
-done
-
-theorem ax_complete: "wf_prog G \<Longrightarrow>
- G,{}\<Turnstile>{P::state assn} t\<succ> {Q} \<Longrightarrow> G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
-apply (erule MGF_complete)
-apply (erule (1) MGF_deriv)
-done
-
+lemma MGF_complete:
+ assumes valid: "G,{}\<Turnstile>{P} t\<succ> {Q}"
+ and mgf: "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
+ and wf: "wf_prog G"
+ shows "G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
+proof (rule ax_no_hazard)
+ from mgf
+ have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y, s')}"
+ by (unfold MGF_def)
+ thus "G,({}::state triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q}"
+ proof (rule conseq12,clarsimp)
+ fix Y s Z Y' s'
+ assume P: "P Y s Z"
+ assume type_ok: "type_ok G t s"
+ assume eval_t: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s')"
+ show "Q Y' s' Z"
+ proof -
+ from eval_t type_ok wf
+ obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
+ by (rule eval_to_evaln [elim_format]) rules
+ from valid have
+ valid_expanded:
+ "\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s
+ \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s') \<longrightarrow> Q Y' s' Z)"
+ by (simp add: ax_valids_def triple_valid_def)
+ from P type_ok evaln
+ show "Q Y' s' Z"
+ by (rule valid_expanded [rule_format])
+ qed
+ qed
+qed
+
+theorem ax_complete:
+ assumes wf: "wf_prog G"
+ and valid: "G,{}\<Turnstile>{P::state assn} t\<succ> {Q}"
+ shows "G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
+proof -
+ from wf have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
+ by (rule MGF_deriv)
+ from valid this wf
+ show ?thesis
+ by (rule MGF_complete)
+qed
+
end