File AxSem.ML

open AxSem;

Goalw [assn_imp_def] "(P \<Rightarrow> Q) = (\<forall>Y s Z. P (Y,s) Z \<longrightarrow> Q (Y,s) Z)";
b y rtac refl 1;
qed "assn_imp_def2";
AddIffs[assn_imp_def2];

Goalw [lsplit_def]  "(lsplit P o f) Y s Z = ((\<lambda>a#Y. P a Y s Z) o f) Y";
b y Simp_tac 1;
qed "lsplit_partial_beta";
Addsimps[lsplit_partial_beta];

Goalw [lsplit_def] "(\<lambda>Y s Z. (lsplit (P s Z) o f) Y) = \
\                            (\<lambda>a#Y s Z. P s Z a Y) o f";
b y rtac ext 1;
b y Simp_tac 1;
qed "assn_lsplit_conc";
Addsimps[assn_lsplit_conc];

Goal "(\<forall>Z. (\<lambda>(Y,s). P Y s) Z \<longrightarrow> Q Z) = (\<forall>Y s. P Y s \<longrightarrow> Q (Y,s))";
b y Auto_tac;
qed "split_paired_All_aux";
Addsimps[split_paired_All_aux];

Goal "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})";
br injI 1;
b y Auto_tac;
qed "inj_triple";

Goal "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')";
b y Auto_tac;
qed "triple_inj_eq";

Goal "(\<forall>(Z::rstate). P Z) = (\<forall>Y s. P (Y,s))";
b y auto_tac (claset(), simpset() addsimps [split_paired_All]);
qed "split_paired_All_rstate";

qed_goalw "the_Res_Res"   thy [the_Res_def ] "the_Res  (Res x) = x"
			  (K [Auto_tac]);
qed_goalw "the_Xcpt_Xcpt" thy [the_Xcpt_def] "the_Xcpt (Xcpt x) = x"
			  (K [Auto_tac]);
qed_goalw "the_Lcls_Lcls" thy [the_Lcls_def] "the_Lcls (Lcls x) = x"
			 (K [Auto_tac]);
Addsimps[the_Res_Res,the_Xcpt_Xcpt,the_Lcls_Lcls];


section "assertion transformers";

Goalw [assn_supd_def] "assn_supd P f Ys Z = (\<exists>s. P (fst Ys,s) Z \<and> snd Ys = f s)";
b y pair_tac "Ys" 1;
b y Simp_tac 1;
qed "assn_supd_def2";
Addsimps[assn_supd_def2];

Goalw [supd_assn_def] "(f .; P) (Y,s) = P (Y,f s)"; 
b y Simp_tac 1;
qed "supd_assn_def2";
Addsimps[supd_assn_def2];

Goal "(f .; split P) = (\<lambda>(Y,s). P Y (f s))";
b y rtac ext 1;
b y Simp_tac 1;
qed "split_supd_assn";
Addsimps[split_supd_assn];

Goal "((f .; Q) ;. f) Ys Z \<Longrightarrow> Q Ys Z";
b y pair_tac "Ys" 1;
b y Auto_tac;
qed "supd_assn_supdD";
AddEs[supd_assn_supdD];

Goal "Q Ys Z \<Longrightarrow> (f .; (Q ;. f)) Ys Z";
b y pair_tac "Ys" 1;
b y Auto_tac;
qed "supd_assn_supdI";
AddEs[supd_assn_supdI];


section "peek_and";

Goalw [peek_and_def] "peek_and P p (Y,s) = (\<lambda>Z. (P (Y,s) Z \<and> p s))";
b y Simp_tac 1;
qed "peek_and_def2";
Addsimps[peek_and_def2];

Goal "(P \<and>. (\<lambda>s. ¬ f s)) = (P \<and>. Not \<circ> f)";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_and_Not";
Addsimps [peek_and_Not];

Goalw [peek_and_def] "peek_and (peek_and P p) p = peek_and P p";
b y Simp_tac 1;
qed "peek_and_and";
Addsimps[peek_and_and];

