# HG changeset patch
# User huffman
# Date 1120783062 -7200
# Node ID 282d092b1dbd18381fb83269bb94bc55becd4294
# Parent  c96aaaf25f48e9ee00640e38e1e295e169f2eaca
add lemma eq_cprod

diff -r c96aaaf25f48 -r 282d092b1dbd src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jul 07 21:41:08 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Fri Jul 08 02:37:42 2005 +0200
@@ -285,9 +285,12 @@
 apply (simp add: cont_fst cont_snd cpair_eq_pair)
 done
 
-lemma less_cprod: "p1 \<sqsubseteq> p2 = (cfst\<cdot>p1 \<sqsubseteq> cfst\<cdot>p2 \<and> csnd\<cdot>p1 \<sqsubseteq> csnd\<cdot>p2)"
+lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
 by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
 
+lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
+by (auto simp add: po_eq_conv less_cprod)
+
 lemma lub_cprod2: 
   "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
 apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)