# HG changeset patch
# User huffman
# Date 1120783085 -7200
# Node ID 7af6723ad741fbd2f07f283e3ca9e503a4391ea8
# Parent  282d092b1dbd18381fb83269bb94bc55becd4294
add lemma eq_sprod

diff -r 282d092b1dbd -r 7af6723ad741 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Jul 08 02:37:42 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Fri Jul 08 02:38:05 2005 +0200
@@ -144,11 +144,14 @@
 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (rule_tac p=p in sprodE, simp_all)
 
-lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)"
+lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
 apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
 apply (rule less_cprod)
 done
 
+lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
+by (auto simp add: po_eq_conv less_sprod)
+
 lemma spair_less:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
 apply (case_tac "a = \<bottom>")