Goal "peek_and (Normal P) p = Normal (peek_and P p)";
b y rtac ext 1;
b y rtac ext 1;
b y Auto_tac;
qed "peek_and_Normal";
Addsimps[peek_and_Normal];

Goal "(\<lambda>(Y,s). Normal P (f Y s, s)) = Normal (\<lambda>(Y,s). P (f Y s, s))"; 
b y rtac ext 1;
b y Auto_tac;
qed "upd_res_Normal";
Addsimps[upd_res_Normal];


section "result handling";

bind_thms ("res_rews", sum3_instantiate res_def);
Addsimps res_rews;

Goalw [res_def] "res t w' Y'=res t w Y = ((is_stmt t \<or> w'=w) \<and> Y'=Y)";
b y auto_tac (claset(), simpset_of Main.thy);
qed "res_partial_inj";
Addsimps[res_partial_inj];

Goalw [res_push_def] "(P\<up>#w) (Y,s) = P (w#Y,s)";
b y Clarsimp_tac 1;
qed "res_push_def2";
Addsimps[res_push_def2];

Goal "split P\<up>#w = (\<lambda>(Y,s). P (w#Y) s)";
b y rtac ext 1;
b y Simp_tac 1;
qed "split_res_push";
Addsimps[split_res_push];

Goal "split (lsplit (P \<circ> f'))\<up>#f x = split (P (f' (f x)))";
b y rtac ext 1;
b y Simp_tac 1;
qed "split_lsplit_res_push";
Addsimps[split_lsplit_res_push];

Goal "(P \<and>. p)\<up>#w = (P\<up>#w \<and>. p)"; 
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_and_push";
Addsimps[peek_and_push];

Goalw [res_pop_def] "res_pop Pf (p#Y,s) = Pf p (Y,s)";
b y Simp_tac 1;
qed "res_pop_def2";
Addsimps[res_pop_def2];

Goal "res_pop (P \<circ> f)\<up>#w = P (f w)";
b y rtac ext 1;
b y Simp_tac 1;
qed "res_pop_res_push";
Addsimps[res_pop_res_push];

Goalw [res_eqpop_def] "(P\<down>#w) (Y,s) Z = (\<exists>Y'. Y=w#Y' \<and> P (Y',s) Z)";
b y Simp_tac 1;
qed "res_eqpop_def2";
Addsimps[res_eqpop_def2];

Goal "(P\<down>#w)\<up>#w = P";
b y rtac ext 1;
b y Simp_tac 1;
qed "res_eqpop_push";
Addsimps[res_eqpop_push];

Goalw [res_ign_def] "(P\<down>) (y#Y,s) = P (Y,s)";
b y Simp_tac 1;
qed "res_ign_def2";
Addsimps[res_ign_def2];

Goal "P\<down>\<up>#w = P";
b y rtac ext 1;
b y Simp_tac 1;
qed "res_ign_push";
Addsimps[res_ign_push];

Goalw [peek_st_def] "(\<lambda>s: Pf s) (Y,s) = Pf (snd s) (Y,s)";
b y Simp_tac 1;
qed "peek_st_def2";
Addsimps[peek_st_def2];

Goal "(\<lambda>s: P) = P";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_st_triv";
Addsimps[peek_st_triv];

Goal "(\<lambda>s: \<lambda>(Y,s'). P s Y s') = (\<lambda>(Y,s). P (snd s) Y s)";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_st_split";
Addsimps [peek_st_split];

Goal "(\<lambda>s: P s)\<up>#w = (\<lambda>s: P s\<up>#w)";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_st_res_push";
Addsimps [peek_st_res_push];

Goal "(\<lambda>s: \<lambda>s': P s s') = (\<lambda>s: P s s)";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_st_st";
Addsimps [peek_st_st];


Goalw [Bool_assn_def] 
"(P\<up>#Bool=b) (Y,s) Z = (\<exists>v. P (Val v#Y,s) Z \<and> (normal s \<longrightarrow> the_Bool v=b))";
b y Simp_tac 1;
qed "Bool_assn_def2";
Addsimps[Bool_assn_def2];

