cleaned up
authorhuffman
Tue Jul 26 18:27:16 2005 +0200 (2005-07-26)
changeset 16920ded12c9e88c2
parent 16919 6df23e3180fb
child 16921 16094ed8ac6b
cleaned up
src/HOLCF/Cfun.thy
src/HOLCF/Sprod.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Jul 26 18:25:27 2005 +0200
     1.2 +++ b/src/HOLCF/Cfun.thy	Tue Jul 26 18:27:16 2005 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  by (simp add: CFun_def inst_fun_pcpo cont_const)
     1.5  
     1.6  instance "->" :: (cpo, pcpo) pcpo
     1.7 -by (rule typedef_pcpo_UU [OF type_definition_CFun less_CFun_def UU_CFun])
     1.8 +by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
     1.9  
    1.10  lemmas Rep_CFun_strict =
    1.11    typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
    1.12 @@ -204,14 +204,11 @@
    1.13  
    1.14  text {* type @{typ "'a -> 'b"} is chain complete *}
    1.15  
    1.16 -lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (LAM x. LUB i. F i$x)"
    1.17 -apply (subst thelub_fun [symmetric])
    1.18 -apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
    1.19 -apply (erule typedef_is_lub [OF type_definition_CFun less_CFun_def adm_CFun])
    1.20 -done
    1.21 +lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.22 +by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
    1.23  
    1.24 -lemmas thelub_cfun = lub_cfun [THEN thelubI, standard]
    1.25 - -- {* @{thm thelub_cfun} *} (* chain F \<Longrightarrow> lub (range F) = (\<Lambda>x. \<Squnion>i. F i\<cdot>x) *)
    1.26 +lemma thelub_cfun: "chain F \<Longrightarrow> lub (range F) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.27 +by (rule lub_cfun [THEN thelubI])
    1.28  
    1.29  subsection {* Miscellaneous *}
    1.30  
     2.1 --- a/src/HOLCF/Sprod.thy	Tue Jul 26 18:25:27 2005 +0200
     2.2 +++ b/src/HOLCF/Sprod.thy	Tue Jul 26 18:27:16 2005 +0200
     2.3 @@ -24,9 +24,6 @@
     2.4  syntax (HTML output)
     2.5    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
     2.6  
     2.7 -lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
     2.8 -by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
     2.9 -
    2.10  lemma spair_lemma:
    2.11    "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
    2.12  by (simp add: Sprod_def strictify_conv_if cpair_strict)
    2.13 @@ -81,10 +78,10 @@
    2.14  subsection {* Properties of @{term spair} *}
    2.15  
    2.16  lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
    2.17 -by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
    2.18 +by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
    2.19  
    2.20  lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
    2.21 -by (simp add: spair_Abs_Sprod UU_Abs_Sprod strictify_conv_if)
    2.22 +by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
    2.23  
    2.24  lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
    2.25  by auto
    2.26 @@ -94,12 +91,7 @@
    2.27  
    2.28  lemma spair_defined [simp]: 
    2.29    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
    2.30 -apply (simp add: spair_Abs_Sprod UU_Abs_Sprod)
    2.31 -apply (subst Abs_Sprod_inject)
    2.32 -apply (simp add: Sprod_def)
    2.33 -apply (simp add: Sprod_def inst_cprod_pcpo2)
    2.34 -apply simp
    2.35 -done
    2.36 +by (simp add: spair_Abs_Sprod Abs_Sprod_defined cpair_defined_iff Sprod_def)
    2.37  
    2.38  lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
    2.39  by (erule contrapos_pp, simp)
    2.40 @@ -176,7 +168,7 @@
    2.41  lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
    2.42  by (simp add: ssplit_def)
    2.43  
    2.44 -lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:)= f\<cdot>x\<cdot>y"
    2.45 +lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y"
    2.46  by (simp add: ssplit_def)
    2.47  
    2.48  lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"