# HG changeset patch
# User huffman
# Date 1344001124 -7200
# Node ID 40a87b4dac19bd6ae016d9f4f6696ed21d3f5c63
# Parent  4c7932270d6da90a480931c6cee593c77fbd632d
declare trE and tr_induct as default cases and induct rules for type tr

diff -r 4c7932270d6d -r 40a87b4dac19 src/HOL/HOLCF/Tr.thy
--- a/src/HOL/HOLCF/Tr.thy	Fri Aug 03 13:06:25 2012 +0200
+++ b/src/HOL/HOLCF/Tr.thy	Fri Aug 03 15:38:44 2012 +0200
@@ -29,13 +29,13 @@
 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
 unfolding FF_def TT_def by (induct t) auto
 
-lemma trE [case_names bottom TT FF]:
+lemma trE [case_names bottom TT FF, cases type: tr]:
   "\<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 [case_names bottom TT FF]:
+lemma tr_induct [case_names bottom TT FF, induct type: tr]:
   "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
-by (cases x rule: trE) simp_all
+by (cases x) simp_all
 
 text {* distinctness for type @{typ tr} *}
 
@@ -48,16 +48,16 @@
 unfolding TT_def FF_def by simp_all
 
 lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
-by (induct x rule: tr_induct) simp_all
+by (induct x) simp_all
 
 lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
-by (induct x rule: tr_induct) simp_all
+by (induct x) simp_all
 
 lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
-by (induct x rule: tr_induct) simp_all
+by (induct x) simp_all
 
 lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
-by (induct x rule: tr_induct) simp_all
+by (induct x) simp_all
 
 
 subsection {* Case analysis *}
@@ -120,8 +120,8 @@
   "(y andalso TT) = y"
   "(y andalso y) = y"
 apply (unfold andalso_def, simp_all)
-apply (cases y rule: trE, simp_all)
-apply (cases y rule: trE, simp_all)
+apply (cases y, simp_all)
+apply (cases y, simp_all)
 done
 
 lemma orelse_thms [simp]:
@@ -131,8 +131,8 @@
   "(y orelse FF) = y"
   "(y orelse y) = y"
 apply (unfold orelse_def, simp_all)
-apply (cases y rule: trE, simp_all)
-apply (cases y rule: trE, simp_all)
+apply (cases y, simp_all)
+apply (cases y, simp_all)
 done
 
 lemma neg_thms [simp]:
@@ -146,7 +146,7 @@
 lemma split_If2:
   "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
 apply (unfold If2_def)
-apply (rule_tac p = "Q" in trE)
+apply (cases Q)
 apply (simp_all)
 done
 
@@ -160,13 +160,13 @@
 
 lemma andalso_or:
   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
-apply (rule_tac p = "t" in trE)
+apply (cases t)
 apply simp_all
 done
 
 lemma andalso_and:
   "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
-apply (rule_tac p = "t" in trE)
+apply (cases t)
 apply simp_all
 done
 
@@ -184,7 +184,7 @@
 
 lemma If_and_if:
   "(If Def P then A else B) = (if P then A else B)"
-apply (rule_tac p = "Def P" in trE)
+apply (cases "Def P")
 apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
 done