src/HOLCF/Ssum0.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4833 2e53109d4bc8
child 8161 bde1391fd0a5
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/ssum0.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory ssum0.thy 
     7 *)
     8 
     9 open Ssum0;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* A non-emptyness result for Sssum                                         *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
    16  (fn prems =>
    17         [
    18         (rtac CollectI 1),
    19         (rtac disjI1 1),
    20         (rtac exI 1),
    21         (rtac refl 1)
    22         ]);
    23 
    24 qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
    25  (fn prems =>
    26         [
    27         (rtac CollectI 1),
    28         (rtac disjI2 1),
    29         (rtac exI 1),
    30         (rtac refl 1)
    31         ]);
    32 
    33 qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
    34 (fn prems =>
    35         [
    36         (rtac inj_on_inverseI 1),
    37         (etac Abs_Ssum_inverse 1)
    38         ]);
    39 
    40 (* ------------------------------------------------------------------------ *)
    41 (* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
    42 (* ------------------------------------------------------------------------ *)
    43 
    44 qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
    45  "Sinl_Rep(UU) = Sinr_Rep(UU)"
    46  (fn prems =>
    47         [
    48         (rtac ext 1),
    49         (rtac ext 1),
    50         (rtac ext 1),
    51         (fast_tac HOL_cs 1)
    52         ]);
    53 
    54 qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
    55  "Isinl(UU) = Isinr(UU)"
    56  (fn prems =>
    57         [
    58         (rtac (strict_SinlSinr_Rep RS arg_cong) 1)
    59         ]);
    60 
    61 
    62 (* ------------------------------------------------------------------------ *)
    63 (* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
    64 (* ------------------------------------------------------------------------ *)
    65 
    66 qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
    67         "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
    68  (fn prems =>
    69         [
    70         (rtac conjI 1),
    71         (case_tac "a=UU" 1),
    72         (atac 1),
    73         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
    74         RS mp RS conjunct1 RS sym) 1),
    75         (fast_tac HOL_cs 1),
    76         (atac 1),
    77         (case_tac "b=UU" 1),
    78         (atac 1),
    79         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
    80         RS mp RS conjunct1 RS sym) 1),
    81         (fast_tac HOL_cs 1),
    82         (atac 1)
    83         ]);
    84 
    85 
    86 qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
    87         "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
    88  (fn prems =>
    89         [
    90         (cut_facts_tac prems 1),
    91         (rtac noteq_SinlSinr_Rep 1),
    92         (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
    93         (rtac SsumIl 1),
    94         (rtac SsumIr 1)
    95         ]);
    96 
    97 
    98 
    99 (* ------------------------------------------------------------------------ *)
   100 (* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
   101 (* ------------------------------------------------------------------------ *)
   102 
   103 qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
   104  "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
   105  (fn prems =>
   106         [
   107         (case_tac "a=UU" 1),
   108         (atac 1),
   109         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
   110         RS iffD2 RS mp RS conjunct1 RS sym) 1),
   111         (fast_tac HOL_cs 1),
   112         (atac 1)
   113         ]);
   114 
   115 qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
   116  "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
   117  (fn prems =>
   118         [
   119         (case_tac "b=UU" 1),
   120         (atac 1),
   121         (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
   122         RS iffD2 RS mp RS conjunct1 RS sym) 1),
   123         (fast_tac HOL_cs 1),
   124         (atac 1)
   125         ]);
   126 
   127 qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
   128 "[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
   129  (fn prems =>
   130         [
   131         (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
   132         RS iffD1 RS mp RS conjunct1) 1),
   133         (fast_tac HOL_cs 1),
   134         (resolve_tac prems 1)
   135         ]);
   136 
   137 qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
   138 "[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
   139  (fn prems =>
   140         [
   141         (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
   142         RS iffD1 RS mp RS conjunct1) 1),
   143         (fast_tac HOL_cs 1),
   144         (resolve_tac prems 1)
   145         ]);
   146 
   147 qed_goal "inject_Sinl_Rep" Ssum0.thy 
   148         "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
   149  (fn prems =>
   150         [
   151         (cut_facts_tac prems 1),
   152         (case_tac "a1=UU" 1),
   153         (hyp_subst_tac 1),
   154         (rtac (inject_Sinl_Rep1 RS sym) 1),
   155         (etac sym 1),
   156         (case_tac "a2=UU" 1),
   157         (hyp_subst_tac 1),
   158         (etac inject_Sinl_Rep1 1),
   159         (etac inject_Sinl_Rep2 1),
   160         (atac 1),
   161         (atac 1)
   162         ]);
   163 
   164 qed_goal "inject_Sinr_Rep" Ssum0.thy 
   165         "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
   166  (fn prems =>
   167         [
   168         (cut_facts_tac prems 1),
   169         (case_tac "b1=UU" 1),
   170         (hyp_subst_tac 1),
   171         (rtac (inject_Sinr_Rep1 RS sym) 1),
   172         (etac sym 1),
   173         (case_tac "b2=UU" 1),
   174         (hyp_subst_tac 1),
   175         (etac inject_Sinr_Rep1 1),
   176         (etac inject_Sinr_Rep2 1),
   177         (atac 1),
   178         (atac 1)
   179         ]);
   180 
   181 qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
   182 "Isinl(a1)=Isinl(a2)==> a1=a2"
   183  (fn prems =>
   184         [
   185         (cut_facts_tac prems 1),
   186         (rtac inject_Sinl_Rep 1),
   187         (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
   188         (rtac SsumIl 1),
   189         (rtac SsumIl 1)
   190         ]);
   191 
   192 qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
   193 "Isinr(b1)=Isinr(b2) ==> b1=b2"
   194  (fn prems =>
   195         [
   196         (cut_facts_tac prems 1),
   197         (rtac inject_Sinr_Rep 1),
   198         (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
   199         (rtac SsumIr 1),
   200         (rtac SsumIr 1)
   201         ]);
   202 
   203 qed_goal "inject_Isinl_rev" Ssum0.thy  
   204 "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
   205  (fn prems =>
   206         [
   207         (cut_facts_tac prems 1),
   208         (rtac contrapos 1),
   209         (etac inject_Isinl 2),
   210         (atac 1)
   211         ]);
   212 
   213 qed_goal "inject_Isinr_rev" Ssum0.thy  
   214 "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
   215  (fn prems =>
   216         [
   217         (cut_facts_tac prems 1),
   218         (rtac contrapos 1),
   219         (etac inject_Isinr 2),
   220         (atac 1)
   221         ]);
   222 
   223 (* ------------------------------------------------------------------------ *)
   224 (* Exhaustion of the strict sum ++                                          *)
   225 (* choice of the bottom representation is arbitrary                         *)
   226 (* ------------------------------------------------------------------------ *)
   227 
   228 qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def]
   229         "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
   230  (fn prems =>
   231         [
   232         (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
   233         (etac disjE 1),
   234         (etac exE 1),
   235         (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
   236         (etac disjI1 1),
   237         (rtac disjI2 1),
   238         (rtac disjI1 1),
   239         (rtac exI 1),
   240         (rtac conjI 1),
   241         (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   242         (etac arg_cong 1),
   243         (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1),
   244         (etac arg_cong 2),
   245         (etac contrapos 1),
   246         (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   247         (rtac trans 1),
   248         (etac arg_cong 1),
   249         (etac arg_cong 1),
   250         (etac exE 1),
   251         (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
   252         (etac disjI1 1),
   253         (rtac disjI2 1),
   254         (rtac disjI2 1),
   255         (rtac exI 1),
   256         (rtac conjI 1),
   257         (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   258         (etac arg_cong 1),
   259         (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1),
   260         (hyp_subst_tac 2),
   261         (rtac (strict_SinlSinr_Rep RS sym) 2),
   262         (etac contrapos 1),
   263         (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
   264         (rtac trans 1),
   265         (etac arg_cong 1),
   266         (etac arg_cong 1)
   267         ]);
   268 
   269 (* ------------------------------------------------------------------------ *)
   270 (* elimination rules for the strict sum ++                                  *)
   271 (* ------------------------------------------------------------------------ *)
   272 
   273 qed_goal "IssumE" Ssum0.thy
   274         "[|p=Isinl(UU) ==> Q ;\
   275 \       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
   276 \       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
   277  (fn prems =>
   278         [
   279         (rtac (Exh_Ssum RS disjE) 1),
   280         (etac disjE 2),
   281         (eresolve_tac prems 1),
   282         (etac exE 1),
   283         (etac conjE 1),
   284         (eresolve_tac prems 1),
   285         (atac 1),
   286         (etac exE 1),
   287         (etac conjE 1),
   288         (eresolve_tac prems 1),
   289         (atac 1)
   290         ]);
   291 
   292 qed_goal "IssumE2" Ssum0.thy 
   293 "[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
   294  (fn prems =>
   295         [
   296         (rtac IssumE 1),
   297         (eresolve_tac prems 1), 
   298         (eresolve_tac prems 1), 
   299         (eresolve_tac prems 1)
   300         ]);
   301 
   302 
   303 
   304 
   305 (* ------------------------------------------------------------------------ *)
   306 (* rewrites for Iwhen                                                       *)
   307 (* ------------------------------------------------------------------------ *)
   308 
   309 qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
   310         "Iwhen f g (Isinl UU) = UU"
   311  (fn prems =>
   312         [
   313         (rtac select_equality 1),
   314         (rtac conjI 1),
   315         (fast_tac HOL_cs  1),
   316         (rtac conjI 1),
   317         (strip_tac 1),
   318         (res_inst_tac [("P","a=UU")] notE 1),
   319         (fast_tac HOL_cs  1),
   320         (rtac inject_Isinl 1),
   321         (rtac sym 1),
   322         (fast_tac HOL_cs  1),
   323         (strip_tac 1),
   324         (res_inst_tac [("P","b=UU")] notE 1),
   325         (fast_tac HOL_cs  1),
   326         (rtac inject_Isinr 1),
   327         (rtac sym 1),
   328         (rtac (strict_IsinlIsinr RS subst) 1),
   329         (fast_tac HOL_cs  1),
   330         (fast_tac HOL_cs  1)
   331         ]);
   332 
   333 
   334 qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
   335         "x~=UU ==> Iwhen f g (Isinl x) = f`x"
   336  (fn prems =>
   337         [
   338         (cut_facts_tac prems 1),
   339         (rtac select_equality 1),
   340         (fast_tac HOL_cs  2),
   341         (rtac conjI 1),
   342         (strip_tac 1),
   343         (res_inst_tac [("P","x=UU")] notE 1),
   344         (atac 1),
   345         (rtac inject_Isinl 1),
   346         (atac 1),
   347         (rtac conjI 1),
   348         (strip_tac 1),
   349         (rtac cfun_arg_cong 1),
   350         (rtac inject_Isinl 1),
   351         (fast_tac HOL_cs  1),
   352         (strip_tac 1),
   353         (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
   354         (fast_tac HOL_cs  2),
   355         (rtac contrapos 1),
   356         (etac noteq_IsinlIsinr 2),
   357         (fast_tac HOL_cs  1)
   358         ]);
   359 
   360 qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
   361         "y~=UU ==> Iwhen f g (Isinr y) = g`y"
   362  (fn prems =>
   363         [
   364         (cut_facts_tac prems 1),
   365         (rtac select_equality 1),
   366         (fast_tac HOL_cs  2),
   367         (rtac conjI 1),
   368         (strip_tac 1),
   369         (res_inst_tac [("P","y=UU")] notE 1),
   370         (atac 1),
   371         (rtac inject_Isinr 1),
   372         (rtac (strict_IsinlIsinr RS subst) 1),
   373         (atac 1),
   374         (rtac conjI 1),
   375         (strip_tac 1),
   376         (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
   377         (fast_tac HOL_cs  2),
   378         (rtac contrapos 1),
   379         (etac (sym RS noteq_IsinlIsinr) 2),
   380         (fast_tac HOL_cs  1),
   381         (strip_tac 1),
   382         (rtac cfun_arg_cong 1),
   383         (rtac inject_Isinr 1),
   384         (fast_tac HOL_cs  1)
   385         ]);
   386 
   387 (* ------------------------------------------------------------------------ *)
   388 (* instantiate the simplifier                                               *)
   389 (* ------------------------------------------------------------------------ *)
   390 
   391 val Ssum0_ss = (simpset_of Cfun3.thy) addsimps 
   392                 [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
   393