src/HOLCF/Ssum0.ML

strengthened some theorems

(*  Title:      HOLCF/Ssum0.ML
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Strict sum with typedef
*)

(* ------------------------------------------------------------------------ *)
(* A non-emptyness result for Sssum                                         *)
(* ------------------------------------------------------------------------ *)

Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
by (Blast_tac 1);
qed "SsumIl";

Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
by (Blast_tac 1);
qed "SsumIr";

Goal "inj_on Abs_Ssum Ssum";
by (rtac inj_on_inverseI 1);
by (etac Abs_Ssum_inverse 1);
qed "inj_on_Abs_Ssum";

(* ------------------------------------------------------------------------ *)
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
(* ------------------------------------------------------------------------ *)

Goalw [Sinr_Rep_def,Sinl_Rep_def]
 "Sinl_Rep(UU) = Sinr_Rep(UU)";
by (rtac ext 1);
by (rtac ext 1);
by (rtac ext 1);
by (fast_tac HOL_cs 1);
qed "strict_SinlSinr_Rep";

Goalw [Isinl_def,Isinr_def]
 "Isinl(UU) = Isinr(UU)";
by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
qed "strict_IsinlIsinr";


(* ------------------------------------------------------------------------ *)
(* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
(* ------------------------------------------------------------------------ *)

Goalw [Sinl_Rep_def,Sinr_Rep_def]
        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "noteq_SinlSinr_Rep";


Goalw [Isinl_def,Isinr_def]
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
by (rtac noteq_SinlSinr_Rep 1);
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
by (rtac SsumIl 1);
by (rtac SsumIr 1);
qed "noteq_IsinlIsinr";



(* ------------------------------------------------------------------------ *)
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
(* ------------------------------------------------------------------------ *)

Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinl_Rep1";

Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinr_Rep1";

Goalw [Sinl_Rep_def]
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinl_Rep2";

Goalw [Sinr_Rep_def]
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
by (blast_tac (claset() addSDs [fun_cong]) 1);
qed "inject_Sinr_Rep2";

Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
by (case_tac "a1=UU" 1);
by (hyp_subst_tac 1);
by (rtac (inject_Sinl_Rep1 RS sym) 1);
by (etac sym 1);
by (case_tac "a2=UU" 1);
by (hyp_subst_tac 1);
by (etac inject_Sinl_Rep1 1);
by (etac inject_Sinl_Rep2 1);
by (atac 1);
by (atac 1);
qed "inject_Sinl_Rep";

Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2";
by (case_tac "b1=UU" 1);
by (hyp_subst_tac 1);
by (rtac (inject_Sinr_Rep1 RS sym) 1);
by (etac sym 1);
by (case_tac "b2=UU" 1);
by (hyp_subst_tac 1);
by (etac inject_Sinr_Rep1 1);
by (etac inject_Sinr_Rep2 1);
by (atac 1);
by (atac 1);
qed "inject_Sinr_Rep";

Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2";
by (rtac inject_Sinl_Rep 1);
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
by (rtac SsumIl 1);
by (rtac SsumIl 1);
qed "inject_Isinl";

Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2";
by (rtac inject_Sinr_Rep 1);
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
by (rtac SsumIr 1);
by (rtac SsumIr 1);
qed "inject_Isinr";

AddSDs [inject_Isinl, inject_Isinr];

Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
by (Blast_tac 1);
qed "inject_Isinl_rev";

Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
by (Blast_tac 1);
qed "inject_Isinr_rev";

(* ------------------------------------------------------------------------ *)
(* Exhaustion of the strict sum ++                                          *)
(* choice of the bottom representation is arbitrary                         *)
(* ------------------------------------------------------------------------ *)

Goalw [Isinl_def,Isinr_def]
        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
by (etac disjE 1);
by (etac exE 1);
by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
by (etac disjI1 1);
by (rtac disjI2 1);
by (rtac disjI1 1);
by (rtac exI 1);
by (rtac conjI 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (etac arg_cong 1);
by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
by (etac arg_cong 2);
by (etac contrapos_nn 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (rtac trans 1);
by (etac arg_cong 1);
by (etac arg_cong 1);
by (etac exE 1);
by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
by (etac disjI1 1);
by (rtac disjI2 1);
by (rtac disjI2 1);
by (rtac exI 1);
by (rtac conjI 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (etac arg_cong 1);
by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
by (hyp_subst_tac 2);
by (rtac (strict_SinlSinr_Rep RS sym) 2);
by (etac contrapos_nn 1);
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
by (rtac trans 1);
by (etac arg_cong 1);
by (etac arg_cong 1);
qed "Exh_Ssum";

(* ------------------------------------------------------------------------ *)
(* elimination rules for the strict sum ++                                  *)
(* ------------------------------------------------------------------------ *)

val prems = Goal
        "[|p=Isinl(UU) ==> Q ;\
\       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
\       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q";
by (rtac (Exh_Ssum RS disjE) 1);
by (etac disjE 2);
by (eresolve_tac prems 1);
by (etac exE 1);
by (etac conjE 1);
by (eresolve_tac prems 1);
by (atac 1);
by (etac exE 1);
by (etac conjE 1);
by (eresolve_tac prems 1);
by (atac 1);
qed "IssumE";

val prems = Goal
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q";
by (rtac IssumE 1);
by (eresolve_tac prems 1);
by (eresolve_tac prems 1);
by (eresolve_tac prems 1);
qed "IssumE2";




(* ------------------------------------------------------------------------ *)
(* rewrites for Iwhen                                                       *)
(* ------------------------------------------------------------------------ *)

Goalw [Iwhen_def]
        "Iwhen f g (Isinl UU) = UU";
by (rtac some_equality 1);
by (rtac conjI 1);
by (fast_tac HOL_cs  1);
by (rtac conjI 1);
by (strip_tac 1);
by (res_inst_tac [("P","a=UU")] notE 1);
by (fast_tac HOL_cs  1);
by (rtac inject_Isinl 1);
by (rtac sym 1);
by (fast_tac HOL_cs  1);
by (strip_tac 1);
by (res_inst_tac [("P","b=UU")] notE 1);
by (fast_tac HOL_cs  1);
by (rtac inject_Isinr 1);
by (rtac sym 1);
by (rtac (strict_IsinlIsinr RS subst) 1);
by (fast_tac HOL_cs  1);
by (fast_tac HOL_cs  1);
qed "Iwhen1";


Goalw [Iwhen_def]
        "x~=UU ==> Iwhen f g (Isinl x) = f$x";
by (rtac some_equality 1);
by (fast_tac HOL_cs  2);
by (rtac conjI 1);
by (strip_tac 1);
by (res_inst_tac [("P","x=UU")] notE 1);
by (atac 1);
by (rtac inject_Isinl 1);
by (atac 1);
by (rtac conjI 1);
by (strip_tac 1);
by (rtac cfun_arg_cong 1);
by (rtac inject_Isinl 1);
by (fast_tac HOL_cs  1);
by (strip_tac 1);
by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
by (fast_tac HOL_cs  2);
by (rtac contrapos_nn 1);
by (etac noteq_IsinlIsinr 2);
by (fast_tac HOL_cs  1);
qed "Iwhen2";

Goalw [Iwhen_def]
        "y~=UU ==> Iwhen f g (Isinr y) = g$y";
by (rtac some_equality 1);
by (fast_tac HOL_cs  2);
by (rtac conjI 1);
by (strip_tac 1);
by (res_inst_tac [("P","y=UU")] notE 1);
by (atac 1);
by (rtac inject_Isinr 1);
by (rtac (strict_IsinlIsinr RS subst) 1);
by (atac 1);
by (rtac conjI 1);
by (strip_tac 1);
by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
by (fast_tac HOL_cs  2);
by (rtac contrapos_nn 1);
by (etac (sym RS noteq_IsinlIsinr) 2);
by (fast_tac HOL_cs  1);
by (strip_tac 1);
by (rtac cfun_arg_cong 1);
by (rtac inject_Isinr 1);
by (fast_tac HOL_cs  1);
qed "Iwhen3";

(* ------------------------------------------------------------------------ *)
(* instantiate the simplifier                                               *)
(* ------------------------------------------------------------------------ *)

val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps 
                [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];

Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3];