# 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 (\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 (\x. (x, y))" @@ -229,21 +229,21 @@ lemma cpair_eq [iff]: "( = ) = (a = a' \ b = b')" by (simp add: cpair_eq_pair) -lemma cpair_less: "( \ ) = (a \ a' \ b \ b')" +lemma cpair_less [iff]: "( \ ) = (a \ a' \ b \ b')" by (simp add: cpair_eq_pair less_cprod_def) -lemma cpair_defined_iff: "( = \) = (x = \ \ y = \)" +lemma cpair_defined_iff [iff]: "( = \) = (x = \ \ y = \)" by (simp add: inst_cprod_pcpo cpair_eq_pair) lemma cpair_strict: "<\, \> = \" -by (simp add: cpair_defined_iff) +by simp lemma inst_cprod_pcpo2: "\ = <\, \>" by (rule cpair_strict [symmetric]) lemma defined_cpair_rev: " = \ \ a = \ \ b = \" -by (simp add: inst_cprod_pcpo cpair_eq_pair) +by simp lemma Exh_Cprod2: "\a b. z = " by (simp add: cpair_eq_pair) @@ -287,6 +287,9 @@ "chain S \ lub (range S) = <\i. cfst\(S i), \i. csnd\(S i)>" by (rule lub_cprod2 [THEN thelubI]) +lemma csplit1 [simp]: "csplit\f\\ = f\\\\" +by (simp add: csplit_def) + lemma csplit2 [simp]: "csplit\f\ = f\x\y" by (simp add: csplit_def)