File AxCompl.ML

open AxCompl;

section "ninitcls";

Goalw [nyinitcls_def] "finite (nyinitcls G s)";
b y res_inst_tac [("B", "{C. is_class G C}")] finite_subset 1;
b y  Fast_tac 1;
b y fold_goals_tac [dom_def];
b y rtac finite_dom_map_of 1;
qed "finite_nyinitcls";
Addsimps[finite_nyinitcls];

Goalw [nyinitcls_def] "nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)";
b y Simp_tac 1;
qed "nyinitcls_set_locals_cong";
Addsimps[nyinitcls_set_locals_cong];

Goalw [nyinitcls_def] "nyinitcls G (f x, y) = nyinitcls G (x, y)";
b y Simp_tac 1;
qed "nyinitcls_xcpt_cong";
Addsimps[nyinitcls_xcpt_cong];

Goalw [nyinitcls_def] 
	"card (nyinitcls G (x, s)) \<le> n \<Longrightarrow> card (nyinitcls G (y, s)) \<le> n";
b y Auto_tac;
qed "card_nyinitcls_xcpt_congE";
AddSEs[card_nyinitcls_xcpt_congE];

Goalw [nyinitcls_def] 
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s";
b y pair_tac "s" 1;
b y Simp_tac 1;
qed "nyinitcls_new_xcpt_var";
Addsimps[nyinitcls_new_xcpt_var];

Goal "nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s";
b y pair_tac "s" 1;
b y simp_tac (simpset()addsimps[init_lvars_def2]addsplits[split_if]) 1;
qed "nyinitcls_init_lvars";
Addsimps[nyinitcls_init_lvars];

Goalw [nyinitcls_def] "\<lbrakk>nyinitcls G s = {}; is_class G C\<rbrakk> \<Longrightarrow> initd C s";
b y Fast_tac 1;
qed "nyinitcls_emptyD";

Goal "\<lbrakk>card (insert a A) \<le> Suc n; a\<notin>A; finite A\<rbrakk> \<Longrightarrow> card A \<le> n";
b y rotate_tac 1 1;
b y Clarsimp_tac 1;
qed "card_Suc_lemma";

Goal
"\<lbrakk>card (nyinitcls G (x,s)) \<le> Suc n; ¬inited C (globs s); class G C=Some y\<rbrakk> \<Longrightarrow>\
\ card (nyinitcls G (x,init_class_obj G C s)) \<le> n";
b y subgoal_tac 
     "nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))" 1;
b y  Clarsimp_tac 1;
b y  etac thin_rl 1;
b y  rtac (finite_nyinitcls RSN (3,card_Suc_lemma)) 1;
b y   auto_tac (claset() addSDs [not_initedD] addSEs [],
	simpset() addsimps [nyinitcls_def,inited_def] addsplits[split_if_asm]);
qed "nyinitcls_le_SucD";

Goalw [nyinitcls_def] "snd s\<le>|snd s' \<Longrightarrow> nyinitcls G s' \<subseteq> nyinitcls G s";
b y force_tac (claset() addSDs [permute_prems 0 1 inited_gext], simpset()) 1;
qed "nyinitcls_gext";

Goal"\<lbrakk>snd s\<le>|snd s'; card (nyinitcls G s) \<le> n\<rbrakk>\<Longrightarrow> card (nyinitcls G s') \<le> n";
b y rtac le_trans 1;
b y  atac 2;
b y rtac card_mono 1;
b y  rtac finite_nyinitcls 1;
b y etac nyinitcls_gext 1;
qed "card_nyinitcls_gext";


section "init_le";

Goalw [init_le_def] "(G\<turnstile>init\<le>n) s = (card (nyinitcls G s)\<le>n)";
b y Auto_tac;
qed "init_le_def2";
Addsimps[init_le_def2];

Goal "\<forall>n::nat. G,A\<turnstile>{P \<and>. G\<turnstile>init\<le>n} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}";
b y rtac escape 1;
b y force_tac (claset() addEs [conseq12], simpset()) 1;
qed "All_init_leD";


section "MGF";

