src/HOLCF/Sprod.thy
author huffman
Fri Mar 04 23:12:36 2005 +0100 (2005-03-04)
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
permissions -rw-r--r--
converted to new-style theories, and combined numbered files
     1 (*  Title:      HOLCF/Sprod0.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Strict product with typedef.
     7 *)
     8 
     9 header {* The type of strict products *}
    10 
    11 theory Sprod = Cfun:
    12 
    13 constdefs
    14   Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
    15  "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
    16 
    17 typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
    18 by auto
    19 
    20 syntax (xsymbols)
    21   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    22 syntax (HTML output)
    23   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    24 
    25 subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
    26 
    27 consts
    28   Ispair        :: "['a,'b] => ('a ** 'b)"
    29   Isfst         :: "('a ** 'b) => 'a"
    30   Issnd         :: "('a ** 'b) => 'b"  
    31 
    32 defs
    33    (*defining the abstract constants*)
    34 
    35   Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
    36 
    37   Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
    38                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
    39 
    40   Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
    41                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
    42 
    43 (* ------------------------------------------------------------------------ *)
    44 (* A non-emptyness result for Sprod                                         *)
    45 (* ------------------------------------------------------------------------ *)
    46 
    47 lemma SprodI: "(Spair_Rep a b):Sprod"
    48 apply (unfold Sprod_def)
    49 apply (rule CollectI, rule exI, rule exI, rule refl)
    50 done
    51 
    52 lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
    53 apply (rule inj_on_inverseI)
    54 apply (erule Abs_Sprod_inverse)
    55 done
    56 
    57 (* ------------------------------------------------------------------------ *)
    58 (* Strictness and definedness of Spair_Rep                                  *)
    59 (* ------------------------------------------------------------------------ *)
    60 
    61 lemma strict_Spair_Rep: 
    62  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
    63 apply (unfold Spair_Rep_def)
    64 apply (rule ext)
    65 apply (rule ext)
    66 apply (rule iffI)
    67 apply fast
    68 apply fast
    69 done
    70 
    71 lemma defined_Spair_Rep_rev: 
    72  "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
    73 apply (unfold Spair_Rep_def)
    74 apply (case_tac "a=UU|b=UU")
    75 apply assumption
    76 apply (fast dest: fun_cong)
    77 done
    78 
    79 (* ------------------------------------------------------------------------ *)
    80 (* injectivity of Spair_Rep and Ispair                                      *)
    81 (* ------------------------------------------------------------------------ *)
    82 
    83 lemma inject_Spair_Rep: 
    84 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
    85 
    86 apply (unfold Spair_Rep_def)
    87 apply (drule fun_cong)
    88 apply (drule fun_cong)
    89 apply (erule iffD1 [THEN mp])
    90 apply auto
    91 done
    92 
    93 lemma inject_Ispair: 
    94         "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
    95 apply (unfold Ispair_def)
    96 apply (erule inject_Spair_Rep)
    97 apply assumption
    98 apply (erule inj_on_Abs_Sprod [THEN inj_onD])
    99 apply (rule SprodI)
   100 apply (rule SprodI)
   101 done
   102 
   103 (* ------------------------------------------------------------------------ *)
   104 (* strictness and definedness of Ispair                                     *)
   105 (* ------------------------------------------------------------------------ *)
   106 
   107 lemma strict_Ispair: 
   108  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
   109 apply (unfold Ispair_def)
   110 apply (erule strict_Spair_Rep [THEN arg_cong])
   111 done
   112 
   113 lemma strict_Ispair1: 
   114         "Ispair UU b  = Ispair UU UU"
   115 apply (unfold Ispair_def)
   116 apply (rule strict_Spair_Rep [THEN arg_cong])
   117 apply (rule disjI1)
   118 apply (rule refl)
   119 done
   120 
   121 lemma strict_Ispair2: 
   122         "Ispair a UU = Ispair UU UU"
   123 apply (unfold Ispair_def)
   124 apply (rule strict_Spair_Rep [THEN arg_cong])
   125 apply (rule disjI2)
   126 apply (rule refl)
   127 done
   128 
   129 lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
   130 apply (rule de_Morgan_disj [THEN subst])
   131 apply (erule contrapos_nn)
   132 apply (erule strict_Ispair)
   133 done
   134 
   135 lemma defined_Ispair_rev: 
   136         "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
   137 apply (unfold Ispair_def)
   138 apply (rule defined_Spair_Rep_rev)
   139 apply (rule inj_on_Abs_Sprod [THEN inj_onD])
   140 apply assumption
   141 apply (rule SprodI)
   142 apply (rule SprodI)
   143 done
   144 
   145 lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
   146 apply (rule contrapos_nn)
   147 apply (erule_tac [2] defined_Ispair_rev)
   148 apply (rule de_Morgan_disj [THEN iffD2])
   149 apply (erule conjI)
   150 apply assumption
   151 done
   152 
   153 
   154 (* ------------------------------------------------------------------------ *)
   155 (* Exhaustion of the strict product **                                      *)
   156 (* ------------------------------------------------------------------------ *)
   157 
   158 lemma Exh_Sprod:
   159         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
   160 apply (unfold Ispair_def)
   161 apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
   162 apply (erule exE)
   163 apply (erule exE)
   164 apply (rule excluded_middle [THEN disjE])
   165 apply (rule disjI2)
   166 apply (rule exI)
   167 apply (rule exI)
   168 apply (rule conjI)
   169 apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
   170 apply (erule arg_cong)
   171 apply (rule de_Morgan_disj [THEN subst])
   172 apply assumption
   173 apply (rule disjI1)
   174 apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
   175 apply (rule_tac f = "Abs_Sprod" in arg_cong)
   176 apply (erule trans)
   177 apply (erule strict_Spair_Rep)
   178 done
   179 
   180 (* ------------------------------------------------------------------------ *)
   181 (* general elimination rule for strict product                              *)
   182 (* ------------------------------------------------------------------------ *)
   183 
   184 lemma IsprodE:
   185 assumes prem1: "p=Ispair UU UU ==> Q"
   186 assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
   187 shows "Q"
   188 apply (rule Exh_Sprod [THEN disjE])
   189 apply (erule prem1)
   190 apply (erule exE)
   191 apply (erule exE)
   192 apply (erule conjE)
   193 apply (erule conjE)
   194 apply (erule prem2)
   195 apply assumption
   196 apply assumption
   197 done
   198 
   199 (* ------------------------------------------------------------------------ *)
   200 (* some results about the selectors Isfst, Issnd                            *)
   201 (* ------------------------------------------------------------------------ *)
   202 
   203 lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
   204 apply (unfold Isfst_def)
   205 apply (rule some_equality)
   206 apply (rule conjI)
   207 apply fast
   208 apply (intro strip)
   209 apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
   210 apply (rule not_sym)
   211 apply (rule defined_Ispair)
   212 apply (fast+)
   213 done
   214 
   215 lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
   216 apply (subst strict_Ispair1)
   217 apply (rule strict_Isfst)
   218 apply (rule refl)
   219 done
   220 
   221 lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
   222 apply (subst strict_Ispair2)
   223 apply (rule strict_Isfst)
   224 apply (rule refl)
   225 done
   226 
   227 lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
   228 apply (unfold Issnd_def)
   229 apply (rule some_equality)
   230 apply (rule conjI)
   231 apply fast
   232 apply (intro strip)
   233 apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
   234 apply (rule not_sym)
   235 apply (rule defined_Ispair)
   236 apply (fast+)
   237 done
   238 
   239 lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
   240 apply (subst strict_Ispair1)
   241 apply (rule strict_Issnd)
   242 apply (rule refl)
   243 done
   244 
   245 lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
   246 apply (subst strict_Ispair2)
   247 apply (rule strict_Issnd)
   248 apply (rule refl)
   249 done
   250 
   251 lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
   252 apply (unfold Isfst_def)
   253 apply (rule some_equality)
   254 apply (rule conjI)
   255 apply (intro strip)
   256 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
   257 apply (erule defined_Ispair)
   258 apply assumption
   259 apply assumption
   260 apply (intro strip)
   261 apply (rule inject_Ispair [THEN conjunct1])
   262 prefer 3 apply fast
   263 apply (fast+)
   264 done
   265 
   266 lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
   267 apply (unfold Issnd_def)
   268 apply (rule some_equality)
   269 apply (rule conjI)
   270 apply (intro strip)
   271 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
   272 apply (erule defined_Ispair)
   273 apply assumption
   274 apply assumption
   275 apply (intro strip)
   276 apply (rule inject_Ispair [THEN conjunct2])
   277 prefer 3 apply fast
   278 apply (fast+)
   279 done
   280 
   281 lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
   282 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   283 apply (erule Isfst)
   284 apply assumption
   285 apply (erule ssubst)
   286 apply (rule strict_Isfst1)
   287 done
   288 
   289 lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
   290 apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
   291 apply (erule Issnd)
   292 apply assumption
   293 apply (erule ssubst)
   294 apply (rule strict_Issnd2)
   295 done
   296 
   297 
   298 (* ------------------------------------------------------------------------ *)
   299 (* instantiate the simplifier                                               *)
   300 (* ------------------------------------------------------------------------ *)
   301 
   302 lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
   303                  Isfst2 Issnd2
   304 
   305 declare Isfst2 [simp] Issnd2 [simp]
   306 
   307 lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
   308 apply (rule_tac p = "p" in IsprodE)
   309 apply simp
   310 apply (erule ssubst)
   311 apply (rule conjI)
   312 apply (simp add: Sprod0_ss)
   313 apply (simp add: Sprod0_ss)
   314 done
   315 
   316 
   317 (* ------------------------------------------------------------------------ *)
   318 (* Surjective pairing: equivalent to Exh_Sprod                              *)
   319 (* ------------------------------------------------------------------------ *)
   320 
   321 lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
   322 apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
   323 apply (simp add: Sprod0_ss)
   324 apply (erule exE)
   325 apply (erule exE)
   326 apply (simp add: Sprod0_ss)
   327 done
   328 
   329 lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
   330 apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
   331 apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
   332 apply simp
   333 done
   334 
   335 subsection {* The strict product is a partial order *}
   336 
   337 instance "**"::(sq_ord,sq_ord)sq_ord ..
   338 
   339 defs (overloaded)
   340   less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   341 
   342 (* ------------------------------------------------------------------------ *)
   343 (* less_sprod is a partial order on Sprod                                   *)
   344 (* ------------------------------------------------------------------------ *)
   345 
   346 lemma refl_less_sprod: "(p::'a ** 'b) << p"
   347 apply (unfold less_sprod_def)
   348 apply (fast intro: refl_less)
   349 done
   350 
   351 lemma antisym_less_sprod: 
   352         "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
   353 apply (unfold less_sprod_def)
   354 apply (rule Sel_injective_Sprod)
   355 apply (fast intro: antisym_less)
   356 apply (fast intro: antisym_less)
   357 done
   358 
   359 lemma trans_less_sprod: 
   360         "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
   361 apply (unfold less_sprod_def)
   362 apply (blast intro: trans_less)
   363 done
   364 
   365 instance "**"::(pcpo,pcpo)po
   366 by intro_classes
   367   (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
   368 
   369 (* for compatibility with old HOLCF-Version *)
   370 lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
   371 apply (fold less_sprod_def)
   372 apply (rule refl)
   373 done
   374 
   375 subsection {* The strict product is pointed *}
   376 (* ------------------------------------------------------------------------ *)
   377 (* type sprod is pointed                                                    *)
   378 (* ------------------------------------------------------------------------ *)
   379 (*
   380 lemma minimal_sprod: "Ispair UU UU << p"
   381 apply (simp add: inst_sprod_po minimal)
   382 done
   383 
   384 lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
   385 
   386 lemma least_sprod: "? x::'a**'b.!y. x<<y"
   387 apply (rule_tac x = "Ispair UU UU" in exI)
   388 apply (rule minimal_sprod [THEN allI])
   389 done
   390 *)
   391 (* ------------------------------------------------------------------------ *)
   392 (* Ispair is monotone in both arguments                                     *)
   393 (* ------------------------------------------------------------------------ *)
   394 
   395 lemma monofun_Ispair1: "monofun(Ispair)"
   396 apply (unfold monofun)
   397 apply (intro strip)
   398 apply (rule less_fun [THEN iffD2])
   399 apply (intro strip)
   400 apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
   401 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   402 apply (frule notUU_I)
   403 apply assumption
   404 apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
   405 done
   406 
   407 lemma monofun_Ispair2: "monofun(Ispair(x))"
   408 apply (unfold monofun)
   409 apply (intro strip)
   410 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   411 apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
   412 apply (frule notUU_I)
   413 apply assumption
   414 apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
   415 done
   416 
   417 lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   418 apply (rule trans_less)
   419 apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
   420 prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
   421 apply assumption
   422 apply assumption
   423 done
   424 
   425 (* ------------------------------------------------------------------------ *)
   426 (* Isfst and Issnd are monotone                                             *)
   427 (* ------------------------------------------------------------------------ *)
   428 
   429 lemma monofun_Isfst: "monofun(Isfst)"
   430 apply (unfold monofun)
   431 apply (simp add: inst_sprod_po)
   432 done
   433 
   434 lemma monofun_Issnd: "monofun(Issnd)"
   435 apply (unfold monofun)
   436 apply (simp add: inst_sprod_po)
   437 done
   438 
   439 subsection {* The strict product is a cpo *}
   440 (* ------------------------------------------------------------------------ *)
   441 (* the type 'a ** 'b is a cpo                                               *)
   442 (* ------------------------------------------------------------------------ *)
   443 
   444 lemma lub_sprod: 
   445 "[|chain(S)|] ==> range(S) <<|  
   446   Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
   447 apply (rule is_lubI)
   448 apply (rule ub_rangeI)
   449 apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
   450 apply (rule monofun_Ispair)
   451 apply (rule is_ub_thelub)
   452 apply (erule monofun_Isfst [THEN ch2ch_monofun])
   453 apply (rule is_ub_thelub)
   454 apply (erule monofun_Issnd [THEN ch2ch_monofun])
   455 apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
   456 apply (rule monofun_Ispair)
   457 apply (rule is_lub_thelub)
   458 apply (erule monofun_Isfst [THEN ch2ch_monofun])
   459 apply (erule monofun_Isfst [THEN ub2ub_monofun])
   460 apply (rule is_lub_thelub)
   461 apply (erule monofun_Issnd [THEN ch2ch_monofun])
   462 apply (erule monofun_Issnd [THEN ub2ub_monofun])
   463 done
   464 
   465 lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
   466 
   467 lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
   468 apply (rule exI)
   469 apply (erule lub_sprod)
   470 done
   471 
   472 instance "**" :: (pcpo, pcpo) cpo
   473 by intro_classes (rule cpo_sprod)
   474 
   475 
   476 subsection {* The strict product is a pcpo *}
   477 
   478 lemma minimal_sprod: "Ispair UU UU << p"
   479 apply (simp add: inst_sprod_po minimal)
   480 done
   481 
   482 lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
   483 
   484 lemma least_sprod: "? x::'a**'b.!y. x<<y"
   485 apply (rule_tac x = "Ispair UU UU" in exI)
   486 apply (rule minimal_sprod [THEN allI])
   487 done
   488 
   489 instance "**" :: (pcpo, pcpo) pcpo
   490 by intro_classes (rule least_sprod)
   491 
   492 
   493 subsection {* Other constants *}
   494 
   495 consts  
   496   spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
   497   sfst		:: "('a**'b)->'a"
   498   ssnd		:: "('a**'b)->'b"
   499   ssplit	:: "('a->'b->'c)->('a**'b)->'c"
   500 
   501 syntax  
   502   "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
   503 
   504 translations
   505         "(:x, y, z:)"   == "(:x, (:y, z:):)"
   506         "(:x, y:)"      == "spair$x$y"
   507 
   508 defs
   509 spair_def:       "spair  == (LAM x y. Ispair x y)"
   510 sfst_def:        "sfst   == (LAM p. Isfst p)"
   511 ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
   512 ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
   513 
   514 (* for compatibility with old HOLCF-Version *)
   515 lemma inst_sprod_pcpo: "UU = Ispair UU UU"
   516 apply (simp add: UU_def UU_sprod_def)
   517 done
   518 
   519 declare inst_sprod_pcpo [symmetric, simp]
   520 
   521 (* ------------------------------------------------------------------------ *)
   522 (* continuity of Ispair, Isfst, Issnd                                       *)
   523 (* ------------------------------------------------------------------------ *)
   524 
   525 lemma sprod3_lemma1: 
   526 "[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
   527   Ispair (lub(range Y)) x = 
   528   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
   529          (lub(range(%i. Issnd(Ispair(Y i) x))))"
   530 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
   531 apply (rule lub_equal)
   532 apply assumption
   533 apply (rule monofun_Isfst [THEN ch2ch_monofun])
   534 apply (rule ch2ch_fun)
   535 apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
   536 apply assumption
   537 apply (rule allI)
   538 apply (simp (no_asm_simp))
   539 apply (rule sym)
   540 apply (drule chain_UU_I_inverse2)
   541 apply (erule exE)
   542 apply (rule lub_chain_maxelem)
   543 apply (erule Issnd2)
   544 apply (rule allI)
   545 apply (rename_tac "j")
   546 apply (case_tac "Y (j) =UU")
   547 apply auto
   548 done
   549 
   550 lemma sprod3_lemma2: 
   551 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
   552     Ispair (lub(range Y)) x = 
   553     Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
   554            (lub(range(%i. Issnd(Ispair(Y i) x))))"
   555 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
   556 apply assumption
   557 apply (rule trans)
   558 apply (rule strict_Ispair1)
   559 apply (rule strict_Ispair [symmetric])
   560 apply (rule disjI1)
   561 apply (rule chain_UU_I_inverse)
   562 apply auto
   563 apply (erule chain_UU_I [THEN spec])
   564 apply assumption
   565 done
   566 
   567 
   568 lemma sprod3_lemma3: 
   569 "[| chain(Y); x = UU |] ==> 
   570            Ispair (lub(range Y)) x = 
   571            Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
   572                   (lub(range(%i. Issnd(Ispair (Y i) x))))"
   573 apply (erule ssubst)
   574 apply (rule trans)
   575 apply (rule strict_Ispair2)
   576 apply (rule strict_Ispair [symmetric])
   577 apply (rule disjI1)
   578 apply (rule chain_UU_I_inverse)
   579 apply (rule allI)
   580 apply (simp add: Sprod0_ss)
   581 done
   582 
   583 lemma contlub_Ispair1: "contlub(Ispair)"
   584 apply (rule contlubI)
   585 apply (intro strip)
   586 apply (rule expand_fun_eq [THEN iffD2])
   587 apply (intro strip)
   588 apply (subst lub_fun [THEN thelubI])
   589 apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
   590 apply (rule trans)
   591 apply (rule_tac [2] thelub_sprod [symmetric])
   592 apply (rule_tac [2] ch2ch_fun)
   593 apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
   594 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   595 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
   596 apply (erule sprod3_lemma1)
   597 apply assumption
   598 apply assumption
   599 apply (erule sprod3_lemma2)
   600 apply assumption
   601 apply assumption
   602 apply (erule sprod3_lemma3)
   603 apply assumption
   604 done
   605 
   606 lemma sprod3_lemma4: 
   607 "[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
   608           Ispair x (lub(range Y)) = 
   609           Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
   610                  (lub(range(%i. Issnd (Ispair x (Y i)))))"
   611 apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
   612 apply (rule sym)
   613 apply (drule chain_UU_I_inverse2)
   614 apply (erule exE)
   615 apply (rule lub_chain_maxelem)
   616 apply (erule Isfst2)
   617 apply (rule allI)
   618 apply (rename_tac "j")
   619 apply (case_tac "Y (j) =UU")
   620 apply auto
   621 done
   622 
   623 lemma sprod3_lemma5: 
   624 "[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
   625           Ispair x (lub(range Y)) = 
   626           Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
   627                  (lub(range(%i. Issnd(Ispair x (Y i)))))"
   628 apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
   629 apply assumption
   630 apply (rule trans)
   631 apply (rule strict_Ispair2)
   632 apply (rule strict_Ispair [symmetric])
   633 apply (rule disjI2)
   634 apply (rule chain_UU_I_inverse)
   635 apply (rule allI)
   636 apply (simp add: Sprod0_ss)
   637 apply (erule chain_UU_I [THEN spec])
   638 apply assumption
   639 done
   640 
   641 lemma sprod3_lemma6: 
   642 "[| chain(Y); x = UU |] ==> 
   643           Ispair x (lub(range Y)) = 
   644           Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
   645                  (lub(range(%i. Issnd (Ispair x (Y i)))))"
   646 apply (rule_tac s = "UU" and t = "x" in ssubst)
   647 apply assumption
   648 apply (rule trans)
   649 apply (rule strict_Ispair1)
   650 apply (rule strict_Ispair [symmetric])
   651 apply (rule disjI1)
   652 apply (rule chain_UU_I_inverse)
   653 apply (rule allI)
   654 apply (simp add: Sprod0_ss)
   655 done
   656 
   657 lemma contlub_Ispair2: "contlub(Ispair(x))"
   658 apply (rule contlubI)
   659 apply (intro strip)
   660 apply (rule trans)
   661 apply (rule_tac [2] thelub_sprod [symmetric])
   662 apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
   663 apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   664 apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
   665 apply (erule sprod3_lemma4)
   666 apply assumption
   667 apply assumption
   668 apply (erule sprod3_lemma5)
   669 apply assumption
   670 apply assumption
   671 apply (erule sprod3_lemma6)
   672 apply assumption
   673 done
   674 
   675 lemma cont_Ispair1: "cont(Ispair)"
   676 apply (rule monocontlub2cont)
   677 apply (rule monofun_Ispair1)
   678 apply (rule contlub_Ispair1)
   679 done
   680 
   681 lemma cont_Ispair2: "cont(Ispair(x))"
   682 apply (rule monocontlub2cont)
   683 apply (rule monofun_Ispair2)
   684 apply (rule contlub_Ispair2)
   685 done
   686 
   687 lemma contlub_Isfst: "contlub(Isfst)"
   688 apply (rule contlubI)
   689 apply (intro strip)
   690 apply (subst lub_sprod [THEN thelubI])
   691 apply assumption
   692 apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
   693 apply (simp add: Sprod0_ss)
   694 apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
   695 apply assumption
   696 apply (rule trans)
   697 apply (simp add: Sprod0_ss)
   698 apply (rule sym)
   699 apply (rule chain_UU_I_inverse)
   700 apply (rule allI)
   701 apply (rule strict_Isfst)
   702 apply (rule contrapos_np)
   703 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
   704 apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
   705 done
   706 
   707 lemma contlub_Issnd: "contlub(Issnd)"
   708 apply (rule contlubI)
   709 apply (intro strip)
   710 apply (subst lub_sprod [THEN thelubI])
   711 apply assumption
   712 apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
   713 apply (simp add: Sprod0_ss)
   714 apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
   715 apply assumption
   716 apply (simp add: Sprod0_ss)
   717 apply (rule sym)
   718 apply (rule chain_UU_I_inverse)
   719 apply (rule allI)
   720 apply (rule strict_Issnd)
   721 apply (rule contrapos_np)
   722 apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
   723 apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
   724 done
   725 
   726 lemma cont_Isfst: "cont(Isfst)"
   727 apply (rule monocontlub2cont)
   728 apply (rule monofun_Isfst)
   729 apply (rule contlub_Isfst)
   730 done
   731 
   732 lemma cont_Issnd: "cont(Issnd)"
   733 apply (rule monocontlub2cont)
   734 apply (rule monofun_Issnd)
   735 apply (rule contlub_Issnd)
   736 done
   737 
   738 lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
   739 apply fast
   740 done
   741 
   742 (* ------------------------------------------------------------------------ *)
   743 (* convert all lemmas to the continuous versions                            *)
   744 (* ------------------------------------------------------------------------ *)
   745 
   746 lemma beta_cfun_sprod [simp]: 
   747         "(LAM x y. Ispair x y)$a$b = Ispair a b"
   748 apply (subst beta_cfun)
   749 apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
   750 apply (subst beta_cfun)
   751 apply (rule cont_Ispair2)
   752 apply (rule refl)
   753 done
   754 
   755 lemma inject_spair: 
   756         "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
   757 apply (unfold spair_def)
   758 apply (erule inject_Ispair)
   759 apply assumption
   760 apply (erule box_equals)
   761 apply (rule beta_cfun_sprod)
   762 apply (rule beta_cfun_sprod)
   763 done
   764 
   765 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
   766 apply (unfold spair_def)
   767 apply (rule sym)
   768 apply (rule trans)
   769 apply (rule beta_cfun_sprod)
   770 apply (rule sym)
   771 apply (rule inst_sprod_pcpo)
   772 done
   773 
   774 lemma strict_spair: 
   775         "(a=UU | b=UU) ==> (:a,b:)=UU"
   776 apply (unfold spair_def)
   777 apply (rule trans)
   778 apply (rule beta_cfun_sprod)
   779 apply (rule trans)
   780 apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   781 apply (erule strict_Ispair)
   782 done
   783 
   784 lemma strict_spair1: "(:UU,b:) = UU"
   785 apply (unfold spair_def)
   786 apply (subst beta_cfun_sprod)
   787 apply (rule trans)
   788 apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   789 apply (rule strict_Ispair1)
   790 done
   791 
   792 lemma strict_spair2: "(:a,UU:) = UU"
   793 apply (unfold spair_def)
   794 apply (subst beta_cfun_sprod)
   795 apply (rule trans)
   796 apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   797 apply (rule strict_Ispair2)
   798 done
   799 
   800 declare strict_spair1 [simp] strict_spair2 [simp]
   801 
   802 lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
   803 apply (unfold spair_def)
   804 apply (rule strict_Ispair_rev)
   805 apply auto
   806 done
   807 
   808 lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
   809 apply (unfold spair_def)
   810 apply (rule defined_Ispair_rev)
   811 apply auto
   812 done
   813 
   814 lemma defined_spair: 
   815         "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
   816 apply (unfold spair_def)
   817 apply (subst beta_cfun_sprod)
   818 apply (subst inst_sprod_pcpo)
   819 apply (erule defined_Ispair)
   820 apply assumption
   821 done
   822 
   823 lemma Exh_Sprod2:
   824         "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
   825 apply (unfold spair_def)
   826 apply (rule Exh_Sprod [THEN disjE])
   827 apply (rule disjI1)
   828 apply (subst inst_sprod_pcpo)
   829 apply assumption
   830 apply (rule disjI2)
   831 apply (erule exE)
   832 apply (erule exE)
   833 apply (rule exI)
   834 apply (rule exI)
   835 apply (rule conjI)
   836 apply (subst beta_cfun_sprod)
   837 apply fast
   838 apply fast
   839 done
   840 
   841 
   842 lemma sprodE:
   843 assumes prem1: "p=UU ==> Q"
   844 assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
   845 shows "Q"
   846 apply (rule IsprodE)
   847 apply (rule prem1)
   848 apply (subst inst_sprod_pcpo)
   849 apply assumption
   850 apply (rule prem2)
   851 prefer 2 apply (assumption)
   852 prefer 2 apply (assumption)
   853 apply (unfold spair_def)
   854 apply (subst beta_cfun_sprod)
   855 apply assumption
   856 done
   857 
   858 
   859 lemma strict_sfst: 
   860         "p=UU==>sfst$p=UU"
   861 apply (unfold sfst_def)
   862 apply (subst beta_cfun)
   863 apply (rule cont_Isfst)
   864 apply (rule strict_Isfst)
   865 apply (rule inst_sprod_pcpo [THEN subst])
   866 apply assumption
   867 done
   868 
   869 lemma strict_sfst1: 
   870         "sfst$(:UU,y:) = UU"
   871 apply (unfold sfst_def spair_def)
   872 apply (subst beta_cfun_sprod)
   873 apply (subst beta_cfun)
   874 apply (rule cont_Isfst)
   875 apply (rule strict_Isfst1)
   876 done
   877  
   878 lemma strict_sfst2: 
   879         "sfst$(:x,UU:) = UU"
   880 apply (unfold sfst_def spair_def)
   881 apply (subst beta_cfun_sprod)
   882 apply (subst beta_cfun)
   883 apply (rule cont_Isfst)
   884 apply (rule strict_Isfst2)
   885 done
   886 
   887 lemma strict_ssnd: 
   888         "p=UU==>ssnd$p=UU"
   889 apply (unfold ssnd_def)
   890 apply (subst beta_cfun)
   891 apply (rule cont_Issnd)
   892 apply (rule strict_Issnd)
   893 apply (rule inst_sprod_pcpo [THEN subst])
   894 apply assumption
   895 done
   896 
   897 lemma strict_ssnd1: 
   898         "ssnd$(:UU,y:) = UU"
   899 apply (unfold ssnd_def spair_def)
   900 apply (subst beta_cfun_sprod)
   901 apply (subst beta_cfun)
   902 apply (rule cont_Issnd)
   903 apply (rule strict_Issnd1)
   904 done
   905 
   906 lemma strict_ssnd2: 
   907         "ssnd$(:x,UU:) = UU"
   908 apply (unfold ssnd_def spair_def)
   909 apply (subst beta_cfun_sprod)
   910 apply (subst beta_cfun)
   911 apply (rule cont_Issnd)
   912 apply (rule strict_Issnd2)
   913 done
   914 
   915 lemma sfst2: 
   916         "y~=UU ==>sfst$(:x,y:)=x"
   917 apply (unfold sfst_def spair_def)
   918 apply (subst beta_cfun_sprod)
   919 apply (subst beta_cfun)
   920 apply (rule cont_Isfst)
   921 apply (erule Isfst2)
   922 done
   923 
   924 lemma ssnd2: 
   925         "x~=UU ==>ssnd$(:x,y:)=y"
   926 apply (unfold ssnd_def spair_def)
   927 apply (subst beta_cfun_sprod)
   928 apply (subst beta_cfun)
   929 apply (rule cont_Issnd)
   930 apply (erule Issnd2)
   931 done
   932 
   933 
   934 lemma defined_sfstssnd: 
   935         "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
   936 apply (unfold sfst_def ssnd_def spair_def)
   937 apply (simplesubst beta_cfun)
   938 apply (rule cont_Issnd)
   939 apply (subst beta_cfun)
   940 apply (rule cont_Isfst)
   941 apply (rule defined_IsfstIssnd)
   942 apply (rule inst_sprod_pcpo [THEN subst])
   943 apply assumption
   944 done
   945  
   946 lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
   947 apply (unfold sfst_def ssnd_def spair_def)
   948 apply (subst beta_cfun_sprod)
   949 apply (simplesubst beta_cfun)
   950 apply (rule cont_Issnd)
   951 apply (subst beta_cfun)
   952 apply (rule cont_Isfst)
   953 apply (rule surjective_pairing_Sprod [symmetric])
   954 done
   955 
   956 lemma lub_sprod2: 
   957 "chain(S) ==> range(S) <<|  
   958                (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
   959 apply (unfold sfst_def ssnd_def spair_def)
   960 apply (subst beta_cfun_sprod)
   961 apply (simplesubst beta_cfun [THEN ext])
   962 apply (rule cont_Issnd)
   963 apply (subst beta_cfun [THEN ext])
   964 apply (rule cont_Isfst)
   965 apply (erule lub_sprod)
   966 done
   967 
   968 
   969 lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
   970 (*
   971  "chain ?S1 ==>
   972  lub (range ?S1) =
   973  (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
   974 *)
   975 
   976 lemma ssplit1: 
   977         "ssplit$f$UU=UU"
   978 apply (unfold ssplit_def)
   979 apply (subst beta_cfun)
   980 apply (simp (no_asm))
   981 apply (subst strictify1)
   982 apply (rule refl)
   983 done
   984 
   985 lemma ssplit2: 
   986         "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
   987 apply (unfold ssplit_def)
   988 apply (subst beta_cfun)
   989 apply (simp (no_asm))
   990 apply (subst strictify2)
   991 apply (rule defined_spair)
   992 apply assumption
   993 apply assumption
   994 apply (subst beta_cfun)
   995 apply (simp (no_asm))
   996 apply (subst sfst2)
   997 apply assumption
   998 apply (subst ssnd2)
   999 apply assumption
  1000 apply (rule refl)
  1001 done
  1002 
  1003 
  1004 lemma ssplit3: 
  1005   "ssplit$spair$z=z"
  1006 apply (unfold ssplit_def)
  1007 apply (subst beta_cfun)
  1008 apply (simp (no_asm))
  1009 apply (case_tac "z=UU")
  1010 apply (erule ssubst)
  1011 apply (rule strictify1)
  1012 apply (rule trans)
  1013 apply (rule strictify2)
  1014 apply assumption
  1015 apply (subst beta_cfun)
  1016 apply (simp (no_asm))
  1017 apply (rule surjective_pairing_Sprod2)
  1018 done
  1019 
  1020 (* ------------------------------------------------------------------------ *)
  1021 (* install simplifier for Sprod                                             *)
  1022 (* ------------------------------------------------------------------------ *)
  1023 
  1024 lemmas Sprod_rews = strict_sfst1 strict_sfst2
  1025                 strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
  1026                 ssplit1 ssplit2
  1027 declare Sprod_rews [simp]
  1028 
  1029 end