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];

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";


section "assertion transformers";

Goalw [assn_supd_def] "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)";
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 .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z";
b y Auto_tac;
qed "supd_assn_supdD";
AddEs[supd_assn_supdD];

Goal "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z";
b y auto_tac (claset(), simpset() delsimps [split_paired_Ex]);
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 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 "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)";
b y rtac ext 1;
b y rtac ext 1;
b y rtac ext 1;
b y Auto_tac;
qed "peek_and_commut";

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


section "subst_res";

Goalw [subst_res_def] "(P\<leftarrow>w) Y = P w";
b y Simp_tac 1;
qed "subst_res_def2";
Addsimps[subst_res_def2];

Goal "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w";
b y rtac ext 1;
b y Simp_tac 1;
qed "subst_subst_res";
Addsimps[subst_subst_res];

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

(*###Do not work for some strange (unification?) reason
Goal "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)";
b y rtac ext 1;
b y Simp_tac 1;
qed "subst_res_Val_beta";
Addsimps[subst_res_Val_beta];

Goal "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)";
b y rtac ext 1;
b y Simp_tac 1;
qed "subst_res_Var_beta";
Addsimps[subst_res_Var_beta];

Goal "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)";
b y rtac ext 1;
b y Simp_tac 1;
qed "subst_res_Vals_beta";
Addsimps[subst_res_Vals_beta];
*)


section "subst_Bool";

Goalw [subst_Bool_def] 
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))";
b y Simp_tac 1;
qed "subst_Bool_def2";
Addsimps[subst_Bool_def2];

Goal "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z";
b y Auto_tac;
qed "subst_Bool_the_BoolI";


section "peek_res";

Goalw [peek_res_def] "peek_res P Y = P Y Y";
b y Simp_tac 1;
qed "peek_res_def2";
Addsimps[peek_res_def2];

Goal "peek_res P\<leftarrow>w = P w\<leftarrow>w";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_res_subst_res";
Addsimps[peek_res_subst_res];

(* unused *)
Goal "(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)";
b y rtac allI 1;
b y Simp_tac 1;
b y resolve_tac (premises()) 1;
qed "peek_subst_res_allI";


section "peek_st";

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 rtac ext 1;
b y Simp_tac 1;
qed "peek_st_triv";
Addsimps[peek_st_triv];

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

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 rtac ext 1;
b y Simp_tac 1;
qed "peek_st_split";
Addsimps [peek_st_split];

Goal "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)";
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_st_subst_res";
Addsimps [peek_st_subst_res];

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


section "ign_res";

Goalw [ign_res_def] "P\<down> Y s Z = (\<exists>Y. P Y s Z)";
b y Simp_tac 1;
qed "ign_res_def2";
Addsimps[ign_res_def2];

Goal "P\<down>\<down> = P\<down>";
b y rtac ext 1;
b y rtac ext 1;
b y rtac ext 1;
b y Simp_tac 1;
qed "ign_ign_res";
Addsimps[ign_ign_res];

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

Goal "(P \<and>. p)\<down> = (P\<down> \<and>. p)"; 
b y rtac ext 1;
b y rtac ext 1;
b y rtac ext 1;
b y Simp_tac 1;
qed "peek_and_ign_res";
Addsimps[peek_and_ign_res];


section "ign_res_eq";

Goalw [ign_res_eq_def] "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)";
b y Auto_tac;
qed "ign_res_eq_def2";
Addsimps[ign_res_eq_def2];

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

(* unused *)
Goal "P\<down>=w\<leftarrow>w = P\<down>";
b y rtac ext 1;
b y rtac ext 1;
b y rtac ext 1;
b y Simp_tac 1;
qed "ign_res_eq_subst_res";

(* unused *)
Goal "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z  \<and> Y=x)";
b y Simp_tac 1;
qed "subst_Bool_ign_res_eq";


section "RefVar";

Goalw [RefVar_def,Let_def] "(vf ..; P) Y s = \
\ P (Var (fst (vf s))) (snd (vf 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)) 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>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))";
b y Simp_tac 1;
qed "triple_valid_def2";