Goal "P (Val b#Y, s) Z \<Longrightarrow> (P\<up>#Bool=the_Bool b) (Y, s) Z";
b y Auto_tac;
qed "Bool_assn_the_BoolI";

Goalw [RefVar_def,Let_def] "RefVar vf P (Val a#Y,s) = \
\ (P\<up>#Var (fst (vf a s))) (Y,(snd (vf a s)))";
b y simp_tac (simpset() addsimps [split_beta]) 1;
qed "RefVar_def2";
Addsimps[RefVar_def2];


section "allocation";

Goalw [Alloc_def] "Alloc G otag P (Y,s) Z = \
\      (\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)#Y,s') Z)";
b y Simp_tac 1;
qed "Alloc_def2";
Addsimps [Alloc_def2];

Goalw[SXAlloc_def]"SXAlloc G P (Y,s) Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P (Y,s') Z)";
b y Simp_tac 1;
qed "SXAlloc_def2";
Addsimps [SXAlloc_def2];


section "validity";

Goalw [triple_valid_def,type_ok_def] "G\<Turnstile>n:{P} t\<succ> {Q} = \
\(\<forall>Y s Z. P (Y,s) Z \<longrightarrow> (\<exists>L. (normal s \<longrightarrow> (\<exists>T. (G,L)\<turnstile>t\<Colon>T)) \<and> s\<Colon>\<preceq>(G,L)) \<longrightarrow>\
\ (\<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s')\<longrightarrow> Q (res t w Y,s') Z))";
b y Simp_tac 1;
qed "triple_valid_def2";


simpset_ref():=simpset() delsimps [split_paired_All,split_paired_Ex]
		 addsimps  [split_paired_All_rstate]
		 delsplits [split_if    , option.split    ]
		 delsplits [split_if_asm, option.split_asm]
		 delloop "split_all_tac";
claset_ref ():=claset()  delSWrapper "split_all_tac";


section "rules derived by induction";

Goal "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts";
b y rewtac ax_valids_def;
b y Fast_tac 1;
qed "cut_valid";

