src/HOLCF/sprod3.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/sprod3.thy
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for Sprod3.thy 
     7 *)
     8 
     9 open Sprod3;
    10 
    11 (* ------------------------------------------------------------------------ *)
    12 (* continuity of Ispair, Isfst, Issnd                                       *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val sprod3_lemma1 = prove_goal Sprod3.thy 
    16 "[| is_chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
    17 \ Ispair(lub(range(Y)),x) =\
    18 \ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
    19 \        lub(range(%i. Issnd(Ispair(Y(i),x)))))"
    20  (fn prems =>
    21 	[
    22 	(cut_facts_tac prems 1),
    23 	(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
    24 	(rtac lub_equal 1),
    25 	(atac 1),
    26 	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
    27 	(rtac ch2ch_fun 1),
    28 	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
    29 	(atac 1),
    30 	(rtac allI 1),
    31 	(asm_simp_tac Sprod_ss 1),
    32 	(rtac sym 1),
    33 	(rtac lub_chain_maxelem 1),
    34 	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
    35 	(rtac ch2ch_fun 1),
    36 	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
    37 	(atac 1),
    38 	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
    39 	(rtac (notall2ex RS iffD1) 1),
    40 	(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
    41 	(atac 1),
    42 	(rtac chain_UU_I_inverse 1),
    43 	(atac 1),
    44 	(rtac exI 1),
    45 	(etac Issnd2 1),
    46 	(rtac allI 1),
    47 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
    48 	(asm_simp_tac Sprod_ss  1),
    49 	(rtac refl_less 1),
    50 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
    51 	(etac sym 1),
    52 	(asm_simp_tac Sprod_ss  1),
    53 	(rtac minimal 1)
    54 	]);
    55 
    56 
    57 val sprod3_lemma2 = prove_goal Sprod3.thy 
    58 "[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
    59 \   Ispair(lub(range(Y)),x) =\
    60 \   Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
    61 \          lub(range(%i. Issnd(Ispair(Y(i),x)))))"
    62  (fn prems =>
    63 	[
    64 	(cut_facts_tac prems 1),
    65 	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
    66 	(atac 1),
    67 	(rtac trans 1),
    68 	(rtac strict_Ispair1 1),
    69 	(rtac (strict_Ispair RS sym) 1),
    70 	(rtac disjI1 1),
    71 	(rtac chain_UU_I_inverse 1),
    72 	(rtac allI 1),
    73 	(asm_simp_tac Sprod_ss  1),
    74 	(etac (chain_UU_I RS spec) 1),
    75 	(atac 1)
    76 	]);
    77 
    78 
    79 val sprod3_lemma3 = prove_goal Sprod3.thy 
    80 "[| is_chain(Y); x = UU |] ==>\
    81 \          Ispair(lub(range(Y)),x) =\
    82 \          Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
    83 \                  lub(range(%i. Issnd(Ispair(Y(i),x)))))"
    84  (fn prems =>
    85 	[
    86 	(cut_facts_tac prems 1),
    87 	(res_inst_tac [("s","UU"),("t","x")] ssubst 1),
    88 	(atac 1),
    89 	(rtac trans 1),
    90 	(rtac strict_Ispair2 1),
    91 	(rtac (strict_Ispair RS sym) 1),
    92 	(rtac disjI1 1),
    93 	(rtac chain_UU_I_inverse 1),
    94 	(rtac allI 1),
    95 	(simp_tac Sprod_ss  1)
    96 	]);
    97 
    98 
    99 val contlub_Ispair1 = prove_goal Sprod3.thy "contlub(Ispair)"
   100 (fn prems =>
   101 	[
   102 	(rtac contlubI 1),
   103 	(strip_tac 1),
   104 	(rtac (expand_fun_eq RS iffD2) 1),
   105 	(strip_tac 1),
   106 	(rtac (lub_fun RS thelubI RS ssubst) 1),
   107 	(etac (monofun_Ispair1 RS ch2ch_monofun) 1),
   108 	(rtac trans 1),
   109 	(rtac (thelub_sprod RS sym) 2),
   110 	(rtac ch2ch_fun 2),
   111 	(etac (monofun_Ispair1 RS ch2ch_monofun) 2),
   112 	(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   113 	(res_inst_tac 
   114 		[("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1),
   115 	(etac sprod3_lemma1 1),
   116 	(atac 1),
   117 	(atac 1),
   118 	(etac sprod3_lemma2 1),
   119 	(atac 1),
   120 	(atac 1),
   121 	(etac sprod3_lemma3 1),
   122 	(atac 1)
   123 	]);
   124 
   125 val sprod3_lemma4 = prove_goal Sprod3.thy 
   126 "[| is_chain(Y); ~ x = UU; ~ lub(range(Y)) = UU |] ==>\
   127 \         Ispair(x,lub(range(Y))) =\
   128 \         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
   129 \                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
   130 (fn prems =>
   131 	[
   132 	(cut_facts_tac prems 1),
   133 	(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
   134 	(rtac sym 1),
   135 	(rtac lub_chain_maxelem 1),
   136 	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
   137 	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
   138 	(atac 1),
   139 	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
   140 	(rtac (notall2ex RS iffD1) 1),
   141 	(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
   142 	(atac 1),
   143 	(rtac chain_UU_I_inverse 1),
   144 	(atac 1),
   145 	(rtac exI 1),
   146 	(etac Isfst2 1),
   147 	(rtac allI 1),
   148 	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
   149 	(asm_simp_tac Sprod_ss 1),
   150 	(rtac refl_less 1),
   151 	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
   152 	(etac sym 1),
   153 	(asm_simp_tac Sprod_ss  1),
   154 	(rtac minimal 1),
   155 	(rtac lub_equal 1),
   156 	(atac 1),
   157 	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
   158 	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
   159 	(atac 1),
   160 	(rtac allI 1),
   161 	(asm_simp_tac Sprod_ss 1)
   162 	]);
   163 
   164 val sprod3_lemma5 = prove_goal Sprod3.thy 
   165 "[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
   166 \         Ispair(x,lub(range(Y))) =\
   167 \         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
   168 \                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
   169  (fn prems =>
   170 	[
   171 	(cut_facts_tac prems 1),
   172 	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
   173 	(atac 1),
   174 	(rtac trans 1),
   175 	(rtac strict_Ispair2 1),
   176 	(rtac (strict_Ispair RS sym) 1),
   177 	(rtac disjI2 1),
   178 	(rtac chain_UU_I_inverse 1),
   179 	(rtac allI 1),
   180 	(asm_simp_tac Sprod_ss  1),
   181 	(etac (chain_UU_I RS spec) 1),
   182 	(atac 1)
   183 	]);
   184 
   185 val sprod3_lemma6 = prove_goal Sprod3.thy 
   186 "[| is_chain(Y); x = UU |] ==>\
   187 \         Ispair(x,lub(range(Y))) =\
   188 \         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
   189 \                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
   190 (fn prems =>
   191 	[
   192 	(cut_facts_tac prems 1),
   193 	(res_inst_tac [("s","UU"),("t","x")] ssubst 1),
   194 	(atac 1),
   195 	(rtac trans 1),
   196 	(rtac strict_Ispair1 1),
   197 	(rtac (strict_Ispair RS sym) 1),
   198 	(rtac disjI1 1),
   199 	(rtac chain_UU_I_inverse 1),
   200 	(rtac allI 1),
   201 	(simp_tac Sprod_ss  1)
   202 	]);
   203 
   204 val contlub_Ispair2 = prove_goal Sprod3.thy "contlub(Ispair(x))"
   205 (fn prems =>
   206 	[
   207 	(rtac contlubI 1),
   208 	(strip_tac 1),
   209 	(rtac trans 1),
   210 	(rtac (thelub_sprod RS sym) 2),
   211 	(etac (monofun_Ispair2 RS ch2ch_monofun) 2),
   212 	(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   213 	(res_inst_tac [("Q","lub(range(Y))=UU")] 
   214 		(excluded_middle RS disjE) 1),
   215 	(etac sprod3_lemma4 1),
   216 	(atac 1),
   217 	(atac 1),
   218 	(etac sprod3_lemma5 1),
   219 	(atac 1),
   220 	(atac 1),
   221 	(etac sprod3_lemma6 1),
   222 	(atac 1)
   223 	]);
   224 
   225 
   226 val contX_Ispair1 = prove_goal Sprod3.thy "contX(Ispair)"
   227 (fn prems =>
   228 	[
   229 	(rtac monocontlub2contX 1),
   230 	(rtac monofun_Ispair1 1),
   231 	(rtac contlub_Ispair1 1)
   232 	]);
   233 
   234 
   235 val contX_Ispair2 = prove_goal Sprod3.thy "contX(Ispair(x))"
   236 (fn prems =>
   237 	[
   238 	(rtac monocontlub2contX 1),
   239 	(rtac monofun_Ispair2 1),
   240 	(rtac contlub_Ispair2 1)
   241 	]);
   242 
   243 val contlub_Isfst = prove_goal Sprod3.thy "contlub(Isfst)"
   244  (fn prems =>
   245 	[
   246 	(rtac contlubI 1),
   247 	(strip_tac 1),
   248 	(rtac (lub_sprod RS thelubI RS ssubst) 1),
   249 	(atac 1),
   250 	(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]	
   251 		(excluded_middle RS disjE) 1),
   252 	(asm_simp_tac Sprod_ss  1),
   253 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
   254 		ssubst 1),
   255 	(atac 1),
   256 	(rtac trans 1),
   257 	(asm_simp_tac Sprod_ss  1),
   258 	(rtac sym 1),
   259 	(rtac chain_UU_I_inverse 1),
   260 	(rtac allI 1),
   261 	(rtac strict_Isfst 1),
   262 	(rtac swap 1),
   263 	(etac (defined_IsfstIssnd RS conjunct2) 2),
   264 	(rtac notnotI 1),
   265 	(rtac (chain_UU_I RS spec) 1),
   266 	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
   267 	(atac 1),
   268 	(atac 1)
   269 	]);
   270 
   271 
   272 val contlub_Issnd = prove_goal Sprod3.thy "contlub(Issnd)"
   273 (fn prems =>
   274 	[
   275 	(rtac contlubI 1),
   276 	(strip_tac 1),
   277 	(rtac (lub_sprod RS thelubI RS ssubst) 1),
   278 	(atac 1),
   279 	(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
   280 	 (excluded_middle RS disjE) 1),
   281 	(asm_simp_tac Sprod_ss  1),
   282 	(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
   283 		ssubst 1),
   284 	(atac 1),
   285 	(asm_simp_tac Sprod_ss  1),
   286 	(rtac sym 1),
   287 	(rtac chain_UU_I_inverse 1),
   288 	(rtac allI 1),
   289 	(rtac strict_Issnd 1),
   290 	(rtac swap 1),
   291 	(etac (defined_IsfstIssnd RS conjunct1) 2),
   292 	(rtac notnotI 1),
   293 	(rtac (chain_UU_I RS spec) 1),
   294 	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
   295 	(atac 1),
   296 	(atac 1)
   297 	]);
   298 
   299 
   300 val contX_Isfst = prove_goal Sprod3.thy "contX(Isfst)"
   301 (fn prems =>
   302 	[
   303 	(rtac monocontlub2contX 1),
   304 	(rtac monofun_Isfst 1),
   305 	(rtac contlub_Isfst 1)
   306 	]);
   307 
   308 val contX_Issnd = prove_goal Sprod3.thy "contX(Issnd)"
   309 (fn prems =>
   310 	[
   311 	(rtac monocontlub2contX 1),
   312 	(rtac monofun_Issnd 1),
   313 	(rtac contlub_Issnd 1)
   314 	]);
   315 
   316 (* 
   317  -------------------------------------------------------------------------- 
   318  more lemmas for Sprod3.thy 
   319  
   320  -------------------------------------------------------------------------- 
   321 *)
   322 
   323 val spair_eq = prove_goal Sprod3.thy "[|x1=x2;y1=y2|] ==> x1##y1 = x2##y2"
   324  (fn prems =>
   325 	[
   326 	(cut_facts_tac prems 1),
   327 	(fast_tac HOL_cs 1)
   328 	]);
   329 
   330 (* ------------------------------------------------------------------------ *)
   331 (* convert all lemmas to the continuous versions                            *)
   332 (* ------------------------------------------------------------------------ *)
   333 
   334 val beta_cfun_sprod = prove_goalw Sprod3.thy [spair_def]
   335 	"(LAM x y.Ispair(x,y))[a][b] = Ispair(a,b)"
   336  (fn prems =>
   337 	[
   338 	(rtac (beta_cfun RS ssubst) 1),
   339 	(contX_tac 1),
   340 	(rtac contX_Ispair2 1),
   341 	(rtac contX2contX_CF1L 1),
   342 	(rtac contX_Ispair1 1),
   343 	(rtac (beta_cfun RS ssubst) 1),
   344 	(rtac contX_Ispair2 1),
   345 	(rtac refl 1)
   346 	]);
   347 
   348 val inject_spair = prove_goalw Sprod3.thy [spair_def]
   349 	"[|~aa=UU ; ~ba=UU ; (a##b)=(aa##ba) |] ==> a=aa & b=ba"
   350  (fn prems =>
   351 	[
   352 	(cut_facts_tac prems 1),
   353 	(etac inject_Ispair 1),
   354 	(atac 1),
   355 	(etac box_equals 1),
   356 	(rtac beta_cfun_sprod 1),
   357 	(rtac beta_cfun_sprod 1)
   358 	]);
   359 
   360 val inst_sprod_pcpo2 = prove_goalw Sprod3.thy [spair_def] "UU = (UU##UU)"
   361  (fn prems =>
   362 	[
   363 	(rtac sym 1),
   364 	(rtac trans 1),
   365 	(rtac beta_cfun_sprod 1),
   366 	(rtac sym 1),
   367 	(rtac inst_sprod_pcpo 1)
   368 	]);
   369 
   370 val strict_spair = prove_goalw Sprod3.thy [spair_def] 
   371 	"(a=UU | b=UU) ==> (a##b)=UU"
   372  (fn prems =>
   373 	[
   374 	(cut_facts_tac prems 1),
   375 	(rtac trans 1),
   376 	(rtac beta_cfun_sprod 1),
   377 	(rtac trans 1),
   378 	(rtac (inst_sprod_pcpo RS sym) 2),
   379 	(etac strict_Ispair 1)
   380 	]);
   381 
   382 val strict_spair1 = prove_goalw Sprod3.thy [spair_def] "(UU##b) = UU"
   383  (fn prems =>
   384 	[
   385 	(rtac (beta_cfun_sprod RS ssubst) 1),
   386 	(rtac trans 1),
   387 	(rtac (inst_sprod_pcpo RS sym) 2),
   388 	(rtac strict_Ispair1 1)
   389 	]);
   390 
   391 val strict_spair2 = prove_goalw Sprod3.thy [spair_def] "(a##UU) = UU"
   392  (fn prems =>
   393 	[
   394 	(rtac (beta_cfun_sprod RS ssubst) 1),
   395 	(rtac trans 1),
   396 	(rtac (inst_sprod_pcpo RS sym) 2),
   397 	(rtac strict_Ispair2 1)
   398 	]);
   399 
   400 val strict_spair_rev = prove_goalw Sprod3.thy [spair_def]
   401 	"~(x##y)=UU ==> ~x=UU & ~y=UU"
   402  (fn prems =>
   403 	[
   404 	(cut_facts_tac prems 1),
   405 	(rtac strict_Ispair_rev 1),
   406 	(rtac (beta_cfun_sprod RS subst) 1),
   407 	(rtac (inst_sprod_pcpo RS subst) 1),
   408 	(atac 1)
   409 	]);
   410 
   411 val defined_spair_rev = prove_goalw Sprod3.thy [spair_def]
   412  "(a##b) = UU ==> (a = UU | b = UU)"
   413  (fn prems =>
   414 	[
   415 	(cut_facts_tac prems 1),
   416 	(rtac defined_Ispair_rev 1),
   417 	(rtac (beta_cfun_sprod RS subst) 1),
   418 	(rtac (inst_sprod_pcpo RS subst) 1),
   419 	(atac 1)
   420 	]);
   421 
   422 val defined_spair = prove_goalw Sprod3.thy [spair_def]
   423 	"[|~a=UU; ~b=UU|] ==> ~(a##b) = UU"
   424  (fn prems =>
   425 	[
   426 	(cut_facts_tac prems 1),
   427 	(rtac (beta_cfun_sprod RS ssubst) 1),
   428 	(rtac (inst_sprod_pcpo RS ssubst) 1),
   429 	(etac defined_Ispair 1),
   430 	(atac 1)
   431 	]);
   432 
   433 val Exh_Sprod2 = prove_goalw Sprod3.thy [spair_def]
   434 	"z=UU | (? a b. z=(a##b) & ~a=UU & ~b=UU)"
   435  (fn prems =>
   436 	[
   437 	(rtac (Exh_Sprod RS disjE) 1),
   438 	(rtac disjI1 1),
   439 	(rtac (inst_sprod_pcpo RS ssubst) 1),
   440 	(atac 1),
   441 	(rtac disjI2 1),
   442 	(etac exE 1),
   443 	(etac exE 1),
   444 	(rtac exI 1),
   445 	(rtac exI 1),
   446 	(rtac conjI 1),
   447 	(rtac (beta_cfun_sprod RS ssubst) 1),
   448 	(fast_tac HOL_cs 1),
   449 	(fast_tac HOL_cs 1)
   450 	]);
   451 
   452 
   453 val sprodE =  prove_goalw Sprod3.thy [spair_def]
   454 "[|p=UU ==> Q;!!x y. [|p=(x##y);~x=UU ; ~y=UU|] ==> Q|] ==> Q"
   455 (fn prems =>
   456 	[
   457 	(rtac IsprodE 1),
   458 	(resolve_tac prems 1),
   459 	(rtac (inst_sprod_pcpo RS ssubst) 1),
   460 	(atac 1),
   461 	(resolve_tac prems 1),
   462 	(atac 2),
   463 	(atac 2),
   464 	(rtac (beta_cfun_sprod RS ssubst) 1),
   465 	(atac 1)
   466 	]);
   467 
   468 
   469 val strict_sfst = prove_goalw Sprod3.thy [sfst_def] 
   470 	"p=UU==>sfst[p]=UU"
   471  (fn prems =>
   472 	[
   473 	(cut_facts_tac prems 1),
   474 	(rtac (beta_cfun RS ssubst) 1),
   475 	(rtac contX_Isfst 1),
   476 	(rtac strict_Isfst 1),
   477 	(rtac (inst_sprod_pcpo RS subst) 1),
   478 	(atac 1)
   479 	]);
   480 
   481 val strict_sfst1 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
   482 	"sfst[UU##y] = UU"
   483  (fn prems =>
   484 	[
   485 	(rtac (beta_cfun_sprod RS ssubst) 1),
   486 	(rtac (beta_cfun RS ssubst) 1),
   487 	(rtac contX_Isfst 1),
   488 	(rtac strict_Isfst1 1)
   489 	]);
   490  
   491 val strict_sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
   492 	"sfst[x##UU] = UU"
   493  (fn prems =>
   494 	[
   495 	(rtac (beta_cfun_sprod RS ssubst) 1),
   496 	(rtac (beta_cfun RS ssubst) 1),
   497 	(rtac contX_Isfst 1),
   498 	(rtac strict_Isfst2 1)
   499 	]);
   500 
   501 val strict_ssnd = prove_goalw Sprod3.thy [ssnd_def] 
   502 	"p=UU==>ssnd[p]=UU"
   503  (fn prems =>
   504 	[
   505 	(cut_facts_tac prems 1),
   506 	(rtac (beta_cfun RS ssubst) 1),
   507 	(rtac contX_Issnd 1),
   508 	(rtac strict_Issnd 1),
   509 	(rtac (inst_sprod_pcpo RS subst) 1),
   510 	(atac 1)
   511 	]);
   512 
   513 val strict_ssnd1 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
   514 	"ssnd[UU##y] = UU"
   515  (fn prems =>
   516 	[
   517 	(rtac (beta_cfun_sprod RS ssubst) 1),
   518 	(rtac (beta_cfun RS ssubst) 1),
   519 	(rtac contX_Issnd 1),
   520 	(rtac strict_Issnd1 1)
   521 	]);
   522 
   523 val strict_ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
   524 	"ssnd[x##UU] = UU"
   525  (fn prems =>
   526 	[
   527 	(rtac (beta_cfun_sprod RS ssubst) 1),
   528 	(rtac (beta_cfun RS ssubst) 1),
   529 	(rtac contX_Issnd 1),
   530 	(rtac strict_Issnd2 1)
   531 	]);
   532 
   533 val sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
   534 	"~y=UU ==>sfst[x##y]=x"
   535  (fn prems =>
   536 	[
   537 	(cut_facts_tac prems 1),
   538 	(rtac (beta_cfun_sprod RS ssubst) 1),
   539 	(rtac (beta_cfun RS ssubst) 1),
   540 	(rtac contX_Isfst 1),
   541 	(etac Isfst2 1)
   542 	]);
   543 
   544 val ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
   545 	"~x=UU ==>ssnd[x##y]=y"
   546  (fn prems =>
   547 	[
   548 	(cut_facts_tac prems 1),
   549 	(rtac (beta_cfun_sprod RS ssubst) 1),
   550 	(rtac (beta_cfun RS ssubst) 1),
   551 	(rtac contX_Issnd 1),
   552 	(etac Issnd2 1)
   553 	]);
   554 
   555 
   556 val defined_sfstssnd = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
   557 	"~p=UU ==> ~sfst[p]=UU & ~ssnd[p]=UU"
   558  (fn prems =>
   559 	[
   560 	(cut_facts_tac prems 1),
   561 	(rtac (beta_cfun RS ssubst) 1),
   562 	(rtac contX_Issnd 1),
   563 	(rtac (beta_cfun RS ssubst) 1),
   564 	(rtac contX_Isfst 1),
   565 	(rtac defined_IsfstIssnd 1),
   566 	(rtac (inst_sprod_pcpo RS subst) 1),
   567 	(atac 1)
   568 	]);
   569  
   570 
   571 val surjective_pairing_Sprod2 = prove_goalw Sprod3.thy 
   572 	[sfst_def,ssnd_def,spair_def] "(sfst[p] ## ssnd[p]) = p"
   573  (fn prems =>
   574 	[
   575 	(rtac (beta_cfun_sprod RS ssubst) 1),
   576 	(rtac (beta_cfun RS ssubst) 1),
   577 	(rtac contX_Issnd 1),
   578 	(rtac (beta_cfun RS ssubst) 1),
   579 	(rtac contX_Isfst 1),
   580 	(rtac (surjective_pairing_Sprod RS sym) 1)
   581 	]);
   582 
   583 
   584 val less_sprod5b = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
   585  "~p1=UU ==> (p1<<p2) = (sfst[p1]<<sfst[p2] & ssnd[p1]<<ssnd[p2])"
   586  (fn prems =>
   587 	[
   588 	(cut_facts_tac prems 1),
   589 	(rtac (beta_cfun RS ssubst) 1),
   590 	(rtac contX_Issnd 1),
   591 	(rtac (beta_cfun RS ssubst) 1),
   592 	(rtac contX_Issnd 1),
   593 	(rtac (beta_cfun RS ssubst) 1),
   594 	(rtac contX_Isfst 1),
   595 	(rtac (beta_cfun RS ssubst) 1),
   596 	(rtac contX_Isfst 1),
   597 	(rtac less_sprod3b 1),
   598 	(rtac (inst_sprod_pcpo RS subst) 1),
   599 	(atac 1)
   600 	]);
   601 
   602  
   603 val less_sprod5c = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
   604  "[|xa##ya<<x##y;~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>xa<<x & ya << y"
   605  (fn prems =>
   606 	[
   607 	(cut_facts_tac prems 1),
   608 	(rtac less_sprod4c 1),
   609 	(REPEAT (atac 2)),
   610 	(rtac (beta_cfun_sprod RS subst) 1),
   611 	(rtac (beta_cfun_sprod RS subst) 1),
   612 	(atac 1)
   613 	]);
   614 
   615 val lub_sprod2 = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
   616 "[|is_chain(S)|] ==> range(S) <<| \
   617 \ (lub(range(%i.sfst[S(i)])) ## lub(range(%i.ssnd[S(i)])))"
   618  (fn prems =>
   619 	[
   620 	(cut_facts_tac prems 1),
   621 	(rtac (beta_cfun_sprod RS ssubst) 1),
   622 	(rtac (beta_cfun RS ext RS ssubst) 1),
   623 	(rtac contX_Issnd 1),
   624 	(rtac (beta_cfun RS ext RS ssubst) 1),
   625 	(rtac contX_Isfst 1),
   626 	(rtac lub_sprod 1),
   627 	(resolve_tac prems 1)
   628 	]);
   629 
   630 
   631 val thelub_sprod2 = (lub_sprod2 RS thelubI);
   632 (* is_chain(?S1) ==> lub(range(?S1)) =                                    *) 
   633 (*     (lub(range(%i. sfst[?S1(i)]))## lub(range(%i. ssnd[?S1(i)])))        *)
   634 
   635 
   636 
   637 val ssplit1 = prove_goalw Sprod3.thy [ssplit_def]
   638 	"ssplit[f][UU]=UU"
   639  (fn prems =>
   640 	[
   641 	(rtac (beta_cfun RS ssubst) 1),
   642 	(contX_tacR 1),
   643 	(rtac (strictify1 RS ssubst) 1),
   644 	(rtac refl 1)
   645 	]);
   646 
   647 val ssplit2 = prove_goalw Sprod3.thy [ssplit_def]
   648 	"[|~x=UU;~y=UU|] ==> ssplit[f][x##y]=f[x][y]"
   649  (fn prems =>
   650 	[
   651 	(rtac (beta_cfun RS ssubst) 1),
   652 	(contX_tacR 1),
   653 	(rtac (strictify2 RS ssubst) 1),
   654 	(rtac defined_spair 1),
   655 	(resolve_tac prems 1),
   656 	(resolve_tac prems 1),
   657 	(rtac (beta_cfun RS ssubst) 1),
   658 	(contX_tacR 1),
   659 	(rtac (sfst2 RS ssubst) 1),
   660 	(resolve_tac prems 1),
   661 	(rtac (ssnd2 RS ssubst) 1),
   662 	(resolve_tac prems 1),
   663 	(rtac refl 1)
   664 	]);
   665 
   666 
   667 val ssplit3 = prove_goalw Sprod3.thy [ssplit_def]
   668   "ssplit[spair][z]=z"
   669  (fn prems =>
   670 	[
   671 	(rtac (beta_cfun RS ssubst) 1),
   672 	(contX_tacR 1),
   673 	(res_inst_tac [("Q","z=UU")] classical2 1),
   674 	(hyp_subst_tac 1),
   675 	(rtac strictify1 1),
   676 	(rtac trans 1),
   677 	(rtac strictify2 1),
   678 	(atac 1),
   679 	(rtac (beta_cfun RS ssubst) 1),
   680 	(contX_tacR 1),
   681 	(rtac surjective_pairing_Sprod2 1)
   682 	]);
   683 
   684 
   685 (* ------------------------------------------------------------------------ *)
   686 (* install simplifier for Sprod                                             *)
   687 (* ------------------------------------------------------------------------ *)
   688 
   689 val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
   690 		strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
   691 		ssplit1,ssplit2];
   692 
   693 val Sprod_ss = Cfun_ss addsimps Sprod_rews;
   694 
   695