# HG changeset patch
# User huffman
# Date 1287857030 25200
# Node ID 5325a062ff538c3b73cd895ab6c91c6bd5e8b0a8
# Parent  0295606b6a36a77056c6be0d17cea218e93b14ff
tuned

diff -r 0295606b6a36 -r 5325a062ff53 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Oct 22 15:49:18 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Sat Oct 23 11:03:50 2010 -0700
@@ -104,6 +104,10 @@
 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
 by simp
 
+lemma spair_below:
+  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
+by (simp add: spair_below_iff)
+
 lemma spair_eq:
   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
 by (simp add: spair_eq_iff)
@@ -148,20 +152,11 @@
 by (cases p, simp_all)
 
 lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
-apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (simp only: below_prod_def)
-done
+by (simp add: Rep_Sprod_simps sfst_def ssnd_def cont_Rep_Sprod)
 
 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 below_sprod)
 
-lemma spair_below:
-  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
-apply (cases "a = \<bottom>", simp)
-apply (cases "b = \<bottom>", simp)
-apply (simp add: below_sprod)
-done
-
 lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)