src/HOLCF/Ssum0.ML

adapted several proofs

(*  Title:      HOLCF/ssum0.ML
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen

Lemmas for theory ssum0.thy 
*)

open Ssum0;

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

qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
 (fn prems =>
        [
        (rtac CollectI 1),
        (rtac disjI1 1),
        (rtac exI 1),
        (rtac refl 1)
        ]);

qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
 (fn prems =>
        [
        (rtac CollectI 1),
        (rtac disjI2 1),
        (rtac exI 1),
        (rtac refl 1)
        ]);

qed_goal "inj_onto_Abs_Ssum" Ssum0.thy "inj_onto Abs_Ssum Ssum"
(fn prems =>
        [
        (rtac inj_onto_inverseI 1),
        (etac Abs_Ssum_inverse 1)
        ]);

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

qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
 "Sinl_Rep(UU) = Sinr_Rep(UU)"
 (fn prems =>
        [
        (rtac ext 1),
        (rtac ext 1),
        (rtac ext 1),
        (fast_tac HOL_cs 1)
        ]);

qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
 "Isinl(UU) = Isinr(UU)"
 (fn prems =>
        [
        (rtac (strict_SinlSinr_Rep RS arg_cong) 1)
        ]);


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

qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
 (fn prems =>
        [
        (rtac conjI 1),
        (case_tac "a=UU" 1),
        (atac 1),
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
        RS mp RS conjunct1 RS sym) 1),
        (fast_tac HOL_cs 1),
        (atac 1),
        (case_tac "b=UU" 1),
        (atac 1),
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
        RS mp RS conjunct1 RS sym) 1),
        (fast_tac HOL_cs 1),
        (atac 1)
        ]);


qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac noteq_SinlSinr_Rep 1),
        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
        (rtac SsumIl 1),
        (rtac SsumIr 1)
        ]);



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

qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
 "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
 (fn prems =>
        [
        (case_tac "a=UU" 1),
        (atac 1),
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
        RS iffD2 RS mp RS conjunct1 RS sym) 1),
        (fast_tac HOL_cs 1),
        (atac 1)
        ]);

qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
 "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
 (fn prems =>
        [
        (case_tac "b=UU" 1),
        (atac 1),
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
        RS iffD2 RS mp RS conjunct1 RS sym) 1),
        (fast_tac HOL_cs 1),
        (atac 1)
        ]);

qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
 (fn prems =>
        [
        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
        RS iffD1 RS mp RS conjunct1) 1),
        (fast_tac HOL_cs 1),
        (resolve_tac prems 1)
        ]);

qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
 (fn prems =>
        [
        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
        RS iffD1 RS mp RS conjunct1) 1),
        (fast_tac HOL_cs 1),
        (resolve_tac prems 1)
        ]);

qed_goal "inject_Sinl_Rep" Ssum0.thy 
        "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (case_tac "a1=UU" 1),
        (hyp_subst_tac 1),
        (rtac (inject_Sinl_Rep1 RS sym) 1),
        (etac sym 1),
        (case_tac "a2=UU" 1),
        (hyp_subst_tac 1),
        (etac inject_Sinl_Rep1 1),
        (etac inject_Sinl_Rep2 1),
        (atac 1),
        (atac 1)
        ]);

qed_goal "inject_Sinr_Rep" Ssum0.thy 
        "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (case_tac "b1=UU" 1),
        (hyp_subst_tac 1),
        (rtac (inject_Sinr_Rep1 RS sym) 1),
        (etac sym 1),
        (case_tac "b2=UU" 1),
        (hyp_subst_tac 1),
        (etac inject_Sinr_Rep1 1),
        (etac inject_Sinr_Rep2 1),
        (atac 1),
        (atac 1)
        ]);

qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
"Isinl(a1)=Isinl(a2)==> a1=a2"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac inject_Sinl_Rep 1),
        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
        (rtac SsumIl 1),
        (rtac SsumIl 1)
        ]);

qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
"Isinr(b1)=Isinr(b2) ==> b1=b2"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac inject_Sinr_Rep 1),
        (etac (inj_onto_Abs_Ssum  RS inj_ontoD) 1),
        (rtac SsumIr 1),
        (rtac SsumIr 1)
        ]);

qed_goal "inject_Isinl_rev" Ssum0.thy  
"a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac contrapos 1),
        (etac inject_Isinl 2),
        (atac 1)
        ]);

qed_goal "inject_Isinr_rev" Ssum0.thy  
"b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac contrapos 1),
        (etac inject_Isinr 2),
        (atac 1)
        ]);

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

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

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

qed_goal "IssumE" Ssum0.thy
        "[|p=Isinl(UU) ==> Q ;\
\       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
\       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
 (fn prems =>
        [
        (rtac (Exh_Ssum RS disjE) 1),
        (etac disjE 2),
        (eresolve_tac prems 1),
        (etac exE 1),
        (etac conjE 1),
        (eresolve_tac prems 1),
        (atac 1),
        (etac exE 1),
        (etac conjE 1),
        (eresolve_tac prems 1),
        (atac 1)
        ]);

qed_goal "IssumE2" Ssum0.thy 
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
 (fn prems =>
        [
        (rtac IssumE 1),
        (eresolve_tac prems 1), 
        (eresolve_tac prems 1), 
        (eresolve_tac prems 1)
        ]);




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

qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
        "Iwhen f g (Isinl UU) = UU"
 (fn prems =>
        [
        (rtac  select_equality 1),
        (rtac conjI 1),
        (fast_tac HOL_cs  1),
        (rtac conjI 1),
        (strip_tac 1),
        (res_inst_tac [("P","a=UU")] notE 1),
        (fast_tac HOL_cs  1),
        (rtac inject_Isinl 1),
        (rtac sym 1),
        (fast_tac HOL_cs  1),
        (strip_tac 1),
        (res_inst_tac [("P","b=UU")] notE 1),
        (fast_tac HOL_cs  1),
        (rtac inject_Isinr 1),
        (rtac sym 1),
        (rtac (strict_IsinlIsinr RS subst) 1),
        (fast_tac HOL_cs  1),
        (fast_tac HOL_cs  1)
        ]);


qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
        "x~=UU ==> Iwhen f g (Isinl x) = f`x"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac  select_equality 1),
        (fast_tac HOL_cs  2),
        (rtac conjI 1),
        (strip_tac 1),
        (res_inst_tac [("P","x=UU")] notE 1),
        (atac 1),
        (rtac inject_Isinl 1),
        (atac 1),
        (rtac conjI 1),
        (strip_tac 1),
        (rtac cfun_arg_cong 1),
        (rtac inject_Isinl 1),
        (fast_tac HOL_cs  1),
        (strip_tac 1),
        (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
        (fast_tac HOL_cs  2),
        (rtac contrapos 1),
        (etac noteq_IsinlIsinr 2),
        (fast_tac HOL_cs  1)
        ]);

qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
        "y~=UU ==> Iwhen f g (Isinr y) = g`y"
 (fn prems =>
        [
        (cut_facts_tac prems 1),
        (rtac  select_equality 1),
        (fast_tac HOL_cs  2),
        (rtac conjI 1),
        (strip_tac 1),
        (res_inst_tac [("P","y=UU")] notE 1),
        (atac 1),
        (rtac inject_Isinr 1),
        (rtac (strict_IsinlIsinr RS subst) 1),
        (atac 1),
        (rtac conjI 1),
        (strip_tac 1),
        (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
        (fast_tac HOL_cs  2),
        (rtac contrapos 1),
        (etac (sym RS noteq_IsinlIsinr) 2),
        (fast_tac HOL_cs  1),
        (strip_tac 1),
        (rtac cfun_arg_cong 1),
        (rtac inject_Isinr 1),
        (fast_tac HOL_cs  1)
        ]);

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

val Ssum0_ss = (simpset_of "Cfun3") addsimps 
                [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];