simpset_ref():=simpset() delsimps [split_paired_All,split_paired_Ex]
                 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'::'a triple set)|\<turnstile>(ts::'a triple set) \<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.Methd, dtac spec, etac mp, Fast_tac] 16);
by (TRYALL(resolve_tac((funpow 5 tl)ax_derivs.intrs) THEN_ALL_NEW Blast_tac));
b y EVERY'[etac ax_derivs.Call, Clarify_tac, Blast_tac, Blast_tac] 1;
qed_spec_mp "ax_thin";

Goal "G,(A::'a triple set)\<turnstile>(t::'a triple) \<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::'a triple set)|\<turnstile>(ts'::'a triple set) \<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;(* unused *)
(*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>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> \
\ Q Y' s' Z)\<rbrakk> \
\ \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }";
b y rtac polymorphic_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 Y' s'. \
\      (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow> \
\      (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  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>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow> \
\ Q 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>Y' s' Z'. (Y',s') = (Y,s)} t\<succ> {\<lambda>Y s Z'. Q Y s Z}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{P} t\<succ> {Q}";
b y rtac polymorphic_conseq 1;
b y Force_tac 1;
qed "ax_escape";

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

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

(* unused *)
Goal "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s";
b y Auto_tac;
qed "ax_nochange_lemma";
Goal "G,A\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {P}";
b y etac conseq12 1;
b y Auto_tac;
b y eatac ax_nochange_lemma 1 1;
qed "ax_nochange";

(* unused *)
Goal "G,A\<turnstile>{P}  t\<succ> {\<lambda>Y s Z. True}";
b y rtac polymorphic_conseq 1;(* unused *)
b y Auto_tac;
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>Y s Z. P1 Y s Z \<or> P2 Y s Z} t\<succ> {\<lambda>Y s Z. Q1 Y s Z \<or> Q2 Y s Z}";
b y rtac ax_escape 1; (* unused *)
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 "ax_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 ax_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; *)(* unused *)(*
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";

Goal "\<forall>v. G,A\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {Q v} \<Longrightarrow> \
\     \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}";
b y force_tac (claset() addSEs [conseq1], simpset()) 1;
qed "ax_subst_Val_allI";

Goal "\<forall>v. G,A\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {Q v} \<Longrightarrow> \
\     \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}";
b y force_tac (claset() addSEs [conseq1], simpset()) 1;
qed "ax_subst_Var_allI";

Goal "(\<forall>v. G,A\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {Q v}) \<Longrightarrow> \
\      \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}";
b y force_tac (claset() addSEs [conseq1], simpset()) 1;
qed "ax_subst_Vals_allI";


section "alternative axioms";

Goal "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}";
b y rtac (ax_derivs.Lit RS conseq1) 1;
b y Force_tac 1;
qed "ax_Lit2";
Goal "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}";
b y rtac (ax_Lit2 RS conseq2) 1;
b y Force_tac 1;
qed "ax_Lit2_test_complete";

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

Goal "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}";
b y rtac (ax_derivs.Super RS conseq1) 1;
b y Force_tac 1;
qed "ax_Super2";

Goal "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}";
b y rtac (ax_derivs.Nil RS conseq1) 1;
b y Force_tac 1;
qed "ax_Nil2";


section "misc derived structural rules";

(* unused *)
Goal "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} 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::'a triple set)|\<turnstile>insert (t::'a triple) 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::'a triple set)|\<turnstile>split f `` ms; (C,sig) \<in> ms\<rbrakk> \<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)";
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::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<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::'a triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q::'a assn} \<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::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> G,A\<turnstile>{Normal P} t\<succ> {Q}";
b y rtac ax_no_hazard 1;
b y rtac ax_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::'a triple set)\<turnstile>{P\<leftarrow>\<bullet>} .Skip. {P::'a assn}";
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 conseq1);


section "derived rules for methd call";

Goal "\<lbrakk>the (cmethd G C (mn,pTs)) = (md,(m,pns,rT),lvars,bdy); \
\  \<forall>vs l. G,A\<turnstile>{R\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (snd s)) ;. \
\              init_lvars G C (mn,pTs) Static any_Addr vs} \
\             Methd C (mn,pTs)-\<succ> {set_lvars l .; S};\
\         G,A\<turnstile>{Normal P} e-\<succ> {Q}; G,(A::'a triple set)\<turnstile>{Q\<down>} args\<doteq>\<succ> {R::'a assn}\<rbrakk> \<Longrightarrow>  \
\         G,A\<turnstile>{Normal P} {t,ClassT C,Static}e..mn({pTs}args)-\<succ> {S}";
b y etac ax_derivs.Call 1;
b y  Safe_tac;
b y  etac conseq1 1;
b y  Force_tac 1;
b y EVERY'[rtac ax_escape, Clarsimp_tac] 1;
b y thin_tac "?P \<longrightarrow> ?Q" 1;
b y EVERY'[dtac spec, dtac spec, etac conseq12] 1;
b y force_tac (claset(), simpset() addsimps [init_lvars_def]) 1;
qed "ax_Call_Static";