(* unused *)
Goalw [MGF_def] "G,{}\<Turnstile>{op =} t\<succ> {G\<rightarrow>}";
b y force_tac (claset() addSDs[evaln_eval], 
                  simpset() addsimps [ax_valids_def,triple_valid_def2]) 1;
qed "MGF_valid";

Goal "(\<forall>Y' Y s. Y = Y' \<and> P s \<longrightarrow> Q s) = (\<forall>s. P s \<longrightarrow> Q s)";
b y Auto_tac;
qed "MGF_res_eq_lemma";
Addsimps[MGF_res_eq_lemma];

Goal 
"G,A\<turnstile>{P} In1r c\<succ> {\<lambda>(Y',s') (Y,s). Y' = Y \<and> (\<exists>w. G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (w, s'))}= \
\G,A\<turnstile>{P} .c. {\<lambda>(Y',s') (Y,s). Y' = Y \<and> G\<turnstile>s \<midarrow>c\<rightarrow> s'}";
b y auto_tac (claset() addEs [conseq12],simpset());
qed "MGF_stmt_eq";

Goalw [MGFn_def,MGF_def]
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} = G,A\<turnstile>{op = \<and>. G\<turnstile>init\<le>n}\
\                   t\<succ> {\<lambda>(Y',s') (Y,s). \<exists>w. Y'=res t w Y \<and> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')}";
b y rtac refl 1;
qed "MGFn_def2";

Goal "G,A\<turnstile>{op =} t\<succ> {G\<rightarrow>} = (\<forall>n. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>})";
b y full_simp_tac (simpset() addsimps [MGFn_def2,MGF_def]) 1;
b y Safe_tac;
b y  etac All_init_leD 2;
b y etac conseq1 1;
b y Force_tac 1;
qed "MGF_MGFn_iff";

Goalw [init_le_def]
"G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow> \
\G,A\<turnstile>{(\<lambda>(Y',s') (Y,s). Y'=Y \<and> s'=s \<and> P s) \<and>. G\<turnstile>init\<le>n} \
\t\<succ>  {(\<lambda>(Y',s') (Y,s). (\<exists>w. Y'=res t w Y \<and> G\<turnstile>s\<midarrow>t\<succ>\<rightarrow>(w,s'))\
                                  \ \<and> P s) \<and>. G\<turnstile>init\<le>n}";
b y full_simp_tac (simpset() addsimps [MGFn_def2]) 1;
b y etac conseq12 1;
b y Clarsimp_tac 1;
b y eatac (eval_gext RS card_nyinitcls_gext) 1 1;
qed "MGFnD";
val MGFnD' = read_instantiate [("P","\<lambda>x. True")] MGFnD;

Goal
"G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<Longrightarrow> \
\G,A\<turnstile>{(\<lambda>(Y',s') (Y,s). Y'=Y \<and> s'=s        \<and> P s) \<and>. G\<turnstile>init\<le>n} \
\.c. {(\<lambda>(Y',s') (Y,s). Y'=Y \<and> G\<turnstile>s \<midarrow>c\<rightarrow> s' \<and> P s) \<and>. G\<turnstile>init\<le>n}";
b y etac (MGFnD RS conseq12) 1;
b y Clarify_tac 1;
b y smp_tac 2 1;
b y Clarsimp_tac 1;
qed "MGFn_stmtD";

fun Xcpt_cases_tac_ ts = EVERY'[res_inst_tac [("C","normal")] ax_cases,
 fn i => EVERY'[resolve_tac (ts RL [conseq1]),
	 clarsimp_tac (claset(), simpset() addsimps[Let_def])]
   (i+1)];
val Xcpt_cases_tac  = Xcpt_cases_tac_ ax_Xcpts;
val Xcpt_cases_tac' = EVERY'[Xcpt_cases_tac_[ax_derivs.Xcpt],
			     etac conseq1, Clarsimp_tac]; (* should solve 1 *)

Goalw [MGF_def] "G,A\<turnstile>{Normal op =} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{op =} t\<succ> {G\<rightarrow>}";
b y Xcpt_cases_tac' 1;
b y Fast_tac 1;
qed "MGFNormalI";

