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