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