Goalw [MGF_def] "G,A\<turnstile>{op =} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{Normal op =} t\<succ> {G\<rightarrow>}";
b y etac conseq1 1;
b y Force_tac 1;
qed "MGFNormalD";

Goal"G,A\<turnstile>{Normal ((\<lambda>(Y',s') (Y,s). Y'=Y \<and> s'=s \<and> normal s) \<and>. G\<turnstile>init\<le>n)} t\<succ> \
\{\<lambda>(Y',s') (Y,s). \<exists>w. Y'=res t w Y \<and> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')} \<Longrightarrow> G,A\<turnstile>{=:n}t\<succ>{G\<rightarrow>}";
b y full_simp_tac (simpset() addsimps [MGFn_def2]) 1;
b y Xcpt_cases_tac' 1;
b y Force_tac 1;
qed "MGFn_NormalI";

Goal "(\<exists>T L. (G,L)\<turnstile>t\<Colon>T) \<longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>} \<Longrightarrow> G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}";
b y rtac MGFn_NormalI 1;
b y rtac ax_free_wt 1;
b y auto_tac (claset() addEs [conseq12], simpset() addsimps [MGFn_def,MGF_def]);
qed "MGFn_free_wt";


section "main lemmas";

Delsimps [fun_upd_apply];
Delsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc];
(*prevents modifying rhs of MGF*)
Delrules[splitI2];(*prevents ugly renaming of state variables*)
val eval_css = (claset() addSIs eval.intrs delrules[eval.Expr,eval.Init] 
                                             addIs [eval.Expr,eval.Init]
           addSEs[eval.Try] delrules[equalityCE],
  simpset() addsimps [split_paired_all,Let_def]
 addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]);
val eval_Force_tac = force_tac eval_css;

fun ax_tac1 rl = EVERY'[rtac (rl RS conseq1) , eval_Force_tac];
fun ax_tac2 rl = EVERY'[etac (MGFnD' RS conseq12 RS rl), eval_Force_tac];

val wt_prepare_tac = EVERY'[
    rtac MGFn_free_wt,clarsimp_tac (claset() addSEs wt_elim_cases, simpset())];
val compl_prepare_tac = EVERY'[
    rtac MGFn_NormalI,simp_tac(simpset()addsimps[MGF_stmt_eq])];
val forw_hyp_tac = EVERY'[etac (MGFnD' RS conseq12), Clarsimp_tac];
val forw_hyp_eval_Force_tac = EVERY'[forw_hyp_tac, eval_Force_tac];

Goal "\<forall>m. Suc m\<le>n \<longrightarrow> (\<forall>t. G,A\<turnstile>{=:m} t\<succ> {G\<rightarrow>}) \<Longrightarrow> \
\ G,A\<turnstile>{=:n} In1r (init C)\<succ> {G\<rightarrow>}"; 
b y wt_prepare_tac 1; 
(* requires is_class G C two times for nyinitcls *)
b y compl_prepare_tac 1; 
b y res_inst_tac [("C","initd C")] ax_cases 1;
b y  rtac (ax_derivs.Done RS conseq1) 1;
b y  clarsimp_tac (claset() addSIs [init_done], simpset()) 1;
b y (res_inst_tac [("y","n")] nat.exhaust THEN_ALL_NEW Clarsimp_tac) 1;
b y  rtac (impossible RS conseq1) 1;
b y  force_tac (claset() addSDs [nyinitcls_emptyD], simpset()) 1;
b y dres_inst_tac [("x","nat")] spec 1;
b y Clarsimp_tac 1;
b y res_inst_tac [("Q","(\<lambda>(Y',s') (Y,(x,s)). \
\ Y'=Lcls (locals (snd s')) # Y \<and> G\<turnstile>(x,init_class_obj G C s)\
\  \<midarrow>(if C=Object then Skip else init (fst (the (class G C))))\<rightarrow> s' \<and> x=None \<and>\
\¬inited C (globs s)) \<and>. G\<turnstile>init\<le>nat")](surjective_pairing5 RS ax_derivs.Init)1;
b y  res_inst_tac [("P'","Normal ((\<lambda>(Y', s') (Y, s). Y' = Y \<and> s' = supd (init_class_obj G C) s \<and> normal s \<and> ¬ initd C s) \<and>. G\<turnstile>init\<le>nat)")] conseq1 1;
b y   force_tac (claset() addSEs [nyinitcls_le_SucD], simpset()) 2;
b y  EVERY'[simp_tac (simpset() addsplits [split_if]), 
		rtac conjI THEN_ALL_NEW Clarify_tac] 1;
