reordered and arranged for document generation, cleaned up some proofs
authorhuffman
Tue Mar 08 00:18:22 2005 +0100 (2005-03-08)
changeset 1559150c3384ca6c4
parent 15590 17f4f5afcd5f
child 15592 40088b01f257
reordered and arranged for document generation, cleaned up some proofs
src/HOLCF/Sprod.thy
     1.1 --- a/src/HOLCF/Sprod.thy	Tue Mar 08 00:15:01 2005 +0100
     1.2 +++ b/src/HOLCF/Sprod.thy	Tue Mar 08 00:18:22 2005 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4  imports Cfun
     1.5  begin
     1.6  
     1.7 +subsection {* Definition of strict product type *}
     1.8 +
     1.9  constdefs
    1.10    Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
    1.11   "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
    1.12 @@ -24,8 +26,6 @@
    1.13  syntax (HTML output)
    1.14    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    1.15  
    1.16 -subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
    1.17 -
    1.18  consts
    1.19    Ispair        :: "['a,'b] => ('a ** 'b)"
    1.20    Isfst         :: "('a ** 'b) => 'a"
    1.21 @@ -42,9 +42,7 @@
    1.22    Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
    1.23                  &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
    1.24  
    1.25 -(* ------------------------------------------------------------------------ *)
    1.26 -(* A non-emptyness result for Sprod                                         *)
    1.27 -(* ------------------------------------------------------------------------ *)
    1.28 +text {* A non-emptiness result for Sprod *}
    1.29  
    1.30  lemma SprodI: "(Spair_Rep a b):Sprod"
    1.31  apply (unfold Sprod_def)
    1.32 @@ -56,9 +54,7 @@
    1.33  apply (erule Abs_Sprod_inverse)
    1.34  done
    1.35  
    1.36 -(* ------------------------------------------------------------------------ *)
    1.37 -(* Strictness and definedness of Spair_Rep                                  *)
    1.38 -(* ------------------------------------------------------------------------ *)
    1.39 +text {* Strictness and definedness of @{term Spair_Rep} *}
    1.40  
    1.41  lemma strict_Spair_Rep: 
    1.42   "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
    1.43 @@ -78,9 +74,7 @@
    1.44  apply (fast dest: fun_cong)
    1.45  done
    1.46  
    1.47 -(* ------------------------------------------------------------------------ *)
    1.48 -(* injectivity of Spair_Rep and Ispair                                      *)
    1.49 -(* ------------------------------------------------------------------------ *)
    1.50 +text {* injectivity of @{term Spair_Rep} and @{term Ispair} *}
    1.51  
    1.52  lemma inject_Spair_Rep: 
    1.53  "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
    1.54 @@ -102,9 +96,7 @@
    1.55  apply (rule SprodI)
    1.56  done
    1.57  
    1.58 -(* ------------------------------------------------------------------------ *)
    1.59 -(* strictness and definedness of Ispair                                     *)
    1.60 -(* ------------------------------------------------------------------------ *)
    1.61 +text {* strictness and definedness of @{term Ispair} *}
    1.62  
    1.63  lemma strict_Ispair: 
    1.64   "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
    1.65 @@ -152,10 +144,7 @@
    1.66  apply assumption
    1.67  done
    1.68  
    1.69 -
    1.70 -(* ------------------------------------------------------------------------ *)
    1.71 -(* Exhaustion of the strict product **                                      *)
    1.72 -(* ------------------------------------------------------------------------ *)
    1.73 +text {* Exhaustion of the strict product @{typ "'a ** 'b"} *}
    1.74  
    1.75  lemma Exh_Sprod:
    1.76          "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
    1.77 @@ -179,9 +168,7 @@
    1.78  apply (erule strict_Spair_Rep)
    1.79  done
    1.80  
    1.81 -(* ------------------------------------------------------------------------ *)
    1.82 -(* general elimination rule for strict product                              *)
    1.83 -(* ------------------------------------------------------------------------ *)
    1.84 +text {* general elimination rule for strict product *}
    1.85  
    1.86  lemma IsprodE:
    1.87  assumes prem1: "p=Ispair UU UU ==> Q"
    1.88 @@ -198,9 +185,7 @@
    1.89  apply assumption
    1.90  done
    1.91  
    1.92 -(* ------------------------------------------------------------------------ *)
    1.93 -(* some results about the selectors Isfst, Issnd                            *)
    1.94 -(* ------------------------------------------------------------------------ *)
    1.95 +text {* some results about the selectors @{term Isfst}, @{term Issnd} *}
    1.96  
    1.97  lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
    1.98  apply (unfold Isfst_def)
    1.99 @@ -297,9 +282,7 @@
   1.100  done
   1.101  
   1.102  
   1.103 -(* ------------------------------------------------------------------------ *)
   1.104 -(* instantiate the simplifier                                               *)
   1.105 -(* ------------------------------------------------------------------------ *)
   1.106 +text {* instantiate the simplifier *}
   1.107  
   1.108  lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
   1.109                   Isfst2 Issnd2
   1.110 @@ -316,9 +299,7 @@
   1.111  done
   1.112  
   1.113  
   1.114 -(* ------------------------------------------------------------------------ *)
   1.115 -(* Surjective pairing: equivalent to Exh_Sprod                              *)
   1.116 -(* ------------------------------------------------------------------------ *)
   1.117 +text {* Surjective pairing: equivalent to @{thm [source] Exh_Sprod} *}
   1.118  
   1.119  lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
   1.120  apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
   1.121 @@ -334,17 +315,13 @@
   1.122  apply simp
   1.123  done
   1.124  
   1.125 -subsection {* The strict product is a partial order *}
   1.126 +subsection {* Type @{typ "'a ** 'b"} is a partial order *}
   1.127  
   1.128 -instance "**"::(sq_ord,sq_ord)sq_ord ..
   1.129 +instance "**" :: (sq_ord, sq_ord) sq_ord ..
   1.130  
   1.131  defs (overloaded)
   1.132    less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
   1.133  
   1.134 -(* ------------------------------------------------------------------------ *)
   1.135 -(* less_sprod is a partial order on Sprod                                   *)
   1.136 -(* ------------------------------------------------------------------------ *)
   1.137 -
   1.138  lemma refl_less_sprod: "(p::'a ** 'b) << p"
   1.139  apply (unfold less_sprod_def)
   1.140  apply (fast intro: refl_less)
   1.141 @@ -359,40 +336,24 @@
   1.142  done
   1.143  
   1.144  lemma trans_less_sprod: 
   1.145 -        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
   1.146 +        "[|(p1::'a ** 'b) << p2;p2 << p3|] ==> p1 << p3"
   1.147  apply (unfold less_sprod_def)
   1.148  apply (blast intro: trans_less)
   1.149  done
   1.150  
   1.151 -instance "**"::(pcpo,pcpo)po
   1.152 +instance "**" :: (pcpo, pcpo) po
   1.153  by intro_classes
   1.154    (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
   1.155  
   1.156 -(* for compatibility with old HOLCF-Version *)
   1.157 +text {* for compatibility with old HOLCF-Version *}
   1.158  lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
   1.159  apply (fold less_sprod_def)
   1.160  apply (rule refl)
   1.161  done
   1.162  
   1.163 -subsection {* The strict product is pointed *}
   1.164 -(* ------------------------------------------------------------------------ *)
   1.165 -(* type sprod is pointed                                                    *)
   1.166 -(* ------------------------------------------------------------------------ *)
   1.167 -(*
   1.168 -lemma minimal_sprod: "Ispair UU UU << p"
   1.169 -apply (simp add: inst_sprod_po minimal)
   1.170 -done
   1.171 +subsection {* Monotonicity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
   1.172  
   1.173 -lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
   1.174 -
   1.175 -lemma least_sprod: "? x::'a**'b.!y. x<<y"
   1.176 -apply (rule_tac x = "Ispair UU UU" in exI)
   1.177 -apply (rule minimal_sprod [THEN allI])
   1.178 -done
   1.179 -*)
   1.180 -(* ------------------------------------------------------------------------ *)
   1.181 -(* Ispair is monotone in both arguments                                     *)
   1.182 -(* ------------------------------------------------------------------------ *)
   1.183 +text {* @{term Ispair} is monotone in both arguments *}
   1.184  
   1.185  lemma monofun_Ispair1: "monofun(Ispair)"
   1.186  apply (unfold monofun)
   1.187 @@ -424,24 +385,15 @@
   1.188  apply assumption
   1.189  done
   1.190  
   1.191 -(* ------------------------------------------------------------------------ *)
   1.192 -(* Isfst and Issnd are monotone                                             *)
   1.193 -(* ------------------------------------------------------------------------ *)
   1.194 +text {* @{term Isfst} and @{term Issnd} are monotone *}
   1.195  
   1.196  lemma monofun_Isfst: "monofun(Isfst)"
   1.197 -apply (unfold monofun)
   1.198 -apply (simp add: inst_sprod_po)
   1.199 -done
   1.200 +by (simp add: monofun inst_sprod_po)
   1.201  
   1.202  lemma monofun_Issnd: "monofun(Issnd)"
   1.203 -apply (unfold monofun)
   1.204 -apply (simp add: inst_sprod_po)
   1.205 -done
   1.206 +by (simp add: monofun inst_sprod_po)
   1.207  
   1.208 -subsection {* The strict product is a cpo *}
   1.209 -(* ------------------------------------------------------------------------ *)
   1.210 -(* the type 'a ** 'b is a cpo                                               *)
   1.211 -(* ------------------------------------------------------------------------ *)
   1.212 +subsection {* Type @{typ "'a ** 'b"} is a cpo *}
   1.213  
   1.214  lemma lub_sprod: 
   1.215  "[|chain(S)|] ==> range(S) <<|  
   1.216 @@ -474,8 +426,7 @@
   1.217  instance "**" :: (pcpo, pcpo) cpo
   1.218  by intro_classes (rule cpo_sprod)
   1.219  
   1.220 -
   1.221 -subsection {* The strict product is a pcpo *}
   1.222 +subsection {* Type @{typ "'a ** 'b"} is pointed *}
   1.223  
   1.224  lemma minimal_sprod: "Ispair UU UU << p"
   1.225  apply (simp add: inst_sprod_po minimal)
   1.226 @@ -491,8 +442,13 @@
   1.227  instance "**" :: (pcpo, pcpo) pcpo
   1.228  by intro_classes (rule least_sprod)
   1.229  
   1.230 +text {* for compatibility with old HOLCF-Version *}
   1.231 +lemma inst_sprod_pcpo: "UU = Ispair UU UU"
   1.232 +by (simp add: UU_def UU_sprod_def)
   1.233  
   1.234 -subsection {* Other constants *}
   1.235 +declare inst_sprod_pcpo [symmetric, simp]
   1.236 +
   1.237 +subsection {* Continuous versions of constants *}
   1.238  
   1.239  consts  
   1.240    spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
   1.241 @@ -513,16 +469,7 @@
   1.242  ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
   1.243  ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
   1.244  
   1.245 -(* for compatibility with old HOLCF-Version *)
   1.246 -lemma inst_sprod_pcpo: "UU = Ispair UU UU"
   1.247 -apply (simp add: UU_def UU_sprod_def)
   1.248 -done
   1.249 -
   1.250 -declare inst_sprod_pcpo [symmetric, simp]
   1.251 -
   1.252 -(* ------------------------------------------------------------------------ *)
   1.253 -(* continuity of Ispair, Isfst, Issnd                                       *)
   1.254 -(* ------------------------------------------------------------------------ *)
   1.255 +subsection {* Continuity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
   1.256  
   1.257  lemma sprod3_lemma1: 
   1.258  "[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
   1.259 @@ -741,9 +688,7 @@
   1.260  apply fast
   1.261  done
   1.262  
   1.263 -(* ------------------------------------------------------------------------ *)
   1.264 -(* convert all lemmas to the continuous versions                            *)
   1.265 -(* ------------------------------------------------------------------------ *)
   1.266 +text {* convert all lemmas to the continuous versions *}
   1.267  
   1.268  lemma beta_cfun_sprod [simp]: 
   1.269          "(LAM x y. Ispair x y)$a$b = Ispair a b"
   1.270 @@ -813,7 +758,7 @@
   1.271  apply auto
   1.272  done
   1.273  
   1.274 -lemma defined_spair: 
   1.275 +lemma defined_spair [simp]: 
   1.276          "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
   1.277  apply (unfold spair_def)
   1.278  apply (subst beta_cfun_sprod)
   1.279 @@ -840,7 +785,6 @@
   1.280  apply fast
   1.281  done
   1.282  
   1.283 -
   1.284  lemma sprodE:
   1.285  assumes prem1: "p=UU ==> Q"
   1.286  assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
   1.287 @@ -857,9 +801,7 @@
   1.288  apply assumption
   1.289  done
   1.290  
   1.291 -
   1.292 -lemma strict_sfst: 
   1.293 -        "p=UU==>sfst$p=UU"
   1.294 +lemma strict_sfst: "p=UU==>sfst$p=UU"
   1.295  apply (unfold sfst_def)
   1.296  apply (subst beta_cfun)
   1.297  apply (rule cont_Isfst)
   1.298 @@ -868,17 +810,15 @@
   1.299  apply assumption
   1.300  done
   1.301  
   1.302 -lemma strict_sfst1: 
   1.303 -        "sfst$(:UU,y:) = UU"
   1.304 +lemma strict_sfst1 [simp]: "sfst$(:UU,y:) = UU"
   1.305  apply (unfold sfst_def spair_def)
   1.306  apply (subst beta_cfun_sprod)
   1.307  apply (subst beta_cfun)
   1.308  apply (rule cont_Isfst)
   1.309  apply (rule strict_Isfst1)
   1.310  done
   1.311 - 
   1.312 -lemma strict_sfst2: 
   1.313 -        "sfst$(:x,UU:) = UU"
   1.314 +
   1.315 +lemma strict_sfst2 [simp]: "sfst$(:x,UU:) = UU"
   1.316  apply (unfold sfst_def spair_def)
   1.317  apply (subst beta_cfun_sprod)
   1.318  apply (subst beta_cfun)
   1.319 @@ -886,8 +826,7 @@
   1.320  apply (rule strict_Isfst2)
   1.321  done
   1.322  
   1.323 -lemma strict_ssnd: 
   1.324 -        "p=UU==>ssnd$p=UU"
   1.325 +lemma strict_ssnd: "p=UU==>ssnd$p=UU"
   1.326  apply (unfold ssnd_def)
   1.327  apply (subst beta_cfun)
   1.328  apply (rule cont_Issnd)
   1.329 @@ -896,8 +835,7 @@
   1.330  apply assumption
   1.331  done
   1.332  
   1.333 -lemma strict_ssnd1: 
   1.334 -        "ssnd$(:UU,y:) = UU"
   1.335 +lemma strict_ssnd1 [simp]: "ssnd$(:UU,y:) = UU"
   1.336  apply (unfold ssnd_def spair_def)
   1.337  apply (subst beta_cfun_sprod)
   1.338  apply (subst beta_cfun)
   1.339 @@ -905,8 +843,7 @@
   1.340  apply (rule strict_Issnd1)
   1.341  done
   1.342  
   1.343 -lemma strict_ssnd2: 
   1.344 -        "ssnd$(:x,UU:) = UU"
   1.345 +lemma strict_ssnd2 [simp]: "ssnd$(:x,UU:) = UU"
   1.346  apply (unfold ssnd_def spair_def)
   1.347  apply (subst beta_cfun_sprod)
   1.348  apply (subst beta_cfun)
   1.349 @@ -914,8 +851,7 @@
   1.350  apply (rule strict_Issnd2)
   1.351  done
   1.352  
   1.353 -lemma sfst2: 
   1.354 -        "y~=UU ==>sfst$(:x,y:)=x"
   1.355 +lemma sfst2 [simp]: "y~=UU ==>sfst$(:x,y:)=x"
   1.356  apply (unfold sfst_def spair_def)
   1.357  apply (subst beta_cfun_sprod)
   1.358  apply (subst beta_cfun)
   1.359 @@ -923,8 +859,7 @@
   1.360  apply (erule Isfst2)
   1.361  done
   1.362  
   1.363 -lemma ssnd2: 
   1.364 -        "x~=UU ==>ssnd$(:x,y:)=y"
   1.365 +lemma ssnd2 [simp]: "x~=UU ==>ssnd$(:x,y:)=y"
   1.366  apply (unfold ssnd_def spair_def)
   1.367  apply (subst beta_cfun_sprod)
   1.368  apply (subst beta_cfun)
   1.369 @@ -933,8 +868,7 @@
   1.370  done
   1.371  
   1.372  
   1.373 -lemma defined_sfstssnd: 
   1.374 -        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
   1.375 +lemma defined_sfstssnd: "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
   1.376  apply (unfold sfst_def ssnd_def spair_def)
   1.377  apply (simplesubst beta_cfun)
   1.378  apply (rule cont_Issnd)
   1.379 @@ -967,7 +901,6 @@
   1.380  apply (erule lub_sprod)
   1.381  done
   1.382  
   1.383 -
   1.384  lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
   1.385  (*
   1.386   "chain ?S1 ==>
   1.387 @@ -975,57 +908,22 @@
   1.388   (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
   1.389  *)
   1.390  
   1.391 -lemma ssplit1: 
   1.392 -        "ssplit$f$UU=UU"
   1.393 -apply (unfold ssplit_def)
   1.394 -apply (subst beta_cfun)
   1.395 -apply (simp (no_asm))
   1.396 -apply (subst strictify1)
   1.397 -apply (rule refl)
   1.398 +lemma ssplit1 [simp]: "ssplit$f$UU=UU"
   1.399 +by (simp add: ssplit_def)
   1.400 +
   1.401 +lemma ssplit2 [simp]: "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
   1.402 +by (simp add: ssplit_def)
   1.403 +
   1.404 +lemma ssplit3: "ssplit$spair$z=z"
   1.405 +apply (simp add: ssplit_def)
   1.406 +apply (simp add: surjective_pairing_Sprod2)
   1.407 +apply (case_tac "z=UU", simp_all)
   1.408  done
   1.409  
   1.410 -lemma ssplit2: 
   1.411 -        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
   1.412 -apply (unfold ssplit_def)
   1.413 -apply (subst beta_cfun)
   1.414 -apply (simp (no_asm))
   1.415 -apply (subst strictify2)
   1.416 -apply (rule defined_spair)
   1.417 -apply assumption
   1.418 -apply assumption
   1.419 -apply (subst beta_cfun)
   1.420 -apply (simp (no_asm))
   1.421 -apply (subst sfst2)
   1.422 -apply assumption
   1.423 -apply (subst ssnd2)
   1.424 -apply assumption
   1.425 -apply (rule refl)
   1.426 -done
   1.427 -
   1.428 -
   1.429 -lemma ssplit3: 
   1.430 -  "ssplit$spair$z=z"
   1.431 -apply (unfold ssplit_def)
   1.432 -apply (subst beta_cfun)
   1.433 -apply (simp (no_asm))
   1.434 -apply (case_tac "z=UU")
   1.435 -apply (erule ssubst)
   1.436 -apply (rule strictify1)
   1.437 -apply (rule trans)
   1.438 -apply (rule strictify2)
   1.439 -apply assumption
   1.440 -apply (subst beta_cfun)
   1.441 -apply (simp (no_asm))
   1.442 -apply (rule surjective_pairing_Sprod2)
   1.443 -done
   1.444 -
   1.445 -(* ------------------------------------------------------------------------ *)
   1.446 -(* install simplifier for Sprod                                             *)
   1.447 -(* ------------------------------------------------------------------------ *)
   1.448 +text {* install simplifier for Sprod *}
   1.449  
   1.450  lemmas Sprod_rews = strict_sfst1 strict_sfst2
   1.451                  strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
   1.452                  ssplit1 ssplit2
   1.453 -declare Sprod_rews [simp]
   1.454  
   1.455  end