declare case_names for various induction rules
authorhuffman
Sat Mar 13 22:00:34 2010 -0800 (2010-03-13)
changeset 3578338538bfe9ca6
parent 35782 8a314dd86714
child 35784 a86ed293b005
declare case_names for various induction rules
src/HOLCF/One.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tr.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/One.thy	Sat Mar 13 21:07:20 2010 -0800
     1.2 +++ b/src/HOLCF/One.thy	Sat Mar 13 22:00:34 2010 -0800
     1.3 @@ -22,10 +22,10 @@
     1.4  lemma Exh_one: "t = \<bottom> \<or> t = ONE"
     1.5  unfolding ONE_def by (induct t) simp_all
     1.6  
     1.7 -lemma oneE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
     1.8 +lemma oneE [case_names bottom ONE]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = ONE \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
     1.9  unfolding ONE_def by (induct p) simp_all
    1.10  
    1.11 -lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
    1.12 +lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
    1.13  by (cases x rule: oneE) simp_all
    1.14  
    1.15  lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
     2.1 --- a/src/HOLCF/Sprod.thy	Sat Mar 13 21:07:20 2010 -0800
     2.2 +++ b/src/HOLCF/Sprod.thy	Sat Mar 13 22:00:34 2010 -0800
     2.3 @@ -80,11 +80,11 @@
     2.4  apply fast
     2.5  done
     2.6  
     2.7 -lemma sprodE [cases type: sprod]:
     2.8 +lemma sprodE [case_names bottom spair, cases type: sprod]:
     2.9    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    2.10 -by (cut_tac z=p in Exh_Sprod, auto)
    2.11 +using Exh_Sprod [of p] by auto
    2.12  
    2.13 -lemma sprod_induct [induct type: sprod]:
    2.14 +lemma sprod_induct [case_names bottom spair, induct type: sprod]:
    2.15    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    2.16  by (cases x, simp_all)
    2.17  
     3.1 --- a/src/HOLCF/Ssum.thy	Sat Mar 13 21:07:20 2010 -0800
     3.2 +++ b/src/HOLCF/Ssum.thy	Sat Mar 13 22:00:34 2010 -0800
     3.3 @@ -151,19 +151,19 @@
     3.4  apply (simp add: sinr_Abs_Ssum Ssum_def)
     3.5  done
     3.6  
     3.7 -lemma ssumE [cases type: ssum]:
     3.8 +lemma ssumE [case_names bottom sinl sinr, cases type: ssum]:
     3.9    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q;
    3.10     \<And>x. \<lbrakk>p = sinl\<cdot>x; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q;
    3.11     \<And>y. \<lbrakk>p = sinr\<cdot>y; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    3.12 -by (cut_tac z=p in Exh_Ssum, auto)
    3.13 +using Exh_Ssum [of p] by auto
    3.14  
    3.15 -lemma ssum_induct [induct type: ssum]:
    3.16 +lemma ssum_induct [case_names bottom sinl sinr, induct type: ssum]:
    3.17    "\<lbrakk>P \<bottom>;
    3.18     \<And>x. x \<noteq> \<bottom> \<Longrightarrow> P (sinl\<cdot>x);
    3.19     \<And>y. y \<noteq> \<bottom> \<Longrightarrow> P (sinr\<cdot>y)\<rbrakk> \<Longrightarrow> P x"
    3.20  by (cases x, simp_all)
    3.21  
    3.22 -lemma ssumE2:
    3.23 +lemma ssumE2 [case_names sinl sinr]:
    3.24    "\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    3.25  by (cases p, simp only: sinl_strict [symmetric], simp, simp)
    3.26  
     4.1 --- a/src/HOLCF/Tr.thy	Sat Mar 13 21:07:20 2010 -0800
     4.2 +++ b/src/HOLCF/Tr.thy	Sat Mar 13 22:00:34 2010 -0800
     4.3 @@ -29,10 +29,12 @@
     4.4  lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
     4.5  unfolding FF_def TT_def by (induct t) auto
     4.6  
     4.7 -lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
     4.8 +lemma trE [case_names bottom TT FF]:
     4.9 +  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    4.10  unfolding FF_def TT_def by (induct p) auto
    4.11  
    4.12 -lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
    4.13 +lemma tr_induct [case_names bottom TT FF]:
    4.14 +  "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
    4.15  by (cases x rule: trE) simp_all
    4.16  
    4.17  text {* distinctness for type @{typ tr} *}
     5.1 --- a/src/HOLCF/Up.thy	Sat Mar 13 21:07:20 2010 -0800
     5.2 +++ b/src/HOLCF/Up.thy	Sat Mar 13 22:00:34 2010 -0800
     5.3 @@ -237,13 +237,15 @@
     5.4  lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
     5.5  by (simp add: up_def cont_Iup)
     5.6  
     5.7 -lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
     5.8 +lemma upE [case_names bottom up, cases type: u]:
     5.9 +  "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    5.10  apply (cases p)
    5.11  apply (simp add: inst_up_pcpo)
    5.12  apply (simp add: up_def cont_Iup)
    5.13  done
    5.14  
    5.15 -lemma up_induct [induct type: u]: "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
    5.16 +lemma up_induct [case_names bottom up, induct type: u]:
    5.17 +  "\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x"
    5.18  by (cases x, simp_all)
    5.19  
    5.20  text {* lifting preserves chain-finiteness *}