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