--- a/src/HOLCF/Sprod.thy Thu Oct 21 06:03:18 2010 -0700
+++ b/src/HOLCF/Sprod.thy Thu Oct 21 12:03:49 2010 -0700
@@ -27,9 +27,6 @@
type_notation (HTML output)
sprod ("(_ \<otimes>/ _)" [21,20] 20)
-lemma spair_lemma: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
-by (simp add: Sprod_def strict_conv_if)
-
subsection {* Definitions of constants *}
definition
@@ -59,15 +56,14 @@
subsection {* Case analysis *}
+lemma spair_Sprod: "(strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b) \<in> Sprod"
+by (simp add: Sprod_def strict_conv_if)
+
lemma spair_Abs_Sprod: "(:a, b:) = Abs_Sprod (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-by (simp add: spair_def cont_Abs_Sprod spair_lemma)
+by (simp add: spair_def cont_Abs_Sprod spair_Sprod)
lemma Rep_Sprod_spair: "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-by (simp add: spair_Abs_Sprod Abs_Sprod_inverse spair_lemma)
-
-lemmas Rep_Sprod_simps =
- Rep_Sprod_inject [symmetric] below_Sprod_def
- Rep_Sprod_strict Rep_Sprod_spair
+by (simp add: spair_Abs_Sprod Abs_Sprod_inverse spair_Sprod)
lemma sprodE [case_names bottom spair, cases type: sprod]:
obtains "p = \<bottom>" | x y where "p = (:x, y:)" and "x \<noteq> \<bottom>" and "y \<noteq> \<bottom>"
@@ -80,6 +76,10 @@
subsection {* Properties of \emph{spair} *}
+lemmas Rep_Sprod_simps =
+ Rep_Sprod_inject [symmetric] below_Sprod_def
+ Rep_Sprod_strict Rep_Sprod_spair
+
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
by (simp add: Rep_Sprod_simps strict_conv_if)