# HG changeset patch
# User huffman
# Date 1199215816 -3600
# Node ID 86d4930373a11268da6e37e443a806890a87a69d
# Parent  9bc082c2cc92b3d9e99c51c291a8556b0a0cc87c
add induction rule ssum_induct

diff -r 9bc082c2cc92 -r 86d4930373a1 src/HOLCF/Ssum.thy
--- 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