added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up

--- a/src/HOLCF/Ssum.ML	Fri Jul 08 02:38:05 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Fri Jul 08 02:39:53 2005 +0200
@@ -14,7 +14,6 @@
 val cont_Iwhen3 = thm "cont_Iwhen3";
 val sinl_strict = thm "sinl_strict";
 val sinr_strict = thm "sinr_strict";
-val noteq_sinlsinr = thm "noteq_sinlsinr";
 val sinl_inject = thm "sinl_inject";
 val sinr_inject = thm "sinr_inject";
 val sinl_eq = thm "sinl_eq";

--- a/src/HOLCF/Ssum.thy	Fri Jul 08 02:38:05 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Fri Jul 08 02:39:53 2005 +0200
@@ -25,7 +25,7 @@
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 
 lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
-by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric])
+by (simp add: Abs_Ssum_strict cpair_strict)
 
 
 subsection {* Definitions of constructors *}
@@ -52,47 +52,46 @@
 by (unfold sinr_def, simp add: cont_Abs_Ssum Abs_Ssum_inverse Ssum_def)
 
 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinl_Abs_Ssum UU_Abs_Ssum)
+by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
 
 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
-by (simp add: sinr_Abs_Ssum UU_Abs_Ssum)
+by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)
 
-lemma noteq_sinlsinr: "sinl\<cdot>a = sinr\<cdot>b \<Longrightarrow> a = \<bottom> \<and> b = \<bottom>"
-apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum)
-apply (simp add: Abs_Ssum_inject Ssum_def)
-done
-
-lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
+lemma sinl_eq [simp]: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
 by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
+lemma sinr_eq [simp]: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
 by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
 
-lemma sinl_eq: "(sinl\<cdot>x = sinl\<cdot>y) = (x = y)"
-by (simp add: sinl_Abs_Ssum Abs_Ssum_inject Ssum_def)
+lemma sinl_inject: "sinl\<cdot>x = sinl\<cdot>y \<Longrightarrow> x = y"
+by (rule sinl_eq [THEN iffD1])
 
-lemma sinr_eq: "(sinr\<cdot>x = sinr\<cdot>y) = (x = y)"
-by (simp add: sinr_Abs_Ssum Abs_Ssum_inject Ssum_def)
+lemma sinr_inject: "sinr\<cdot>x = sinr\<cdot>y \<Longrightarrow> x = y"
+by (rule sinr_eq [THEN iffD1])
 
-lemma sinl_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
-apply (erule contrapos_nn)
-apply (rule sinl_inject)
-apply auto
+lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
+apply (rule sinl_strict [THEN subst])
+apply (rule sinl_eq)
 done
 
-lemma sinr_defined [simp]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
-apply (erule contrapos_nn)
-apply (rule sinr_inject)
-apply auto
+lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
+apply (rule sinr_strict [THEN subst])
+apply (rule sinr_eq)
 done
 
+lemma sinl_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinl\<cdot>x \<noteq> \<bottom>"
+by simp
+
+lemma sinr_defined [intro!]: "x \<noteq> \<bottom> \<Longrightarrow> sinr\<cdot>x \<noteq> \<bottom>"
+by simp
+
 subsection {* Case analysis *}
 
 lemma Exh_Ssum1: 
   "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 (rule_tac x=z in Abs_Ssum_induct)
+apply (rule_tac p=y in cprodE)
 apply (simp add: sinl_Abs_Ssum sinr_Abs_Ssum UU_Abs_Ssum)
-apply (rule_tac x=z in Abs_Ssum_cases)
-apply (rule_tac p=y in cprodE)
 apply (auto simp add: Ssum_def)
 done
 
@@ -112,32 +111,38 @@
 
 subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
-lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
 
-lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
 
-lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+
+lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
 by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
-lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+lemma sinl_eq_sinr [simp]: "(sinl\<cdot>x = sinr\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
+by (simp add: po_eq_conv)
+
+lemma sinr_eq_sinl [simp]: "(sinr\<cdot>x = sinl\<cdot>y) = (x = \<bottom> \<and> y = \<bottom>)"
+by (simp add: po_eq_conv)
 
 subsection {* Chains of strict sums *}
 
 lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
 apply (rule_tac p=p in ssumE)
 apply (rule_tac x="\<bottom>" in exI, simp)
-apply (simp add: sinl_less sinl_eq)
-apply (simp add: sinr_less_sinl)
+apply simp
+apply simp
 done
 
 lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
 apply (rule_tac p=p in ssumE)
 apply (rule_tac x="\<bottom>" in exI, simp)
-apply (simp add: sinl_less_sinr)
-apply (simp add: sinr_less sinr_eq)
+apply simp
+apply simp
 done
 
 lemma ssum_chain_lemma:
@@ -151,7 +156,7 @@
    apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
   apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
   apply (drule less_sinlD, clarify)
-  apply (simp add: sinl_eq Rep_Ssum_sinl)
+  apply (simp add: Rep_Ssum_sinl)
  apply (rule disjI2)
  apply (rule_tac x="\<lambda>i. csnd\<cdot>(Rep_Ssum (Y i))" in exI)
  apply (rule conjI)
@@ -159,7 +164,7 @@
   apply (erule cont_Rep_Ssum [THEN ch2ch_cont])
  apply (rule ext, drule_tac x=i in is_ub_thelub, simp)
  apply (drule less_sinrD, clarify)
- apply (simp add: sinr_eq Rep_Ssum_sinr)
+ apply (simp add: Rep_Ssum_sinr)
 done
 
 subsection {* Definitions of constants *}