make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
authorhuffman
Thu Nov 03 01:02:29 2005 +0100 (2005-11-03)
changeset 18077f1f4f951ec8d
parent 18076 e2e626b673b3
child 18078 20e5a6440790
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Nov 03 00:57:35 2005 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Nov 03 01:02:29 2005 +0100
     1.3 @@ -136,14 +136,14 @@
     1.4  apply (rule contlubI)
     1.5  apply (subst thelub_cprod)
     1.6  apply (erule monofun_pair1 [THEN ch2ch_monofun])
     1.7 -apply (simp add: thelub_const)
     1.8 +apply simp
     1.9  done
    1.10  
    1.11  lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
    1.12  apply (rule contlubI)
    1.13  apply (subst thelub_cprod)
    1.14  apply (erule monofun_pair2 [THEN ch2ch_monofun])
    1.15 -apply (simp add: thelub_const)
    1.16 +apply simp
    1.17  done
    1.18  
    1.19  lemma cont_pair1: "cont (\<lambda>x. (x, y))"
    1.20 @@ -229,21 +229,21 @@
    1.21  lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
    1.22  by (simp add: cpair_eq_pair)
    1.23  
    1.24 -lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
    1.25 +lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
    1.26  by (simp add: cpair_eq_pair less_cprod_def)
    1.27  
    1.28 -lemma cpair_defined_iff: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
    1.29 +lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
    1.30  by (simp add: inst_cprod_pcpo cpair_eq_pair)
    1.31  
    1.32  lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
    1.33 -by (simp add: cpair_defined_iff)
    1.34 +by simp
    1.35  
    1.36  lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
    1.37  by (rule cpair_strict [symmetric])
    1.38  
    1.39  lemma defined_cpair_rev: 
    1.40   "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
    1.41 -by (simp add: inst_cprod_pcpo cpair_eq_pair)
    1.42 +by simp
    1.43  
    1.44  lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
    1.45  by (simp add: cpair_eq_pair)
    1.46 @@ -287,6 +287,9 @@
    1.47    "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.48  by (rule lub_cprod2 [THEN thelubI])
    1.49  
    1.50 +lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    1.51 +by (simp add: csplit_def)
    1.52 +
    1.53  lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
    1.54  by (simp add: csplit_def)
    1.55