# HG changeset patch
# User huffman
# Date 1122395236 -7200
# Node ID ded12c9e88c23ff1f270b273dd2c4bbe9a6de21c
# Parent  6df23e3180fb62cd34028b12981d35faaca4c474
cleaned up

diff -r 6df23e3180fb -r ded12c9e88c2 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Jul 26 18:25:27 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Tue Jul 26 18:27:16 2005 +0200
@@ -46,7 +46,7 @@
 by (simp add: CFun_def inst_fun_pcpo cont_const)
 
 instance "->" :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo_UU [OF type_definition_CFun less_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
 
 lemmas Rep_CFun_strict =
   typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
@@ -204,14 +204,11 @@
 
 text {* type @{typ "'a -> 'b"} is chain complete *}
 
-lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (LAM x. LUB i. F i$x)"
-apply (subst thelub_fun [symmetric])
-apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
-apply (erule typedef_is_lub [OF type_definition_CFun less_CFun_def adm_CFun])
-done
+lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
+by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
 
-lemmas thelub_cfun = lub_cfun [THEN thelubI, standard]
- -- {* @{thm thelub_cfun} *} (* chain F \<Longrightarrow> lub (range F) = (\<Lambda>x. \<Squnion>i. F i\<cdot>x) *)
+lemma thelub_cfun: "chain F \<Longrightarrow> lub (range F) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
+by (rule lub_cfun [THEN thelubI])
 
 subsection {* Miscellaneous *}
 
diff -r 6df23e3180fb -r ded12c9e88c2 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Tue Jul 26 18:25:27 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Tue Jul 26 18:27:16 2005 +0200
@@ -24,9 +24,6 @@
 syntax (HTML output)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 
-lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
-by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
-
 lemma spair_lemma:
   "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
 by (simp add: Sprod_def strictify_conv_if cpair_strict)
@@ -81,10 +78,10 @@
 subsection {* Properties of @{term spair} *}
 
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
+by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
 
 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
+by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
 
 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
 by auto
@@ -94,12 +91,7 @@
 
 lemma spair_defined [simp]: 
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
-apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
-apply (subst Abs_Sprod_inject)
-apply (simp add: Sprod_def)
-apply (simp add: Sprod_def inst_cprod_pcpo2)
-apply simp
-done
+by (simp add: spair_Abs_Sprod Abs_Sprod_defined cpair_defined_iff Sprod_def)
 
 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
 by (erule contrapos_pp, simp)
@@ -176,7 +168,7 @@
 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: ssplit_def)
 
-lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y"
+lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y"
 by (simp add: ssplit_def)
 
 lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"