Goal "\<lbrakk>the (cmethd G C (mn,pTs)) = (md,(m,pns,rT),lvars,bdy); G\<turnstile>IntVir\<rightarrow>C\<preceq>t; \
\  \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (snd s)) ;. \
\ init_lvars G C (mn,pTs) IntVir a vs)} Methd C (mn,pTs)-\<succ> {set_lvars l .; S};\
\ \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> \
\         {R a \<and>. (\<lambda>s. C = obj_class (the (heap (snd s) (the_Addr a))))}; \
\      G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk> \
\  \<Longrightarrow> G,A\<turnstile>{Normal P} {t,cT,IntVir}e..mn({pTs}args)-\<succ> {S}";
b y etac ax_derivs.Call 1;
b y  Safe_tac;
b y  etac spec 1;
b y EVERY'[rtac ax_escape, Clarsimp_tac] 1;
b y EVERY'[dtac spec, dtac spec, dtac spec, etac conseq12] 1;
b y Force_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";

Goal "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}";
b y rtac ax_derivs.Cast 1;
b y rtac (ax_Lit2 RS conseq2) 1;
b y Clarsimp_tac 1;
qed "ax_StatRef";

section "rules derived from Init and Done";

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

Goal 
"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<bullet> \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars l'}\
\ .Skip. {(set_lvars l .; P)::'a assn}";
b y rtac allI 1;
b y rtac ax_SkipI 1;
b y Clarsimp_tac 1;
qed "ax_Init_Skip_lemma";

Goal "\<lbrakk>the (class G C) = (sc,si,fs,ms,Skip); C \<noteq> Object;\
\      P\<leftarrow>\<bullet> \<Rightarrow> (supd (init_class_obj G C) .; P); \
\      G,A\<turnstile>{Normal (P \<and>. initd C)} .init sc. {(P \<and>. initd C)\<leftarrow>\<bullet>}\<rbrakk> \<Longrightarrow> \
\      G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<bullet>} .init C. {(P \<and>. initd C)::'a assn}"; 
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 Simp_tac 1;
b y eatac ax_InitS 1 1;
b y  rtac ax_Init_Skip_lemma 1;
b y etac conseq1 1;
b y Force_tac 1;
qed "ax_triv_InitS";

Goal "wf_prog G \<Longrightarrow> \
\G,(A::'a triple set)\<turnstile>{Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<bullet>) \<and>. Not \<circ> initd Object)}\
\      .init Object. {(P \<and>. initd Object)::'a assn}";
b y res_inst_tac [] ax_derivs.Init 1;
b y   EVERY'[dtac class_Object, Force_tac] 1;
b y  rtac ax_Init_Skip_lemma 2;
b y Simp_tac 1;
b y EVERY'[rtac ax_SkipI, Clarsimp_tac] 1;
qed "ax_Init_Object";

Goal "\<lbrakk>wf_prog G; \
\      (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow> \
\ G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<bullet>} .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 "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 "G,A\<turnstile>{P} t\<succ> {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> \
\Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. heap_free 2}\
\ \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}";
b y etac conseq2 1;
b y auto_tac (claset() addSEs halloc_elim_cases, simpset());
qed "ax_Alloc";

Goal "G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. ¬the_Intg i<#0 \<and> \
\ (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow> \
\ Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.\
\  heap_free 2} \<Longrightarrow> \
\G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. xupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}";
b y etac conseq2 1;
b y auto_tac (claset() addSEs halloc_elim_cases, simpset());
qed "ax_Alloc_Arr";

Goal "\<lbrakk>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)) \
\ \<and>. heap_free 2}\<rbrakk> \<Longrightarrow> \
\ G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}";
b y etac conseq2 1;
b y auto_tac (claset() addSEs sxalloc_elim_cases@halloc_elim_cases, simpset());
qed "ax_SXAlloc_catch_SXcpt";

val ax_tac = REPEAT o rtac allI THEN'
             resolve_tac(ax_Skip::ax_StatRef::ax_MethdN::ax_Alloc::ax_Alloc_Arr
                       ::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)];

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 *)