simplify proofs of ssumE, sprodE

--- a/src/HOLCF/Sprod.thy	Wed Oct 20 21:26:51 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Thu Oct 21 05:35:32 2010 -0700
@@ -59,28 +59,20 @@
 
 subsection {* Case analysis *}
 
-lemma Rep_Sprod_spair:
-  "Rep_Sprod (:a, b:) = (strict\<cdot>b\<cdot>a, strict\<cdot>a\<cdot>b)"
-unfolding spair_def
-by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
+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)
+
+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
 
-lemma Exh_Sprod:
-  "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
-apply (insert Rep_Sprod [of z])
-apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
-apply (simp add: Sprod_def)
-apply (erule disjE, simp)
-apply (simp add: strict_conv_if)
-apply fast
-done
-
 lemma sprodE [case_names bottom spair, cases type: sprod]:
-  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Sprod [of p] by auto
+  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)
 
 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"

--- a/src/HOLCF/Ssum.thy	Wed Oct 20 21:26:51 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Thu Oct 21 05:35:32 2010 -0700
@@ -13,9 +13,9 @@
 subsection {* Definition of strict sum type *}
 
 pcpodef (Ssum)  ('a, 'b) ssum (infixr "++" 10) = 
-  "{p :: tr \<times> ('a \<times> 'b).
-    (fst p \<sqsubseteq> TT \<longleftrightarrow> snd (snd p) = \<bottom>) \<and>
-    (fst p \<sqsubseteq> FF \<longleftrightarrow> fst (snd p) = \<bottom>)}"
+  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
+    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
 by simp_all
 
 instance ssum :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
@@ -47,10 +47,10 @@
 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 (unfold sinl_def, simp add: cont_Abs_Ssum sinl_Ssum)
+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 (unfold sinr_def, simp add: cont_Abs_Ssum sinr_Ssum)
+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)
@@ -103,10 +103,10 @@
 by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)
 
 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
+using sinl_eq [of "x" "\<bottom>"] by simp
 
 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
-by (cut_tac sinr_eq [of "x" "\<bottom>"], simp)
+using sinr_eq [of "x" "\<bottom>"] by simp
 
 lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
 by simp
@@ -117,10 +117,10 @@
 text {* Compactness *}
 
 lemma compact_sinl: "compact x \<Longrightarrow> compact (sinl\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinl strict_conv_if)
+by (rule compact_Ssum, simp add: Rep_Ssum_sinl)
 
 lemma compact_sinr: "compact x \<Longrightarrow> compact (sinr\<cdot>x)"
-by (rule compact_Ssum, simp add: Rep_Ssum_sinr strict_conv_if)
+by (rule compact_Ssum, simp add: Rep_Ssum_sinr)
 
 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
@@ -138,24 +138,12 @@
 
 subsection {* Case analysis *}
 
-lemma Exh_Ssum: 
-  "z = \<bottom> \<or> (\<exists>a. z = sinl\<cdot>a \<and> a \<noteq> \<bottom>) \<or> (\<exists>b. z = sinr\<cdot>b \<and> b \<noteq> \<bottom>)"
-apply (induct z rule: Abs_Ssum_induct)
-apply (case_tac y, rename_tac t a b)
-apply (case_tac t rule: trE)
-apply (rule disjI1)
-apply (simp add: Ssum_def Abs_Ssum_strict)
-apply (rule disjI2, rule disjI1, rule_tac x=a in exI)
-apply (simp add: sinl_Abs_Ssum Ssum_def)
-apply (rule disjI2, rule disjI2, rule_tac x=b in exI)
-apply (simp add: sinr_Abs_Ssum Ssum_def)
-done
-
 lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
-  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
-   \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
-   \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-using Exh_Ssum [of p] by auto
+  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)
 
 lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
   "\<lbrakk>P \<bottom>;