lemma card_nyinitcls_bound: "card (nyinitcls G s) \ card {C. is_class G C}" apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]]) done
lemma nyinitcls_set_locals_cong [simp]: "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)" by (simp add: nyinitcls_def)
lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)" by (simp add: nyinitcls_def)
lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s" by (simp add: nyinitcls_def)
lemma card_nyinitcls_abrupt_congE [elim!]: "card (nyinitcls G (x, s)) \ n \ card (nyinitcls G (y, s)) \ n" unfolding nyinitcls_def by auto
lemma nyinitcls_new_xcpt_var [simp]: "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s" by (induct s) (simp_all add: nyinitcls_def)
lemma nyinitcls_init_lvars [simp]: "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s" by (induct s) (simp add: init_lvars_def2 split: if_split)
lemma nyinitcls_emptyD: "\nyinitcls G s = {}; is_class G C\ \ initd C s" unfolding nyinitcls_def by fast
lemma card_Suc_lemma: "\card (insert a A) \ Suc n; a\A; finite A\ \ card A \ n" by auto
lemma nyinitcls_le_SucD: "\card (nyinitcls G (x,s)) \ Suc n; \inited C (globs s); class G C=Some y\ \
card (nyinitcls G (x,init_class_obj G C s)) \<le> n" apply (subgoal_tac "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))") apply clarsimp apply (erule_tac V="nyinitcls G (x, s) = rhs"for rhs in thin_rl) apply (rule card_Suc_lemma [OF _ _ finite_nyinitcls]) apply (auto dest!: not_initedD elim!:
simp add: nyinitcls_def inited_def split: if_split_asm) done
lemma inited_gext': "\s\|s';inited C (globs s)\ \ inited C (globs s')" by (rule inited_gext)
lemma nyinitcls_gext: "snd s\|snd s' \ nyinitcls G s' \ nyinitcls G s" unfolding nyinitcls_def by (force dest!: inited_gext')
lemma MGFnD: "G,(A::state triple set)\{=:n} t\ {G\} \
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) apply (simp (no_asm_use) add: MGFn_def2) apply (erule conseq12) apply clarsimp apply (erule (1) eval_gext [THEN card_nyinitcls_gext]) done lemmas MGFnD' = MGFnD [of _ _ _ _ "\x. True"]
text\<open>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. \<close> lemma MGFNormalI: "G,A\{Normal \} t\ {G\} \
G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}" apply (unfold MGF_def) apply (rule ax_Normal_cases) apply (erule conseq1) apply clarsimp apply (rule ax_derivs.Abrupt [THEN conseq1]) apply (clarsimp simp add: Let_def) done
text\<open>Additionally to \<open>MGFNormalI\<close>, we also expand the definition of
the most general formula here\<close> lemma MGFn_NormalI: "G,(A::state triple set)\{Normal((\Y' s' s. s'=s \ normal s) \. G\init\n)}t\
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}" apply (simp (no_asm_use) add: MGFn_def2) apply (rule ax_Normal_cases) apply (erule conseq1) apply clarsimp apply (rule ax_derivs.Abrupt [THEN conseq1]) apply (clarsimp simp add: Let_def) done
text\<open>To derive the most general formula, we can restrict ourselves to
welltyped terms, since all others can be uniformally handled by the hazard
rule.\<close> lemma MGFn_free_wt: "(\T L C. \prg=G,cls=C,lcl=L\\t\T) \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}" apply (rule MGFn_NormalI) apply (rule ax_free_wt) apply (auto elim: conseq12 simp add: MGFn_def MGF_def) done
text\<open>To derive the most general formula, we can restrict ourselves to
welltyped terms andassume that the state in the precondition conforms to the
environment. All type violations can be uniformally handled by the hazard
rule.\<close> lemma MGFn_free_wt_NormalConformI: "(\ T L C . \prg=G,cls=C,lcl=L\\t\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>
{\<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 (1) mp) apply (erule conseq12) apply blast done
text\<open>To derive the most general formula, we can restrict ourselves to
welltyped terms andassume that the state in the precondition conforms to the
environment and that the termis definetly assigned with respect to this state.
All type violations can be uniformally handled by the hazard rule.\<close> lemma MGFn_free_wt_da_NormalConformI: "(\ T L C B. \prg=G,cls=C,lcl=L\\t\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
subsubsection "main lemmas"
lemma MGFn_Init: assumes mgf_hyp: "\m. Suc m\n \ (\t. G,A\{=:m} t\ {G\})" shows"G,(A::state triple set)\{=:n} \Init C\\<^sub>s\ {G\}" proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI) fix T L accC assume"\prg=G, cls=accC, lcl= L\\\Init C\\<^sub>s\T" hence is_cls: "is_class G C" by cases simp show"G,A\{Normal ((\Y' s' s. s' = s \ normal s) \. G\init\n)}
.Init C.
{\<lambda>Y s' s. G\<turnstile>s \<midarrow>\<langle>Init C\<rangle>\<^sub>s\<succ>\<rightarrow> (Y, s')}"
(is"G,A\{Normal ?P} .Init C. {?R}") proof (rule ax_cases [where ?C="initd C"]) show"G,A\{Normal ?P \. initd C} .Init C. {?R}" by (rule ax_derivs.Done [THEN conseq1]) (fastforce intro: init_done) next have"G,A\{Normal (?P \. Not \ initd C)} .Init C. {?R}" proof (cases n) case 0 show ?thesis by (rule ax_impossible [THEN conseq1]) (use is_cls 0 in\<open>fastforce dest: nyinitcls_emptyD\<close>) next case (Suc m) with mgf_hyp have mgf_hyp': "\ t. G,A\{=:m} t\ {G\}" by simp from is_cls obtain c where c: "the (class G C) = c" by auto let ?Q= "(\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 ((\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\{Normal (?P \. Not \ 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\{?P'} .(if C = Object then Skip else Init (super c)). {?Q}" proof (cases "C=Object") case True have"G,A\{?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\{?P'} .Init (super c). {?Q}" by (rule MGFnD' [THEN conseq12]) (fastforce simp add: False c) with False show ?thesis by simp qed next from Suc is_cls show"Normal (?P \. Not \ initd C ;. supd (init_class_obj G C)) \<Rightarrow> ?P'" by (fastforce elim: nyinitcls_le_SucD) qed next from mgf_hyp' show"\l. G,A\{?Q \. (\s. l = locals (snd s)) ;. set_lvars Map.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]) using c apply auto done qed qed thus"G,A\{Normal ?P \. Not \ initd C} .Init C. {?R}" by clarsimp qed qed lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
lemma MGFn_Call: assumes mgf_methds: "\C sig. G,(A::state triple set)\{=:n} \(Methd C sig)\\<^sub>e\ {G\}" and mgf_e: "G,A\{=:n} \e\\<^sub>e\ {G\}" and mgf_ps: "G,A\{=:n} \ps\\<^sub>l\ {G\}" and wf: "wf_prog G" shows"G,A\{=:n} \{accC,statT,mode}e\mn({pTs'}ps)\\<^sub>e\ {G\}" proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) note inj_term_simps [simp] fix T L accC' E assume wt: "\prg=G,cls=accC',lcl = L\\\({accC,statT,mode}e\mn( {pTs'}ps))\\<^sub>e\T" thenobtain pTs statDeclT statM where
wt_e: "\prg=G,cls=accC,lcl=L\\e\-RefT statT" and
wt_args: "\prg=G,cls=accC,lcl=L\\ps\\pTs" and
statM: "max_spec G accC statT \name=mn,parTs=pTs\
= {((statDeclT,statM),pTs')}" and
mode: "mode = invmode statM e"and
T: "T =Inl (resTy statM)"and
eq_accC_accC': "accC=accC'" by cases fastforce+ let ?Q="(\Y s1 (x,s) . x = None \
(\<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="\a. ((\Y (x2,s2) (x,s) . x = None \
(\<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"
show"G,A\{Normal ((\Y' s' s. s' = s \ abrupt s = None) \. G\init\n \.
(\<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\{Normal ?P} {accC,statT,mode}e\mn( {pTs'}ps)-\ {?S}") proof (rule ax_derivs.Call [where ?Q="?Q"and ?R="?R"]) from mgf_e show"G,A\{Normal ?P} e-\ {?Q}" proof (rule MGFnD' [THEN conseq12],clarsimp) fix s0 s1 a assume conf_s0: "Norm s0\\(G, L)" assume da: "\prg=G,cls=accC',lcl=L\\
dom (locals s0) \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E" assume eval_e: "G\Norm s0 \e-\a\ s1" show"(abrupt s1 = None \ G,store s1\a\\RefT statT) \
(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: "\prg=G,cls=accC,lcl=L\\
dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
da_ps: "\prg=G,cls=accC,lcl=L\\ nrm C \\ps\\<^sub>l\ E" by cases (simp add: eq_accC_accC') from eval_e conf_s0 wt_e da_e wf obtain"(abrupt s1 = None \ G,store s1\a\\RefT statT)" and"s1\\(G, L)" by (rule eval_type_soundE) simp moreoverhave"\P. \prg=G,cls=accC,lcl=L\\ dom (locals (store s1)) \\ps\\<^sub>l\ P" if normal_s1: "normal s1" proof - from eval_e wt_e da_e wf normal_s1 have"nrm C \ dom (locals (store s1))" by (cases rule: da_good_approxE') iprover with da_ps show ?thesis by (rule da_weakenE) iprover qed ultimatelyshow ?thesis using eq_accC_accC' by simp qed qed next show"\a. G,A\{?Q\In1 a} ps\\ {?R a}" (is "\ 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\\(G, L)" assume eval_e: "G\Norm s0 \e-\a\ s1" assume conf_a: "abrupt s1 = None \ G,store s1\a\\RefT statT" assume eval_ps: "G\s1 \ps\\vs\ s2" assume da_ps: "abrupt s1 = None \
(\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P)" show"(\s1. G\Norm s0 \e-\a\ s1 \
(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 "\prg=G,cls=accC,lcl=L\\ dom (locals (store s1)) \\ps\\<^sub>l\ P" by auto from eval_ps conf_s1 wt_args this wf have"s2\\(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"\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"\ 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 \name=mn, parTs=pTs'\ 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\\(G, L)" assume conf_a: "abrupt s1 = None \ G,store s1\a\\RefT statT" assume eval_e: "G\Norm s0 \e-\a\ s1" assume eval_ps: "G\s1 \ps\\vs\ s2" assume eval_mthd: "G\?s3 \Methd ?D \name=mn,parTs=pTs'\-\v\ s4" show"G\Norm s0 \{accC,statT,mode}e\mn( {pTs'}ps)-\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 \
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\s3' \Methd D \name=mn,parTs=pTs'\-\v\ 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\s0 \e-\v\ s1" and no_jmp: "abrupt s0 \ Some (Jump j)" and wt: "\prg=G, cls=C,lcl=L\\e\-T" and wf: "wf_prog G" shows"abrupt s1 \ Some (Jump j)" by (rule eval_expression_no_jump [where ?Env="\prg=G, cls=C,lcl=L\",simplified])
(use eval no_jmp wt wf in auto)
text\<open>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.\<close>
definition
unroll :: "prog \ label \ expr \ stmt \ (state \ state) set" where "unroll G l e c = {(s,t). \ 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) \ (unroll G l e c)\<^sup>*" and eval_e: "G\t \e-\v\ s'" and normal_termination: "normal s' \ \ the_Bool v" and wt: "\prg=G,cls=C,lcl=L\\e\-T" and wf: "wf_prog G" shows"G\s \l\ While(e) c\ s'" using unroll (* normal_s *) proof (induct rule: converse_rtrancl_induct) show"G\t \l\ While(e) c\ 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' \ Some (Jump (Cont l))" by (rule eval_expression_no_jump') (use normal_t in 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\s' \c\ s'" by auto moreoverfrom abrupt_s' no_cont have no_absorb: "(abupd (absorb (Cont l)) s')=s'" by (cases s') (simp add: absorb_def split: if_split) moreover from no_absorb abrupt_s' have"G\(abupd (absorb (Cont l)) s') \l\ While(e) c\ s'" by auto ultimatelyshow ?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) \ unroll G l e c" assume while: "G\s3 \l\ While(e) c\ s'" show"G\s \l\ While(e) c\ s'" proof - from unroll obtain v s1 s2 where
normal_s1: "normal s1"and
eval_e: "G\s \e-\v\ s1" and
continue: "the_Bool v"and
eval_c: "G\s1 \c\ 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: assumes mfg_e: "G,(A::state triple set)\{=:n} \e\\<^sub>e\ {G\}" and mfg_c: "G,A\{=:n} \c\\<^sub>s\ {G\}" and wf: "wf_prog G" shows"G,A\{=:n} \l\ While(e) c\\<^sub>s\ {G\}" proof (rule MGFn_free_wt [rule_format],elim exE) fix T L C assume wt: "\prg = G, cls = C, lcl = L\\\l\ While(e) c\\<^sub>s\T" thenobtain eT where
wt_e: "\prg = G, cls = C, lcl = L\\e\-eT" by cases simp show ?thesis proof (rule MGFn_NormalI) show"G,A\{Normal ((\Y' s' s. s' = s \ normal s) \. G\init\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'="(\ Y s' s. (s,s') \ (unroll G l e c)\<^sup>* ) \. G\init\n" and ?Q'="((\ Y s' s. (\ t b. (s,t) \ (unroll G l e c)\<^sup>* \
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\{(\Y s' s. (s, s') \ (unroll G l e c)\<^sup>*) \. G\init\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\{(\Y s' s. (s, s') \ (unroll G l e c)\<^sup>*) \. G\init\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) \ (unroll G l e c)\<^sup>*" moreover assume"G\s \e-\v\ s'" ultimately show"\t. (Z, t) \ (unroll G l e c)\<^sup>* \ G\t \e-\v\ s'" by blast qed next from mfg_c show"G,A\{Normal (((\Y s' s. \t b. (s, t) \ (unroll G l e c)\<^sup>* \
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) \ (unroll G l e c)\<^sup>*" assume eval_e: "G\t \e-\v\ Norm s" assume true: "the_Bool v" assume eval_c: "G\Norm s \c\ s'" show"(Z, abupd (absorb (Cont l)) s') \ (unroll G l e c)\<^sup>*" proof - note unroll also from eval_e true eval_c have"(t,abupd (absorb (Cont l)) s') \ unroll G l e c" by (unfold unroll_def) force ultimatelyshow ?thesis .. qed qed qed next show "\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: "\Z'. (Z', Norm s) \ (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 \ \ the_Bool v)) \ Y' = \" show"Y' = \ \ G\Norm s \l\ While(e) c\ s'" proof - from asm obtain v t where \<comment> \<open>\<^term>\<open>Z'\<close> gets instantiated with \<^term>\<open>Norm s\<close>\<close>
unroll: "(Norm s, t) \ (unroll G l e c)\<^sup>*" and
eval_e: "G\t \e-\v\ s'" and
normal_termination: "normal s' \ \ the_Bool v" and
Y': "Y' = \<diamondsuit>" by auto from unroll eval_e normal_termination wt_e wf have"G\Norm s \l\ While(e) c\ s'" by (rule unroll_while) with Y' show ?thesis by simp qed qed qed qed qed
lemma MGFn_FVar: fixes A :: "state triple set" assumes mgf_init: "G,A\{=:n} \Init statDeclC\\<^sub>s\ {G\}" and mgf_e: "G,A\{=:n} \e\\<^sub>e\ {G\}" and wf: "wf_prog G" shows"G,A\{=:n} \{accC,statDeclC,stat}e..fn\\<^sub>v\ {G\}" proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) note inj_term_simps [simp] fix T L accC' V assume wt: "\prg = G, cls = accC', lcl = L\\\{accC,statDeclC,stat}e..fn\\<^sub>v\T" thenobtain statC f where
wt_e: "\prg=G, cls=accC', lcl=L\\e\-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="(\Y s1 (x,s) . x = None \
(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\{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\{Normal ?P} {accC,statDeclC,stat}e..fn=\ {?R}") proof (rule ax_derivs.FVar [where ?Q="?Q" ]) from mgf_init show"G,A\{Normal ?P} .Init statDeclC. {?Q}" proof (rule MGFnD' [THEN conseq12],clarsimp) fix s s' assume conf_s: "Norm s\\(G, L)" assume da: "\prg=G,cls=accC',lcl=L\ \<turnstile> dom (locals s) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V" assume eval_init: "G\Norm s \Init statDeclC\ s'" show"(\E. \prg=G, cls=accC', lcl=L\\ dom (locals (store s')) \\e\\<^sub>e\ E) \
s'\\(G, L)" proof - from da obtain E where "\prg=G, cls=accC', lcl=L\\ dom (locals s) \\e\\<^sub>e\ E" by cases simp moreover from eval_init have"dom (locals s) \ dom (locals (store s'))" by (rule dom_locals_eval_mono [elim_format]) simp ultimatelyobtain E' where "\prg=G, cls=accC', lcl=L\\ dom (locals (store s')) \\e\\<^sub>e\ E'" by (rule da_weakenE) moreover have"s'\\(G, L)" proof - have wt_init: "\prg=G, cls=accC, lcl=L\\(Init statDeclC)\\" 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: "\prg=G,cls=accC,lcl=L\ \<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 ultimatelyshow ?thesis by iprover qed qed next from mgf_e show"G,A\{?Q} e-\ {\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\Norm s0 \Init statDeclC\ s1" assume eval_e: "G\s1 \e-\a\ s2" assume conf_s1: "s1\\(G, L)" assume da_e: "\prg=G,cls=accC',lcl=L\\ dom (locals (store s1)) \\e\\<^sub>e\ E" show"G\Norm s0 \{accC,statDeclC,stat}e..fn=\fst ?fvar\ 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\\(G, L)" and
conf_a: "normal s2 \ G,store s2\a\\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
lemma MGFn_Fin: assumes wf: "wf_prog G" and mgf_c1: "G,A\{=:n} \c1\\<^sub>s\ {G\}" and mgf_c2: "G,A\{=:n} \c2\\<^sub>s\ {G\}" shows"G,(A::state triple set)\{=:n} \c1 Finally c2\\<^sub>s\ {G\}" proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) fix T L accC C assume wt: "\prg=G,cls=accC,lcl=L\\In1r (c1 Finally c2)\T" thenobtain
wt_c1: "\prg=G,cls=accC,lcl=L\\c1\\" and
wt_c2: "\prg=G,cls=accC,lcl=L\\c2\\" by cases simp let ?Q = "(\Y' s' s. normal s \ G\s \c1\ s' \
(\<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\{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\{Normal ?P} .c1 Finally c2. {?R}") proof (rule ax_derivs.Fin [where ?Q="?Q"]) from mgf_c1 show"G,A\{Normal ?P} .c1. {?Q}" proof (rule MGFnD' [THEN conseq12],clarsimp) fix s0 assume"\prg=G,cls=accC,lcl=L\\ dom (locals s0) \\c1 Finally c2\\<^sub>s\ C" thus"\C1. \prg=G,cls=accC,lcl=L\\ dom (locals s0) \\c1\\<^sub>s\ C1" by cases (auto simp add: inj_term_simps) qed next from mgf_c2 show"\abr. G,A\{?Q \. (\s. abr = abrupt s) ;. abupd (\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:"\prg=G,cls=accC,lcl=L\\ dom (locals s0) \\c1\\<^sub>s\ C1" assume conf_s0: "Norm s0\\(G, L)" assume eval_c1: "G\Norm s0 \c1\ s1" assume eval_c2: "G\abupd (\abr. None) s1 \c2\ s2" show"G\Norm s0 \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) with eval_c1 eval_c2 obtain
eval_c1': "G\Norm s0 \c1\ (abr1,str1)" and
eval_c2': "G\Norm str1 \c2\ s2" by simp obtain s3 where
s3: "s3 = (if \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 \ 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\Norm s0 \Init D\ s1" and eval_c: "G\s1 \c\ s2" and jmpOk: "jumpNestingOkS {Ret} c" and wt_c: "\prg=G, cls=C, lcl=L\\c\\" and clsD: "class G D=Some d" and wf: "wf_prog G" shows"\ l. abrupt s2 \ Some (Jump (Break l)) \
abrupt s2 \<noteq> Some (Jump (Cont l))" proof fix l show"abrupt s2 \ Some (Jump (Break l)) \
abrupt s2 \<noteq> Some (Jump (Cont l))" proof - fix accC from clsD have wt_init: "\prg=G, cls=accC, lcl=L\\(Init D)\\" by auto have s1_no_jmp: "\ j. abrupt s1 \ Some (Jump j)" by (rule eval_statement_no_jump [OF _ _ _ wt_init]) (use eval_init wf in auto) from eval_c _ wt_c wf show ?thesis by (rule jumpNestingOk_eval [THEN conjE, elim_format]) (use jmpOk s1_no_jmp in auto) qed qed
lemma MGFn_Body: assumes wf: "wf_prog G" and mgf_init: "G,A\{=:n} \Init D\\<^sub>s\ {G\}" and mgf_c: "G,A\{=:n} \c\\<^sub>s\ {G\}" shows"G,(A::state triple set)\{=:n} \Body D c\\<^sub>e\ {G\}" proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) fix T L accC E assume wt: "\prg=G, cls=accC,lcl=L\\\Body D c\\<^sub>e\T" let ?Q="(\Y' s' s. normal s \ G\s \Init D\ s' \ jumpNestingOkS {Ret} c) \<and>. G\<turnstile>init\<le>n" show"G,A\{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\{Normal ?P} Body D c-\ {?R}") proof (rule ax_derivs.Body [where ?Q="?Q"]) from mgf_init show"G,A\{Normal ?P} .Init D. {?Q}" proof (rule MGFnD' [THEN conseq12],clarsimp) fix s0 assume da: "\prg=G,cls=accC,lcl=L\\ dom (locals s0) \\Body D c\\<^sub>e\ E" thus"jumpNestingOkS {Ret} c" by cases simp qed next from mgf_c show"G,A\{?Q}.c.{\s.. abupd (absorb Ret) .; ?R\\the (locals s Result)\\<^sub>e}" proof (rule MGFnD' [THEN conseq12],clarsimp) fix s0 s1 s2 assume eval_init: "G\Norm s0 \Init D\ s1" assume eval_c: "G\s1 \c\ s2" assume nestingOk: "jumpNestingOkS {Ret} c" show"G\Norm s0 \Body D c-\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: "\prg = G, cls = accC, lcl = L\\c\\" by cases auto obtain s3 where
s3: "s3= (if \l. fst s2 = Some (Jump (Break l)) \
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
lemma MGFn_lemma: assumes mgf_methds: "\ n. \ C sig. G,(A::state triple set)\{=:n} \Methd C sig\\<^sub>e\ {G\}" and wf: "wf_prog G" shows"\ t. G,A\{=:n} t\ {G\}" proof (induct rule: full_nat_induct) fix n t assume hyp: "\ m. Suc m \ n \ (\ t. G,A\{=:m} t\ {G\})" show"G,A\{=:n} t\ {G\}" proof - fix v e c es have"G,A\{=:n} \v\\<^sub>v\ {G\}" and "G,A\{=:n} \e\\<^sub>e\ {G\}" and "G,A\{=:n} \c\\<^sub>s\ {G\}" and "G,A\{=:n} \es\\<^sub>l\ {G\}" for v e c es proof (induct rule: compat_var.induct compat_expr.induct compat_stmt.induct compat_expr_list.induct) case (LVar v) show"G,A\{=:n} \LVar v\\<^sub>v\ {G\}" 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) from MGFn_Init [OF hyp] and\<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> and wf show ?case by (rule MGFn_FVar) next case (AVar e1 e2) note mgf_e1 = \<open>G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> note mgf_e2 = \<open>G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> show"G,A\{=:n} \e1.[e2]\\<^sub>v\ {G\}" 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 (fastforce 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 (fastforce intro: eval.NewC) done next case (NewA T e) thus ?case apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.NewA
[where ?Q = "(\Y' s' s. normal s \ G\s \In1r (init_comp_ty T) \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"]) apply (simp add: init_comp_ty_def split: if_split) 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 (fastforce 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 (fastforce 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 (fastforce intro: eval.Inst) done next case (Lit v) show ?case apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.Lit [THEN conseq1]) apply (fastforce 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 (fastforce 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 (fastforce 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 (fastforce intro: eval.BinOp) done next case Super show ?case apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.Super [THEN conseq1]) apply (fastforce 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 (fastforce intro: eval.Acc simp add: split_paired_all) done next case (Ass v e) thus"G,A\{=:n} \v:=e\\<^sub>e\ {G\}" 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 (fastforce intro: eval.Ass simp add: split_paired_all) done next case (Cond e1 e2 e3) thus"G,A\{=:n} \e1 ? e2 : e3\\<^sub>e\ {G\}" 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 (fastforce intro: eval.Cond) apply (case_tac "b") apply simp apply (erule MGFnD'[THEN conseq12]) apply (fastforce intro: eval.Cond) apply simp apply (erule MGFnD'[THEN conseq12]) apply (fastforce intro: eval.Cond) done next case (Call accC statT mode e mn pTs' ps) note mgf_e = \<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> note mgf_ps = \<open>G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}\<close> from mgf_methds mgf_e mgf_ps wf show"G,A\{=:n} \{accC,statT,mode}e\mn({pTs'}ps)\\<^sub>e\ {G\}" by (rule MGFn_Call) next case (Methd D mn) from mgf_methds show"G,A\{=:n} \Methd D mn\\<^sub>e\ {G\}" by simp next case (Body D c) note mgf_c = \<open>G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close> from wf MGFn_Init [OF hyp] mgf_c show"G,A\{=:n} \Body D c\\<^sub>e\ {G\}" 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 (fastforce 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 (fastforce intro: eval.Expr) done next case (Lab l c) thus"G,A\{=:n} \l\ c\\<^sub>s\ {G\}" apply - apply (rule MGFn_NormalI) apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab]) apply (fastforce intro: eval.Lab) done next case (Comp c1 c2) thus"G,A\{=:n} \c1;; c2\\<^sub>s\ {G\}" apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.Comp) apply (erule MGFnD [THEN ax_NormalD]) apply (erule MGFnD' [THEN conseq12]) apply (fastforce intro: eval.Comp) done next case (If' e c1 c2) thus"G,A\{=:n} \If(e) c1 Else c2\\<^sub>s\ {G\}" 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 (fastforce intro: eval.If) apply (case_tac "b") apply simp apply (erule MGFnD' [THEN conseq12]) apply (fastforce intro: eval.If) apply simp apply (erule MGFnD' [THEN conseq12]) apply (fastforce intro: eval.If) done next case (Loop l e c) note mgf_e = \<open>G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}\<close> note mgf_c = \<open>G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close> from mgf_e mgf_c wf show"G,A\{=:n} \l\ While(e) c\\<^sub>s\ {G\}" 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) done next case (Throw e) thus ?case apply - apply (rule MGFn_NormalI) apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw]) apply (fastforce intro: eval.Throw) done next case (TryC c1 C vn c2) thus"G,A\{=:n} \Try c1 Catch(C vn) c2\\<^sub>s\ {G\}" apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.Try [where
?Q = " (\Y' s' s. normal s \ (\s''. G\s \\c1\\<^sub>s\\ (Y',s'') \
G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n"]) apply (erule MGFnD [THEN ax_NormalD, THEN conseq2]) apply (fastforce elim: sxalloc_gext [THEN card_nyinitcls_gext]) apply (erule MGFnD'[THEN conseq12]) apply (fastforce intro: eval.Try) apply (fastforce intro: eval.Try) done next case (Fin c1 c2) note mgf_c1 = \<open>G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close> note mgf_c2 = \<open>G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}\<close> from wf mgf_c1 mgf_c2 show"G,A\{=:n} \c1 Finally c2\\<^sub>s\ {G\}" 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\{=:n} \Init C\\<^sub>s\ {G\}" by (rule MGFn_Init) next case Nil_expr show"G,A\{=:n} \[]\\<^sub>l\ {G\}" apply - apply (rule MGFn_NormalI) apply (rule ax_derivs.Nil [THEN conseq1]) apply (fastforce intro: eval.Nil) done next case (Cons_expr e es) thus"G,A\{=:n} \e# es\\<^sub>l\ {G\}" 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 (fastforce intro: eval.Cons) done qed thus ?thesis by (cases rule: term_cases) auto qed qed
lemma MGF_asm: "\\C sig. is_methd G C sig \ G,A\{\} In1l (Methd C sig)\ {G\}; wf_prog G\ \<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}" apply (simp (no_asm_use) add: MGF_MGFn_iff) apply (rule allI) apply (rule MGFn_lemma) apply (intro strip) apply (rule MGFn_free_wt) apply (force dest: wt_Methd_is_methd) apply assumption (* wf_prog G *) done
subsubsection "nested version"
lemma nesting_lemma' [rule_format (no_asm)]: assumes ax_derivs_asm: "\A ts. ts \ A \ P A ts" and MGF_nested_Methd: "\A pn. \b\bdy pn. P (insert (mgf_call pn) A) {mgf b} \<Longrightarrow> P A {mgf_call pn}" and MGF_asm: "\A t. \pn\U. P A {mgf_call pn} \ P A {mgf t}" and finU: "finite U" and uA: "uA = mgf_call`U" shows"\A. A \ uA \ n \ card uA \ 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 \<^context>)") apply (tactic \<open>dresolve_tac \<^context> [Thm.permute_prems 0 1 @{thm card_seteq}] 1\<close>) 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 hypsubst_thin apply fast apply (drule finite_subset) apply (erule finite_imageI) apply auto done
lemma nesting_lemma [rule_format (no_asm)]: assumes ax_derivs_asm: "\A ts. ts \ A \ P A ts" and MGF_nested_Methd: "\A pn. \b\bdy pn. P (insert (mgf (f pn)) A) {mgf b} \<Longrightarrow> P A {mgf (f pn)}" and MGF_asm: "\A t. \pn\U. P A {mgf (f pn)} \ 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: "\
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) apply clarsimp apply (erule MethdI) done
lemma MGF_deriv: "wf_prog G \ G,({}::state triple set)\{\} t\ {G\}" apply (rule MGFNormalI) apply (rule_tac mgf = "\t. {Normal \} t\ {G\}" and
bdy = "\ (C,sig) .{\body G C sig\\<^sub>e }" and
f = "\ (C,sig) . \Methd C sig\\<^sub>e " in nesting_lemma) apply (erule ax_derivs.asm) apply (clarsimp simp add: split_tupled_all) apply (erule MGF_nested_Methd) apply (erule_tac [2] finite_is_methd [OF wf_ws_prog]) apply (rule MGF_asm [THEN MGFNormalD]) apply (auto intro: MGFNormalI) done
subsubsection "simultaneous version"
lemma MGF_simult_Methd_lemma: "finite 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) prefer 2 apply (rule ax_derivs.asm) apply fast apply clarsimp apply (rule conseq2) apply (erule (1) ax_methods_spec) apply clarsimp apply (erule eval_Methd) done
lemma MGF_simult_Methd: "wf_prog G \
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.35 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
