# HG changeset patch
# User huffman
# Date 1110237502 -3600
# Node ID 50c3384ca6c4e3ac7e86370a70270e264c136e93
# Parent  17f4f5afcd5faf039852184c37455bfe97ce04bf
reordered and arranged for document generation, cleaned up some proofs

diff -r 17f4f5afcd5f -r 50c3384ca6c4 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Mar 08 00:15:01 2005 +0100
+++ b/src/HOLCF/Sprod.thy	Tue Mar 08 00:18:22 2005 +0100
@@ -12,6 +12,8 @@
 imports Cfun
 begin
 
+subsection {* Definition of strict product type *}
+
 constdefs
   Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
  "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
@@ -24,8 +26,6 @@
 syntax (HTML output)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 
-subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
-
 consts
   Ispair        :: "['a,'b] => ('a ** 'b)"
   Isfst         :: "('a ** 'b) => 'a"
@@ -42,9 +42,7 @@
   Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
-(* ------------------------------------------------------------------------ *)
-(* A non-emptyness result for Sprod                                         *)
-(* ------------------------------------------------------------------------ *)
+text {* A non-emptiness result for Sprod *}
 
 lemma SprodI: "(Spair_Rep a b):Sprod"
 apply (unfold Sprod_def)
@@ -56,9 +54,7 @@
 apply (erule Abs_Sprod_inverse)
 done
 
-(* ------------------------------------------------------------------------ *)
-(* Strictness and definedness of Spair_Rep                                  *)
-(* ------------------------------------------------------------------------ *)
+text {* Strictness and definedness of @{term Spair_Rep} *}
 
 lemma strict_Spair_Rep: 
  "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
@@ -78,9 +74,7 @@
 apply (fast dest: fun_cong)
 done
 
-(* ------------------------------------------------------------------------ *)
-(* injectivity of Spair_Rep and Ispair                                      *)
-(* ------------------------------------------------------------------------ *)
+text {* injectivity of @{term Spair_Rep} and @{term Ispair} *}
 
 lemma inject_Spair_Rep: 
 "[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
@@ -102,9 +96,7 @@
 apply (rule SprodI)
 done
 
-(* ------------------------------------------------------------------------ *)
-(* strictness and definedness of Ispair                                     *)
-(* ------------------------------------------------------------------------ *)
+text {* strictness and definedness of @{term Ispair} *}
 
 lemma strict_Ispair: 
  "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
@@ -152,10 +144,7 @@
 apply assumption
 done
 
-
-(* ------------------------------------------------------------------------ *)
-(* Exhaustion of the strict product **                                      *)
-(* ------------------------------------------------------------------------ *)
+text {* Exhaustion of the strict product @{typ "'a ** 'b"} *}
 
 lemma Exh_Sprod:
         "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
@@ -179,9 +168,7 @@
 apply (erule strict_Spair_Rep)
 done
 
-(* ------------------------------------------------------------------------ *)
-(* general elimination rule for strict product                              *)
-(* ------------------------------------------------------------------------ *)
+text {* general elimination rule for strict product *}
 
 lemma IsprodE:
 assumes prem1: "p=Ispair UU UU ==> Q"
@@ -198,9 +185,7 @@
 apply assumption
 done
 
-(* ------------------------------------------------------------------------ *)
-(* some results about the selectors Isfst, Issnd                            *)
-(* ------------------------------------------------------------------------ *)
+text {* some results about the selectors @{term Isfst}, @{term Issnd} *}
 
 lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
 apply (unfold Isfst_def)
@@ -297,9 +282,7 @@
 done
 
 
-(* ------------------------------------------------------------------------ *)
-(* instantiate the simplifier                                               *)
-(* ------------------------------------------------------------------------ *)
+text {* instantiate the simplifier *}
 
 lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
                  Isfst2 Issnd2
@@ -316,9 +299,7 @@
 done
 
 
-(* ------------------------------------------------------------------------ *)
-(* Surjective pairing: equivalent to Exh_Sprod                              *)
-(* ------------------------------------------------------------------------ *)
+text {* Surjective pairing: equivalent to @{thm [source] Exh_Sprod} *}
 
 lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
 apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
@@ -334,17 +315,13 @@
 apply simp
 done
 
-subsection {* The strict product is a partial order *}
+subsection {* Type @{typ "'a ** 'b"} is a partial order *}
 
-instance "**"::(sq_ord,sq_ord)sq_ord ..
+instance "**" :: (sq_ord, sq_ord) sq_ord ..
 
 defs (overloaded)
   less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
 
-(* ------------------------------------------------------------------------ *)
-(* less_sprod is a partial order on Sprod                                   *)
-(* ------------------------------------------------------------------------ *)
-
 lemma refl_less_sprod: "(p::'a ** 'b) << p"
 apply (unfold less_sprod_def)
 apply (fast intro: refl_less)
