paulson@9169: (*  Title:      HOLCF/Ssum0.ML
nipkow@243:     ID:         $Id$
clasohm@1461:     Author:     Franz Regensburger
wenzelm@12030:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243: 
paulson@9169: Strict sum with typedef
nipkow@243: *)
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* A non-emptyness result for Sssum                                         *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
paulson@10230: by (Blast_tac 1);
paulson@9245: qed "SsumIl";
nipkow@243: 
paulson@9248: Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
paulson@10230: by (Blast_tac 1);
paulson@9245: qed "SsumIr";
nipkow@243: 
paulson@9169: Goal "inj_on Abs_Ssum Ssum";
paulson@9169: by (rtac inj_on_inverseI 1);
paulson@9169: by (etac Abs_Ssum_inverse 1);
paulson@9169: qed "inj_on_Abs_Ssum";
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Sinr_Rep_def,Sinl_Rep_def]
paulson@9245:  "Sinl_Rep(UU) = Sinr_Rep(UU)";
paulson@9245: by (rtac ext 1);
paulson@9245: by (rtac ext 1);
paulson@9245: by (rtac ext 1);
paulson@9245: by (fast_tac HOL_cs 1);
paulson@9245: qed "strict_SinlSinr_Rep";
nipkow@243: 
paulson@9248: Goalw [Isinl_def,Isinr_def]
paulson@9245:  "Isinl(UU) = Isinr(UU)";
paulson@9245: by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
paulson@9245: qed "strict_IsinlIsinr";
nipkow@243: 
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Sinl_Rep_def,Sinr_Rep_def]
paulson@9245:         "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
paulson@9248: by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245: qed "noteq_SinlSinr_Rep";
nipkow@243: 
nipkow@243: 
paulson@9248: Goalw [Isinl_def,Isinr_def]
paulson@9245:         "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
paulson@9245: by (rtac noteq_SinlSinr_Rep 1);
paulson@9245: by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245: by (rtac SsumIl 1);
paulson@9245: by (rtac SsumIr 1);
paulson@9245: qed "noteq_IsinlIsinr";
nipkow@243: 
nipkow@243: 
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
paulson@9248: by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245: qed "inject_Sinl_Rep1";
nipkow@243: 
paulson@9248: Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
paulson@9248: by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245: qed "inject_Sinr_Rep1";
nipkow@243: 
paulson@9248: Goalw [Sinl_Rep_def]
paulson@9245: "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
paulson@9248: by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245: qed "inject_Sinl_Rep2";
nipkow@243: 
paulson@9248: Goalw [Sinr_Rep_def]
paulson@9245: "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
paulson@9248: by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245: qed "inject_Sinr_Rep2";
nipkow@243: 
paulson@9169: Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
paulson@9169: by (case_tac "a1=UU" 1);
paulson@9169: by (hyp_subst_tac 1);
paulson@9169: by (rtac (inject_Sinl_Rep1 RS sym) 1);
paulson@9169: by (etac sym 1);
paulson@9169: by (case_tac "a2=UU" 1);
paulson@9169: by (hyp_subst_tac 1);
paulson@9169: by (etac inject_Sinl_Rep1 1);
paulson@9169: by (etac inject_Sinl_Rep2 1);
paulson@9169: by (atac 1);
paulson@9169: by (atac 1);
paulson@9169: qed "inject_Sinl_Rep";
nipkow@243: 
paulson@9169: Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2";
paulson@9169: by (case_tac "b1=UU" 1);
paulson@9169: by (hyp_subst_tac 1);
paulson@9169: by (rtac (inject_Sinr_Rep1 RS sym) 1);
paulson@9169: by (etac sym 1);
paulson@9169: by (case_tac "b2=UU" 1);
paulson@9169: by (hyp_subst_tac 1);
paulson@9169: by (etac inject_Sinr_Rep1 1);
paulson@9169: by (etac inject_Sinr_Rep2 1);
paulson@9169: by (atac 1);
paulson@9169: by (atac 1);
paulson@9169: qed "inject_Sinr_Rep";
nipkow@243: 
paulson@9248: Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2";
paulson@9245: by (rtac inject_Sinl_Rep 1);
paulson@9245: by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245: by (rtac SsumIl 1);
paulson@9245: by (rtac SsumIl 1);
paulson@9245: qed "inject_Isinl";
nipkow@243: 
paulson@9248: Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2";
paulson@9245: by (rtac inject_Sinr_Rep 1);
paulson@9245: by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245: by (rtac SsumIr 1);
paulson@9245: by (rtac SsumIr 1);
paulson@9245: qed "inject_Isinr";
nipkow@243: 
paulson@10230: AddSDs [inject_Isinl, inject_Isinr];
paulson@10230: 
paulson@9169: Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
paulson@10230: by (Blast_tac 1);
paulson@9169: qed "inject_Isinl_rev";
nipkow@243: 
paulson@9169: Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
paulson@10230: by (Blast_tac 1);
paulson@9169: qed "inject_Isinr_rev";
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* Exhaustion of the strict sum ++                                          *)
nipkow@243: (* choice of the bottom representation is arbitrary                         *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Isinl_def,Isinr_def]
paulson@9245:         "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
paulson@9245: by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
paulson@9245: by (etac disjE 1);
paulson@9245: by (etac exE 1);
paulson@9245: by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
paulson@9245: by (etac disjI1 1);
paulson@9245: by (rtac disjI2 1);
paulson@9245: by (rtac disjI1 1);
paulson@9245: by (rtac exI 1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245: by (etac arg_cong 1);
paulson@10230: by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
paulson@9245: by (etac arg_cong 2);
paulson@10230: by (etac contrapos_nn 1);
paulson@9245: by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245: by (rtac trans 1);
paulson@9245: by (etac arg_cong 1);
paulson@9245: by (etac arg_cong 1);
paulson@9245: by (etac exE 1);
paulson@9245: by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
paulson@9245: by (etac disjI1 1);
paulson@9245: by (rtac disjI2 1);
paulson@9245: by (rtac disjI2 1);
paulson@9245: by (rtac exI 1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245: by (etac arg_cong 1);
paulson@10230: by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
paulson@9245: by (hyp_subst_tac 2);
paulson@9245: by (rtac (strict_SinlSinr_Rep RS sym) 2);
paulson@10230: by (etac contrapos_nn 1);
paulson@9245: by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245: by (rtac trans 1);
paulson@9245: by (etac arg_cong 1);
paulson@9245: by (etac arg_cong 1);
paulson@9245: qed "Exh_Ssum";
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* elimination rules for the strict sum ++                                  *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9169: val prems = Goal
clasohm@1461:         "[|p=Isinl(UU) ==> Q ;\
clasohm@1461: \       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
paulson@9169: \       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q";
paulson@9169: by (rtac (Exh_Ssum RS disjE) 1);
paulson@9169: by (etac disjE 2);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: by (etac exE 1);
paulson@9169: by (etac conjE 1);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: by (atac 1);
paulson@9169: by (etac exE 1);
paulson@9169: by (etac conjE 1);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: by (atac 1);
paulson@9169: qed "IssumE";
nipkow@243: 
paulson@9169: val prems = Goal
paulson@9169: "[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q";
paulson@9169: by (rtac IssumE 1);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: by (eresolve_tac prems 1);
paulson@9169: qed "IssumE2";
nipkow@243: 
nipkow@243: 
nipkow@243: 
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* rewrites for Iwhen                                                       *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
paulson@9248: Goalw [Iwhen_def]
paulson@9245:         "Iwhen f g (Isinl UU) = UU";
paulson@9969: by (rtac some_equality 1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","a=UU")] notE 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (rtac inject_Isinl 1);
paulson@9245: by (rtac sym 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","b=UU")] notE 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (rtac inject_Isinr 1);
paulson@9245: by (rtac sym 1);
paulson@9245: by (rtac (strict_IsinlIsinr RS subst) 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: qed "Iwhen1";
nipkow@243: 
nipkow@243: 
paulson@9248: Goalw [Iwhen_def]
nipkow@10834:         "x~=UU ==> Iwhen f g (Isinl x) = f$x";
paulson@9969: by (rtac some_equality 1);
paulson@9245: by (fast_tac HOL_cs  2);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","x=UU")] notE 1);
paulson@9245: by (atac 1);
paulson@9245: by (rtac inject_Isinl 1);
paulson@9245: by (atac 1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (rtac cfun_arg_cong 1);
paulson@9245: by (rtac inject_Isinl 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
paulson@9245: by (fast_tac HOL_cs  2);
paulson@10230: by (rtac contrapos_nn 1);
paulson@9245: by (etac noteq_IsinlIsinr 2);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: qed "Iwhen2";
nipkow@243: 
paulson@9248: Goalw [Iwhen_def]
nipkow@10834:         "y~=UU ==> Iwhen f g (Isinr y) = g$y";
paulson@9969: by (rtac some_equality 1);
paulson@9245: by (fast_tac HOL_cs  2);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","y=UU")] notE 1);
paulson@9245: by (atac 1);
paulson@9245: by (rtac inject_Isinr 1);
paulson@9245: by (rtac (strict_IsinlIsinr RS subst) 1);
paulson@9245: by (atac 1);
paulson@9245: by (rtac conjI 1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
paulson@9245: by (fast_tac HOL_cs  2);
paulson@10230: by (rtac contrapos_nn 1);
paulson@9245: by (etac (sym RS noteq_IsinlIsinr) 2);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: by (strip_tac 1);
paulson@9245: by (rtac cfun_arg_cong 1);
paulson@9245: by (rtac inject_Isinr 1);
paulson@9245: by (fast_tac HOL_cs  1);
paulson@9245: qed "Iwhen3";
nipkow@243: 
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: (* instantiate the simplifier                                               *)
nipkow@243: (* ------------------------------------------------------------------------ *)
nipkow@243: 
oheimb@8161: val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps 
regensbu@1277:                 [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
regensbu@1277: 
paulson@9248: Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3];