declare case_names for various induction rules

--- a/src/HOLCF/One.thy	Sat Mar 13 21:07:20 2010 -0800
+++ b/src/HOLCF/One.thy	Sat Mar 13 22:00:34 2010 -0800
@@ -22,10 +22,10 @@
 lemma Exh_one: "t = \<bottom> \<or> t = ONE"
 unfolding ONE_def by (induct t) simp_all
 
-lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 unfolding ONE_def by (induct p) simp_all
 
-lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
+lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
 by (cases x rule: oneE) simp_all
 
 lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"

--- a/src/HOLCF/Sprod.thy	Sat Mar 13 21:07:20 2010 -0800
+++ b/src/HOLCF/Sprod.thy	Sat Mar 13 22:00:34 2010 -0800
@@ -80,11 +80,11 @@
 apply fast
 done
 
-lemma sprodE [cases type: sprod]:
+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"
-by (cut_tac z=p in Exh_Sprod, auto)
+using Exh_Sprod [of p] by auto
 
-lemma sprod_induct [induct type: sprod]:
+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"
 by (cases x, simp_all)
 

--- a/src/HOLCF/Ssum.thy	Sat Mar 13 21:07:20 2010 -0800
+++ b/src/HOLCF/Ssum.thy	Sat Mar 13 22:00:34 2010 -0800
@@ -151,19 +151,19 @@
 apply (simp add: sinr_Abs_Ssum Ssum_def)
 done
 
-lemma ssumE [cases type: ssum]:
+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"
-by (cut_tac z=p in Exh_Ssum, auto)
+using Exh_Ssum [of p] by auto
 
-lemma ssum_induct [induct type: ssum]:
+lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
   "\<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:
+lemma ssumE2 [case_names sinl sinr]:
   "\<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)
 

--- a/src/HOLCF/Tr.thy	Sat Mar 13 21:07:20 2010 -0800
+++ b/src/HOLCF/Tr.thy	Sat Mar 13 22:00:34 2010 -0800
@@ -29,10 +29,12 @@
 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
 unfolding FF_def TT_def by (induct t) auto
 
-lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+lemma trE [case_names bottom TT FF]:
+  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 unfolding FF_def TT_def by (induct p) auto
 
-lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
+lemma tr_induct [case_names bottom TT FF]:
+  "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
 by (cases x rule: trE) simp_all
 
 text {* distinctness for type @{typ tr} *}

--- a/src/HOLCF/Up.thy	Sat Mar 13 21:07:20 2010 -0800
+++ b/src/HOLCF/Up.thy	Sat Mar 13 22:00:34 2010 -0800
@@ -237,13 +237,15 @@
 lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
 by (simp add: up_def cont_Iup)
 
-lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+lemma upE [case_names bottom up, cases type: u]:
+  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
 apply (cases p)
 apply (simp add: inst_up_pcpo)
 apply (simp add: up_def cont_Iup)
 done
 
-lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
+lemma up_induct [case_names bottom up, induct type: u]:
+  "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
 by (cases x, simp_all)
 
 text {* lifting preserves chain-finiteness *}