@@ -359,40 +336,24 @@
 done
 
 lemma trans_less_sprod: 
-        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
+        "[|(p1::'a ** 'b) << p2;p2 << p3|] ==> p1 << p3"
 apply (unfold less_sprod_def)
 apply (blast intro: trans_less)
 done
 
-instance "**"::(pcpo,pcpo)po
+instance "**" :: (pcpo, pcpo) po
 by intro_classes
   (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
 
-(* for compatibility with old HOLCF-Version *)
+text {* for compatibility with old HOLCF-Version *}
 lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
 apply (fold less_sprod_def)
 apply (rule refl)
 done
 
-subsection {* The strict product is pointed *}
-(* ------------------------------------------------------------------------ *)
-(* type sprod is pointed                                                    *)
-(* ------------------------------------------------------------------------ *)
-(*
-lemma minimal_sprod: "Ispair UU UU << p"
-apply (simp add: inst_sprod_po minimal)
-done
+subsection {* Monotonicity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
 
-lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
-
-lemma least_sprod: "? x::'a**'b.!y. x<<y"
-apply (rule_tac x = "Ispair UU UU" in exI)
-apply (rule minimal_sprod [THEN allI])
-done
-*)
-(* ------------------------------------------------------------------------ *)
-(* Ispair is monotone in both arguments                                     *)
-(* ------------------------------------------------------------------------ *)
+text {* @{term Ispair} is monotone in both arguments *}
 
 lemma monofun_Ispair1: "monofun(Ispair)"
 apply (unfold monofun)
@@ -424,24 +385,15 @@
 apply assumption
 done
 
-(* ------------------------------------------------------------------------ *)
-(* Isfst and Issnd are monotone                                             *)
-(* ------------------------------------------------------------------------ *)
+text {* @{term Isfst} and @{term Issnd} are monotone *}
 
 lemma monofun_Isfst: "monofun(Isfst)"
-apply (unfold monofun)
-apply (simp add: inst_sprod_po)
-done
+by (simp add: monofun inst_sprod_po)
 
 lemma monofun_Issnd: "monofun(Issnd)"
-apply (unfold monofun)
-apply (simp add: inst_sprod_po)
-done
+by (simp add: monofun inst_sprod_po)
 
-subsection {* The strict product is a cpo *}
-(* ------------------------------------------------------------------------ *)
-(* the type 'a ** 'b is a cpo                                               *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Type @{typ "'a ** 'b"} is a cpo *}
 
 lemma lub_sprod: 
 "[|chain(S)|] ==> range(S) <<|  
@@ -474,8 +426,7 @@
 instance "**" :: (pcpo, pcpo) cpo
 by intro_classes (rule cpo_sprod)
 
-
-subsection {* The strict product is a pcpo *}
+subsection {* Type @{typ "'a ** 'b"} is pointed *}
 
 lemma minimal_sprod: "Ispair UU UU << p"
 apply (simp add: inst_sprod_po minimal)
@@ -491,8 +442,13 @@
 instance "**" :: (pcpo, pcpo) pcpo
 by intro_classes (rule least_sprod)
 
+text {* for compatibility with old HOLCF-Version *}
+lemma inst_sprod_pcpo: "UU = Ispair UU UU"
+by (simp add: UU_def UU_sprod_def)
 
-subsection {* Other constants *}
+declare inst_sprod_pcpo [symmetric, simp]
+
+subsection {* Continuous versions of constants *}
 
 consts  
   spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
@@ -513,16 +469,7 @@
 ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
 ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
 
-(* for compatibility with old HOLCF-Version *)
-lemma inst_sprod_pcpo: "UU = Ispair UU UU"
-apply (simp add: UU_def UU_sprod_def)
-done
-
-declare inst_sprod_pcpo [symmetric, simp]
-
-(* ------------------------------------------------------------------------ *)
-(* continuity of Ispair, Isfst, Issnd                                       *)
-(* ------------------------------------------------------------------------ *)
+subsection {* Continuity of @{term Ispair}, @{term Isfst}, @{term Issnd} *}
 
 lemma sprod3_lemma1: 
 "[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
@@ -741,9 +688,7 @@
 apply fast
 done
 
-(* ------------------------------------------------------------------------ *)
-(* convert all lemmas to the continuous versions                            *)
-(* ------------------------------------------------------------------------ *)
+text {* convert all lemmas to the continuous versions *}
 
 lemma beta_cfun_sprod [simp]: 
         "(LAM x y. Ispair x y)$a$b = Ispair a b"
@@ -813,7 +758,7 @@
 apply auto
 done
 
-lemma defined_spair: 
+lemma defined_spair [simp]: 
         "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
 apply (unfold spair_def)
 apply (subst beta_cfun_sprod)
@@ -840,7 +785,6 @@
 apply fast
 done
 
-
 lemma sprodE:
 assumes prem1: "p=UU ==> Q"
 assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
@@ -857,9 +801,7 @@
 apply assumption
 done
 
-
-lemma strict_sfst: 
-        "p=UU==>sfst$p=UU"
+lemma strict_sfst: "p=UU==>sfst$p=UU"
 apply (unfold sfst_def)
 apply (subst beta_cfun)
 apply (rule cont_Isfst)
@@ -868,17 +810,15 @@
 apply assumption
 done
 
-lemma strict_sfst1: 
-        "sfst$(:UU,y:) = UU"
+lemma strict_sfst1 [simp]: "sfst$(:UU,y:) = UU"
 apply (unfold sfst_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
 apply (rule cont_Isfst)
 apply (rule strict_Isfst1)
 done
- 
-lemma strict_sfst2: 
-        "sfst$(:x,UU:) = UU"
+
+lemma strict_sfst2 [simp]: "sfst$(:x,UU:) = UU"
 apply (unfold sfst_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
@@ -886,8 +826,7 @@
 apply (rule strict_Isfst2)
 done
 
-lemma strict_ssnd: 
-        "p=UU==>ssnd$p=UU"
+lemma strict_ssnd: "p=UU==>ssnd$p=UU"
 apply (unfold ssnd_def)
 apply (subst beta_cfun)
 apply (rule cont_Issnd)
@@ -896,8 +835,7 @@
 apply assumption
 done
 
-lemma strict_ssnd1: 
-        "ssnd$(:UU,y:) = UU"
+lemma strict_ssnd1 [simp]: "ssnd$(:UU,y:) = UU"
 apply (unfold ssnd_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
@@ -905,8 +843,7 @@
 apply (rule strict_Issnd1)
 done
 
-lemma strict_ssnd2: 
-        "ssnd$(:x,UU:) = UU"
+lemma strict_ssnd2 [simp]: "ssnd$(:x,UU:) = UU"
 apply (unfold ssnd_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
@@ -914,8 +851,7 @@
 apply (rule strict_Issnd2)
 done
 
-lemma sfst2: 
-        "y~=UU ==>sfst$(:x,y:)=x"
+lemma sfst2 [simp]: "y~=UU ==>sfst$(:x,y:)=x"
 apply (unfold sfst_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
@@ -923,8 +859,7 @@
 apply (erule Isfst2)
 done
 
-lemma ssnd2: 
-        "x~=UU ==>ssnd$(:x,y:)=y"
+lemma ssnd2 [simp]: "x~=UU ==>ssnd$(:x,y:)=y"
 apply (unfold ssnd_def spair_def)
 apply (subst beta_cfun_sprod)
 apply (subst beta_cfun)
@@ -933,8 +868,7 @@
 done
 
 
-lemma defined_sfstssnd: 
-        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
+lemma defined_sfstssnd: "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
 apply (unfold sfst_def ssnd_def spair_def)
 apply (simplesubst beta_cfun)
 apply (rule cont_Issnd)
@@ -967,7 +901,6 @@
 apply (erule lub_sprod)
 done
 
-
 lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
 (*
  "chain ?S1 ==>
@@ -975,57 +908,22 @@
  (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
 *)
 
-lemma ssplit1: 
-        "ssplit$f$UU=UU"
-apply (unfold ssplit_def)
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (subst strictify1)
-apply (rule refl)
+lemma ssplit1 [simp]: "ssplit$f$UU=UU"
+by (simp add: ssplit_def)
+
+lemma ssplit2 [simp]: "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
+by (simp add: ssplit_def)
+
+lemma ssplit3: "ssplit$spair$z=z"
+apply (simp add: ssplit_def)
+apply (simp add: surjective_pairing_Sprod2)
+apply (case_tac "z=UU", simp_all)
 done
 
-lemma ssplit2: 
-        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
-apply (unfold ssplit_def)
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (subst strictify2)
-apply (rule defined_spair)
-apply assumption
-apply assumption
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (subst sfst2)
-apply assumption
-apply (subst ssnd2)
-apply assumption
-apply (rule refl)
-done
-
-
-lemma ssplit3: 
-  "ssplit$spair$z=z"
-apply (unfold ssplit_def)
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (case_tac "z=UU")
-apply (erule ssubst)
-apply (rule strictify1)
-apply (rule trans)
-apply (rule strictify2)
-apply assumption
-apply (subst beta_cfun)
-apply (simp (no_asm))
-apply (rule surjective_pairing_Sprod2)
-done
-
-(* ------------------------------------------------------------------------ *)
-(* install simplifier for Sprod                                             *)
-(* ------------------------------------------------------------------------ *)
+text {* install simplifier for Sprod *}
 
 lemmas Sprod_rews = strict_sfst1 strict_sfst2
                 strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
                 ssplit1 ssplit2
-declare Sprod_rews [simp]
 
 end