b y   ax_tac1 ax_derivs.Skip 1;
b y  dtac spec 1;
b y  etac (MGFnD' RS conseq12) 1;
b y  force_tac (claset(), simpset()addsimprocs[eval_stmt_proc]) 1;
b y dtac spec 1;
b y etac (MGFnD' RS conseq12) 1;
b y Clarsimp_tac 1;
b y pair_tac "sb" 1;
b y clarsimp_tac (claset(),simpset()addsimprocs[eval_stmt_proc]) 1;
b y (rtac eval_Init THEN' REPEAT o Force_tac) 1;
qed "MGFn_Init";
val MGFn_InitD = MGFn_Init RS MGFn_stmtD RS ax_NormalD;

Goal
"\<lbrakk>\<forall>C sig. G,A\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>}; \
\ G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In3 ps\<succ> {G\<rightarrow>}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{=:n} In1l ({t,cT,mode}e..mn({pTs'}ps))\<succ> {G\<rightarrow>}";
b y wt_prepare_tac 1;  (* required for equating mode = invmode m e *)
b y compl_prepare_tac 1;
b y res_inst_tac [("R","(\<lambda>(Y',s') (Y,(x,s)). x = None \<and> \
\(\<exists>a' s1. G\<turnstile>Norm s \<midarrow>e-\<succ>a'\<rightarrow> s1 \<and> (\<exists>pvs x2 s2. G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2,s2) \<and> \
\ (let C = target (invmode m e) s2 a' cT  in \
\ init_lvars G C (mn, pTs') (invmode m e) a' pvs (x2,s2) = s' \<and>\
\ Y'=DynT C # Lcls (locals s2) #Y)))) \<and>. G\<turnstile>init\<le>n")] ax_derivs.Call 1;
b y   etac (MGFnD RS ax_NormalD) 1;
b y  EVERY'[thin_All_tac,forw_hyp_eval_Force_tac] 1;
b y rtac allI 1;
b y Xcpt_cases_tac 1;
b y  EVERY'[thin_All_tac, res_inst_tac [("s3'","(?x,?s)")] eval_Call, 
            REPEAT o Force_tac] 2;
b y rtac escape 1;
b y rewtac Let_def;
b y Clarsimp_tac 1;
b y EVERY'[dtac spec, dtac spec] 1;
b y etac (MGFnD' RS conseq12) 1;
b y clarsimp_tac (claset(),simpset()addsimprocs [eval_stmt_proc]) 1;
b y EVERY'[eatac eval_Call 1, rtac refl, K (Asm_simp_tac 2)] 1;
b y clarsimp_tac (claset(),simpset()addsimprocs[eval_expr_proc]) 1;
qed "MGFn_Call";

Goal"G,A\<turnstile>{Normal (op = \<and>. p)} .c. {\<lambda>(Y',s') (Y,s). Y'=Y \<and> G\<turnstile>s\<midarrow>c\<rightarrow>s'} = \
\G,A\<turnstile>{Normal ((\<lambda>(Y,s) (Y',s'). Y'=Y \<and> (\<forall>t. G\<turnstile>s \<midarrow>c\<rightarrow> t \<longrightarrow> t=s')) \<and>. p)}\
\ .c. {op =}";
b y auto_tac (claset() delrules[conjI] addSEs [conseq12], simpset());
b y case_tac "\<exists>t. G\<turnstile>Norm sa \<midarrow>c\<rightarrow> t" 1;
b y  fast_tac (claset() addDs [unique_eval]) 1;
b y clarsimp_tac (claset() addSEs [state_not_single], simpset()) 1;
qed "MGF_stmt_altern";

Goal "\<lbrakk>G,A\<turnstile>{=:n} In1l expr\<succ> {G\<rightarrow>}; G,A\<turnstile>{=:n} In1r stmt\<succ> {G\<rightarrow>}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{=:n} In1r (While(expr) stmt)\<succ> {G\<rightarrow>}";
b y compl_prepare_tac 1;
b y res_inst_tac [("p2","\<lambda>s. card (nyinitcls G s) \<le> n")]
		(MGF_stmt_altern RS iffD2 RS conseq1) 1;
b y  Clarsimp_tac 2;
b y EVERY[res_inst_tac [("P","Normal ?P'")] conseq12 1, Clarsimp_tac 2];
b y  res_inst_tac [("P'","(\<lambda>(Y,s) (Y',s'). \<exists>b. Y = Res b#Y' \<and> \
\ (\<exists>s0. G\<turnstile>s0 \<midarrow>In1l expr\<succ>\<rightarrow> (b,s)) \<and> \
\ (if (normal s \<longrightarrow> the_Bool (the_In1 b)) then (\<forall>s'' t. G\<turnstile>s \<midarrow>stmt\<rightarrow> s'' \<and>\
\ G\<turnstile>s'' \<midarrow>While(expr) stmt\<rightarrow> t \<longrightarrow> t=s') else s=s')) \<and>. G\<turnstile>init\<le>n")] 
           ax_derivs.Loop 1;
b y   force_tac (claset(), simpset() addsplits[split_if_asm]) 3;
b y  EVERY'[etac (MGFnD' RS conseq12), Clarsimp_tac] 1;
b y  EVERY'[rtac conjI, etac exI] 1;
b y  pair_tac "s" 1;
b y  ftac eval_Inj_elim 1;
b y  Clarsimp_tac 1;
b y  case_tac "x" 1;
b y   Force_tac 2;
b y  clarsimp_tac (claset(), simpset() addsplits[split_if]) 1;
b y   rtac conjI 1;
b y   force_tac (claset() addSDs [eval.Loop], simpset()) 2;
b y  (case_tac "fst s'" THEN_ALL_NEW 
      force_tac (claset() addSDs [eval.Loop], simpset() addsplits[split_if])) 1;
b y etac (MGFnD' RS conseq12) 1;
b y Clarsimp_noAllAsm_tac 1;
b y thin_tac "card (nyinitcls G s') \<le> n" 1;
b y eval_Force_tac 1;
qed "MGFn_Loop";

Goal "\<forall>n C sig. G,A\<turnstile>{=:n} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow> \
\ \<forall>t. G,A\<turnstile>{=:n} t\<succ> {G\<rightarrow>}";
b y rtac full_nat_induct 1;
b y rtac allI 1;
b y dres_inst_tac [("x","n")] spec 1;
b y dres_inst_tac [("psi","All ?P")] asm_rl 1;
b y subgoal_tac "\<forall>v e c es. \
\ G,A\<turnstile>{=:n} In2  v\<succ> {G\<rightarrow>} \<and> \
\ G,A\<turnstile>{=:n} In1l e\<succ> {G\<rightarrow>} \<and> \
\ G,A\<turnstile>{=:n} In1r c\<succ> {G\<rightarrow>} \<and> \
\ G,A\<turnstile>{=:n} In3 es\<succ> {G\<rightarrow>}" 1;
b y  strip_tac 2;
b y  induct_tac "t" 1;
b y    induct_tac "a" 1;
b y     REPEAT (Fast_tac 1);
b y rtac var_expr_stmt.induct 1;
(* 26 subgoals *)
b y Fast_tac 14; (* Methd *)
b y eatac MGFn_Call 2 13;
b y ALLGOALS thin_All_tac; (* assumptions on Methd  *)
b y etac MGFn_Init 22;
b y eatac MGFn_Loop 1 18;
b y ALLGOALS compl_prepare_tac;

b y ax_tac1 ax_derivs.LVar 1;

b y rtac ax_derivs.FVar 1;
b y  etac MGFn_InitD 1;
b y forw_hyp_eval_Force_tac 1;

b y rtac ax_derivs.AVar 1;
b y  etac (MGFnD RS ax_NormalD) 1;
b y forw_hyp_eval_Force_tac 1;

b y rtac ax_derivs.NewC 1;
b y etac (MGFn_InitD RS conseq2) 1;
b y eval_Force_tac 1;

b y res_inst_tac [("Q","(\<lambda>(Y',s') (Y,s). Y' = Y \<and> \
\ G\<turnstile>s \<midarrow>init_comp_ty ty\<rightarrow> s' \<and> normal s) \<and>. G\<turnstile>init\<le>n")] ax_derivs.NewA 1;
b y  EVERY'[simp_tac (simpset() addsimps [init_comp_ty_def]addsplits[split_if]),
            rtac conjI THEN_ALL_NEW Clarsimp_tac] 1;
b y   etac MGFn_InitD 1;
b y  ax_tac1 ax_derivs.Skip 1;
b y forw_hyp_eval_Force_tac 1;

b y ax_tac2 ax_derivs.Cast 1;
b y ax_tac2 ax_derivs.Inst 1;
b y ax_tac1 ax_derivs.Lit 1;
b y ax_tac1 ax_derivs.Super 1;
b y ax_tac2 ax_derivs.Acc 1;

b y rtac ax_derivs.Ass 1;
b y  etac (MGFnD RS ax_NormalD) 1;
b y forw_hyp_eval_Force_tac 1;

b y rtac ax_derivs.Cond 1;
b y  etac (MGFnD RS ax_NormalD) 1;
b y rtac allI 1;
b y Xcpt_cases_tac 1;
b y  eval_Force_tac 2;
b y (case_tac "b" THEN_ALL_NEW EVERY'[Asm_simp_tac, forw_hyp_eval_Force_tac]) 1;

b y res_inst_tac [("R","(\<lambda>(Y',s') (Y,s). Y' = Y \<and> normal s \<and> (\<exists>s''.\
\ G\<turnstile>s \<midarrow>init tname\<rightarrow> s'' \<and> G\<turnstile>s'' \<midarrow>stmt\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n")] ax_derivs.Body 1;
b y   etac MGFn_InitD 1;
b y  forw_hyp_eval_Force_tac 1;
b y forw_hyp_eval_Force_tac 1;

b y ax_tac1 ax_derivs.Skip 1;

b y ax_tac2 ax_derivs.Expr 1;

b y rtac ax_derivs.Comp 1;
b y  etac (MGFn_stmtD RS ax_NormalD) 1;
b y forw_hyp_eval_Force_tac 1;

b y rtac ax_derivs.If 1;
b y  etac (MGFnD RS ax_NormalD) 1;
b y rtac allI 1;
b y Xcpt_cases_tac 1;
b y  eval_Force_tac 2;
b y (case_tac "b" THEN_ALL_NEW EVERY'[Asm_simp_tac, forw_hyp_eval_Force_tac]) 1;

b y etac (MGFnD' RS conseq12 RS ax_derivs.Throw) 1;
b y clarsimp_tac eval_css 1;

b y res_inst_tac [("Q","(\<lambda>(Y',s') (Y,s). Y' = Y \<and> normal s \<and> \
\ (\<exists>s''. G\<turnstile>s \<midarrow>stmt1\<rightarrow> s'' \<and> G\<turnstile>s'' \<midarrow>sxalloc\<rightarrow> s')) \<and>. G\<turnstile>init\<le>n")] 
         ax_derivs.Try 1;
b y   etac (MGFn_stmtD RS ax_NormalD RS conseq2) 1;
b y   force_tac(claset()addEs[sxalloc_gext RS card_nyinitcls_gext],simpset())1;
b y  forw_hyp_eval_Force_tac 1;
b y eval_Force_tac 1;

b y res_inst_tac [("Q","(\<lambda>(Y',s') (Y,s). \<exists>a. Y' = Xcpt a # Y \<and> \
\ normal s \<and> G\<turnstile>s \<midarrow>stmt1\<rightarrow> (a,snd s')) \<and>. G\<turnstile>init\<le>n")] ax_derivs.Fin 1;
b y  forw_hyp_eval_Force_tac 1;
b y forw_hyp_tac 1;
b y pair_tac "s'" 1;
b y clarsimp_tac (claset(),simpset()addsimprocs [eval_stmt_proc]) 1;
b y datac eval.Fin 1 1;
b y Clarsimp_tac 1;

b y ax_tac1 ax_derivs.Nil 1;

b y rtac ax_derivs.Cons 1;
b y  etac (MGFnD RS ax_NormalD) 1;
b y forw_hyp_eval_Force_tac 1;
qed_spec_mp "MGFn_lemma";

Goal "\<forall>C sig. is_methd G C sig \<longrightarrow> G,A\<turnstile>{op =} In1l (Methd C sig)\<succ> {G\<rightarrow>} \<Longrightarrow> \
\ G,A\<turnstile>{op =} t\<succ> {G\<rightarrow>}";
b y full_simp_tac (simpset()addsimps[MGF_MGFn_iff]) 1;
b y rtac allI 1;
b y rtac MGFn_lemma 1;
b y strip_tac 1;
b y rtac MGFn_free_wt 1;
b y fast_tac (claset() addDs [wt_Methd_is_methd]) 1;
qed "MGF_lemma";

AddSIs[splitI2];
Addsimprocs [ eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc];


section "nested version";

Goal "[| !!A ts. ts <= A ==> P A ts;\
\ !!A pn. !b:bdy pn. P (insert (mgf_call pn) A) {mgf b} ==> P A {mgf_call pn};\
\         !!A t. !pn:U. P A {mgf_call pn} ==> P A {mgf t}; \
\         finite U; uA = mgf_call``U |] ==> \
\ !A. A <= uA --> n <= card uA --> card A = card uA - n --> (!t. P A {mgf t})";
by (cut_facts_tac (premises()) 1);
by (induct_tac "n" 1);
by  (ALLGOALS Clarsimp_tac);
bd  (permute_prems 0 1 card_seteq) 1;
by    (Asm_simp_tac 1);
be   finite_imageI 1;
by  (Asm_full_simp_tac 1);
by  (resolve_tac (tl(tl(premises()))) 1); (*MGF_lemma*)
br  ballI 1;
by  (resolve_tac (premises()) 1); (*ax_derivs.asm*)
by  (Fast_tac 1);
by (resolve_tac (tl(tl(premises()))) 1); (*MGF_lemma*)
br ballI 1;
by (case_tac "mgf_call pn : A" 1);
by  (resolve_tac (premises()) 1); (*ax_derivs.asm*)
by  (Fast_tac 1);
by (resolve_tac (tl(premises())) 1); (*MGF_nested_Methd*)
br ballI 1;
byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, dtac spec 4];
by    (fast_tac (claset() addSDs [hd (tl(tl(tl(premises()))))]) 4);
by   (Fast_tac 1);
be  Suc_leD 1;
bd finite_subset 1;
be  finite_imageI 1;
by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1);
qed_spec_mp "nesting_lemma'";

Goal "[| !!A ts. ts <= A ==> P A ts;\
\ !!A pn. !b:bdy pn. P (insert (mgf (f pn)) A) {mgf b} ==> P A {mgf (f pn)};\
\         !!A t. !pn:U. P A {mgf (f pn)} ==> P A {mgf t};\
\         finite U |] ==> P {} {mgf t}";
by (res_inst_tac [("mgf","mgf")] nesting_lemma' 1);
by (eresolve_tac (tl (premises())) 2);
by (resolve_tac (tl (tl (premises()))) 2);
by (TRYALL (resolve_tac (premises())));
br le_refl 5;
by Auto_tac;
qed_spec_mp "nesting_lemma";

Goalw [MGF_def] "\<lbrakk> \
\ G,insert ({Normal op =} In1l (Methd  C sig) \<succ>{G\<rightarrow>}) A\<turnstile> \
\           {Normal op =} In1l (body G C sig) \<succ>{G\<rightarrow>} \
\\<rbrakk> \<Longrightarrow>  G,A\<turnstile>{Normal op =} In1l (Methd  C sig) \<succ>{G\<rightarrow>}";
b y rtac ax_MethdN 1;
b y etac conseq2 1;
b y Clarsimp_tac 1;
b y etac MethdI 1;
qed "MGF_nested_Methd";

Goal "ws_prog G \<Longrightarrow> G,{}\<turnstile>{op =} t\<succ> {G\<rightarrow>}";
b y rtac MGFNormalI 1;
b y res_inst_tac [
 ("mgf","\<lambda>t. {Normal op =} t\<succ> {G\<rightarrow>}"),
 ("bdy","\<lambda>(C,sig).{In1l (body G C sig)}"),
 ("f","\<lambda>(C,sig). In1l (Methd C sig)")
                 ] nesting_lemma 1;
b y    etac ax_derivs.asm 1;
b y   EVERY'[pair_tac "pn", Clarsimp_tac] 1;
b y   etac MGF_nested_Methd 1;
b y  etac finite_is_methd 2;
b y rtac (MGF_lemma RS MGFNormalD) 1;
b y Clarify_tac 1;
b y rtac MGFNormalI 1;
b y Force_tac 1;
qed "MGF_deriv";


section "simultaneous version";

Goalw [MGF_def]"finite ms \<Longrightarrow> \
\ G,A\<union> (\<lambda>(C,sig). {Normal op =} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) `` ms \
\    |\<turnstile>(\<lambda>(C,sig). {Normal op =} In1l (body G C sig)\<succ> {G\<rightarrow>}) `` ms \<Longrightarrow> \
\ G,A|\<turnstile>(\<lambda>(C,sig). {Normal op =} In1l (Methd  C sig)\<succ> {G\<rightarrow>}) `` ms";
b y rtac (rewrite_rule [mtriples_def] ax_derivs.Methd) 1;
b y etac ax_finite_pointwise 1;
b y  rtac (ax_derivs.asm) 2;
b y  Fast_tac 2;
b y Clarsimp_tac 1;
b y rtac conseq2 1;
b y  eatac ax_methods_spec 1 1;
b y Clarsimp_tac 1;
b y etac eval_Methd 1;
qed "MGF_simult_Methd_lemma";

Goal "ws_prog G \<Longrightarrow> G,{}|\<turnstile>(\<lambda>(C,sig). {Normal op =} In1l (Methd C sig)\<succ> {G\<rightarrow>})\
\  `` Collect (split (is_methd G)) ";
b y ftac finite_is_methd 1;
b y rtac MGF_simult_Methd_lemma 1;
b y  atac 1;
b y etac ax_finite_pointwise 1;
b y  rtac ax_derivs.asm 2;
b y  Fast_tac 2;
b y clarsimp_tac (claset(),simpset()delsimps[normal_def2]) 1;(*####*)
b y rtac (MGF_lemma RS MGFNormalD) 1;
b y Clarify_tac 1;
b y rtac MGFNormalI 1;
b y Fast_tac 1;
qed "MGF_simult_Methd";

Goal "ws_prog G \<Longrightarrow> G,{}\<turnstile>{op =} t\<succ> {G\<rightarrow>}";
b y rtac MGF_lemma 1;
b y strip_tac 1;
b y rtac MGFNormalI 1;
b y rtac ax_derivs.weaken 1;
b y  etac MGF_simult_Methd 1;
b y Force_tac 1;
qed "MGF_deriv";


section "corollaries";

Goal "G,{}\<turnstile>{op =} t\<succ> {G\<rightarrow>} \<Longrightarrow> \
\ G,{}\<Turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,{}\<turnstile>{P::rstate assn} t\<succ> {Q}";
b y rtac ax_no_hazard 1;
b y rewtac MGF_def;
b y etac conseq12 1;
b y clarsimp_tac (claset() addSDs[eval_evaln], simpset() addsimps 
     [ax_valids_def,triple_valid_def]) 1;
b y EVERY'[smp_tac 5, etac impE, Fast_tac, smp_tac 2] 1;
b y EVERY'[case_tac "is_stmt t", dtac is_stmtD] 1;
b y  Auto_tac;
qed "MGF_complete";

Goal "ws_prog G \<Longrightarrow> G,{}\<Turnstile>{P::rstate assn} t\<succ> {Q} \<Longrightarrow> G,{}\<turnstile>{P} t\<succ> {Q}";
b y rtac MGF_complete 1;
b y  etac MGF_deriv 1;
b y atac 1;
qed "ax_complete";