wenzelm@12857: (*  Title:      HOL/Bali/AxCompl.thy
schirmer@13688:     Author:     David von Oheimb and Norbert Schirmer
schirmer@12854: *)
schirmer@12854: 
wenzelm@58887: subsection {*
schirmer@12854: Completeness proof for Axiomatic semantics of Java expressions and statements
schirmer@12854: *}
schirmer@12854: 
haftmann@16417: theory AxCompl imports AxSem begin
schirmer@12854: 
schirmer@12854: text {*
schirmer@12854: design issues:
schirmer@12854: \begin{itemize}
schirmer@12854: \item proof structured by Most General Formulas (-> Thomas Kleymann)
schirmer@12854: \end{itemize}
schirmer@12854: *}
schirmer@12925: 
schirmer@12925: 
schirmer@12925: 
schirmer@13688:            
wenzelm@58887: subsubsection "set of not yet initialzed classes"
schirmer@12854: 
wenzelm@37956: definition
wenzelm@37956:   nyinitcls :: "prog \<Rightarrow> state \<Rightarrow> qtname set"
wenzelm@37956:   where "nyinitcls G s = {C. is_class G C \<and> \<not> initd C s}"
schirmer@12854: 
schirmer@12854: lemma nyinitcls_subset_class: "nyinitcls G s \<subseteq> {C. is_class G C}"
schirmer@12854: apply (unfold nyinitcls_def)
schirmer@12854: apply fast
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemmas finite_nyinitcls [simp] =
wenzelm@45605:    finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset]]
schirmer@12854: 
schirmer@12854: lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
schirmer@12854: apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma nyinitcls_set_locals_cong [simp]: 
schirmer@12854:   "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"
wenzelm@48001:   by (simp add: nyinitcls_def)
schirmer@12854: 
schirmer@12854: lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"
wenzelm@48001:   by (simp add: nyinitcls_def)
schirmer@12854: 
wenzelm@48001: lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s"
wenzelm@48001:   by (simp add: nyinitcls_def)
schirmer@12854: 
schirmer@12854: lemma card_nyinitcls_abrupt_congE [elim!]: 
wenzelm@48001:   "card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n"
wenzelm@48001:   unfolding nyinitcls_def by auto
schirmer@12854: 
schirmer@12854: lemma nyinitcls_new_xcpt_var [simp]: 
wenzelm@48001:   "nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
wenzelm@48001:   by (induct s) (simp_all add: nyinitcls_def)
schirmer@12854: 
schirmer@12854: lemma nyinitcls_init_lvars [simp]: 
schirmer@12854:   "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
wenzelm@48001:   by (induct s) (simp add: init_lvars_def2 split add: split_if)
schirmer@12854: 
schirmer@12854: lemma nyinitcls_emptyD: "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s"
wenzelm@48001:   unfolding nyinitcls_def by fast
schirmer@12854: 
schirmer@13688: lemma card_Suc_lemma: 
schirmer@13688:   "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n"
wenzelm@48001:   by auto
schirmer@12854: 
schirmer@12854: lemma nyinitcls_le_SucD: 
schirmer@12854: "\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; \<not>inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow> 
schirmer@12854:   card (nyinitcls G (x,init_class_obj G C s)) \<le> n"
schirmer@12854: apply (subgoal_tac 
schirmer@12854:         "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
schirmer@12854: apply  clarsimp
wenzelm@59807: apply  (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
schirmer@12854: apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
schirmer@12854: apply   (auto dest!: not_initedD elim!: 
schirmer@12854:               simp add: nyinitcls_def inited_def split add: split_if_asm)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: lemma inited_gext': "\<lbrakk>s\<le>|s';inited C (globs s)\<rbrakk> \<Longrightarrow> inited C (globs s')"
wenzelm@48001:   by (rule inited_gext)
schirmer@12854: 
schirmer@12854: lemma nyinitcls_gext: "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s"
wenzelm@48001:   unfolding nyinitcls_def by (force dest!: inited_gext')
schirmer@12854: 
schirmer@12854: lemma card_nyinitcls_gext: 
schirmer@12854:   "\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n"
schirmer@12854: apply (rule le_trans)
schirmer@12854: apply  (rule card_mono)
schirmer@12854: apply   (rule finite_nyinitcls)
schirmer@12854: apply  (erule nyinitcls_gext)
schirmer@12854: apply assumption
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
wenzelm@58887: subsubsection "init-le"
schirmer@12854: 
wenzelm@37956: definition
wenzelm@37956:   init_le :: "prog \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool" ("_\<turnstile>init\<le>_"  [51,51] 50)
wenzelm@37956:   where "G\<turnstile>init\<le>n = (\<lambda>s. card (nyinitcls G s) \<le> n)"
schirmer@12854:   
schirmer@12854: lemma init_le_def2 [simp]: "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)"
schirmer@12854: apply (unfold init_le_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@13688: lemma All_init_leD: 
schirmer@13688:  "\<forall>n::nat. G,(A::'a triple set)\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q::'a assn} 
schirmer@13688:   \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
schirmer@12854: apply (drule spec)
schirmer@12854: apply (erule conseq1)
schirmer@12854: apply clarsimp
schirmer@12854: apply (rule card_nyinitcls_bound)
schirmer@12854: done
schirmer@12854: 
wenzelm@58887: subsubsection "Most General Triples and Formulas"
schirmer@12854: 
wenzelm@37956: definition
wenzelm@37956:   remember_init_state :: "state assn" ("\<doteq>")
wenzelm@37956:   where "\<doteq> \<equiv> \<lambda>Y s Z. s = Z"
schirmer@12854: 
schirmer@12854: lemma remember_init_state_def2 [simp]: "\<doteq> Y = op ="
schirmer@12854: apply (unfold remember_init_state_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
wenzelm@37956: definition
schirmer@12854:   MGF ::"[state assn, term, prog] \<Rightarrow> state triple"   ("{_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
wenzelm@37956:   where "{P} t\<succ> {G\<rightarrow>} = {P} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
schirmer@12854: 
wenzelm@37956: definition
wenzelm@37956:   MGFn :: "[nat, term, prog] \<Rightarrow> state triple" ("{=:_} _\<succ> {_\<rightarrow>}"[3,65,3]62)
wenzelm@37956:   where "{=:n} t\<succ> {G\<rightarrow>} = {\<doteq> \<and>. G\<turnstile>init\<le>n} t\<succ> {G\<rightarrow>}"
schirmer@12854: 
schirmer@12854: (* unused *)
schirmer@12925: lemma MGF_valid: "wf_prog G \<Longrightarrow> G,{}\<Turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (unfold MGF_def)
schirmer@12925: apply (simp add:  ax_valids_def triple_valid_def2)
schirmer@12925: apply (auto elim: evaln_eval)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: 
schirmer@12854: lemma MGF_res_eq_lemma [simp]: 
schirmer@12854:   "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)"
wenzelm@48001:   by auto
schirmer@12854: 
schirmer@12854: lemma MGFn_def2: 
schirmer@12854: "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{\<doteq> \<and>. G\<turnstile>init\<le>n} 
schirmer@12854:                     t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}"
wenzelm@48001:   unfolding MGFn_def MGF_def by fast
schirmer@12854: 
schirmer@13688: lemma MGF_MGFn_iff: 
schirmer@13688: "G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})"
wenzelm@48001: apply (simp add: MGFn_def2 MGF_def)
schirmer@12854: apply safe
schirmer@12854: apply  (erule_tac [2] All_init_leD)
schirmer@12854: apply (erule conseq1)
schirmer@12854: apply clarsimp
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma MGFnD: 
schirmer@13688: "G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854:  G,A\<turnstile>{(\<lambda>Y' s' s. s' = s           \<and> P s) \<and>. G\<turnstile>init\<le>n}  
schirmer@12854:  t\<succ>  {(\<lambda>Y' s' s. G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(Y',s') \<and> P s) \<and>. G\<turnstile>init\<le>n}"
schirmer@12854: apply (unfold init_le_def)
schirmer@12854: apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854: apply (erule conseq12)
schirmer@12854: apply clarsimp
schirmer@12854: apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
schirmer@12854: done
schirmer@12854: lemmas MGFnD' = MGFnD [of _ _ _ _ "\<lambda>x. True"] 
schirmer@12854: 
schirmer@13688: text {* To derive the most general formula, we can always assume a normal
schirmer@13688: state in the precondition, since abrupt cases can be handled uniformally by
schirmer@13688: the abrupt rule.
schirmer@13688: *}
schirmer@12854: lemma MGFNormalI: "G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow>  
schirmer@12854:   G,(A::state triple set)\<turnstile>{\<doteq>::state assn} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (unfold MGF_def)
schirmer@12854: apply (rule ax_Normal_cases)
schirmer@12854: apply  (erule conseq1)
schirmer@12854: apply  clarsimp
schirmer@12854: apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854: apply (clarsimp simp add: Let_def)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: lemma MGFNormalD: 
schirmer@13688: "G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal \<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (unfold MGF_def)
schirmer@12854: apply (erule conseq1)
schirmer@12854: apply clarsimp
schirmer@12854: done
schirmer@12854: 
schirmer@13688: text {* Additionally to @{text MGFNormalI}, we also expand the definition of 
schirmer@13688: the most general formula here *} 
schirmer@12854: lemma MGFn_NormalI: 
schirmer@12854: "G,(A::state triple set)\<turnstile>{Normal((\<lambda>Y' s' s. s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)}t\<succ> 
schirmer@12854:  {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12854: apply (simp (no_asm_use) add: MGFn_def2)
schirmer@12854: apply (rule ax_Normal_cases)
schirmer@12854: apply  (erule conseq1)
schirmer@12854: apply  clarsimp
schirmer@12854: apply (rule ax_derivs.Abrupt [THEN conseq1])
schirmer@12854: apply (clarsimp simp add: Let_def)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688: welltyped terms, since all others can be uniformally handled by the hazard
schirmer@13688: rule. *} 
schirmer@12854: lemma MGFn_free_wt: 
schirmer@12854:   "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
schirmer@12854:     \<longrightarrow> G,(A::state triple set)\<turnstile>{=:n} t\<succ> {G\<rightarrow>} 
schirmer@12854:    \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (rule MGFn_NormalI)
schirmer@12854: apply (rule ax_free_wt)
schirmer@12854: apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
schirmer@12854: done
schirmer@12854: 
schirmer@13688: text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688: welltyped terms and assume that the state in the precondition conforms to the
schirmer@13688: environment. All type violations can be uniformally handled by the hazard
schirmer@13688: rule. *} 
schirmer@12925: lemma MGFn_free_wt_NormalConformI: 
schirmer@13688: "(\<forall> T L C . \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T 
schirmer@12925:   \<longrightarrow> G,(A::state triple set)
schirmer@12925:       \<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))}
schirmer@12925:       t\<succ> 
schirmer@12925:       {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
schirmer@12925:  \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@12925: apply (rule MGFn_NormalI)
schirmer@12925: apply (rule ax_no_hazard)
schirmer@12925: apply (rule ax_escape)
schirmer@12925: apply (intro strip)
schirmer@12925: apply (simp only: type_ok_def peek_and_def)
schirmer@12925: apply (erule conjE)+
schirmer@13688: apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
schirmer@13688:        erule conjE)
schirmer@12925: apply (drule spec,drule spec, drule spec, drule (1) mp)
schirmer@12925: apply (erule conseq12)
schirmer@12925: apply blast
schirmer@12925: done
schirmer@12925: 
schirmer@13688: text {* To derive the most general formula, we can restrict ourselves to 
schirmer@13688: welltyped terms and assume that the state in the precondition conforms to the
schirmer@13688: environment and that the term is definetly assigned with respect to this state.
schirmer@13688: All type violations can be uniformally handled by the hazard rule. *} 
schirmer@13688: lemma MGFn_free_wt_da_NormalConformI: 
schirmer@13688: "(\<forall> T L C B. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T
schirmer@13688:   \<longrightarrow> G,(A::state triple set)
schirmer@13688:       \<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))
schirmer@13688:         \<and>. (\<lambda> s. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>B)}
schirmer@13688:       t\<succ> 
schirmer@13688:       {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y,s')}) 
schirmer@13688:  \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}"
schirmer@13688: apply (rule MGFn_NormalI)
schirmer@13688: apply (rule ax_no_hazard)
schirmer@13688: apply (rule ax_escape)
schirmer@13688: apply (intro strip)
schirmer@13688: apply (simp only: type_ok_def peek_and_def)
schirmer@13688: apply (erule conjE)+
schirmer@13688: apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
schirmer@13688:        erule conjE)
schirmer@13688: apply (drule spec,drule spec, drule spec,drule spec, drule (1) mp)
schirmer@13688: apply (erule conseq12)
schirmer@13688: apply blast
schirmer@13688: done
schirmer@12854: 
wenzelm@58887: subsubsection "main lemmas"
schirmer@12854: 
schirmer@13688: lemma MGFn_Init: 
schirmer@13688:  assumes mgf_hyp: "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
schirmer@13688:  shows "G,(A::state triple set)\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI)
schirmer@13688:   fix T L accC
schirmer@13688:   assume "\<lparr>prg=G, cls=accC, lcl= L\<rparr>\<turnstile>\<langle>Init C\<rangle>\<^sub>s\<Colon>T"
schirmer@13688:   hence is_cls: "is_class G C"
schirmer@13688:     by cases simp
schirmer@13688:   show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)} 
schirmer@13688:             .Init C.
schirmer@13688:             {\<lambda>Y s' s. G\<turnstile>s \<midarrow>\<langle>Init C\<rangle>\<^sub>s\<succ>\<rightarrow> (Y, s')}"
schirmer@13688:        (is "G,A\<turnstile>{Normal ?P} .Init C. {?R}")
schirmer@13688:   proof (rule ax_cases [where ?C="initd C"])
schirmer@13688:     show "G,A\<turnstile>{Normal ?P  \<and>. initd C} .Init C. {?R}"
nipkow@44890:       by (rule ax_derivs.Done [THEN conseq1]) (fastforce intro: init_done)
schirmer@13688:   next
schirmer@13688:     have "G,A\<turnstile>{Normal (?P  \<and>. Not \<circ> initd C)} .Init C. {?R}" 
schirmer@13688:     proof (cases n)
schirmer@13688:       case 0
schirmer@13688:       with is_cls
schirmer@13688:       show ?thesis
nipkow@44890:         by - (rule ax_impossible [THEN conseq1],fastforce dest: nyinitcls_emptyD)
schirmer@13688:     next
schirmer@13688:       case (Suc m)
schirmer@13688:       with mgf_hyp have mgf_hyp': "\<And> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}"
wenzelm@32960:         by simp
schirmer@13688:       from is_cls obtain c where c: "the (class G C) = c"
wenzelm@32960:         by auto
schirmer@13688:       let ?Q= "(\<lambda>Y s' (x,s) . 
schirmer@13688:           G\<turnstile> (x,init_class_obj G C s) 
schirmer@13688:              \<midarrow> (if C=Object then Skip else Init (super (the (class G C))))\<rightarrow> s'
schirmer@13688:           \<and> x=None \<and> \<not>inited C (globs s)) \<and>. G\<turnstile>init\<le>m"
schirmer@13688:       from c
schirmer@13688:       show ?thesis
schirmer@13688:       proof (rule ax_derivs.Init [where ?Q="?Q"])
wenzelm@32960:         let ?P' = "Normal ((\<lambda>Y s' s. s' = supd (init_class_obj G C) s 
schirmer@13688:                            \<and> normal s \<and> \<not> initd C s) \<and>. G\<turnstile>init\<le>m)" 
wenzelm@32960:         show "G,A\<turnstile>{Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))}
schirmer@13688:                   .(if C = Object then Skip else Init (super c)). 
schirmer@13688:                   {?Q}"
wenzelm@32960:         proof (rule conseq1 [where ?P'="?P'"])
wenzelm@32960:           show "G,A\<turnstile>{?P'} .(if C = Object then Skip else Init (super c)). {?Q}"
wenzelm@32960:           proof (cases "C=Object")
wenzelm@32960:             case True
wenzelm@32960:             have "G,A\<turnstile>{?P'} .Skip. {?Q}"
wenzelm@32960:               by (rule ax_derivs.Skip [THEN conseq1])
wenzelm@32960:                  (auto simp add: True intro: eval.Skip)
schirmer@13688:             with True show ?thesis 
wenzelm@32960:               by simp
wenzelm@32960:           next
wenzelm@32960:             case False
wenzelm@32960:             from mgf_hyp'
wenzelm@32960:             have "G,A\<turnstile>{?P'} .Init (super c). {?Q}"
nipkow@44890:               by (rule MGFnD' [THEN conseq12]) (fastforce simp add: False c)
wenzelm@32960:             with False show ?thesis
wenzelm@32960:               by simp
wenzelm@32960:           qed
wenzelm@32960:         next
wenzelm@32960:           from Suc is_cls
wenzelm@32960:           show "Normal (?P \<and>. Not \<circ> initd C ;. supd (init_class_obj G C))
schirmer@13688:                 \<Rightarrow> ?P'"
nipkow@44890:             by (fastforce elim: nyinitcls_le_SucD)
wenzelm@32960:         qed
schirmer@13688:       next
wenzelm@32960:         from mgf_hyp'
wenzelm@32960:         show "\<forall>l. G,A\<turnstile>{?Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty} 
schirmer@13688:                       .init c.
schirmer@13688:                       {set_lvars l .; ?R}"
wenzelm@32960:           apply (rule MGFnD' [THEN conseq12, THEN allI])
wenzelm@32960:           apply (clarsimp simp add: split_paired_all)
wenzelm@32960:           apply (rule eval.Init [OF c])
wenzelm@32960:           apply (insert c)
wenzelm@32960:           apply auto
wenzelm@32960:           done
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:     thus "G,A\<turnstile>{Normal ?P  \<and>. Not \<circ> initd C} .Init C. {?R}"
schirmer@13688:       by clarsimp
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12854: lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]
schirmer@12854: 
schirmer@12854: lemma MGFn_Call: 
schirmer@13688:   assumes mgf_methds: 
schirmer@13688:            "\<forall>C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>(Methd C sig)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688:   and mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688:   and mgf_ps: "G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
schirmer@13688:   and wf: "wf_prog G"
schirmer@13688:   shows "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
schirmer@13688:   note inj_term_simps [simp]
schirmer@13688:   fix T L accC' E
schirmer@13688:   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"
schirmer@13688:   then obtain pTs statDeclT statM where
schirmer@13688:                  wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
schirmer@13688:               wt_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>ps\<Colon>\<doteq>pTs" and
schirmer@13688:                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@13688:                          = {((statDeclT,statM),pTs')}" and
schirmer@13688:                  mode: "mode = invmode statM e" and
schirmer@13688:                     T: "T =Inl (resTy statM)" and
schirmer@13688:         eq_accC_accC': "accC=accC'"
nipkow@44890:         by cases fastforce+
schirmer@13688:   let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@13688:               (\<exists>a. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> 
schirmer@13688:                    (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)
schirmer@13688:                    \<and> Y = In1 a) \<and> 
schirmer@13688:               (\<exists> P. normal s1
schirmer@13688:                   \<longrightarrow> \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright>P)) 
schirmer@13688:           \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))::state assn"
schirmer@13688:   let ?R="\<lambda>a. ((\<lambda>Y (x2,s2) (x,s) . x = None \<and> 
schirmer@13688:                 (\<exists>s1 pvs. G\<turnstile>Norm s \<midarrow>e-\<succ>a\<rightarrow> s1 \<and> 
schirmer@13688:                           (normal s1 \<longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT)\<and> 
schirmer@13688:                           Y = \<lfloor>pvs\<rfloor>\<^sub>l \<and> G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2))) 
schirmer@13688:                \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L)))::state assn"
schirmer@12925: 
schirmer@13688:   show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688:                      (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688:                      (\<lambda>s. \<lparr>prg=G, cls=accC',lcl=L\<rparr> \<turnstile> dom (locals (store s)) 
schirmer@13688:                            \<guillemotright> \<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E))}
schirmer@13688:              {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>
schirmer@13688:              {\<lambda>Y s' s. \<exists>v. Y = \<lfloor>v\<rfloor>\<^sub>e \<and> 
schirmer@13688:                            G\<turnstile>s \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v\<rightarrow> s'}"
schirmer@13688:     (is "G,A\<turnstile>{Normal ?P} {accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ> {?S}")
schirmer@13688:   proof (rule ax_derivs.Call [where ?Q="?Q" and ?R="?R"])
schirmer@13688:     from mgf_e
schirmer@13688:     show "G,A\<turnstile>{Normal ?P} e-\<succ> {?Q}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s0 s1 a
schirmer@13688:       assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
schirmer@13688:       assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> 
schirmer@13688:                      dom (locals s0) \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688:       assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
schirmer@13688:       show "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
schirmer@13688:             (abrupt s1 = None \<longrightarrow>
schirmer@13688:               (\<exists>P. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P))
schirmer@13688:             \<and> s1\<Colon>\<preceq>(G, L)"
schirmer@13688:       proof -
wenzelm@32960:         from da obtain C where
wenzelm@32960:           da_e:  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>
schirmer@13688:                     dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> C" and
wenzelm@32960:           da_ps: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm C \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> E" 
wenzelm@32960:           by cases (simp add: eq_accC_accC')
wenzelm@32960:         from eval_e conf_s0 wt_e da_e wf
wenzelm@32960:         obtain "(abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT)"
wenzelm@32960:           and  "s1\<Colon>\<preceq>(G, L)"
wenzelm@32960:           by (rule eval_type_soundE) simp
wenzelm@32960:         moreover
wenzelm@32960:         {
wenzelm@32960:           assume normal_s1: "normal s1"
wenzelm@32960:           have "\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
wenzelm@32960:           proof -
wenzelm@32960:             from eval_e wt_e da_e wf normal_s1
wenzelm@32960:             have "nrm C \<subseteq>  dom (locals (store s1))"
wenzelm@32960:               by (cases rule: da_good_approxE') iprover
wenzelm@32960:             with da_ps show ?thesis
wenzelm@32960:               by (rule da_weakenE) iprover
wenzelm@32960:           qed
wenzelm@32960:         }
wenzelm@32960:         ultimately show ?thesis
wenzelm@32960:           using eq_accC_accC' by simp
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   next
schirmer@13688:     show "\<forall>a. G,A\<turnstile>{?Q\<leftarrow>In1 a} ps\<doteq>\<succ> {?R a}" (is "\<forall> a. ?PS a")
schirmer@13688:     proof 
schirmer@13688:       fix a  
schirmer@13688:       show "?PS a"
schirmer@13688:       proof (rule MGFnD' [OF mgf_ps, THEN conseq12],
schirmer@13688:              clarsimp simp add: eq_accC_accC' [symmetric])
wenzelm@32960:         fix s0 s1 s2 vs
wenzelm@32960:         assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
wenzelm@32960:         assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
wenzelm@32960:         assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
wenzelm@32960:         assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
wenzelm@32960:         assume da_ps: "abrupt s1 = None \<longrightarrow> 
schirmer@13688:                        (\<exists>P. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
schirmer@13688:                                dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P)"
wenzelm@32960:         show "(\<exists>s1. G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1 \<and>
schirmer@13688:                 (abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT) \<and>
schirmer@13688:                 G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2) \<and>
schirmer@13688:               s2\<Colon>\<preceq>(G, L)"
wenzelm@32960:         proof (cases "normal s1")
wenzelm@32960:           case True
wenzelm@32960:           with da_ps obtain P where
wenzelm@32960:            "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>ps\<rangle>\<^sub>l\<guillemotright> P"
wenzelm@32960:             by auto
wenzelm@32960:           from eval_ps conf_s1 wt_args this wf
wenzelm@32960:           have "s2\<Colon>\<preceq>(G, L)"
wenzelm@32960:             by (rule eval_type_soundE)
wenzelm@32960:           with eval_e conf_a eval_ps 
wenzelm@32960:           show ?thesis 
wenzelm@32960:             by auto
wenzelm@32960:         next
wenzelm@32960:           case False
wenzelm@32960:           with eval_ps have "s2=s1" by auto
wenzelm@32960:           with eval_e conf_a eval_ps conf_s1 
wenzelm@32960:           show ?thesis 
wenzelm@32960:             by auto
wenzelm@32960:         qed
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   next
schirmer@13688:     show "\<forall>a vs invC declC l.
schirmer@13688:       G,A\<turnstile>{?R a\<leftarrow>\<lfloor>vs\<rfloor>\<^sub>l \<and>.
schirmer@13688:              (\<lambda>s. declC =
schirmer@13688:                   invocation_declclass G mode (store s) a statT
schirmer@13688:                       \<lparr>name=mn, parTs=pTs'\<rparr> \<and>
schirmer@13688:                   invC = invocation_class mode (store s) a statT \<and>
schirmer@13688:                   l = locals (store s)) ;.
schirmer@13688:              init_lvars G declC \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs \<and>.
schirmer@13688:              (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
schirmer@13688:           Methd declC \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ> 
schirmer@13688:           {set_lvars l .; ?S}" 
schirmer@13688:       (is "\<forall> a vs invC declC l. ?METHD a vs invC declC l")
schirmer@13688:     proof (intro allI)
schirmer@13688:       fix a vs invC declC l
schirmer@13688:       from mgf_methds [rule_format]
schirmer@13688:       show "?METHD a vs invC declC l"
schirmer@13688:       proof (rule MGFnD' [THEN conseq12],clarsimp)
wenzelm@32960:         fix s4 s2 s1::state
wenzelm@32960:         fix s0 v
wenzelm@32960:         let ?D= "invocation_declclass G mode (store s2) a statT 
schirmer@13688:                     \<lparr>name=mn,parTs=pTs'\<rparr>"
wenzelm@32960:         let ?s3= "init_lvars G ?D \<lparr>name=mn, parTs=pTs'\<rparr> mode a vs s2"
wenzelm@32960:         assume inv_prop: "abrupt ?s3=None 
schirmer@13688:              \<longrightarrow> G\<turnstile>mode\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
wenzelm@32960:         assume conf_s2: "s2\<Colon>\<preceq>(G, L)"
wenzelm@32960:         assume conf_a: "abrupt s1 = None \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>RefT statT"
wenzelm@32960:         assume eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1"
wenzelm@32960:         assume eval_ps: "G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>vs\<rightarrow> s2"
wenzelm@32960:         assume eval_mthd: "G\<turnstile>?s3 \<midarrow>Methd ?D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
wenzelm@32960:         show "G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn( {pTs'}ps)-\<succ>v
schirmer@13688:                         \<rightarrow> (set_lvars (locals (store s2))) s4"
wenzelm@32960:         proof -
wenzelm@32960:           obtain D where D: "D=?D" by simp
wenzelm@32960:           obtain s3 where s3: "s3=?s3" by simp
wenzelm@32960:           obtain s3' where 
wenzelm@32960:             s3': "s3' = check_method_access G accC statT mode 
schirmer@13688:                            \<lparr>name=mn,parTs=pTs'\<rparr> a s3"
wenzelm@32960:             by simp
wenzelm@32960:           have eq_s3'_s3: "s3'=s3"
wenzelm@32960:           proof -
wenzelm@32960:             from inv_prop s3 mode
wenzelm@32960:             have "normal s3 \<Longrightarrow> 
schirmer@13688:              G\<turnstile>invmode statM e\<rightarrow>invocation_class mode (store s2) a statT\<preceq>statT"
wenzelm@32960:               by auto
wenzelm@32960:             with eval_ps wt_e statM conf_s2 conf_a [rule_format] 
wenzelm@32960:             have "check_method_access G accC statT (invmode statM e)
schirmer@13688:                       \<lparr>name=mn,parTs=pTs'\<rparr> a s3 = s3"
wenzelm@32960:               by (rule error_free_call_access) (auto simp add: s3 mode wf)
wenzelm@32960:             thus ?thesis 
wenzelm@32960:               by (simp add: s3' mode)
wenzelm@32960:           qed
wenzelm@32960:           with eval_mthd D s3
wenzelm@32960:           have "G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs'\<rparr>-\<succ>v\<rightarrow> s4"
wenzelm@32960:             by simp
wenzelm@32960:           with eval_e eval_ps D _ s3' 
wenzelm@32960:           show ?thesis
wenzelm@32960:             by (rule eval_Call) (auto simp add: s3 mode D)
wenzelm@32960:         qed
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   qed
schirmer@13688: qed
wenzelm@32960:                   
schirmer@13688: lemma eval_expression_no_jump':
schirmer@13688:   assumes eval: "G\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1"
schirmer@13688:   and   no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
schirmer@13688:   and      wt: "\<lparr>prg=G, cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T" 
schirmer@13688:   and      wf: "wf_prog G"
schirmer@13688: shows "abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688: using eval no_jmp wt wf
schirmer@13688: by - (rule eval_expression_no_jump 
schirmer@13688:             [where ?Env="\<lparr>prg=G, cls=C,lcl=L\<rparr>",simplified],auto)
schirmer@12854: 
schirmer@13688: 
schirmer@13688: text {* To derive the most general formula for the loop statement, we need to
schirmer@13688: come up with a proper loop invariant, which intuitively states that we are 
schirmer@13688: currently inside the evaluation of the loop. To define such an invariant, we
schirmer@13688: unroll the loop in iterated evaluations of the expression and evaluations of
schirmer@13688: the loop body. *}
schirmer@13688: 
wenzelm@37956: definition
wenzelm@37956:   unroll :: "prog \<Rightarrow> label \<Rightarrow> expr \<Rightarrow> stmt \<Rightarrow> (state \<times>  state) set" where
wenzelm@37956:   "unroll G l e c = {(s,t). \<exists> v s1 s2.
schirmer@13688:                              G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1 \<and> the_Bool v \<and> normal s1 \<and>
schirmer@13688:                              G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> t=(abupd (absorb (Cont l)) s2)}"
schirmer@13688: 
schirmer@13688: 
schirmer@13688: lemma unroll_while:
schirmer@13688:   assumes unroll: "(s, t) \<in> (unroll G l e c)\<^sup>*"
schirmer@13688:   and     eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" 
schirmer@13688:   and     normal_termination: "normal s'  \<longrightarrow> \<not> the_Bool v"
schirmer@13688:   and     wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T"
schirmer@13688:   and     wf: "wf_prog G" 
schirmer@13688:   shows "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688: using unroll (* normal_s *)
schirmer@13688: proof (induct rule: converse_rtrancl_induct) 
schirmer@13688:   show "G\<turnstile>t \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688:   proof (cases "normal t")
schirmer@13688:     case False
schirmer@13688:     with eval_e have "s'=t" by auto
schirmer@13688:     with False show ?thesis by auto
schirmer@13688:   next
schirmer@13688:     case True
schirmer@13688:     note normal_t = this
schirmer@13688:     show ?thesis
schirmer@13688:     proof (cases "normal s'")
schirmer@13688:       case True
schirmer@13688:       with normal_t eval_e normal_termination
schirmer@13688:       show ?thesis
wenzelm@32960:         by (auto intro: eval.Loop)
schirmer@13688:     next
schirmer@13688:       case False
schirmer@13688:       note abrupt_s' = this
schirmer@13688:       from eval_e _ wt wf
schirmer@13688:       have no_cont: "abrupt s' \<noteq> Some (Jump (Cont l))"
wenzelm@32960:         by (rule eval_expression_no_jump') (insert normal_t,simp)
schirmer@13688:       have
wenzelm@32960:         "if the_Bool v 
schirmer@13688:              then (G\<turnstile>s' \<midarrow>c\<rightarrow> s' \<and> 
schirmer@13688:                    G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s')
wenzelm@32960:              else s' = s'"
schirmer@13688:       proof (cases "the_Bool v")
wenzelm@32960:         case False thus ?thesis by simp
schirmer@13688:       next
wenzelm@32960:         case True
wenzelm@32960:         with abrupt_s' have "G\<turnstile>s' \<midarrow>c\<rightarrow> s'" by auto
wenzelm@32960:         moreover from abrupt_s' no_cont 
wenzelm@32960:         have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
wenzelm@32960:           by (cases s') (simp add: absorb_def split: split_if)
wenzelm@32960:         moreover
wenzelm@32960:         from no_absorb abrupt_s'
wenzelm@32960:         have "G\<turnstile>(abupd (absorb (Cont l)) s') \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
wenzelm@32960:           by auto
wenzelm@32960:         ultimately show ?thesis
wenzelm@32960:           using True by simp
schirmer@13688:       qed
schirmer@13688:       with eval_e 
schirmer@13688:       show ?thesis
wenzelm@32960:         using normal_t by (auto intro: eval.Loop)
schirmer@13688:     qed
schirmer@13688:   qed
schirmer@13688: next
schirmer@13688:   fix s s3
schirmer@13688:   assume unroll: "(s,s3) \<in> unroll G l e c"
schirmer@13688:   assume while: "G\<turnstile>s3 \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688:   show "G\<turnstile>s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
schirmer@13688:   proof -
schirmer@13688:     from unroll obtain v s1 s2 where
schirmer@13688:       normal_s1: "normal s1" and
schirmer@13688:       eval_e: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1" and
schirmer@13688:       continue: "the_Bool v" and
schirmer@13688:       eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and
schirmer@13688:       s3: "s3=(abupd (absorb (Cont l)) s2)"
schirmer@13688:       by  (unfold unroll_def) fast 
schirmer@13688:     from eval_e normal_s1 have
schirmer@13688:       "normal s"
schirmer@13688:       by (rule eval_no_abrupt_lemma [rule_format])
schirmer@13688:     with while eval_e continue eval_c s3 show ?thesis
schirmer@13688:       by (auto intro!: eval.Loop)
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12854: 
schirmer@13688: lemma MGFn_Loop:
schirmer@13688:   assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688:   and     mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688:   and     wf: "wf_prog G" 
schirmer@13688: shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt [rule_format],elim exE)
schirmer@13688:   fix T L C
schirmer@13688:   assume wt: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<Colon>T"
schirmer@13688:   then obtain eT where
schirmer@13688:     wt_e: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" 
schirmer@13688:     by cases simp
schirmer@13688:   show ?thesis
schirmer@13688:   proof (rule MGFn_NormalI)
schirmer@13688:     show "G,A\<turnstile>{Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)} 
schirmer@13688:               .l\<bullet> While(e) c.
schirmer@13688:               {\<lambda>Y s' s. G\<turnstile>s \<midarrow>In1r (l\<bullet> While(e) c)\<succ>\<rightarrow> (Y, s')}"
schirmer@13688:     proof (rule conseq12 
schirmer@13688:            [where ?P'="(\<lambda> Y s' s. (s,s') \<in> (unroll G l e c)\<^sup>* ) \<and>. G\<turnstile>init\<le>n"
schirmer@13688:              and  ?Q'="((\<lambda> Y s' s. (\<exists> t b. (s,t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688:                           Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688:                         \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>"])
schirmer@13688:       show  "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n} 
schirmer@13688:                   .l\<bullet> While(e) c.
schirmer@13688:                  {((\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688:                                   Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688:                               \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>}"
schirmer@13688:       proof (rule ax_derivs.Loop)
wenzelm@32960:         from mfg_e
wenzelm@32960:         show "G,A\<turnstile>{(\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n} 
schirmer@13688:                    e-\<succ>
schirmer@13688:                   {(\<lambda>Y s' s. (\<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and> 
schirmer@13688:                                      Y = In1 b \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s')) 
schirmer@13688:                    \<and>. G\<turnstile>init\<le>n}"
wenzelm@32960:         proof (rule MGFnD' [THEN conseq12],clarsimp)
wenzelm@32960:           fix s Z s' v
wenzelm@32960:           assume "(Z, s) \<in> (unroll G l e c)\<^sup>*"
wenzelm@32960:           moreover
wenzelm@32960:           assume "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s'"
wenzelm@32960:           ultimately
wenzelm@32960:           show "\<exists>t. (Z, t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'"
wenzelm@32960:             by blast
wenzelm@32960:         qed
schirmer@13688:       next
wenzelm@32960:         from mfg_c
wenzelm@32960:         show "G,A\<turnstile>{Normal (((\<lambda>Y s' s. \<exists>t b. (s, t) \<in> (unroll G l e c)\<^sup>* \<and>
schirmer@13688:                                        Y = \<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
schirmer@13688:                           \<and>. G\<turnstile>init\<le>n)\<leftarrow>=True)}
schirmer@13688:                   .c.
schirmer@13688:                   {abupd (absorb (Cont l)) .;
schirmer@13688:                    ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n)}"
wenzelm@32960:         proof (rule MGFnD' [THEN conseq12],clarsimp)
wenzelm@32960:           fix Z s' s v t
wenzelm@32960:           assume unroll: "(Z, t) \<in> (unroll G l e c)\<^sup>*"
wenzelm@32960:           assume eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> Norm s" 
wenzelm@32960:           assume true: "the_Bool v"
wenzelm@32960:           assume eval_c: "G\<turnstile>Norm s \<midarrow>c\<rightarrow> s'"
wenzelm@32960:           show "(Z, abupd (absorb (Cont l)) s') \<in> (unroll G l e c)\<^sup>*"
wenzelm@32960:           proof -
wenzelm@32960:             note unroll
wenzelm@32960:             also
wenzelm@32960:             from eval_e true eval_c
wenzelm@32960:             have "(t,abupd (absorb (Cont l)) s') \<in> unroll G l e c" 
wenzelm@32960:               by (unfold unroll_def) force
wenzelm@32960:             ultimately show ?thesis ..
wenzelm@32960:           qed
wenzelm@32960:         qed
schirmer@13688:       qed
schirmer@13688:     next
schirmer@13688:       show 
wenzelm@32960:         "\<forall>Y s Z.
schirmer@13688:          (Normal ((\<lambda>Y' s' s. s' = s \<and> normal s) \<and>. G\<turnstile>init\<le>n)) Y s Z 
schirmer@13688:          \<longrightarrow> (\<forall>Y' s'.
schirmer@13688:                (\<forall>Y Z'. 
schirmer@13688:                  ((\<lambda>Y s' s. (s, s') \<in> (unroll G l e c)\<^sup>*) \<and>. G\<turnstile>init\<le>n) Y s Z' 
schirmer@13688:                  \<longrightarrow> (((\<lambda>Y s' s. \<exists>t b. (s,t) \<in> (unroll G l e c)\<^sup>* 
schirmer@13688:                                        \<and> Y=\<lfloor>b\<rfloor>\<^sub>e \<and> G\<turnstile>t \<midarrow>e-\<succ>b\<rightarrow> s') 
schirmer@13688:                      \<and>. G\<turnstile>init\<le>n)\<leftarrow>=False\<down>=\<diamondsuit>) Y' s' Z') 
schirmer@13688:                \<longrightarrow> G\<turnstile>Z \<midarrow>\<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ>\<rightarrow> (Y', s'))"
schirmer@13688:       proof (clarsimp)
wenzelm@32960:         fix Y' s' s
wenzelm@32960:         assume asm:
wenzelm@32960:           "\<forall>Z'. (Z', Norm s) \<in> (unroll G l e c)\<^sup>* 
schirmer@13688:                  \<longrightarrow> card (nyinitcls G s') \<le> n \<and>
schirmer@13688:                      (\<exists>v. (\<exists>t. (Z', t) \<in> (unroll G l e c)\<^sup>* \<and> G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s') \<and>
schirmer@13688:                      (fst s' = None \<longrightarrow> \<not> the_Bool v)) \<and> Y' = \<diamondsuit>"
wenzelm@32960:         show "Y' = \<diamondsuit> \<and> G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
wenzelm@32960:         proof -
wenzelm@32960:           from asm obtain v t where 
wenzelm@32960:             -- {* @{term "Z'"} gets instantiated with @{term "Norm s"} *}  
wenzelm@32960:             unroll: "(Norm s, t) \<in> (unroll G l e c)\<^sup>*" and
schirmer@13688:             eval_e: "G\<turnstile>t \<midarrow>e-\<succ>v\<rightarrow> s'" and
schirmer@13688:             normal_termination: "normal s' \<longrightarrow> \<not> the_Bool v" and
wenzelm@32960:              Y': "Y' = \<diamondsuit>"
wenzelm@32960:             by auto
wenzelm@32960:           from unroll eval_e normal_termination wt_e wf
wenzelm@32960:           have "G\<turnstile>Norm s \<midarrow>l\<bullet> While(e) c\<rightarrow> s'"
wenzelm@32960:             by (rule unroll_while)
wenzelm@32960:           with Y' 
wenzelm@32960:           show ?thesis
wenzelm@32960:             by simp
wenzelm@32960:         qed
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12854: 
schirmer@12925: lemma MGFn_FVar:
schirmer@13688:   fixes A :: "state triple set"
schirmer@13688:  assumes mgf_init: "G,A\<turnstile>{=:n} \<langle>Init statDeclC\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" 
schirmer@13688:   and    mgf_e: "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688:   and    wf: "wf_prog G"
schirmer@13688:   shows "G,A\<turnstile>{=:n} \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp) 
schirmer@13688:   note inj_term_simps [simp]
schirmer@13688:   fix T L accC' V
schirmer@13688:   assume wt: "\<lparr>prg = G, cls = accC', lcl = L\<rparr>\<turnstile>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<Colon>T"
schirmer@13688:   then obtain statC f where
schirmer@13688:     wt_e: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@13688:     accfield: "accfield G accC' statC fn = Some (statDeclC,f )" and
schirmer@13688:     eq_accC: "accC=accC'" and
schirmer@13688:     stat: "stat=is_static  f"
schirmer@13688:     by (cases) (auto simp add: member_is_static_simp)
schirmer@13688:   let ?Q="(\<lambda>Y s1 (x,s) . x = None \<and> 
schirmer@13688:                 (G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s1) \<and>
schirmer@13688:                 (\<exists> E. \<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E))
schirmer@13688:                 \<and>. G\<turnstile>init\<le>n \<and>. (\<lambda> s. s\<Colon>\<preceq>(G, L))"
schirmer@13688:   show "G,A\<turnstile>{Normal
schirmer@13688:              ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688:               (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688:               (\<lambda>s. \<lparr>prg=G,cls=accC',lcl=L\<rparr>
schirmer@13688:                  \<turnstile> dom (locals (store s)) \<guillemotright> \<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V))
schirmer@13688:              } {accC,statDeclC,stat}e..fn=\<succ>
schirmer@13688:              {\<lambda>Y s' s. \<exists>vf. Y = \<lfloor>vf\<rfloor>\<^sub>v \<and> 
schirmer@13688:                         G\<turnstile>s \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>vf\<rightarrow> s'}"
schirmer@13688:     (is "G,A\<turnstile>{Normal ?P} {accC,statDeclC,stat}e..fn=\<succ> {?R}")
schirmer@13688:   proof (rule ax_derivs.FVar [where ?Q="?Q" ])
schirmer@13688:     from mgf_init
schirmer@13688:     show "G,A\<turnstile>{Normal ?P} .Init statDeclC. {?Q}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s s'
schirmer@13688:       assume conf_s: "Norm s\<Colon>\<preceq>(G, L)"
schirmer@13688:       assume da: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>
schirmer@13688:                     \<turnstile> dom (locals s) \<guillemotright>\<langle>{accC,statDeclC,stat}e..fn\<rangle>\<^sub>v\<guillemotright> V"
schirmer@13688:       assume eval_init: "G\<turnstile>Norm s \<midarrow>Init statDeclC\<rightarrow> s'"
schirmer@13688:       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>
schirmer@13688:             s'\<Colon>\<preceq>(G, L)"
schirmer@13688:       proof -
wenzelm@32960:         from da 
wenzelm@32960:         obtain E where
wenzelm@32960:           "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals s) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
wenzelm@32960:           by cases simp
wenzelm@32960:         moreover
wenzelm@32960:         from eval_init
wenzelm@32960:         have "dom (locals s) \<subseteq> dom (locals (store s'))"
wenzelm@32960:           by (rule dom_locals_eval_mono [elim_format]) simp
wenzelm@32960:         ultimately obtain E' where
wenzelm@32960:           "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile> dom (locals (store s')) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E'"
wenzelm@32960:           by (rule da_weakenE)
wenzelm@32960:         moreover
wenzelm@32960:         have "s'\<Colon>\<preceq>(G, L)"
wenzelm@32960:         proof -
wenzelm@32960:           have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
wenzelm@32960:           proof -
wenzelm@32960:             from wf wt_e 
wenzelm@32960:             have iscls_statC: "is_class G statC"
wenzelm@32960:               by (auto dest: ty_expr_is_type type_is_class)
wenzelm@32960:             with wf accfield 
wenzelm@32960:             have iscls_statDeclC: "is_class G statDeclC"
wenzelm@32960:               by (auto dest!: accfield_fields dest: fields_declC)
wenzelm@32960:             thus ?thesis by simp
wenzelm@32960:           qed
wenzelm@32960:           obtain I where 
wenzelm@32960:             da_init: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688:                \<turnstile> dom (locals (store ((Norm s)::state))) \<guillemotright>\<langle>Init statDeclC\<rangle>\<^sub>s\<guillemotright> I"
wenzelm@32960:             by (auto intro: da_Init [simplified] assigned.select_convs)
wenzelm@32960:           from eval_init conf_s wt_init da_init  wf
wenzelm@32960:           show ?thesis
wenzelm@32960:             by (rule eval_type_soundE)
wenzelm@32960:         qed
wenzelm@32960:         ultimately show ?thesis by iprover
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   next
schirmer@13688:     from mgf_e
schirmer@13688:     show "G,A\<turnstile>{?Q} e-\<succ> {\<lambda>Val:a:. fvar statDeclC stat fn a ..; ?R}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s0 s1 s2 E a
schirmer@13688:       let ?fvar = "fvar statDeclC stat fn a s2"
schirmer@13688:       assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
schirmer@13688:       assume eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
schirmer@13688:       assume conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@13688:       assume da_e: "\<lparr>prg=G,cls=accC',lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688:       show "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>fst ?fvar\<rightarrow> snd ?fvar"
schirmer@13688:       proof -
wenzelm@32960:         obtain v s2' where
wenzelm@32960:           v: "v=fst ?fvar" and s2': "s2'=snd ?fvar"
wenzelm@32960:           by simp
wenzelm@32960:         obtain s3 where
wenzelm@32960:           s3: "s3= check_field_access G accC' statDeclC fn stat a s2'"
wenzelm@32960:           by simp
wenzelm@32960:         have eq_s3_s2': "s3=s2'"
wenzelm@32960:         proof -
wenzelm@32960:           from eval_e conf_s1 wt_e da_e wf obtain
wenzelm@32960:             conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
wenzelm@32960:             conf_a: "normal s2 \<Longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
wenzelm@32960:             by (rule eval_type_soundE) simp
wenzelm@32960:           from accfield wt_e eval_init eval_e conf_s2 conf_a _ wf
wenzelm@32960:           show ?thesis
wenzelm@32960:             by (rule  error_free_field_access 
schirmer@13688:                       [where ?v=v and ?s2'=s2',elim_format])
wenzelm@32960:                (simp add: s3 v s2' stat)+
schirmer@13688:         qed
wenzelm@32960:         from eval_init eval_e 
wenzelm@32960:         show ?thesis
wenzelm@32960:           apply (rule eval.FVar [where ?s2'=s2'])
wenzelm@32960:           apply  (simp add: s2')
wenzelm@32960:           apply  (simp add: s3 [symmetric]   eq_s3_s2' eq_accC s2' [symmetric])
wenzelm@32960:           done
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12925: 
schirmer@13337: 
schirmer@13688: lemma MGFn_Fin:
schirmer@13688:   assumes wf: "wf_prog G" 
schirmer@13688:   and     mgf_c1: "G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688:   and     mgf_c2: "G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@61076:   shows "G,(A::state triple set)\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
schirmer@13688:   fix T L accC C 
schirmer@13688:   assume wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T"
schirmer@13688:   then obtain
schirmer@13688:     wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@13688:     wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@13688:     by cases simp
schirmer@13688:   let  ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>c1\<rightarrow> s' \<and> 
schirmer@13688:                (\<exists> C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1)
schirmer@13688:                \<and> s\<Colon>\<preceq>(G, L)) 
schirmer@13688:              \<and>. G\<turnstile>init\<le>n"
schirmer@13688:   show "G,A\<turnstile>{Normal
schirmer@13688:               ((\<lambda>Y' s' s. s' = s \<and> abrupt s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688:               (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688:               (\<lambda>s. \<lparr>prg=G,cls=accC,lcl =L\<rparr>  
schirmer@13688:                      \<turnstile>dom (locals (store s)) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C))}
schirmer@13688:              .c1 Finally c2. 
schirmer@13688:              {\<lambda>Y s' s. Y = \<diamondsuit> \<and> G\<turnstile>s \<midarrow>c1 Finally c2\<rightarrow> s'}"
schirmer@13688:     (is "G,A\<turnstile>{Normal ?P} .c1 Finally c2. {?R}")
schirmer@13688:   proof (rule ax_derivs.Fin [where ?Q="?Q"])
schirmer@13688:     from mgf_c1
schirmer@13688:     show "G,A\<turnstile>{Normal ?P} .c1. {?Q}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s0
schirmer@13688:       assume "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1 Finally c2\<rangle>\<^sub>s\<guillemotright> C"
schirmer@13688:       thus "\<exists>C1. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
wenzelm@32960:         by cases (auto simp add: inj_term_simps)
schirmer@13688:     qed
schirmer@13688:   next
schirmer@13688:     from mgf_c2
schirmer@13688:     show "\<forall>abr. G,A\<turnstile>{?Q \<and>. (\<lambda>s. abr = abrupt s) ;. abupd (\<lambda>abr. None)} .c2.
schirmer@13688:           {abupd (abrupt_if (abr \<noteq> None) abr) .; ?R}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12, THEN allI],clarsimp)
schirmer@13688:       fix s0 s1 s2 C1
schirmer@13688:       assume da_c1:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1"
schirmer@13688:       assume conf_s0: "Norm s0\<Colon>\<preceq>(G, L)"
schirmer@13688:       assume eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
schirmer@13688:       assume eval_c2: "G\<turnstile>abupd (\<lambda>abr. None) s1 \<midarrow>c2\<rightarrow> s2"
schirmer@13688:       show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2
schirmer@13688:                \<rightarrow> abupd (abrupt_if (\<exists>y. abrupt s1 = Some y) (abrupt s1)) s2"
schirmer@13688:       proof -
wenzelm@32960:         obtain abr1 str1 where s1: "s1=(abr1,str1)"
wenzelm@32960:           by (cases s1)
wenzelm@32960:         with eval_c1 eval_c2 obtain
wenzelm@32960:           eval_c1': "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (abr1,str1)" and
wenzelm@32960:           eval_c2': "G\<turnstile>Norm str1 \<midarrow>c2\<rightarrow> s2"
wenzelm@32960:           by simp
wenzelm@32960:         obtain s3 where 
wenzelm@32960:           s3: "s3 = (if \<exists>err. abr1 = Some (Error err) 
wenzelm@32960:                         then (abr1, str1)
schirmer@13688:                         else abupd (abrupt_if (abr1 \<noteq> None) abr1) s2)"
wenzelm@32960:           by simp
wenzelm@32960:         from eval_c1' conf_s0 wt_c1 _ wf 
wenzelm@32960:         have "error_free (abr1,str1)"
wenzelm@32960:           by (rule eval_type_soundE) (insert da_c1,auto)
wenzelm@32960:         with s3 have eq_s3: "s3=abupd (abrupt_if (abr1 \<noteq> None) abr1) s2"
wenzelm@32960:           by (simp add: error_free_def)
wenzelm@32960:         from eval_c1' eval_c2' s3
wenzelm@32960:         show ?thesis
wenzelm@32960:           by (rule eval.Fin [elim_format]) (simp add: s1 eq_s3)
schirmer@13688:       qed
schirmer@13688:     qed 
schirmer@13688:   qed
schirmer@13688: qed
schirmer@13688:       
schirmer@13688: lemma Body_no_break:
schirmer@13688:  assumes eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" 
schirmer@13688:    and      eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" 
schirmer@13688:    and       jmpOk: "jumpNestingOkS {Ret} c"
schirmer@13688:    and        wt_c: "\<lparr>prg=G, cls=C, lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@13688:    and        clsD: "class G D=Some d"
schirmer@13688:    and          wf: "wf_prog G" 
schirmer@13688:   shows "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l)) \<and> 
schirmer@13688:               abrupt s2 \<noteq> Some (Jump (Cont l))"
schirmer@13688: proof
schirmer@13688:   fix l show "abrupt s2 \<noteq> Some (Jump (Break l)) \<and>  
schirmer@13688:               abrupt s2 \<noteq> Some (Jump (Cont l))"
schirmer@13688:   proof -
wenzelm@26932:     fix accC from clsD have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
schirmer@13688:       by auto
schirmer@13688:     from eval_init wf
schirmer@13688:     have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
schirmer@13688:       by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
schirmer@13688:     from eval_c _ wt_c wf
schirmer@13688:     show ?thesis
schirmer@13688:       apply (rule jumpNestingOk_eval [THEN conjE, elim_format])
schirmer@13688:       using jmpOk s1_no_jmp
schirmer@13688:       apply auto
schirmer@13688:       done
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12854: 
schirmer@13688: lemma MGFn_Body:
schirmer@13688:   assumes wf: "wf_prog G"
schirmer@13688:   and     mgf_init: "G,A\<turnstile>{=:n} \<langle>Init D\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
schirmer@13688:   and     mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@61076:   shows  "G,(A::state triple set)\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688: proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
schirmer@13688:   fix T L accC E
schirmer@13688:   assume wt: "\<lparr>prg=G, cls=accC,lcl=L\<rparr>\<turnstile>\<langle>Body D c\<rangle>\<^sub>e\<Colon>T"
schirmer@13688:   let ?Q="(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>Init D\<rightarrow> s' \<and> jumpNestingOkS {Ret} c) 
schirmer@13688:           \<and>. G\<turnstile>init\<le>n" 
schirmer@13688:   show "G,A\<turnstile>{Normal
schirmer@13688:                ((\<lambda>Y' s' s. s' = s \<and> fst s = None) \<and>. G\<turnstile>init\<le>n \<and>.
schirmer@13688:                 (\<lambda>s. s\<Colon>\<preceq>(G, L)) \<and>.
schirmer@13688:                 (\<lambda>s. \<lparr>prg=G,cls=accC,lcl=L\<rparr>
schirmer@13688:                        \<turnstile> dom (locals (store s)) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E))}
schirmer@13688:              Body D c-\<succ> 
schirmer@13688:              {\<lambda>Y s' s. \<exists>v. Y = In1 v \<and> G\<turnstile>s \<midarrow>Body D c-\<succ>v\<rightarrow> s'}"
schirmer@13688:     (is "G,A\<turnstile>{Normal ?P} Body D c-\<succ> {?R}")
schirmer@13688:   proof (rule ax_derivs.Body [where ?Q="?Q"])
schirmer@13688:     from mgf_init
schirmer@13688:     show "G,A\<turnstile>{Normal ?P} .Init D. {?Q}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s0
schirmer@13688:       assume da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals s0) \<guillemotright>\<langle>Body D c\<rangle>\<^sub>e\<guillemotright> E"
schirmer@13688:       thus "jumpNestingOkS {Ret} c"
wenzelm@32960:         by cases simp
schirmer@13688:     qed
schirmer@13688:   next
schirmer@13688:     from mgf_c
schirmer@13688:     show "G,A\<turnstile>{?Q}.c.{\<lambda>s.. abupd (absorb Ret) .; ?R\<leftarrow>\<lfloor>the (locals s Result)\<rfloor>\<^sub>e}"
schirmer@13688:     proof (rule MGFnD' [THEN conseq12],clarsimp)
schirmer@13688:       fix s0 s1 s2
schirmer@13688:       assume eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1"
schirmer@13688:       assume eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
schirmer@13688:       assume nestingOk: "jumpNestingOkS {Ret} c"
schirmer@13688:       show "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
schirmer@13688:               \<rightarrow> abupd (absorb Ret) s2"
schirmer@13688:       proof -
wenzelm@32960:         from wt obtain d where 
schirmer@13688:           d: "class G D=Some d" and
schirmer@13688:           wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
wenzelm@32960:           by cases auto
wenzelm@32960:         obtain s3 where 
wenzelm@32960:           s3: "s3= (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
schirmer@13688:                            fst s2 = Some (Jump (Cont l))
schirmer@13688:                        then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
schirmer@13688:                        else s2)"
wenzelm@32960:           by simp
wenzelm@32960:         from eval_init eval_c nestingOk wt_c d wf
wenzelm@32960:         have eq_s3_s2: "s3=s2"
wenzelm@32960:           by (rule Body_no_break [elim_format]) (simp add: s3)
wenzelm@32960:         from eval_init eval_c s3
wenzelm@32960:         show ?thesis
wenzelm@32960:           by (rule eval.Body [elim_format]) (simp add: eq_s3_s2)
schirmer@13688:       qed
schirmer@13688:     qed
schirmer@13688:   qed
schirmer@13688: qed
schirmer@13337: 
schirmer@13688: lemma MGFn_lemma:
schirmer@13688:   assumes mgf_methds: 
schirmer@13688:            "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
schirmer@13688:   and wf: "wf_prog G"
schirmer@13688:   shows "\<And> t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@13688: proof (induct rule: full_nat_induct)
schirmer@13688:   fix n t
schirmer@13688:   assume hyp: "\<forall> m. Suc m \<le> n \<longrightarrow> (\<forall> t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>})"
schirmer@13688:   show "G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}"
schirmer@13688:   proof -
schirmer@13688:   { 
schirmer@13688:     fix v e c es
schirmer@13688:     have "G,A\<turnstile>{=:n} \<langle>v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}" and 
schirmer@13688:       "G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" and
schirmer@13688:       "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" and  
schirmer@13688:       "G,A\<turnstile>{=:n} \<langle>es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
blanchet@58251:     proof (induct rule: compat_var.induct compat_expr.induct compat_stmt.induct compat_expr_list.induct)
schirmer@13688:       case (LVar v)
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>LVar v\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.LVar [THEN conseq1])
wenzelm@32960:         apply (clarsimp)
wenzelm@32960:         apply (rule eval.LVar)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (FVar accC statDeclC stat e fn)
wenzelm@23366:       from MGFn_Init [OF hyp] and `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}` and wf
schirmer@13688:       show ?case
wenzelm@32960:         by (rule MGFn_FVar)
schirmer@13688:     next
schirmer@13688:       case (AVar e1 e2)
wenzelm@23366:       note mgf_e1 = `G,A\<turnstile>{=:n} \<langle>e1\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366:       note mgf_e2 = `G,A\<turnstile>{=:n} \<langle>e2\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>e1.[e2]\<rangle>\<^sub>v\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.AVar)
wenzelm@32960:         apply  (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.AVar)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (InsInitV c v)
schirmer@13688:       show ?case
wenzelm@32960:         by (rule MGFn_NormalI) (rule ax_derivs.InsInitV)
schirmer@13688:     next
schirmer@13688:       case (NewC C)
schirmer@13688:       show ?case
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.NewC)
wenzelm@32960:         apply (rule MGFn_InitD [OF hyp, THEN conseq2])
nipkow@44890:         apply (fastforce intro: eval.NewC)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (NewA T e)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI) 
wenzelm@32960:         apply (rule ax_derivs.NewA 
schirmer@13688:                [where ?Q = "(\<lambda>Y' s' s. normal s \<and> G\<turnstile>s \<midarrow>In1r (init_comp_ty T) 
schirmer@13688:                               \<succ>\<rightarrow> (Y',s')) \<and>. G\<turnstile>init\<le>n"])
wenzelm@32960:         apply  (simp add: init_comp_ty_def split add: split_if)
wenzelm@32960:         apply  (rule conjI, clarsimp)
wenzelm@32960:         apply   (rule MGFn_InitD [OF hyp, THEN conseq2])
wenzelm@32960:         apply   (clarsimp intro: eval.Init)
wenzelm@32960:         apply  clarsimp
wenzelm@32960:         apply  (rule ax_derivs.Skip [THEN conseq1])
wenzelm@32960:         apply  (clarsimp intro: eval.Skip)
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.NewA)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Cast C e)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast])
nipkow@44890:         apply (fastforce intro: eval.Cast)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Inst e C)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst])
nipkow@44890:         apply (fastforce intro: eval.Inst)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Lit v)
schirmer@13688:       show ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Lit [THEN conseq1])
nipkow@44890:         apply (fastforce intro: eval.Lit)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (UnOp unop e)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.UnOp)
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.UnOp)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (BinOp binop e1 e2)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.BinOp)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (case_tac "need_second_arg binop v1")
wenzelm@32960:         apply  simp
wenzelm@32960:         apply  (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply  (fastforce intro: eval.BinOp)
wenzelm@32960:         apply simp
wenzelm@32960:         apply (rule ax_Normal_cases)
wenzelm@32960:         apply  (rule ax_derivs.Skip [THEN conseq1])
wenzelm@32960:         apply  clarsimp
wenzelm@32960:         apply  (rule eval_BinOp_arg2_indepI)
wenzelm@32960:         apply   simp
wenzelm@32960:         apply  simp
wenzelm@32960:         apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
nipkow@44890:         apply (fastforce intro: eval.BinOp)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case Super
schirmer@13688:       show ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Super [THEN conseq1])
nipkow@44890:         apply (fastforce intro: eval.Super)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Acc v)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc])
nipkow@44890:         apply (fastforce intro: eval.Acc simp add: split_paired_all)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Ass v e)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>v:=e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Ass)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.Ass simp add: split_paired_all)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Cond e1 e2 e3)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>e1 ? e2 : e3\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Cond)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (rule ax_Normal_cases)
wenzelm@32960:         prefer 2
wenzelm@32960:         apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
nipkow@44890:         apply  (fastforce intro: eval.Cond)
wenzelm@32960:         apply (case_tac "b")
wenzelm@32960:         apply  simp
wenzelm@32960:         apply  (erule MGFnD'[THEN conseq12])
nipkow@44890:         apply  (fastforce intro: eval.Cond)
wenzelm@32960:         apply simp
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.Cond)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Call accC statT mode e mn pTs' ps)
wenzelm@23366:       note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366:       note mgf_ps = `G,A\<turnstile>{=:n} \<langle>ps\<rangle>\<^sub>l\<succ> {G\<rightarrow>}`
schirmer@13688:       from mgf_methds mgf_e mgf_ps wf
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
wenzelm@32960:         by (rule MGFn_Call)
schirmer@13688:     next
schirmer@13688:       case (Methd D mn)
schirmer@13688:       from mgf_methds
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
wenzelm@32960:         by simp
schirmer@13688:     next
schirmer@13688:       case (Body D c)
wenzelm@23366:       note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688:       from wf MGFn_Init [OF hyp] mgf_c
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>Body D c\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
wenzelm@32960:         by (rule MGFn_Body)
schirmer@13688:     next
schirmer@13688:       case (InsInitE c e)
schirmer@13688:       show ?case
wenzelm@32960:         by (rule MGFn_NormalI) (rule ax_derivs.InsInitE)
schirmer@13688:     next
schirmer@13688:       case (Callee l e)
schirmer@13688:       show ?case
wenzelm@32960:         by (rule MGFn_NormalI) (rule ax_derivs.Callee)
schirmer@13688:     next
schirmer@13688:       case Skip
schirmer@13688:       show ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Skip [THEN conseq1])
nipkow@44890:         apply (fastforce intro: eval.Skip)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Expr e)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr])
nipkow@44890:         apply (fastforce intro: eval.Expr)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Lab l c)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>l\<bullet> c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
nipkow@44890:         apply (fastforce intro: eval.Lab)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Comp c1 c2)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>c1;; c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Comp)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.Comp) 
wenzelm@32960:         done
schirmer@13688:     next
wenzelm@24783:       case (If' e c1 c2)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.If)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (rule ax_Normal_cases)
wenzelm@32960:         prefer 2
wenzelm@32960:         apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
nipkow@44890:         apply  (fastforce intro: eval.If)
wenzelm@32960:         apply (case_tac "b")
wenzelm@32960:         apply  simp
wenzelm@32960:         apply  (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply  (fastforce intro: eval.If)
wenzelm@32960:         apply simp
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.If)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Loop l e c)
wenzelm@23366:       note mgf_e = `G,A\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}`
wenzelm@23366:       note mgf_c = `G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688:       from mgf_e mgf_c wf
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         by (rule MGFn_Loop)
schirmer@13688:     next
schirmer@13688:       case (Jmp j)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Jmp [THEN conseq1])
wenzelm@46714:         apply (auto intro: eval.Jmp)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Throw e)
schirmer@13688:       thus ?case
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
nipkow@44890:         apply (fastforce intro: eval.Throw)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (TryC c1 C vn c2)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>Try c1 Catch(C vn) c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Try [where 
schirmer@13688:           ?Q = " (\<lambda>Y' s' s. normal s \<and> (\<exists>s''. G\<turnstile>s \<midarrow>\<langle>c1\<rangle>\<^sub>s\<succ>\<rightarrow> (Y',s'') \<and> 
schirmer@13688:                             G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n"])
wenzelm@32960:         apply   (erule MGFnD [THEN ax_NormalD, THEN conseq2])
nipkow@44890:         apply   (fastforce elim: sxalloc_gext [THEN card_nyinitcls_gext])
wenzelm@32960:         apply  (erule MGFnD'[THEN conseq12])
nipkow@44890:         apply  (fastforce intro: eval.Try)
nipkow@44890:         apply (fastforce intro: eval.Try)
wenzelm@32960:         done
schirmer@13688:     next
schirmer@13688:       case (Fin c1 c2)
wenzelm@23366:       note mgf_c1 = `G,A\<turnstile>{=:n} \<langle>c1\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
wenzelm@23366:       note mgf_c2 = `G,A\<turnstile>{=:n} \<langle>c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}`
schirmer@13688:       from wf mgf_c1 mgf_c2
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>c1 Finally c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         by (rule MGFn_Fin)
schirmer@13688:     next
schirmer@13688:       case (FinA abr c)
schirmer@13688:       show ?case
wenzelm@32960:         by (rule MGFn_NormalI) (rule ax_derivs.FinA)
schirmer@13688:     next
schirmer@13688:       case (Init C)
schirmer@13688:       from hyp
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>Init C\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
wenzelm@32960:         by (rule MGFn_Init)
schirmer@13688:     next
blanchet@58287:       case Nil_expr
schirmer@13688:       show "G,A\<turnstile>{=:n} \<langle>[]\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Nil [THEN conseq1])
nipkow@44890:         apply (fastforce intro: eval.Nil)
wenzelm@32960:         done
schirmer@13688:     next
blanchet@58287:       case (Cons_expr e es)
schirmer@13688:       thus "G,A\<turnstile>{=:n} \<langle>e# es\<rangle>\<^sub>l\<succ> {G\<rightarrow>}"
wenzelm@32960:         apply -
wenzelm@32960:         apply (rule MGFn_NormalI)
wenzelm@32960:         apply (rule ax_derivs.Cons)
wenzelm@32960:         apply  (erule MGFnD [THEN ax_NormalD])
wenzelm@32960:         apply (rule allI)
wenzelm@32960:         apply (erule MGFnD'[THEN conseq12])
nipkow@44890:         apply (fastforce intro: eval.Cons)
wenzelm@32960:         done
schirmer@13688:     qed
schirmer@13688:   }
schirmer@13688:   thus ?thesis
schirmer@13688:     by (cases rule: term_cases) auto
schirmer@13688:   qed
schirmer@13688: qed
schirmer@12854: 
schirmer@12925: lemma MGF_asm: 
schirmer@12925: "\<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>
schirmer@12925:  \<Longrightarrow> G,(A::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (simp (no_asm_use) add: MGF_MGFn_iff)
schirmer@12854: apply (rule allI)
schirmer@12854: apply (rule MGFn_lemma)
schirmer@12854: apply (intro strip)
schirmer@12854: apply (rule MGFn_free_wt)
schirmer@12854: apply (force dest: wt_Methd_is_methd)
schirmer@12925: apply assumption (* wf_prog G *)
schirmer@12854: done
schirmer@12854: 
wenzelm@58887: subsubsection "nested version"
schirmer@12854: 
schirmer@13688: lemma nesting_lemma' [rule_format (no_asm)]: 
schirmer@13688:   assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts" 
schirmer@13688:   and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf_call pn) A) {mgf b}
schirmer@13688:                                   \<Longrightarrow> P A {mgf_call pn}"
schirmer@13688:   and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf_call pn} \<Longrightarrow> P A {mgf t}"
schirmer@13688:   and finU: "finite U"
schirmer@13688:   and uA: "uA = mgf_call`U"
schirmer@13688:   shows "\<forall>A. A \<subseteq> uA \<longrightarrow> n \<le> card uA \<longrightarrow> card A = card uA - n 
schirmer@13688:              \<longrightarrow> (\<forall>t. P A {mgf t})"
schirmer@13688: using finU uA
schirmer@13688: apply -
schirmer@13688: apply (induct_tac "n")
wenzelm@42793: apply  (tactic "ALLGOALS (clarsimp_tac @{context})")
wenzelm@60754: apply  (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *})
schirmer@13688: apply    simp
schirmer@13688: apply   (erule finite_imageI)
schirmer@13688: apply  (simp add: MGF_asm ax_derivs_asm)
schirmer@13688: apply (rule MGF_asm)
schirmer@13688: apply (rule ballI)
schirmer@13688: apply (case_tac "mgf_call pn : A")
schirmer@13688: apply  (fast intro: ax_derivs_asm)
schirmer@13688: apply (rule MGF_nested_Methd)
schirmer@13688: apply (rule ballI)
schirmer@13688: apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
thomas@57492: apply hypsubst_thin
schirmer@13688: apply   fast
schirmer@13688: apply (drule finite_subset)
schirmer@13688: apply (erule finite_imageI)
schirmer@13688: apply auto
schirmer@13688: done
schirmer@12854: 
schirmer@13688: 
schirmer@13688: lemma nesting_lemma [rule_format (no_asm)]:
schirmer@13688:   assumes ax_derivs_asm: "\<And>A ts. ts \<subseteq> A \<Longrightarrow> P A ts"
schirmer@13688:   and MGF_nested_Methd: "\<And>A pn. \<forall>b\<in>bdy pn. P (insert (mgf (f pn)) A) {mgf b}
schirmer@13688:                                   \<Longrightarrow> P A {mgf (f pn)}"
schirmer@13688:   and MGF_asm: "\<And>A t. \<forall>pn\<in>U. P A {mgf (f pn)} \<Longrightarrow> P A {mgf t}"
schirmer@13688:   and finU: "finite U"
schirmer@13688: shows "P {} {mgf t}"
schirmer@13688: using ax_derivs_asm MGF_nested_Methd MGF_asm finU
schirmer@13688: by (rule nesting_lemma') (auto intro!: le_refl)
schirmer@13688: 
schirmer@12854: 
schirmer@12854: lemma MGF_nested_Methd: "\<lbrakk>  
schirmer@13688:  G,insert ({Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}) A
schirmer@13688:     \<turnstile>{Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}  
schirmer@13688:  \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal \<doteq>}  \<langle>Methd  C sig\<rangle>\<^sub>e \<succ>{G\<rightarrow>}"
schirmer@12854: apply (unfold MGF_def)
schirmer@12854: apply (rule ax_MethdN)
schirmer@12854: apply (erule conseq2)
schirmer@12854: apply clarsimp
schirmer@12854: apply (erule MethdI)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@12854: apply (rule MGFNormalI)
schirmer@12854: apply (rule_tac mgf = "\<lambda>t. {Normal \<doteq>} t\<succ> {G\<rightarrow>}" and 
schirmer@13688:                 bdy = "\<lambda> (C,sig) .{\<langle>body G C sig\<rangle>\<^sub>e }" and 
schirmer@13688:                 f = "\<lambda> (C,sig) . \<langle>Methd C sig\<rangle>\<^sub>e " in nesting_lemma)
schirmer@12854: apply    (erule ax_derivs.asm)
schirmer@12854: apply   (clarsimp simp add: split_tupled_all)
schirmer@12854: apply   (erule MGF_nested_Methd)
schirmer@12925: apply  (erule_tac [2] finite_is_methd [OF wf_ws_prog])
schirmer@12854: apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925: apply (auto intro: MGFNormalI)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
wenzelm@58887: subsubsection "simultaneous version"
schirmer@12854: 
schirmer@12854: lemma MGF_simult_Methd_lemma: "finite ms \<Longrightarrow>  
schirmer@13688:   G,A \<union> (\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms  
schirmer@13688:       |\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>body G C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms \<Longrightarrow>  
schirmer@13688:   G,A|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd  C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) ` ms"
schirmer@12854: apply (unfold MGF_def)
schirmer@12854: apply (rule ax_derivs.Methd [unfolded mtriples_def])
schirmer@12854: apply (erule ax_finite_pointwise)
schirmer@12854: prefer 2
schirmer@12854: apply  (rule ax_derivs.asm)
schirmer@12854: apply  fast
schirmer@12854: apply clarsimp
schirmer@12854: apply (rule conseq2)
schirmer@12854: apply  (erule (1) ax_methods_spec)
schirmer@12854: apply clarsimp
schirmer@12854: apply (erule eval_Methd)
schirmer@12854: done
schirmer@12854: 
schirmer@12925: lemma MGF_simult_Methd: "wf_prog G \<Longrightarrow> 
schirmer@13688:    G,({}::state triple set)|\<turnstile>(\<lambda>(C,sig). {Normal \<doteq>} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}) 
haftmann@61424:    ` Collect (case_prod (is_methd G)) "
schirmer@12925: apply (frule finite_is_methd [OF wf_ws_prog])
schirmer@12854: apply (rule MGF_simult_Methd_lemma)
schirmer@12854: apply  assumption
schirmer@12854: apply (erule ax_finite_pointwise)
schirmer@12854: prefer 2
schirmer@12854: apply  (rule ax_derivs.asm)
schirmer@12854: apply  blast
schirmer@12854: apply clarsimp
schirmer@12854: apply (rule MGF_asm [THEN MGFNormalD])
schirmer@12925: apply   (auto intro: MGFNormalI)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
wenzelm@58887: subsubsection "corollaries"
schirmer@12854: 
schirmer@12925: lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk>
schirmer@12925:  \<Longrightarrow>   \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
schirmer@12925: apply (cases "normal s")
schirmer@12925: apply   (force simp add: type_ok_def intro: eval_evaln)
schirmer@12925: apply   (force intro: evaln.Abrupt)
schirmer@12925: done
schirmer@12925: 
schirmer@13688: lemma MGF_complete:
schirmer@13688:   assumes valid: "G,{}\<Turnstile>{P} t\<succ> {Q}"
schirmer@13688:   and     mgf: "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@13688:   and      wf: "wf_prog G"
schirmer@13688:   shows "G,({}::state triple set)\<turnstile>{P::state assn} t\<succ> {Q}"
schirmer@13688: proof (rule ax_no_hazard)
schirmer@13688:   from mgf
schirmer@13688:   have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {\<lambda>Y s' s. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y, s')}"  
schirmer@13688:     by  (unfold MGF_def) 
schirmer@13688:   thus "G,({}::state triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q}"
schirmer@13688:   proof (rule conseq12,clarsimp)
schirmer@13688:     fix Y s Z Y' s'
schirmer@13688:     assume P: "P Y s Z"
schirmer@13688:     assume type_ok: "type_ok G t s"
schirmer@13688:     assume eval_t: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s')"
schirmer@13688:     show "Q Y' s' Z"
schirmer@13688:     proof -
schirmer@13688:       from eval_t type_ok wf 
schirmer@13688:       obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
wenzelm@32960:         by (rule eval_to_evaln [elim_format]) iprover
schirmer@13688:       from valid have 
wenzelm@32960:         valid_expanded:
wenzelm@32960:         "\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s 
schirmer@13688:                    \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s') \<longrightarrow> Q Y' s' Z)"
wenzelm@32960:         by (simp add: ax_valids_def triple_valid_def)
schirmer@13688:       from P type_ok evaln
schirmer@13688:       show "Q Y' s' Z"
wenzelm@32960:         by (rule valid_expanded [rule_format])
schirmer@13688:     qed
schirmer@13688:   qed 
schirmer@13688: qed
schirmer@13688:    
schirmer@13688: theorem ax_complete: 
schirmer@13688:   assumes wf: "wf_prog G" 
schirmer@13688:   and valid: "G,{}\<Turnstile>{P::state assn} t\<succ> {Q}"
schirmer@13688:   shows "G,({}::state triple set)\<turnstile>{P} t\<succ> {Q}"
schirmer@13688: proof -
schirmer@13688:   from wf have "G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
schirmer@13688:     by (rule MGF_deriv)
schirmer@13688:   from valid this wf
schirmer@13688:   show ?thesis
schirmer@13688:     by (rule MGF_complete)
schirmer@13688: qed
schirmer@13688:  
schirmer@12854: end