src/HOLCF/Sprod.thy
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Sprod.thy	Fri Mar 04 23:12:36 2005 +0100
     1.3 @@ -0,0 +1,1029 @@
     1.4 +(*  Title:      HOLCF/Sprod0.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Franz Regensburger
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Strict product with typedef.
    1.10 +*)
    1.11 +
    1.12 +header {* The type of strict products *}
    1.13 +
    1.14 +theory Sprod = Cfun:
    1.15 +
    1.16 +constdefs
    1.17 +  Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
    1.18 + "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
    1.19 +
    1.20 +typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
    1.21 +by auto
    1.22 +
    1.23 +syntax (xsymbols)
    1.24 +  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    1.25 +syntax (HTML output)
    1.26 +  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    1.27 +
    1.28 +subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
    1.29 +
    1.30 +consts
    1.31 +  Ispair        :: "['a,'b] => ('a ** 'b)"
    1.32 +  Isfst         :: "('a ** 'b) => 'a"
    1.33 +  Issnd         :: "('a ** 'b) => 'b"  
    1.34 +
    1.35 +defs
    1.36 +   (*defining the abstract constants*)
    1.37 +
    1.38 +  Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
    1.39 +
    1.40 +  Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
    1.41 +                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
    1.42 +
    1.43 +  Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
    1.44 +                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
    1.45 +
    1.46 +(* ------------------------------------------------------------------------ *)
    1.47 +(* A non-emptyness result for Sprod                                         *)
    1.48 +(* ------------------------------------------------------------------------ *)
    1.49 +
    1.50 +lemma SprodI: "(Spair_Rep a b):Sprod"
    1.51 +apply (unfold Sprod_def)
    1.52 +apply (rule CollectI, rule exI, rule exI, rule refl)
    1.53 +done
    1.54 +
    1.55 +lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
    1.56 +apply (rule inj_on_inverseI)
    1.57 +apply (erule Abs_Sprod_inverse)
    1.58 +done
    1.59 +
    1.60 +(* ------------------------------------------------------------------------ *)
    1.61 +(* Strictness and definedness of Spair_Rep                                  *)
    1.62 +(* ------------------------------------------------------------------------ *)
    1.63 +
    1.64 +lemma strict_Spair_Rep: 
    1.65 + "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
    1.66 +apply (unfold Spair_Rep_def)
    1.67 +apply (rule ext)
    1.68 +apply (rule ext)
    1.69 +apply (rule iffI)
    1.70 +apply fast
    1.71 +apply fast
    1.72 +done
    1.73 +
    1.74 +lemma defined_Spair_Rep_rev: 
    1.75 + "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
    1.76 +apply (unfold Spair_Rep_def)
    1.77 +apply (case_tac "a=UU|b=UU")
    1.78 +apply assumption
    1.79 +apply (fast dest: fun_cong)
    1.80 +done
    1.81 +
    1.82 +(* ------------------------------------------------------------------------ *)
    1.83 +(* injectivity of Spair_Rep and Ispair                                      *)
    1.84 +(* ------------------------------------------------------------------------ *)
    1.85 +
    1.86 +lemma inject_Spair_Rep: 
    1.87 +"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
    1.88 +
    1.89 +apply (unfold Spair_Rep_def)
    1.90 +apply (drule fun_cong)
    1.91 +apply (drule fun_cong)
    1.92 +apply (erule iffD1 [THEN mp])
    1.93 +apply auto
    1.94 +done
    1.95 +
    1.96 +lemma inject_Ispair: 
    1.97 +        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
    1.98 +apply (unfold Ispair_def)
    1.99 +apply (erule inject_Spair_Rep)
   1.100 +apply assumption
   1.101 +apply (erule inj_on_Abs_Sprod [THEN inj_onD])
   1.102 +apply (rule SprodI)
   1.103 +apply (rule SprodI)
   1.104 +done
   1.105 +
   1.106 +(* ------------------------------------------------------------------------ *)
   1.107 +(* strictness and definedness of Ispair                                     *)
   1.108 +(* ------------------------------------------------------------------------ *)
   1.109 +
   1.110 +lemma strict_Ispair: 
   1.111 + "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
   1.112 +apply (unfold Ispair_def)
   1.113 +apply (erule strict_Spair_Rep [THEN arg_cong])
   1.114 +done
   1.115 +
   1.116 +lemma strict_Ispair1: 
   1.117 +        "Ispair UU b  = Ispair UU UU"
   1.118 +apply (unfold Ispair_def)
   1.119 +apply (rule strict_Spair_Rep [THEN arg_cong])
   1.120 +apply (rule disjI1)
   1.121 +apply (rule refl)
   1.122 +done
   1.123 +
   1.124 +lemma strict_Ispair2: 
   1.125 +        "Ispair a UU = Ispair UU UU"
   1.126 +apply (unfold Ispair_def)
   1.127 +apply (rule strict_Spair_Rep [THEN arg_cong])
   1.128 +apply (rule disjI2)
   1.129 +apply (rule refl)
   1.130 +done
   1.131 +
   1.132 +lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
   1.133 +apply (rule de_Morgan_disj [THEN subst])
   1.134 +apply (erule contrapos_nn)
   1.135 +apply (erule strict_Ispair)
   1.136 +done
   1.137 +
   1.138 +lemma defined_Ispair_rev: 
   1.139 +        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
   1.140 +apply (unfold Ispair_def)
   1.141 +apply (rule defined_Spair_Rep_rev)
   1.142 +apply (rule inj_on_Abs_Sprod [THEN inj_onD])
   1.143 +apply assumption
   1.144 +apply (rule SprodI)
   1.145 +apply (rule SprodI)
   1.146 +done
   1.147 +
   1.148 +lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
   1.149 +apply (rule contrapos_nn)
   1.150 +apply (erule_tac [2] defined_Ispair_rev)
   1.151 +apply (rule de_Morgan_disj [THEN iffD2])
   1.152 +apply (erule conjI)
   1.153 +apply assumption
   1.154 +done
   1.155 +
   1.156 +
   1.157 +(* ------------------------------------------------------------------------ *)
   1.158 +(* Exhaustion of the strict product **                                      *)
   1.159 +(* ------------------------------------------------------------------------ *)
   1.160 +
   1.161 +lemma Exh_Sprod:
   1.162 +        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
   1.163 +apply (unfold Ispair_def)
   1.164 +apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
   1.165 +apply (erule exE)
   1.166 +apply (erule exE)
   1.167 +apply (rule excluded_middle [THEN disjE])
   1.168 +apply (rule disjI2)
   1.169 +apply (rule exI)
   1.170 +apply (rule exI)
   1.171 +apply (rule conjI)
   1.172 +apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
   1.173 +apply (erule arg_cong)
   1.174 +apply (rule de_Morgan_disj [THEN subst])
   1.175 +apply assumption
   1.176 +apply (rule disjI1)
   1.177 +apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
   1.178 +apply (rule_tac f = "Abs_Sprod" in arg_cong)
   1.179 +apply (erule trans)
   1.180 +apply (erule strict_Spair_Rep)
   1.181 +done
   1.182 +
   1.183 +(* ------------------------------------------------------------------------ *)
   1.184 +(* general elimination rule for strict product                              *)
   1.185 +(* ------------------------------------------------------------------------ *)
   1.186 +
   1.187 +lemma IsprodE:
   1.188 +assumes prem1: "p=Ispair UU UU ==> Q"
   1.189 +assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
   1.190 +shows "Q"
   1.191 +apply (rule Exh_Sprod [THEN disjE])
   1.192 +apply (erule prem1)
   1.193 +apply (erule exE)
   1.194 +apply (erule exE)
   1.195 +apply (erule conjE)
   1.196 +apply (erule conjE)
   1.197 +apply (erule prem2)
   1.198 +apply assumption
   1.199 +apply assumption
   1.200 +done
   1.201 +
   1.202 +(* ------------------------------------------------------------------------ *)
   1.203 +(* some results about the selectors Isfst, Issnd                            *)
   1.204 +(* ------------------------------------------------------------------------ *)
   1.205 +
   1.206 +lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
   1.207 +apply (unfold Isfst_def)
   1.208 +apply (rule some_equality)
   1.209 +apply (rule conjI)
   1.210 +apply fast
   1.211 +apply (intro strip)
   1.212 +apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
   1.213 +apply (rule not_sym)
   1.214 +apply (rule defined_Ispair)
   1.215 +apply (fast+)
   1.216 +done
   1.217 +
   1.218 +lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
   1.219 +apply (subst strict_Ispair1)
   1.220 +apply (rule strict_Isfst)
   1.221 +apply (rule refl)
   1.222 +done
   1.223 +
   1.224 +lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
   1.225 +apply (subst strict_Ispair2)
   1.226 +apply (rule strict_Isfst)
   1.227 +apply (rule refl)
   1.228 +done
   1.229 +
   1.230 +lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
   1.231 +apply (unfold Issnd_def)
   1.232 +apply (rule some_equality)
   1.233 +apply (rule conjI)
   1.234 +apply fast
   1.235 +apply (intro strip)
   1.236 +apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
   1.237 +apply (rule not_sym)
   1.238 +apply (rule defined_Ispair)
   1.239 +apply (fast+)
   1.240 +done
   1.241 +
   1.242 +lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
   1.243 +apply (subst strict_Ispair1)
   1.244 +apply (rule strict_Issnd)
   1.245 +apply (rule refl)
   1.246 +done
   1.247 +
   1.248 +lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
   1.249 +apply (subst strict_Ispair2)
   1.250 +apply (rule strict_Issnd)
   1.251 +apply (rule refl)
   1.252 +done
   1.253 +
   1.254 +lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
   1.255 +apply (unfold Isfst_def)
   1.256 +apply (rule some_equality)
   1.257 +apply (rule conjI)
   1.258 +apply (intro strip)
   1.259 +apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
   1.260 +apply (erule defined_Ispair)
   1.261 +apply assumption
   1.262 +apply assumption
   1.263 +apply (intro strip)
   1.264 +apply (rule inject_Ispair [THEN conjunct1])
   1.265 +prefer 3 apply fast
   1.266 +apply (fast+)
   1.267 +done
   1.268 +
   1.269 +lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
   1.270 +apply (unfold Issnd_def)
   1.271 +apply (rule some_equality)
   1.272 +apply (rule conjI)
   1.273 +apply (intro strip)
   1.274 +apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
   1.275 +apply (erule defined_Ispair)
   1.276 +apply assumption
   1.277 +apply assumption
   1.278 +apply (intro strip)
   1.279 +apply (rule inject_Ispair [THEN conjunct2])
   1.280 +prefer 3 apply fast
   1.281 +apply (fast+)
   1.282 +done
   1.283 +
   1.284 +lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
   1.285 +apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   1.286 +apply (erule Isfst)
   1.287 +apply assumption
   1.288 +apply (erule ssubst)
   1.289 +apply (rule strict_Isfst1)
   1.290 +done
   1.291 +
   1.292 +lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
   1.293 +apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
   1.294 +apply (erule Issnd)
   1.295 +apply assumption
   1.296 +apply (erule ssubst)
   1.297 +apply (rule strict_Issnd2)
   1.298 +done
   1.299 +
   1.300 +
   1.301 +(* ------------------------------------------------------------------------ *)
   1.302 +(* instantiate the simplifier                                               *)
   1.303 +(* ------------------------------------------------------------------------ *)
   1.304 +
   1.305 +lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
   1.306 +                 Isfst2 Issnd2
   1.307 +
   1.308 +declare Isfst2 [simp] Issnd2 [simp]
   1.309 +
   1.310 +lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
   1.311 +apply (rule_tac p = "p" in IsprodE)
   1.312 +apply simp
   1.313 +apply (erule ssubst)
   1.314 +apply (rule conjI)
   1.315 +apply (simp add: Sprod0_ss)
   1.316 +apply (simp add: Sprod0_ss)
   1.317 +done
   1.318 +
   1.319 +
   1.320 +(* ------------------------------------------------------------------------ *)
   1.321 +(* Surjective pairing: equivalent to Exh_Sprod                              *)
   1.322 +(* ------------------------------------------------------------------------ *)
   1.323 +
   1.324 +lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
   1.325 +apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
   1.326 +apply (simp add: Sprod0_ss)
   1.327 +apply (erule exE)
   1.328 +apply (erule exE)
   1.329 +apply (simp add: Sprod0_ss)
   1.330 +done
   1.331 +
   1.332 +lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
   1.333 +apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
   1.334 +apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
   1.335 +apply simp
   1.336 +done
   1.337 +
   1.338 +subsection {* The strict product is a partial order *}
   1.339 +
   1.340 +instance "**"::(sq_ord,sq_ord)sq_ord ..
   1.341 +
   1.342 +defs (overloaded)
   1.343 +  less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   1.344 +
   1.345 +(* ------------------------------------------------------------------------ *)
   1.346 +(* less_sprod is a partial order on Sprod                                   *)
   1.347 +(* ------------------------------------------------------------------------ *)
   1.348 +
   1.349 +lemma refl_less_sprod: "(p::'a ** 'b) << p"
   1.350 +apply (unfold less_sprod_def)
   1.351 +apply (fast intro: refl_less)
   1.352 +done
   1.353 +
   1.354 +lemma antisym_less_sprod: 
   1.355 +        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
   1.356 +apply (unfold less_sprod_def)
   1.357 +apply (rule Sel_injective_Sprod)
   1.358 +apply (fast intro: antisym_less)
   1.359 +apply (fast intro: antisym_less)
   1.360 +done
   1.361 +
   1.362 +lemma trans_less_sprod: 
   1.363 +        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
   1.364 +apply (unfold less_sprod_def)
   1.365 +apply (blast intro: trans_less)
   1.366 +done
   1.367 +
   1.368 +instance "**"::(pcpo,pcpo)po
   1.369 +by intro_classes
   1.370 +  (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
   1.371 +
   1.372 +(* for compatibility with old HOLCF-Version *)
   1.373 +lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
   1.374 +apply (fold less_sprod_def)
   1.375 +apply (rule refl)
   1.376 +done
   1.377 +
   1.378 +subsection {* The strict product is pointed *}
   1.379 +(* ------------------------------------------------------------------------ *)
   1.380 +(* type sprod is pointed                                                    *)
   1.381 +(* ------------------------------------------------------------------------ *)
   1.382 +(*
   1.383 +lemma minimal_sprod: "Ispair UU UU << p"
   1.384 +apply (simp add: inst_sprod_po minimal)
   1.385 +done
   1.386 +
   1.387 +lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
   1.388 +
   1.389 +lemma least_sprod: "? x::'a**'b.!y. x<<y"
   1.390 +apply (rule_tac x = "Ispair UU UU" in exI)
   1.391 +apply (rule minimal_sprod [THEN allI])
   1.392 +done
   1.393 +*)
   1.394 +(* ------------------------------------------------------------------------ *)
   1.395 +(* Ispair is monotone in both arguments                                     *)
   1.396 +(* ------------------------------------------------------------------------ *)
   1.397 +
   1.398 +lemma monofun_Ispair1: "monofun(Ispair)"
   1.399 +apply (unfold monofun)
   1.400 +apply (intro strip)
   1.401 +apply (rule less_fun [THEN iffD2])
   1.402 +apply (intro strip)
   1.403 +apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
   1.404 +apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   1.405 +apply (frule notUU_I)
   1.406 +apply assumption
   1.407 +apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
   1.408 +done
   1.409 +
   1.410 +lemma monofun_Ispair2: "monofun(Ispair(x))"
   1.411 +apply (unfold monofun)
   1.412 +apply (intro strip)
   1.413 +apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   1.414 +apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
   1.415 +apply (frule notUU_I)
   1.416 +apply assumption
   1.417 +apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
   1.418 +done
   1.419 +
   1.420 +lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   1.421 +apply (rule trans_less)
   1.422 +apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
   1.423 +prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
   1.424 +apply assumption
   1.425 +apply assumption
   1.426 +done
   1.427 +
   1.428 +(* ------------------------------------------------------------------------ *)
   1.429 +(* Isfst and Issnd are monotone                                             *)
   1.430 +(* ------------------------------------------------------------------------ *)
   1.431 +
   1.432 +lemma monofun_Isfst: "monofun(Isfst)"
   1.433 +apply (unfold monofun)
   1.434 +apply (simp add: inst_sprod_po)
   1.435 +done
   1.436 +
   1.437 +lemma monofun_Issnd: "monofun(Issnd)"
   1.438 +apply (unfold monofun)
   1.439 +apply (simp add: inst_sprod_po)
   1.440 +done
   1.441 +
   1.442 +subsection {* The strict product is a cpo *}
   1.443 +(* ------------------------------------------------------------------------ *)
   1.444 +(* the type 'a ** 'b is a cpo                                               *)
   1.445 +(* ------------------------------------------------------------------------ *)
   1.446 +
   1.447 +lemma lub_sprod: 
   1.448 +"[|chain(S)|] ==> range(S) <<|  
   1.449 +  Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
   1.450 +apply (rule is_lubI)
   1.451 +apply (rule ub_rangeI)
   1.452 +apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
   1.453 +apply (rule monofun_Ispair)
   1.454 +apply (rule is_ub_thelub)
   1.455 +apply (erule monofun_Isfst [THEN ch2ch_monofun])
   1.456 +apply (rule is_ub_thelub)
   1.457 +apply (erule monofun_Issnd [THEN ch2ch_monofun])
   1.458 +apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
   1.459 +apply (rule monofun_Ispair)
   1.460 +apply (rule is_lub_thelub)
   1.461 +apply (erule monofun_Isfst [THEN ch2ch_monofun])
   1.462 +apply (erule monofun_Isfst [THEN ub2ub_monofun])
   1.463 +apply (rule is_lub_thelub)
   1.464 +apply (erule monofun_Issnd [THEN ch2ch_monofun])
   1.465 +apply (erule monofun_Issnd [THEN ub2ub_monofun])
   1.466 +done
   1.467 +
   1.468 +lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
   1.469 +
   1.470 +lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
   1.471 +apply (rule exI)
   1.472 +apply (erule lub_sprod)
   1.473 +done
   1.474 +
   1.475 +instance "**" :: (pcpo, pcpo) cpo
   1.476 +by intro_classes (rule cpo_sprod)
   1.477 +
   1.478 +
   1.479 +subsection {* The strict product is a pcpo *}
   1.480 +
   1.481 +lemma minimal_sprod: "Ispair UU UU << p"
   1.482 +apply (simp add: inst_sprod_po minimal)
   1.483 +done
   1.484 +
   1.485 +lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
   1.486 +
   1.487 +lemma least_sprod: "? x::'a**'b.!y. x<<y"
   1.488 +apply (rule_tac x = "Ispair UU UU" in exI)
   1.489 +apply (rule minimal_sprod [THEN allI])
   1.490 +done
   1.491 +
   1.492 +instance "**" :: (pcpo, pcpo) pcpo
   1.493 +by intro_classes (rule least_sprod)
   1.494 +
   1.495 +
   1.496 +subsection {* Other constants *}
   1.497 +
   1.498 +consts  
   1.499 +  spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
   1.500 +  sfst		:: "('a**'b)->'a"
   1.501 +  ssnd		:: "('a**'b)->'b"
   1.502 +  ssplit	:: "('a->'b->'c)->('a**'b)->'c"
   1.503 +
   1.504 +syntax  
   1.505 +  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
   1.506 +
   1.507 +translations
   1.508 +        "(:x, y, z:)"   == "(:x, (:y, z:):)"
   1.509 +        "(:x, y:)"      == "spair$x$y"
   1.510 +
   1.511 +defs
   1.512 +spair_def:       "spair  == (LAM x y. Ispair x y)"
   1.513 +sfst_def:        "sfst   == (LAM p. Isfst p)"
   1.514 +ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
   1.515 +ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
   1.516 +
   1.517 +(* for compatibility with old HOLCF-Version *)
   1.518 +lemma inst_sprod_pcpo: "UU = Ispair UU UU"
   1.519 +apply (simp add: UU_def UU_sprod_def)
   1.520 +done
   1.521 +
   1.522 +declare inst_sprod_pcpo [symmetric, simp]
   1.523 +
   1.524 +(* ------------------------------------------------------------------------ *)
   1.525 +(* continuity of Ispair, Isfst, Issnd                                       *)
   1.526 +(* ------------------------------------------------------------------------ *)
   1.527 +
   1.528 +lemma sprod3_lemma1: 
   1.529 +"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
   1.530 +  Ispair (lub(range Y)) x = 
   1.531 +  Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
   1.532 +         (lub(range(%i. Issnd(Ispair(Y i) x))))"
   1.533 +apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
   1.534 +apply (rule lub_equal)
   1.535 +apply assumption
   1.536 +apply (rule monofun_Isfst [THEN ch2ch_monofun])
   1.537 +apply (rule ch2ch_fun)
   1.538 +apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
   1.539 +apply assumption
   1.540 +apply (rule allI)
   1.541 +apply (simp (no_asm_simp))
   1.542 +apply (rule sym)
   1.543 +apply (drule chain_UU_I_inverse2)
   1.544 +apply (erule exE)
   1.545 +apply (rule lub_chain_maxelem)
   1.546 +apply (erule Issnd2)
   1.547 +apply (rule allI)
   1.548 +apply (rename_tac "j")
   1.549 +apply (case_tac "Y (j) =UU")
   1.550 +apply auto
   1.551 +done
   1.552 +
   1.553 +lemma sprod3_lemma2: 
   1.554 +"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
   1.555 +    Ispair (lub(range Y)) x = 
   1.556 +    Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
   1.557 +           (lub(range(%i. Issnd(Ispair(Y i) x))))"
   1.558 +apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
   1.559 +apply assumption
   1.560 +apply (rule trans)
   1.561 +apply (rule strict_Ispair1)
   1.562 +apply (rule strict_Ispair [symmetric])
   1.563 +apply (rule disjI1)
   1.564 +apply (rule chain_UU_I_inverse)
   1.565 +apply auto
   1.566 +apply (erule chain_UU_I [THEN spec])
   1.567 +apply assumption
   1.568 +done
   1.569 +
   1.570 +
   1.571 +lemma sprod3_lemma3: 
   1.572 +"[| chain(Y); x = UU |] ==> 
   1.573 +           Ispair (lub(range Y)) x = 
   1.574 +           Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
   1.575 +                  (lub(range(%i. Issnd(Ispair (Y i) x))))"
   1.576 +apply (erule ssubst)
   1.577 +apply (rule trans)
   1.578 +apply (rule strict_Ispair2)
   1.579 +apply (rule strict_Ispair [symmetric])
   1.580 +apply (rule disjI1)
   1.581 +apply (rule chain_UU_I_inverse)
   1.582 +apply (rule allI)
   1.583 +apply (simp add: Sprod0_ss)
   1.584 +done
   1.585 +
   1.586 +lemma contlub_Ispair1: "contlub(Ispair)"
   1.587 +apply (rule contlubI)
   1.588 +apply (intro strip)
   1.589 +apply (rule expand_fun_eq [THEN iffD2])
   1.590 +apply (intro strip)
   1.591 +apply (subst lub_fun [THEN thelubI])
   1.592 +apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
   1.593 +apply (rule trans)
   1.594 +apply (rule_tac [2] thelub_sprod [symmetric])
   1.595 +apply (rule_tac [2] ch2ch_fun)
   1.596 +apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
   1.597 +apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   1.598 +apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
   1.599 +apply (erule sprod3_lemma1)
   1.600 +apply assumption
   1.601 +apply assumption
   1.602 +apply (erule sprod3_lemma2)
   1.603 +apply assumption
   1.604 +apply assumption
   1.605 +apply (erule sprod3_lemma3)
   1.606 +apply assumption
   1.607 +done
   1.608 +
   1.609 +lemma sprod3_lemma4: 
   1.610 +"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
   1.611 +          Ispair x (lub(range Y)) = 
   1.612 +          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
   1.613 +                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
   1.614 +apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
   1.615 +apply (rule sym)
   1.616 +apply (drule chain_UU_I_inverse2)
   1.617 +apply (erule exE)
   1.618 +apply (rule lub_chain_maxelem)
   1.619 +apply (erule Isfst2)
   1.620 +apply (rule allI)
   1.621 +apply (rename_tac "j")
   1.622 +apply (case_tac "Y (j) =UU")
   1.623 +apply auto
   1.624 +done
   1.625 +
   1.626 +lemma sprod3_lemma5: 
   1.627 +"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
   1.628 +          Ispair x (lub(range Y)) = 
   1.629 +          Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
   1.630 +                 (lub(range(%i. Issnd(Ispair x (Y i)))))"
   1.631 +apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
   1.632 +apply assumption
   1.633 +apply (rule trans)
   1.634 +apply (rule strict_Ispair2)
   1.635 +apply (rule strict_Ispair [symmetric])
   1.636 +apply (rule disjI2)
   1.637 +apply (rule chain_UU_I_inverse)
   1.638 +apply (rule allI)
   1.639 +apply (simp add: Sprod0_ss)
   1.640 +apply (erule chain_UU_I [THEN spec])
   1.641 +apply assumption
   1.642 +done
   1.643 +
   1.644 +lemma sprod3_lemma6: 
   1.645 +"[| chain(Y); x = UU |] ==> 
   1.646 +          Ispair x (lub(range Y)) = 
   1.647 +          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
   1.648 +                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
   1.649 +apply (rule_tac s = "UU" and t = "x" in ssubst)
   1.650 +apply assumption
   1.651 +apply (rule trans)
   1.652 +apply (rule strict_Ispair1)
   1.653 +apply (rule strict_Ispair [symmetric])
   1.654 +apply (rule disjI1)
   1.655 +apply (rule chain_UU_I_inverse)
   1.656 +apply (rule allI)
   1.657 +apply (simp add: Sprod0_ss)
   1.658 +done
   1.659 +
   1.660 +lemma contlub_Ispair2: "contlub(Ispair(x))"
   1.661 +apply (rule contlubI)
   1.662 +apply (intro strip)
   1.663 +apply (rule trans)
   1.664 +apply (rule_tac [2] thelub_sprod [symmetric])
   1.665 +apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
   1.666 +apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
   1.667 +apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
   1.668 +apply (erule sprod3_lemma4)
   1.669 +apply assumption
   1.670 +apply assumption
   1.671 +apply (erule sprod3_lemma5)
   1.672 +apply assumption
   1.673 +apply assumption
   1.674 +apply (erule sprod3_lemma6)
   1.675 +apply assumption
   1.676 +done
   1.677 +
   1.678 +lemma cont_Ispair1: "cont(Ispair)"
   1.679 +apply (rule monocontlub2cont)
   1.680 +apply (rule monofun_Ispair1)
   1.681 +apply (rule contlub_Ispair1)
   1.682 +done
   1.683 +
   1.684 +lemma cont_Ispair2: "cont(Ispair(x))"
   1.685 +apply (rule monocontlub2cont)
   1.686 +apply (rule monofun_Ispair2)
   1.687 +apply (rule contlub_Ispair2)
   1.688 +done
   1.689 +
   1.690 +lemma contlub_Isfst: "contlub(Isfst)"
   1.691 +apply (rule contlubI)
   1.692 +apply (intro strip)
   1.693 +apply (subst lub_sprod [THEN thelubI])
   1.694 +apply assumption
   1.695 +apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
   1.696 +apply (simp add: Sprod0_ss)
   1.697 +apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
   1.698 +apply assumption
   1.699 +apply (rule trans)
   1.700 +apply (simp add: Sprod0_ss)
   1.701 +apply (rule sym)
   1.702 +apply (rule chain_UU_I_inverse)
   1.703 +apply (rule allI)
   1.704 +apply (rule strict_Isfst)
   1.705 +apply (rule contrapos_np)
   1.706 +apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
   1.707 +apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
   1.708 +done
   1.709 +
   1.710 +lemma contlub_Issnd: "contlub(Issnd)"
   1.711 +apply (rule contlubI)
   1.712 +apply (intro strip)
   1.713 +apply (subst lub_sprod [THEN thelubI])
   1.714 +apply assumption
   1.715 +apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
   1.716 +apply (simp add: Sprod0_ss)
   1.717 +apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
   1.718 +apply assumption
   1.719 +apply (simp add: Sprod0_ss)
   1.720 +apply (rule sym)
   1.721 +apply (rule chain_UU_I_inverse)
   1.722 +apply (rule allI)
   1.723 +apply (rule strict_Issnd)
   1.724 +apply (rule contrapos_np)
   1.725 +apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
   1.726 +apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
   1.727 +done
   1.728 +
   1.729 +lemma cont_Isfst: "cont(Isfst)"
   1.730 +apply (rule monocontlub2cont)
   1.731 +apply (rule monofun_Isfst)
   1.732 +apply (rule contlub_Isfst)
   1.733 +done
   1.734 +
   1.735 +lemma cont_Issnd: "cont(Issnd)"
   1.736 +apply (rule monocontlub2cont)
   1.737 +apply (rule monofun_Issnd)
   1.738 +apply (rule contlub_Issnd)
   1.739 +done
   1.740 +
   1.741 +lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
   1.742 +apply fast
   1.743 +done
   1.744 +
   1.745 +(* ------------------------------------------------------------------------ *)
   1.746 +(* convert all lemmas to the continuous versions                            *)
   1.747 +(* ------------------------------------------------------------------------ *)
   1.748 +
   1.749 +lemma beta_cfun_sprod [simp]: 
   1.750 +        "(LAM x y. Ispair x y)$a$b = Ispair a b"
   1.751 +apply (subst beta_cfun)
   1.752 +apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
   1.753 +apply (subst beta_cfun)
   1.754 +apply (rule cont_Ispair2)
   1.755 +apply (rule refl)
   1.756 +done
   1.757 +
   1.758 +lemma inject_spair: 
   1.759 +        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
   1.760 +apply (unfold spair_def)
   1.761 +apply (erule inject_Ispair)
   1.762 +apply assumption
   1.763 +apply (erule box_equals)
   1.764 +apply (rule beta_cfun_sprod)
   1.765 +apply (rule beta_cfun_sprod)
   1.766 +done
   1.767 +
   1.768 +lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
   1.769 +apply (unfold spair_def)
   1.770 +apply (rule sym)
   1.771 +apply (rule trans)
   1.772 +apply (rule beta_cfun_sprod)
   1.773 +apply (rule sym)
   1.774 +apply (rule inst_sprod_pcpo)
   1.775 +done
   1.776 +
   1.777 +lemma strict_spair: 
   1.778 +        "(a=UU | b=UU) ==> (:a,b:)=UU"
   1.779 +apply (unfold spair_def)
   1.780 +apply (rule trans)
   1.781 +apply (rule beta_cfun_sprod)
   1.782 +apply (rule trans)
   1.783 +apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   1.784 +apply (erule strict_Ispair)
   1.785 +done
   1.786 +
   1.787 +lemma strict_spair1: "(:UU,b:) = UU"
   1.788 +apply (unfold spair_def)
   1.789 +apply (subst beta_cfun_sprod)
   1.790 +apply (rule trans)
   1.791 +apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   1.792 +apply (rule strict_Ispair1)
   1.793 +done
   1.794 +
   1.795 +lemma strict_spair2: "(:a,UU:) = UU"
   1.796 +apply (unfold spair_def)
   1.797 +apply (subst beta_cfun_sprod)
   1.798 +apply (rule trans)
   1.799 +apply (rule_tac [2] inst_sprod_pcpo [symmetric])
   1.800 +apply (rule strict_Ispair2)
   1.801 +done
   1.802 +
   1.803 +declare strict_spair1 [simp] strict_spair2 [simp]
   1.804 +
   1.805 +lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
   1.806 +apply (unfold spair_def)
   1.807 +apply (rule strict_Ispair_rev)
   1.808 +apply auto
   1.809 +done
   1.810 +
   1.811 +lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
   1.812 +apply (unfold spair_def)
   1.813 +apply (rule defined_Ispair_rev)
   1.814 +apply auto
   1.815 +done
   1.816 +
   1.817 +lemma defined_spair: 
   1.818 +        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
   1.819 +apply (unfold spair_def)
   1.820 +apply (subst beta_cfun_sprod)
   1.821 +apply (subst inst_sprod_pcpo)
   1.822 +apply (erule defined_Ispair)
   1.823 +apply assumption
   1.824 +done
   1.825 +
   1.826 +lemma Exh_Sprod2:
   1.827 +        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
   1.828 +apply (unfold spair_def)
   1.829 +apply (rule Exh_Sprod [THEN disjE])
   1.830 +apply (rule disjI1)
   1.831 +apply (subst inst_sprod_pcpo)
   1.832 +apply assumption
   1.833 +apply (rule disjI2)
   1.834 +apply (erule exE)
   1.835 +apply (erule exE)
   1.836 +apply (rule exI)
   1.837 +apply (rule exI)
   1.838 +apply (rule conjI)
   1.839 +apply (subst beta_cfun_sprod)
   1.840 +apply fast
   1.841 +apply fast
   1.842 +done
   1.843 +
   1.844 +
   1.845 +lemma sprodE:
   1.846 +assumes prem1: "p=UU ==> Q"
   1.847 +assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
   1.848 +shows "Q"
   1.849 +apply (rule IsprodE)
   1.850 +apply (rule prem1)
   1.851 +apply (subst inst_sprod_pcpo)
   1.852 +apply assumption
   1.853 +apply (rule prem2)
   1.854 +prefer 2 apply (assumption)
   1.855 +prefer 2 apply (assumption)
   1.856 +apply (unfold spair_def)
   1.857 +apply (subst beta_cfun_sprod)
   1.858 +apply assumption
   1.859 +done
   1.860 +
   1.861 +
   1.862 +lemma strict_sfst: 
   1.863 +        "p=UU==>sfst$p=UU"
   1.864 +apply (unfold sfst_def)
   1.865 +apply (subst beta_cfun)
   1.866 +apply (rule cont_Isfst)
   1.867 +apply (rule strict_Isfst)
   1.868 +apply (rule inst_sprod_pcpo [THEN subst])
   1.869 +apply assumption
   1.870 +done
   1.871 +
   1.872 +lemma strict_sfst1: 
   1.873 +        "sfst$(:UU,y:) = UU"
   1.874 +apply (unfold sfst_def spair_def)
   1.875 +apply (subst beta_cfun_sprod)
   1.876 +apply (subst beta_cfun)
   1.877 +apply (rule cont_Isfst)
   1.878 +apply (rule strict_Isfst1)
   1.879 +done
   1.880 + 
   1.881 +lemma strict_sfst2: 
   1.882 +        "sfst$(:x,UU:) = UU"
   1.883 +apply (unfold sfst_def spair_def)
   1.884 +apply (subst beta_cfun_sprod)
   1.885 +apply (subst beta_cfun)
   1.886 +apply (rule cont_Isfst)
   1.887 +apply (rule strict_Isfst2)
   1.888 +done
   1.889 +
   1.890 +lemma strict_ssnd: 
   1.891 +        "p=UU==>ssnd$p=UU"
   1.892 +apply (unfold ssnd_def)
   1.893 +apply (subst beta_cfun)
   1.894 +apply (rule cont_Issnd)
   1.895 +apply (rule strict_Issnd)
   1.896 +apply (rule inst_sprod_pcpo [THEN subst])
   1.897 +apply assumption
   1.898 +done
   1.899 +
   1.900 +lemma strict_ssnd1: 
   1.901 +        "ssnd$(:UU,y:) = UU"
   1.902 +apply (unfold ssnd_def spair_def)
   1.903 +apply (subst beta_cfun_sprod)
   1.904 +apply (subst beta_cfun)
   1.905 +apply (rule cont_Issnd)
   1.906 +apply (rule strict_Issnd1)
   1.907 +done
   1.908 +
   1.909 +lemma strict_ssnd2: 
   1.910 +        "ssnd$(:x,UU:) = UU"
   1.911 +apply (unfold ssnd_def spair_def)
   1.912 +apply (subst beta_cfun_sprod)
   1.913 +apply (subst beta_cfun)
   1.914 +apply (rule cont_Issnd)
   1.915 +apply (rule strict_Issnd2)
   1.916 +done
   1.917 +
   1.918 +lemma sfst2: 
   1.919 +        "y~=UU ==>sfst$(:x,y:)=x"
   1.920 +apply (unfold sfst_def spair_def)
   1.921 +apply (subst beta_cfun_sprod)
   1.922 +apply (subst beta_cfun)
   1.923 +apply (rule cont_Isfst)
   1.924 +apply (erule Isfst2)
   1.925 +done
   1.926 +
   1.927 +lemma ssnd2: 
   1.928 +        "x~=UU ==>ssnd$(:x,y:)=y"
   1.929 +apply (unfold ssnd_def spair_def)
   1.930 +apply (subst beta_cfun_sprod)
   1.931 +apply (subst beta_cfun)
   1.932 +apply (rule cont_Issnd)
   1.933 +apply (erule Issnd2)
   1.934 +done
   1.935 +
   1.936 +
   1.937 +lemma defined_sfstssnd: 
   1.938 +        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
   1.939 +apply (unfold sfst_def ssnd_def spair_def)
   1.940 +apply (simplesubst beta_cfun)
   1.941 +apply (rule cont_Issnd)
   1.942 +apply (subst beta_cfun)
   1.943 +apply (rule cont_Isfst)
   1.944 +apply (rule defined_IsfstIssnd)
   1.945 +apply (rule inst_sprod_pcpo [THEN subst])
   1.946 +apply assumption
   1.947 +done
   1.948 + 
   1.949 +lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
   1.950 +apply (unfold sfst_def ssnd_def spair_def)
   1.951 +apply (subst beta_cfun_sprod)
   1.952 +apply (simplesubst beta_cfun)
   1.953 +apply (rule cont_Issnd)
   1.954 +apply (subst beta_cfun)
   1.955 +apply (rule cont_Isfst)
   1.956 +apply (rule surjective_pairing_Sprod [symmetric])
   1.957 +done
   1.958 +
   1.959 +lemma lub_sprod2: 
   1.960 +"chain(S) ==> range(S) <<|  
   1.961 +               (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
   1.962 +apply (unfold sfst_def ssnd_def spair_def)
   1.963 +apply (subst beta_cfun_sprod)
   1.964 +apply (simplesubst beta_cfun [THEN ext])
   1.965 +apply (rule cont_Issnd)
   1.966 +apply (subst beta_cfun [THEN ext])
   1.967 +apply (rule cont_Isfst)
   1.968 +apply (erule lub_sprod)
   1.969 +done
   1.970 +
   1.971 +
   1.972 +lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
   1.973 +(*
   1.974 + "chain ?S1 ==>
   1.975 + lub (range ?S1) =
   1.976 + (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
   1.977 +*)
   1.978 +
   1.979 +lemma ssplit1: 
   1.980 +        "ssplit$f$UU=UU"
   1.981 +apply (unfold ssplit_def)
   1.982 +apply (subst beta_cfun)
   1.983 +apply (simp (no_asm))
   1.984 +apply (subst strictify1)
   1.985 +apply (rule refl)
   1.986 +done
   1.987 +
   1.988 +lemma ssplit2: 
   1.989 +        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
   1.990 +apply (unfold ssplit_def)
   1.991 +apply (subst beta_cfun)
   1.992 +apply (simp (no_asm))
   1.993 +apply (subst strictify2)
   1.994 +apply (rule defined_spair)
   1.995 +apply assumption
   1.996 +apply assumption
   1.997 +apply (subst beta_cfun)
   1.998 +apply (simp (no_asm))
   1.999 +apply (subst sfst2)
  1.1000 +apply assumption
  1.1001 +apply (subst ssnd2)
  1.1002 +apply assumption
  1.1003 +apply (rule refl)
  1.1004 +done
  1.1005 +
  1.1006 +
  1.1007 +lemma ssplit3: 
  1.1008 +  "ssplit$spair$z=z"
  1.1009 +apply (unfold ssplit_def)
  1.1010 +apply (subst beta_cfun)
  1.1011 +apply (simp (no_asm))
  1.1012 +apply (case_tac "z=UU")
  1.1013 +apply (erule ssubst)
  1.1014 +apply (rule strictify1)
  1.1015 +apply (rule trans)
  1.1016 +apply (rule strictify2)
  1.1017 +apply assumption
  1.1018 +apply (subst beta_cfun)
  1.1019 +apply (simp (no_asm))
  1.1020 +apply (rule surjective_pairing_Sprod2)
  1.1021 +done
  1.1022 +
  1.1023 +(* ------------------------------------------------------------------------ *)
  1.1024 +(* install simplifier for Sprod                                             *)
  1.1025 +(* ------------------------------------------------------------------------ *)
  1.1026 +
  1.1027 +lemmas Sprod_rews = strict_sfst1 strict_sfst2
  1.1028 +                strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
  1.1029 +                ssplit1 ssplit2
  1.1030 +declare Sprod_rews [simp]
  1.1031 +
  1.1032 +end