(*if cut is available
Goal "\<lbrakk>G,A'|\<turnstile>ts; A' \<subseteq> A; \<forall>P Q t. {P} t\<succ> {Q} \<in> A' \<longrightarrow> (\<exists>T. (G,L)\<turnstile>t\<Colon>T) \<rbrakk> \<Longrightarrow> \
\      G,A|\<turnstile>ts";
b y etac ax_derivs.cut 1;
b y eatac ax_derivs.asm 1 1;
qed "ax_thin";
*)
Goal "G,A'|\<turnstile>ts \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts";
by (etac ax_derivs.induct 1);
by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
br		  ax_derivs.empty 1;
by               (eatac ax_derivs.insert 1 1);
by              (fast_tac (claset() addIs [ax_derivs.asm]) 1);
(*by           (fast_tac (claset() addIs [ax_derivs.cut]) 1);*)
by            (fast_tac (claset() addIs [ax_derivs.weaken]) 1);
by           (EVERY'[rtac ax_derivs.conseq, strip_tac, smp_tac 3,Clarify_tac,
	             smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
(* 29 subgoals *)
by (EVERY'[rtac ax_derivs.Init THEN_ALL_NEW Force_tac] 29);
by (EVERY'[rtac ax_derivs.Methd, dtac spec, etac mp, Fast_tac] 16);
by (TRYALL(resolve_tac((funpow 5 tl)ax_derivs.intrs) THEN_ALL_NEW Blast_tac));
qed_spec_mp "ax_thin";

Goal "G,A\<turnstile>t \<Longrightarrow> G,insert x A\<turnstile>t";
be ax_thin 1;
by (Fast_tac 1);
qed "ax_thin_insert";

Goalw [mtriples_def]
  "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})";
b y rtac subset_image_iff 1;
qed "subset_mtriples_iff";

Goal "G,A|\<turnstile>ts' \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts";
b y etac ax_derivs.induct 1;
(*34 subgoals*)
b y       ALLGOALS strip_tac;
b y       ALLGOALS (REPEAT o (EVERY'[dtac subset_singletonD,etac disjE,
              		      fast_tac (claset() addSIs [ax_derivs.empty])]));
b y       TRYALL hyp_subst_tac;
b y       EVERY'[Asm_full_simp_tac, rtac ax_derivs.empty] 1;
b y      dtac subset_insertD 1;
b y      blast_tac (claset() addIs [ax_derivs.insert]) 1;
b y     fast_tac (claset() addIs [ax_derivs.asm]) 1;
(*b y  blast_tac (claset() addIs [ax_derivs.cut]) 1;*)
b y   fast_tac (claset() addIs [ax_derivs.weaken]) 1;
b y  EVERY'[rtac ax_derivs.conseq, Clarify_tac, smp_tac 3, Blast_tac] 1;
(*29 subgoals*)
b y TRYALL (resolve_tac ((funpow 5 tl) ax_derivs.intrs) THEN_ALL_NEW Fast_tac);
(*1 subgoal*)
b y clarsimp_tac (claset(), simpset() addsimps [subset_mtriples_iff]) 1;
b y rtac ax_derivs.Methd 1;
b y dtac spec 1;
b y etac impE 1;
b y  rtac exI 1;
b y  etac conjI 1;
b y  rtac refl 1;
(* dead end
Methd is to blame
b y defer_tac 1;
qed_spec_mp "weaken";
*)


section "rules derived from conseq";

Goal "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'}; \
\\<forall>Y s Z. P (Y,s) Z \<longrightarrow> (\<forall>w s'. (\<forall>Y' Z'. P' (Y',s) Z' \<longrightarrow> Q' (res t w Y',s') Z') \<longrightarrow> Q (res t w Y,s') Z)\<rbrakk> \
\ \<Longrightarrow>  G,A\<turnstile>{P } t\<succ> {Q }";
b y rtac ax_derivs.conseq 1;
b y Clarsimp_tac 1;
b y Blast_tac 1;
qed "conseq12";

(*unused, but nice variant*)
Goal "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'}; \<forall>s w s'. \
\      (\<forall>Y Z. P' (Y,s) Z \<longrightarrow> Q' (res t w Y,s') Z) \<longrightarrow> \
\      (\<forall>Y Z. P  (Y,s) Z \<longrightarrow> Q  (res t w Y,s') Z)\<rbrakk> \
\ \<Longrightarrow>  G,A\<turnstile>{P } t\<succ> {Q }";
b y etac conseq12 1;
b y Fast_tac 1;
qed "conseq12'";

Goal "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'}; \
\\<forall>Y s Z. P (Y,s) Z \<longrightarrow> (\<forall>w s'. (\<forall>Y' Z'. P' (Y',s) Z' \<longrightarrow> Q' (res t w Y',s') Z') \<longrightarrow> Q (res t w Y,s') Z)\<rbrakk> \
\ \<Longrightarrow>  G,A\<turnstile>{P } t\<succ> {Q }";
b y etac conseq12' 1;
b y Blast_tac 1;
qed "conseq12_from_conseq12'";

Goal "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q}";
b y etac conseq12 1;
b y Blast_tac 1;
qed "conseq1";

Goal "\<lbrakk>G,A\<turnstile>{P} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}";
b y etac conseq12 1;
b y Blast_tac 1;
qed "conseq2";

Goal "\<lbrakk>\<forall>Y s Z. P (Y,s) Z \<longrightarrow> G,A\<turnstile>{\<lambda>Ys' Z'. Ys' = (Y,s)} t\<succ> {\<lambda>Ys Z'. Q Ys Z}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{P} t\<succ> {Q}";
b y rtac ax_derivs.conseq 1;
b y Fast_tac 1;
qed "escape";

Goal"\<lbrakk>C\<Longrightarrow>G,A\<turnstile>{\<lambda>(Y,s) Z. P Y s Z} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{\<lambda>(Y,s) Z. C \<and> P Y s Z} t\<succ> {Q}";
b y rtac escape 1;
b y Clarify_tac 1;
b y etac (hd (premises()) RS conseq12) 1;
b y Blast_tac 1;
(*alternative (more direct) proof:
b y rtac ax_derivs.conseq 1;
by (fast_tac (claset() addDs (premises())) 1);
*)
qed "constant";

Goal "G,A\<turnstile>{\<lambda>Ys Z. False} t\<succ> {Q}";
b y rtac escape 1;
b y Clarify_tac 1;
qed "impossible";
AddIs[impossible];

(* unused *)
Goal "G,A\<turnstile>{P}  t\<succ> {\<lambda>Ys Z. True}";
b y rtac ax_derivs.conseq 1;
b y Clarify_tac 1;
b y rtac exI 1;
b y rtac exI 1;
b y rtac (impossible RS conjI) 1;
b y Clarify_tac 1;
qed "ax_trivial";

(* unused *)
Goal "\<lbrakk>G,A\<turnstile>{P1} t\<succ> {Q1}; G,A\<turnstile>{P2} t\<succ> {Q2}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{\<lambda>Ys Z. P1 Ys Z \<or> P2 Ys Z} t\<succ> {\<lambda>Ys Z. Q1 Ys Z \<or> Q2 Ys Z}";
b y rtac escape 1;
b y Safe_tac;
b y  ALLGOALS (EVERY'[etac conseq12, Fast_tac]);
qed "ax_disj";

(* unused *)
Goal  "(\<exists>Q. G,A\<turnstile>{P} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) = \
\      (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})";
b y best_tac (claset() addSEs [conseq1, conseq2]) 1;
qed "supd_shuffle";

Goalw [peek_and_def] "\<lbrakk>G,A\<turnstile>{P \<and>.       C} t\<succ> {Q}; \
                      \G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}";
b y rtac escape 1;
b y Clarify_tac 1;
b y (case_tac "C s" THEN_ALL_NEW EVERY'[etac conseq12, Force_tac]) 1;
(*alternative (more direct) proof:
b y rtac ax_derivs.conseq 1;
b y Clarify_tac 1;
b y case_tac "C s" 1;
b y  ALLGOALS Force_tac;
*)
qed "ax_cases";

Goal "G,A\<turnstile>{Normal P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}";
b y etac conseq1 1;
b y Simp_tac 1;
qed "peek_and_forget1_Normal";

Goal "G,A\<turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}";
b y etac conseq1 1;
b y Simp_tac 1;
qed "peek_and_forget1";

bind_thm ("ax_NormalD", read_instantiate [("p","normal")] peek_and_forget1);

Goal "G,A\<turnstile>{P} t\<succ> {Q \<and>. p} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}";
b y etac conseq2 1;
b y Simp_tac 1;
qed "peek_and_forget2";

(*unused*)
Goal "G,A\<turnstile>{op =} t\<succ> {op =} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {P}";
b y etac conseq12 1;
b y Clarsimp_tac 1;
qed "nochange";

(* unused *)
Goal 
"G,A\<turnstile>{P} t\<succ> {Q}\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {\<lambda>(Y,s) Z. \<exists>v Y'. Y=res t v Y' \<and> Q (Y,s) Z}";
b y etac conseq12 1;
b y Force_tac 1;
qed "exists_res";

(* unused *)
Goal "G,A\<turnstile>{P} t\<succ> {Q}\<Longrightarrow> \
\ G,A\<turnstile>{P\<up>#y} t\<succ> {\<lambda>(Y,s) Z. \<exists>v Y'. Y=res t v Y' \<and> Q (res t v (y # Y'), s) Z}";
b y etac conseq12 1;
b y Force_tac 1;
qed "extend_res";

(* unused *)
Goal "G,A\<turnstile>{P} .c. {Q} \<Longrightarrow> G,A\<turnstile>{P\<up>#y} .c. {Q\<up>#y}"; 
b y etac conseq12 1;
b y Clarsimp_tac 1;
qed "extend_res_stmt";


section "alternative axioms";

Goal "G,A\<turnstile>{Normal P} LVar vn=\<succ> {Normal (\<lambda>s: P\<down>#Var (lvar vn s))}";
b y rtac (ax_derivs.LVar RS conseq1) 1;
b y Clarsimp_tac 1;
qed "ax_LVar2";

Goal "G,A\<turnstile>{Normal P} Lit v-\<succ> {Normal (P\<down>#Val v)}";
b y rtac (ax_derivs.Lit RS conseq1) 1;
b y Clarsimp_tac 1;
qed "ax_Lit2";

Goal "G,A\<turnstile>{Normal P} Super-\<succ> {Normal (\<lambda>s: P\<down>#Val (val_this s))}";
b y rtac (ax_derivs.Super RS conseq1) 1;
b y Clarsimp_tac 1;
qed "ax_Super2";

Goal "G,A\<turnstile>{Normal P} []\<doteq>\<succ> {Normal (P\<down>#Vals [])}";
b y rtac (ax_derivs.Nil RS conseq1) 1;
b y Clarsimp_tac 1;
qed "ax_Nil2";


section "other derived rules";

(* unused *)
Goal "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. G,A\<turnstile>{Normal (P C sig)} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow>\
\      G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}";
b y fatac finite_subset 1 1;
b y make_imp_tac 1;
b y etac thin_rl 1;
b y etac finite_induct 1;
b y  rewtac mtriples_def;
b y  ALLGOALS Clarsimp_tac;
b y  rtac ax_derivs.empty 1;
b y rtac ax_derivs.insert 1; 
b y  ALLGOALS Force_tac;
bind_thm ("ax_finite_mtriples", subset_refl RS result());

Goal "G,A|\<turnstile>insert t ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts";
by (fast_tac (claset() addIs [ax_derivs.weaken]) 1);
qed "ax_derivs_insertD";

Goal "\<lbrakk>G,A|\<turnstile>split f `` ms; (C,sig) \<in> ms\<rbrakk> \<Longrightarrow> G,A\<turnstile>f C sig";
b y etac ax_derivs.weaken 1;
b y force_tac (claset() delrules [image_eqI] addIs [rev_image_eqI],simpset()) 1;
qed "ax_methods_spec";

(* this version is used to avoid using the cut rule *)
Goal "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow> \
\ ((\<forall>(C,sig)\<in>F. G,A\<turnstile>f C sig) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>g C sig)) \<longrightarrow> \
\     G,A|\<turnstile>split f `` F \<longrightarrow> G,A|\<turnstile>split g `` F";
b y fatac finite_subset 1 1;
b y make_imp_tac 1;
b y etac thin_rl 1;
b y etac finite_induct 1;
b y  ALLGOALS Clarsimp_tac;
b y dtac ax_derivs_insertD 1;
b y rtac ax_derivs.insert 1;
b y  split_all_tac 1;
b y  Auto_tac;
b y eatac ax_methods_spec 1 1;
bind_thm ("ax_finite_pointwise", subset_refl RS result() RS mp RS mp);

Goal "G,A\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}";
b y etac ax_cases 1;
b y rtac (ax_derivs.hazard RS conseq1) 1;
b y Force_tac 1;
qed "ax_no_hazard";

Goal "(\<exists>T L. (G,L)\<turnstile>t\<Colon>T) \<longrightarrow> G,A\<turnstile>{Normal P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{Normal P} t\<succ> {Q}";
b y rtac ax_no_hazard 1;
b y rtac escape 1;
b y Clarify_tac 1;
b y etac (mp RS conseq12) 1;
b y  auto_tac (claset(), simpset() addsimps [type_ok_def]);
qed "ax_free_wt";

bind_thms ("ax_Xcpts", sum3_instantiate ax_derivs.Xcpt);
AddSIs ax_Xcpts;

Goal "G,A\<turnstile>{P} .Skip. {P}";
b y res_inst_tac [("C","normal")] ax_cases 1;
b y  rtac ax_derivs.Skip 1;
b y Fast_tac 1;
qed "ax_Skip";
AddSIs[ax_Skip];
bind_thm ("ax_SkipI", ax_Skip RS conseq2);

Goal "\<lbrakk>the (cmethd G C (mn,pTs)) = (md,(m,pns,rT),lvars,bdy);\
\         G,A\<turnstile>{Normal P} e-\<succ> {Q\<down>}; \
\         G,A\<turnstile>{Q} args\<doteq>\<succ> {\<lambda>Vals:vs#. \<lambda>s: set_lvars ((init_vals \
\              (table_of lvars)(pns[\<mapsto>]vs)) (+) empty) .; R\<up>#Lcls (locals s)};\
\         G,A\<turnstile>{R} Methd C (mn,pTs)-\<succ> \
\             {\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v}\<rbrakk> \<Longrightarrow> \
\         G,A\<turnstile>{Normal P} {t,ClassT C,Static}e..mn({pTs}args)-\<succ> {S}";
b y res_inst_tac [("Q","\<lambda>(Y,s) Z. \<exists>w Y'. Y=w#Y' \<and> Q (Y',s) Z"),("R","\<lambda>(v#Y,s) Z. v=DynT C \<and> R (Y,s) Z")] ax_derivs.Call 1;
b y   etac conseq12 1;
b y   Clarsimp_tac 1;
b y  ALLGOALS (full_simp_tac (simpset() addsimps [Let_def, init_lvars_def]));
b y  etac conseq12 1;
b y  Clarsimp_tac 1;
b y  pair_tac "s'" 1;
b y  Clarsimp_tac 1;
b y EVERY'[rtac allI, rtac escape, Clarsimp_tac] 1;
b y EVERY'[etac conseq12, Clarsimp_tac] 1;
qed "ax_Call_Static";

Goal "\<lbrakk>the (cmethd G C (mn,pTs)) = (md,(m,pns,rT),lvars,bdy);\
\         G,A\<turnstile>{Normal P} e-\<succ> {Q}; \
\         G,A\<turnstile>{Q} args\<doteq>\<succ> {\<lambda>Vals:vs#Val:a#. (\<lambda>s: (\<lambda>(x,s). (np a x, \
\  set_locals (init_vals(table_of lvars)(pns[\<mapsto>]vs) (+)¬False ?\<mapsto>a) s)) .; \
\ R\<up>#Lcls (locals s)) \<and>. (\<lambda>s. C=obj_class (the (heap (snd s) (the_Addr a))))};\
\         G,A\<turnstile>{R \<and>. (\<lambda>s. normal s \<longrightarrow> G\<turnstile>IntVir\<rightarrow>C\<preceq>t)} Methd C (mn,pTs)-\<succ> \
\             {\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v}\<rbrakk> \<Longrightarrow> \
\         G,A\<turnstile>{Normal P} {t,cT,IntVir}e..mn({pTs}args)-\<succ> {S}";
b y res_inst_tac [("Q","\<lambda>(Y,s) Z. \<exists>a Y'. Y=a#Y' \<and> Q (Y,s) Z"),
		  ("R","\<lambda>(v#Y,s) Z. v=DynT C \<and> R (Y,s) Z")] ax_derivs.Call 1;
b y   etac conseq12 1;
b y   Clarsimp_tac 1;
b y  ALLGOALS (full_simp_tac (simpset() addsimps [Let_def, init_lvars_def]));
b y  etac conseq12 1;
b y  Force_tac 1;
b y EVERY'[rtac allI, rtac escape, Clarsimp_tac] 1;
b y EVERY'[etac conseq12, Clarsimp_tac] 1;
qed "ax_Call_known_DynT";

Goal "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk>\<Longrightarrow>\
\      G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}";
b y dtac ax_derivs.Methd 1;
b y rewtac mtriples_def;
b y eatac ax_methods_spec 1 1;
qed "ax_Methd1";

Goal
"G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile>\
\         {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow> \
\      G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}";
b y rtac ax_Methd1 1;
b y  rtac singletonI 2;
b y rewtac mtriples_def;
b y Clarsimp_tac 1;
qed "ax_MethdN";


section "rules derived from Init and Done";

Goal "\<lbrakk>the (class G C) = (sc,si,fs,ms,ini); C \<noteq> Object;\
\      G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))} .init sc.\
\          {\<lambda>s: Q\<up>#Lcls (locals s)}; \
\      G,A\<turnstile>{Q ;. set_lvars empty} .ini.\
\          {\<lambda>Lcls:l#. set_lvars l .; R}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .init C. {R}";
b y etac ax_derivs.Init 1;
b y  Asm_simp_tac 1;
b y atac 1;
qed "ax_InitS";

Goal "\<lbrakk>the (class G C) = (sc,si,fs,ms,Skip); C \<noteq> Object;\
\      P \<Rightarrow> (supd (init_class_obj G C) .; P); \
\      G,A\<turnstile>{Normal (P \<and>. initd C)} .init sc. {P \<and>. initd C}\<rbrakk> \<Longrightarrow> \
\      G,A\<turnstile>{Normal P} .init C. {P \<and>. initd C}"; 
b y res_inst_tac [("C","initd C")] ax_cases 1;
b y  EVERY'[rtac conseq1, rtac ax_derivs.Done, Clarsimp_tac] 1;
b y res_inst_tac [("P1","P"),("Q1","\<lambda>s: P\<down>#Lcls (locals s) \<and>. initd C")] (ax_InitS RS conseq1) 1;
b y     Force_tac 1;
b y    atac 1;
b y   Clarsimp_tac 3;
b y  EVERY'[rtac ax_SkipI, Clarsimp_tac] 2;
b y Simp_tac 1;
b y etac conseq1 1;
b y Force_tac 1;
qed "ax_triv_InitS";

Goal "wf_prog G \<Longrightarrow> \
\ G,A\<turnstile>{Normal ((supd (init_class_obj G Object) .; P) \<and>. Not \<circ> initd Object)} .init Object. \
\     {P \<and>. initd Object}";
b y res_inst_tac [("Q","\<lambda>s: P\<down>#Lcls (locals s) \<and>. initd Object")] 
		ax_derivs.Init 1;
b y   EVERY'[dtac class_Object, Force_tac] 1;
b y  Simp_tac 1;
b y  ALLGOALS (EVERY'[rtac ax_SkipI, Clarsimp_tac]);
qed "ax_Init_Object";

Goal "\<lbrakk>wf_prog G; \
\      P \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{Normal P} .init Object. {P \<and>. initd Object}";
b y res_inst_tac [("C","initd Object")] ax_cases 1;
b y  EVERY'[rtac conseq1, rtac ax_derivs.Done, Clarsimp_tac] 1;
b y etac (ax_Init_Object RS conseq1) 1;
b y Force_tac 1;
qed "ax_triv_Init_Object";


section "introduction rules for Alloc and SXAlloc";

Goal "\<lbrakk>enough_mem; G,A\<turnstile>{P} t\<succ> {\<lambda>(Y,x,s) Z. x = None \<and> \
\ (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> \
\   Q (Val (Addr a)#Y,Norm(init_obj G (CInst C) (Heap a) s)) Z)}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}";
b y etac conseq2 1;
b y force_tac(claset() addSEs halloc_elim_cases addDs [enough_memD],simpset())1;
qed "ax_Alloc_Normal";

Goal "G,A\<turnstile>{P} .c. {Normal Q} \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}";
b y etac conseq2 1;
b y clarsimp_tac (claset() addSEs sxalloc_elim_cases,simpset())1;
qed "ax_SXAlloc_Normal";

Goal "\<lbrakk>enough_mem; G,A\<turnstile>{P} t\<succ> {\<lambda>(Y,x,s) Z. x=Some (StdXcpt xn) \<and> \
\ (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> \
\   Q (Y,Some (XcptLoc a),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z)}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{P} t\<succ> {SXAlloc G (Q \<and>. (\<lambda>s. G,s\<turnstile>catch SXcpt xn))}";
b y etac conseq2 1;
b y force_tac (claset() addSEs sxalloc_elim_cases@halloc_elim_cases
                           addDs [enough_memD], simpset()) 1;
qed "ax_SXAlloc_catch_SXcpt";


val ax_tac = resolve_tac(ax_Skip::ax_MethdN::ax_Alloc_Normal::ax_SXAlloc_Normal::
			 funpow 7 tl ax_derivs.intrs);
val Normal_tac = EVERY'[res_inst_tac [("P'","Normal ?P")] conseq1,
			fn i => Clarsimp_tac (i+1)];