# HG changeset patch
# User huffman
# Date 1287771892 25200
# Node ID baf5953615da000491f6487cc881263069644935
# Parent  1ca61fbd8a794c02ec10af8b34caca29f626ddf2
do proofs using Rep_Sprod_simps, Rep_Ssum_simps; remove unused lemmas

diff -r 1ca61fbd8a79 -r baf5953615da src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Oct 22 07:45:32 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Fri Oct 22 11:24:52 2010 -0700
@@ -56,16 +56,17 @@
 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_Sprod)
+lemma Rep_Sprod_spair: "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
+by (simp add: spair_def cont_Abs_Sprod Abs_Sprod_inverse 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_Sprod)
+lemmas Rep_Sprod_simps =
+  Rep_Sprod_inject [symmetric] below_Sprod_def
+  Pair_fst_snd_eq below_prod_def
+  Rep_Sprod_strict Rep_Sprod_spair
 
 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>"
-by (induct p rule: Abs_Sprod_induct)
-   (auto simp add: Sprod_def spair_Abs_Sprod Abs_Sprod_strict)
+using Rep_Sprod [of p] by (auto simp add: Sprod_def Rep_Sprod_simps)
 
 lemma sprod_induct [case_names bottom spair, induct type: sprod]:
   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
@@ -73,10 +74,6 @@
 
 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)
 
diff -r 1ca61fbd8a79 -r baf5953615da src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Fri Oct 22 07:45:32 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Fri Oct 22 11:24:52 2010 -0700
@@ -43,33 +43,32 @@
 lemma sinr_Ssum: "(strict\<cdot>b\<cdot>FF, \<bottom>, b) \<in> Ssum"
 by (simp add: Ssum_def strict_conv_if)
 
-lemma sinl_Abs_Ssum: "sinl\<cdot>a = Abs_Ssum (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (simp add: sinl_def cont_Abs_Ssum sinl_Ssum)
-
-lemma sinr_Abs_Ssum: "sinr\<cdot>b = Abs_Ssum (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (simp add: sinr_def cont_Abs_Ssum sinr_Ssum)
-
 lemma Rep_Ssum_sinl: "Rep_Ssum (sinl\<cdot>a) = (strict\<cdot>a\<cdot>TT, a, \<bottom>)"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
+by (simp add: sinl_def cont_Abs_Ssum Abs_Ssum_inverse sinl_Ssum)
 
 lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strict\<cdot>b\<cdot>FF, \<bottom>, b)"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
+by (simp add: sinr_def cont_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
+
+lemmas Rep_Ssum_simps =
+  Rep_Ssum_inject [symmetric] below_Ssum_def
+  Pair_fst_snd_eq below_prod_def
+  Rep_Ssum_strict Rep_Ssum_sinl Rep_Ssum_sinr
 
 subsection {* Properties of \emph{sinl} and \emph{sinr} *}
 
 text {* Ordering *}
 
 lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl strict_conv_if)
+by (simp add: Rep_Ssum_simps strict_conv_if)
 
 lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: below_Ssum_def Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_Ssum_simps strict_conv_if)
 
 lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_Ssum_simps strict_conv_if)
 
 lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strict_conv_if)
+by (simp add: Rep_Ssum_simps strict_conv_if)
 
 text {* Equality *}
 
@@ -94,10 +93,10 @@
 text {* Strictness *}
 
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_Ssum_simps)
 
 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)
+by (simp add: Rep_Ssum_simps)
 
 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
 using sinl_eq [of "x" "\<bottom>"] by simp
@@ -139,8 +138,7 @@
   obtains "p = \<bottom>"
   | x where "p = sinl\<cdot>x" and "x \<noteq> \<bottom>"
   | y where "p = sinr\<cdot>y" and "y \<noteq> \<bottom>"
-by (induct p rule: Abs_Ssum_induct)
-   (auto simp add: Ssum_def sinl_Abs_Ssum sinr_Abs_Ssum Abs_Ssum_strict)
+using Rep_Ssum [of p] by (auto simp add: Ssum_def Rep_Ssum_simps)
 
 lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
   "\<lbrakk>P \<bottom>;