# HG changeset patch
# User huffman
# Date 1130976149 -3600
# Node ID f1f4f951ec8d3656557bfb6e45300ee881b3a77d
# Parent  e2e626b673b3fd7787bf64dd5d1cb16ce760871a
make cpair_less, cpair_defined_iff into iff rules; add lemma csplit1

diff -r e2e626b673b3 -r f1f4f951ec8d src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Nov 03 00:57:35 2005 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Nov 03 01:02:29 2005 +0100
@@ -136,14 +136,14 @@
 apply (rule contlubI)
 apply (subst thelub_cprod)
 apply (erule monofun_pair1 [THEN ch2ch_monofun])
-apply (simp add: thelub_const)
+apply simp
 done
 
 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
 apply (rule contlubI)
 apply (subst thelub_cprod)
 apply (erule monofun_pair2 [THEN ch2ch_monofun])
-apply (simp add: thelub_const)
+apply simp
 done
 
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"
@@ -229,21 +229,21 @@
 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
 by (simp add: cpair_eq_pair)
 
-lemma cpair_less: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
+lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
 by (simp add: cpair_eq_pair less_cprod_def)
 
-lemma cpair_defined_iff: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
+lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
 by (simp add: inst_cprod_pcpo cpair_eq_pair)
 
 lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
-by (simp add: cpair_defined_iff)
+by simp
 
 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
 by (rule cpair_strict [symmetric])
 
 lemma defined_cpair_rev: 
  "<a,b> = \<bottom> \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
-by (simp add: inst_cprod_pcpo cpair_eq_pair)
+by simp
 
 lemma Exh_Cprod2: "\<exists>a b. z = <a, b>"
 by (simp add: cpair_eq_pair)
@@ -287,6 +287,9 @@
   "chain S \<Longrightarrow> lub (range S) = <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
 by (rule lub_cprod2 [THEN thelubI])
 
+lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
+by (simp add: csplit_def)
+
 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
 by (simp add: csplit_def)