# HG changeset patch # User huffman # Date 1122394923 -7200 # Node ID da331e0a4a81265939ff8c60d8bd95dfeea4ff97 # Parent bca4c3b1afca6f51d7f2d6c26c39d19067a90cf8 add theorem cpair_defined_iff diff -r bca4c3b1afca -r da331e0a4a81 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Tue Jul 26 15:29:37 2005 +0200 +++ b/src/HOLCF/Cprod.thy Tue Jul 26 18:22:03 2005 +0200 @@ -132,7 +132,7 @@ subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *} -lemma contlub_pair1: "contlub (\x. (x,y))" +lemma contlub_pair1: "contlub (\x. (x, y))" apply (rule contlubI) apply (subst thelub_cprod) apply (erule monofun_pair1 [THEN ch2ch_monofun]) @@ -252,11 +252,14 @@ lemma cpair_less: "( \ ) = (a \ a' \ b \ b')" by (simp add: cpair_eq_pair less_cprod_def) +lemma cpair_defined_iff: "( = \) = (x = \ \ y = \)" +by (simp add: inst_cprod_pcpo cpair_eq_pair) + lemma cpair_strict: "<\, \> = \" -by (simp add: cpair_eq_pair inst_cprod_pcpo) +by (simp add: cpair_defined_iff) lemma inst_cprod_pcpo2: "\ = <\, \>" -by (simp add: cpair_eq_pair inst_cprod_pcpo) +by (rule cpair_strict [symmetric]) lemma defined_cpair_rev: " = \ \ a = \ \ b = \"