src/HOLCF/Ssum.thy
 changeset 25756 86d4930373a1 parent 25740 de65baf89106 child 25827 c2adeb1bae5c
```--- a/src/HOLCF/Ssum.thy	Tue Jan 01 16:09:29 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Tue Jan 01 20:30:16 2008 +0100
@@ -141,6 +141,12 @@
\<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cut_tac z=p in Exh_Ssum, auto)

+lemma ssum_induct [induct type: ++]:
+  "\<lbrakk>P \<bottom>;
+   \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
+   \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
+by (cases x, simp_all)
+
lemma ssumE2:
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cases p, simp only: sinl_strict [symmetric], simp, simp)
@@ -178,6 +184,6 @@
unfolding beta_sscase by (simp add: Rep_Ssum_sinr)

lemma sscase4 [simp]: "sscase\<cdot>sinl\<cdot>sinr\<cdot>z = z"
-by (rule_tac p=z in ssumE, simp_all)
+by (cases z, simp_all)

end```