src/HOLCF/Sprod0.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4833 2e53109d4bc8
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/sprod0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Lemmas for theory sprod0.thy
     7 *)
     8 
     9 open Sprod0;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* A non-emptyness result for Sprod                                         *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 qed_goalw "SprodI" Sprod0.thy [Sprod_def]
    16         "(Spair_Rep a b):Sprod"
    17 (fn prems =>
    18         [
    19         (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
    20         ]);
    21 
    22 qed_goal "inj_on_Abs_Sprod" Sprod0.thy 
    23         "inj_on Abs_Sprod Sprod"
    24 (fn prems =>
    25         [
    26         (rtac inj_on_inverseI 1),
    27         (etac Abs_Sprod_inverse 1)
    28         ]);
    29 
    30 (* ------------------------------------------------------------------------ *)
    31 (* Strictness and definedness of Spair_Rep                                  *)
    32 (* ------------------------------------------------------------------------ *)
    33 
    34 qed_goalw "strict_Spair_Rep" Sprod0.thy [Spair_Rep_def]
    35  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
    36  (fn prems =>
    37         [
    38         (cut_facts_tac prems 1),
    39         (rtac ext 1),
    40         (rtac ext 1),
    41         (rtac iffI 1),
    42         (fast_tac HOL_cs 1),
    43         (fast_tac HOL_cs 1)
    44         ]);
    45 
    46 qed_goalw "defined_Spair_Rep_rev" Sprod0.thy [Spair_Rep_def]
    47  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
    48  (fn prems =>
    49         [
    50         (case_tac "a=UU|b=UU" 1),
    51         (atac 1),
    52         (rtac disjI1 1),
    53         (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS 
    54         conjunct1 RS sym) 1),
    55         (fast_tac HOL_cs 1),
    56         (fast_tac HOL_cs 1)
    57         ]);
    58 
    59 
    60 (* ------------------------------------------------------------------------ *)
    61 (* injectivity of Spair_Rep and Ispair                                      *)
    62 (* ------------------------------------------------------------------------ *)
    63 
    64 qed_goalw "inject_Spair_Rep" Sprod0.thy [Spair_Rep_def]
    65 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
    66  (fn prems =>
    67         [
    68         (cut_facts_tac prems 1),
    69         (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong 
    70                 RS iffD1 RS mp) 1),
    71         (fast_tac HOL_cs 1),
    72         (fast_tac HOL_cs 1)
    73         ]);
    74 
    75 
    76 qed_goalw "inject_Ispair" Sprod0.thy [Ispair_def]
    77         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
    78 (fn prems =>
    79         [
    80         (cut_facts_tac prems 1),
    81         (etac inject_Spair_Rep 1),
    82         (atac 1),
    83         (etac (inj_on_Abs_Sprod  RS inj_onD) 1),
    84         (rtac SprodI 1),
    85         (rtac SprodI 1)
    86         ]);
    87 
    88 
    89 (* ------------------------------------------------------------------------ *)
    90 (* strictness and definedness of Ispair                                     *)
    91 (* ------------------------------------------------------------------------ *)
    92 
    93 qed_goalw "strict_Ispair" Sprod0.thy [Ispair_def] 
    94  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
    95 (fn prems =>
    96         [
    97         (cut_facts_tac prems 1),
    98         (etac (strict_Spair_Rep RS arg_cong) 1)
    99         ]);
   100 
   101 qed_goalw "strict_Ispair1" Sprod0.thy [Ispair_def]
   102         "Ispair UU b  = Ispair UU UU"
   103 (fn prems =>
   104         [
   105         (rtac (strict_Spair_Rep RS arg_cong) 1),
   106         (rtac disjI1 1),
   107         (rtac refl 1)
   108         ]);
   109 
   110 qed_goalw "strict_Ispair2" Sprod0.thy [Ispair_def]
   111         "Ispair a UU = Ispair UU UU"
   112 (fn prems =>
   113         [
   114         (rtac (strict_Spair_Rep RS arg_cong) 1),
   115         (rtac disjI2 1),
   116         (rtac refl 1)
   117         ]);
   118 
   119 qed_goal "strict_Ispair_rev" Sprod0.thy 
   120         "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
   121 (fn prems =>
   122         [
   123         (cut_facts_tac prems 1),
   124         (rtac (de_Morgan_disj RS subst) 1),
   125         (etac contrapos 1),
   126         (etac strict_Ispair 1)
   127         ]);
   128 
   129 qed_goalw "defined_Ispair_rev" Sprod0.thy [Ispair_def]
   130         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
   131 (fn prems =>
   132         [
   133         (cut_facts_tac prems 1),
   134         (rtac defined_Spair_Rep_rev 1),
   135         (rtac (inj_on_Abs_Sprod  RS inj_onD) 1),
   136         (atac 1),
   137         (rtac SprodI 1),
   138         (rtac SprodI 1)
   139         ]);
   140 
   141 qed_goal "defined_Ispair" Sprod0.thy  
   142 "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)" 
   143 (fn prems =>
   144         [
   145         (cut_facts_tac prems 1),
   146         (rtac contrapos 1),
   147         (etac defined_Ispair_rev 2),
   148         (rtac (de_Morgan_disj RS iffD2) 1),
   149         (etac conjI 1),
   150         (atac 1)
   151         ]);
   152 
   153 
   154 (* ------------------------------------------------------------------------ *)
   155 (* Exhaustion of the strict product **                                      *)
   156 (* ------------------------------------------------------------------------ *)
   157 
   158 qed_goalw "Exh_Sprod" Sprod0.thy [Ispair_def]
   159         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
   160 (fn prems =>
   161         [
   162         (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1),
   163         (etac exE 1),
   164         (etac exE 1),
   165         (rtac (excluded_middle RS disjE) 1),
   166         (rtac disjI2 1),
   167         (rtac exI 1),
   168         (rtac exI 1),
   169         (rtac conjI 1),
   170         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
   171         (etac arg_cong 1),
   172         (rtac (de_Morgan_disj RS subst) 1),
   173         (atac 1),
   174         (rtac disjI1 1),
   175         (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
   176         (res_inst_tac [("f","Abs_Sprod")] arg_cong 1),
   177         (etac trans 1),
   178         (etac strict_Spair_Rep 1)
   179         ]);
   180 
   181 (* ------------------------------------------------------------------------ *)
   182 (* general elimination rule for strict product                              *)
   183 (* ------------------------------------------------------------------------ *)
   184 
   185 qed_goal "IsprodE" Sprod0.thy
   186 "[|p=Ispair UU UU ==> Q ;!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] ==> Q"
   187 (fn prems =>
   188         [
   189         (rtac (Exh_Sprod RS disjE) 1),
   190         (etac (hd prems) 1),
   191         (etac exE 1),
   192         (etac exE 1),
   193         (etac conjE 1),
   194         (etac conjE 1),
   195         (etac (hd (tl prems)) 1),
   196         (atac 1),
   197         (atac 1)
   198         ]);
   199 
   200 
   201 (* ------------------------------------------------------------------------ *)
   202 (* some results about the selectors Isfst, Issnd                            *)
   203 (* ------------------------------------------------------------------------ *)
   204 
   205 qed_goalw "strict_Isfst" Sprod0.thy [Isfst_def] 
   206         "p=Ispair UU UU ==> Isfst p = UU"
   207 (fn prems =>
   208         [
   209         (cut_facts_tac prems 1),
   210         (rtac select_equality 1),
   211         (rtac conjI 1),
   212         (fast_tac HOL_cs  1),
   213         (strip_tac 1),
   214         (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
   215         (rtac not_sym 1),
   216         (rtac defined_Ispair 1),
   217         (REPEAT (fast_tac HOL_cs  1))
   218         ]);
   219 
   220 
   221 qed_goal "strict_Isfst1" Sprod0.thy
   222         "Isfst(Ispair UU y) = UU"
   223 (fn prems =>
   224         [
   225         (stac strict_Ispair1 1),
   226         (rtac strict_Isfst 1),
   227         (rtac refl 1)
   228         ]);
   229 
   230 qed_goal "strict_Isfst2" Sprod0.thy
   231         "Isfst(Ispair x UU) = UU"
   232 (fn prems =>
   233         [
   234         (stac strict_Ispair2 1),
   235         (rtac strict_Isfst 1),
   236         (rtac refl 1)
   237         ]);
   238 
   239 
   240 qed_goalw "strict_Issnd" Sprod0.thy [Issnd_def] 
   241         "p=Ispair UU UU ==>Issnd p=UU"
   242 (fn prems =>
   243         [
   244         (cut_facts_tac prems 1),
   245         (rtac select_equality 1),
   246         (rtac conjI 1),
   247         (fast_tac HOL_cs  1),
   248         (strip_tac 1),
   249         (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
   250         (rtac not_sym 1),
   251         (rtac defined_Ispair 1),
   252         (REPEAT (fast_tac HOL_cs  1))
   253         ]);
   254 
   255 qed_goal "strict_Issnd1" Sprod0.thy
   256         "Issnd(Ispair UU y) = UU"
   257 (fn prems =>
   258         [
   259         (stac strict_Ispair1 1),
   260         (rtac strict_Issnd 1),
   261         (rtac refl 1)
   262         ]);
   263 
   264 qed_goal "strict_Issnd2" Sprod0.thy
   265         "Issnd(Ispair x UU) = UU"
   266 (fn prems =>
   267         [
   268         (stac strict_Ispair2 1),
   269         (rtac strict_Issnd 1),
   270         (rtac refl 1)
   271         ]);
   272 
   273 qed_goalw "Isfst" Sprod0.thy [Isfst_def]
   274         "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
   275 (fn prems =>
   276         [
   277         (cut_facts_tac prems 1),
   278         (rtac select_equality 1),
   279         (rtac conjI 1),
   280         (strip_tac 1),
   281         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   282         (etac defined_Ispair 1),
   283         (atac 1),
   284         (atac 1),
   285         (strip_tac 1),
   286         (rtac (inject_Ispair RS conjunct1) 1),
   287         (fast_tac HOL_cs  3),
   288         (fast_tac HOL_cs  1),
   289         (fast_tac HOL_cs  1),
   290         (fast_tac HOL_cs  1)
   291         ]);
   292 
   293 qed_goalw "Issnd" Sprod0.thy [Issnd_def]
   294         "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
   295 (fn prems =>
   296         [
   297         (cut_facts_tac prems 1),
   298         (rtac select_equality 1),
   299         (rtac conjI 1),
   300         (strip_tac 1),
   301         (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   302         (etac defined_Ispair 1),
   303         (atac 1),
   304         (atac 1),
   305         (strip_tac 1),
   306         (rtac (inject_Ispair RS conjunct2) 1),
   307         (fast_tac HOL_cs  3),
   308         (fast_tac HOL_cs  1),
   309         (fast_tac HOL_cs  1),
   310         (fast_tac HOL_cs  1)
   311         ]);
   312 
   313 qed_goal "Isfst2" Sprod0.thy "y~=UU ==>Isfst(Ispair x y)=x"
   314 (fn prems =>
   315         [
   316         (cut_facts_tac prems 1),
   317         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   318         (etac Isfst 1),
   319         (atac 1),
   320         (hyp_subst_tac 1),
   321         (rtac strict_Isfst1 1)
   322         ]);
   323 
   324 qed_goal "Issnd2" Sprod0.thy "~x=UU ==>Issnd(Ispair x y)=y"
   325 (fn prems =>
   326         [
   327         (cut_facts_tac prems 1),
   328         (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1),
   329         (etac Issnd 1),
   330         (atac 1),
   331         (hyp_subst_tac 1),
   332         (rtac strict_Issnd2 1)
   333         ]);
   334 
   335 
   336 (* ------------------------------------------------------------------------ *)
   337 (* instantiate the simplifier                                               *)
   338 (* ------------------------------------------------------------------------ *)
   339 
   340 val Sprod0_ss = 
   341         HOL_ss 
   342         addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
   343                  Isfst2,Issnd2];
   344 
   345 qed_goal "defined_IsfstIssnd" Sprod0.thy 
   346         "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
   347  (fn prems =>
   348         [
   349         (cut_facts_tac prems 1),
   350         (res_inst_tac [("p","p")] IsprodE 1),
   351         (contr_tac 1),
   352         (hyp_subst_tac 1),
   353         (rtac conjI 1),
   354         (asm_simp_tac Sprod0_ss 1),
   355         (asm_simp_tac Sprod0_ss 1)
   356         ]);
   357 
   358 
   359 (* ------------------------------------------------------------------------ *)
   360 (* Surjective pairing: equivalent to Exh_Sprod                              *)
   361 (* ------------------------------------------------------------------------ *)
   362 
   363 qed_goal "surjective_pairing_Sprod" Sprod0.thy 
   364         "z = Ispair(Isfst z)(Issnd z)"
   365 (fn prems =>
   366         [
   367         (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
   368         (asm_simp_tac Sprod0_ss 1),
   369         (etac exE 1),
   370         (etac exE 1),
   371         (asm_simp_tac Sprod0_ss 1)
   372         ]);
   373 
   374 qed_goal "Sel_injective_Sprod" thy 
   375         "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
   376 (fn prems =>
   377         [
   378         (cut_facts_tac prems 1),
   379         (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1),
   380         (rotate_tac ~1 1),
   381         (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1),
   382         (Asm_simp_tac 1)
   383         ]);