# HG changeset patch # User huffman # Date 1287687829 25200 # Node ID 54159b52f3392238b6d59695c2e6df67d881bf12 # Parent f4be971c574648535615d0aa922c287849bb4d97 rename lemma spair_lemma to spair_Sprod diff -r f4be971c5746 -r 54159b52f339 src/HOLCF/Sprod.thy --- 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 ("(_ \/ _)" [21,20] 20) -lemma spair_lemma: "(strict\b\a, strict\a\b) \ 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\b\a, strict\a\b) \ Sprod" +by (simp add: Sprod_def strict_conv_if) + lemma spair_Abs_Sprod: "(:a, b:) = Abs_Sprod (strict\b\a, strict\a\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\b\a, strict\a\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 = \" | x y where "p = (:x, y:)" and "x \ \" and "y \ \" @@ -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]: "(:\, y:) = \" by (simp add: Rep_Sprod_simps strict_conv_if)