declare trE and tr_induct as default cases and induct rules for type tr
authorhuffman
Fri Aug 03 15:38:44 2012 +0200 (2012-08-03)
changeset 4865940a87b4dac19
parent 48658 4c7932270d6d
child 48663 49c080255a57
declare trE and tr_induct as default cases and induct rules for type tr
src/HOL/HOLCF/Tr.thy
     1.1 --- a/src/HOL/HOLCF/Tr.thy	Fri Aug 03 13:06:25 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Tr.thy	Fri Aug 03 15:38:44 2012 +0200
     1.3 @@ -29,13 +29,13 @@
     1.4  lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
     1.5  unfolding FF_def TT_def by (induct t) auto
     1.6  
     1.7 -lemma trE [case_names bottom TT FF]:
     1.8 +lemma trE [case_names bottom TT FF, cases type: tr]:
     1.9    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.10  unfolding FF_def TT_def by (induct p) auto
    1.11  
    1.12 -lemma tr_induct [case_names bottom TT FF]:
    1.13 +lemma tr_induct [case_names bottom TT FF, induct type: tr]:
    1.14    "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
    1.15 -by (cases x rule: trE) simp_all
    1.16 +by (cases x) simp_all
    1.17  
    1.18  text {* distinctness for type @{typ tr} *}
    1.19  
    1.20 @@ -48,16 +48,16 @@
    1.21  unfolding TT_def FF_def by simp_all
    1.22  
    1.23  lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
    1.24 -by (induct x rule: tr_induct) simp_all
    1.25 +by (induct x) simp_all
    1.26  
    1.27  lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
    1.28 -by (induct x rule: tr_induct) simp_all
    1.29 +by (induct x) simp_all
    1.30  
    1.31  lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
    1.32 -by (induct x rule: tr_induct) simp_all
    1.33 +by (induct x) simp_all
    1.34  
    1.35  lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
    1.36 -by (induct x rule: tr_induct) simp_all
    1.37 +by (induct x) simp_all
    1.38  
    1.39  
    1.40  subsection {* Case analysis *}
    1.41 @@ -120,8 +120,8 @@
    1.42    "(y andalso TT) = y"
    1.43    "(y andalso y) = y"
    1.44  apply (unfold andalso_def, simp_all)
    1.45 -apply (cases y rule: trE, simp_all)
    1.46 -apply (cases y rule: trE, simp_all)
    1.47 +apply (cases y, simp_all)
    1.48 +apply (cases y, simp_all)
    1.49  done
    1.50  
    1.51  lemma orelse_thms [simp]:
    1.52 @@ -131,8 +131,8 @@
    1.53    "(y orelse FF) = y"
    1.54    "(y orelse y) = y"
    1.55  apply (unfold orelse_def, simp_all)
    1.56 -apply (cases y rule: trE, simp_all)
    1.57 -apply (cases y rule: trE, simp_all)
    1.58 +apply (cases y, simp_all)
    1.59 +apply (cases y, simp_all)
    1.60  done
    1.61  
    1.62  lemma neg_thms [simp]:
    1.63 @@ -146,7 +146,7 @@
    1.64  lemma split_If2:
    1.65    "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
    1.66  apply (unfold If2_def)
    1.67 -apply (rule_tac p = "Q" in trE)
    1.68 +apply (cases Q)
    1.69  apply (simp_all)
    1.70  done
    1.71  
    1.72 @@ -160,13 +160,13 @@
    1.73  
    1.74  lemma andalso_or:
    1.75    "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
    1.76 -apply (rule_tac p = "t" in trE)
    1.77 +apply (cases t)
    1.78  apply simp_all
    1.79  done
    1.80  
    1.81  lemma andalso_and:
    1.82    "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)"
    1.83 -apply (rule_tac p = "t" in trE)
    1.84 +apply (cases t)
    1.85  apply simp_all
    1.86  done
    1.87  
    1.88 @@ -184,7 +184,7 @@
    1.89  
    1.90  lemma If_and_if:
    1.91    "(If Def P then A else B) = (if P then A else B)"
    1.92 -apply (rule_tac p = "Def P" in trE)
    1.93 +apply (cases "Def P")
    1.94  apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
    1.95  done
    1.96