added compactness lemmas; cleaned up
authorhuffman
Wed Oct 12 01:43:37 2005 +0200 (2005-10-12)
changeset 178372922be3544f8
parent 17836 5d9c9e284d16
child 17838 3032e90c4975
added compactness lemmas; cleaned up
src/HOLCF/Cprod.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Tue Oct 11 23:47:29 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Oct 12 01:43:37 2005 +0200
     1.3 @@ -274,6 +274,9 @@
     1.4  lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
     1.5  by (auto simp add: po_eq_conv less_cprod)
     1.6  
     1.7 +lemma compact_cpair [simp]: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
     1.8 +by (rule compactI, simp add: less_cprod)
     1.9 +
    1.10  lemma lub_cprod2: 
    1.11    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.12  apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
     2.1 --- a/src/HOLCF/Sprod.thy	Tue Oct 11 23:47:29 2005 +0200
     2.2 +++ b/src/HOLCF/Sprod.thy	Wed Oct 12 01:43:37 2005 +0200
     2.3 @@ -110,6 +110,15 @@
     2.4  lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
     2.5  by simp
     2.6  
     2.7 +lemma Rep_Sprod_spair:
     2.8 +  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
     2.9 +apply (unfold spair_def)
    2.10 +apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    2.11 +done
    2.12 +
    2.13 +lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
    2.14 +by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
    2.15 +
    2.16  subsection {* Properties of @{term sfst} and @{term ssnd} *}
    2.17  
    2.18  lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    2.19 @@ -118,12 +127,6 @@
    2.20  lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
    2.21  by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
    2.22  
    2.23 -lemma Rep_Sprod_spair:
    2.24 -  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
    2.25 -apply (unfold spair_def)
    2.26 -apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    2.27 -done
    2.28 -
    2.29  lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
    2.30  by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
    2.31  
     3.1 --- a/src/HOLCF/Ssum.thy	Tue Oct 11 23:47:29 2005 +0200
     3.2 +++ b/src/HOLCF/Ssum.thy	Wed Oct 12 01:43:37 2005 +0200
     3.3 @@ -48,6 +48,12 @@
     3.4  lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = <\<bottom>, b>"
     3.5  by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
     3.6  
     3.7 +lemma compact_sinl [simp]: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
     3.8 +by (rule compact_Ssum, simp add: Rep_Ssum_sinl)
     3.9 +
    3.10 +lemma compact_sinr [simp]: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
    3.11 +by (rule compact_Ssum, simp add: Rep_Ssum_sinr)
    3.12 +
    3.13  lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
    3.14  by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
    3.15  
    3.16 @@ -67,14 +73,10 @@
    3.17  by (rule sinr_eq [THEN iffD1])
    3.18  
    3.19  lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
    3.20 -apply (rule sinl_strict [THEN subst])
    3.21 -apply (rule sinl_eq)
    3.22 -done
    3.23 +by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
    3.24  
    3.25  lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
    3.26 -apply (rule sinr_strict [THEN subst])
    3.27 -apply (rule sinr_eq)
    3.28 -done
    3.29 +by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
    3.30  
    3.31  lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
    3.32  by simp