src/HOL/Nitpick.thy
changeset 41792 ff3cb0c418b7
parent 41052 3db267a01c1d
child 41797 0c6093d596d6
     1.1 --- a/src/HOL/Nitpick.thy	Mon Feb 21 10:42:29 2011 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Feb 21 10:44:19 2011 +0100
     1.3 @@ -47,11 +47,7 @@
     1.4  Alternative definitions.
     1.5  *}
     1.6  
     1.7 -lemma If_def [nitpick_def, no_atp]:
     1.8 -"(if P then Q else R) \<equiv> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
     1.9 -by (rule eq_reflection) (rule if_bool_eq_conj)
    1.10 -
    1.11 -lemma Ex1_def [nitpick_def, no_atp]:
    1.12 +lemma Ex1_def [nitpick_unfold, no_atp]:
    1.13  "Ex1 P \<equiv> \<exists>x. P = {x}"
    1.14  apply (rule eq_reflection)
    1.15  apply (simp add: Ex1_def set_eq_iff)
    1.16 @@ -64,14 +60,14 @@
    1.17   apply (erule_tac x = y in allE)
    1.18  by (auto simp: mem_def)
    1.19  
    1.20 -lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.21 +lemma rtrancl_def [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.22  by simp
    1.23  
    1.24 -lemma rtranclp_def [nitpick_def, no_atp]:
    1.25 +lemma rtranclp_def [nitpick_unfold, no_atp]:
    1.26  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    1.27  by (rule eq_reflection) (auto dest: rtranclpD)
    1.28  
    1.29 -lemma tranclp_def [nitpick_def, no_atp]:
    1.30 +lemma tranclp_def [nitpick_unfold, no_atp]:
    1.31  "tranclp r a b \<equiv> trancl (split r) (a, b)"
    1.32  by (simp add: trancl_def Collect_def mem_def)
    1.33  
    1.34 @@ -119,7 +115,7 @@
    1.35  apply (erule contrapos_np)
    1.36  by (rule someI)
    1.37  
    1.38 -lemma unit_case_def [nitpick_def, no_atp]:
    1.39 +lemma unit_case_def [nitpick_unfold, no_atp]:
    1.40  "unit_case x u \<equiv> x"
    1.41  apply (subgoal_tac "u = ()")
    1.42   apply (simp only: unit.cases)
    1.43 @@ -127,7 +123,7 @@
    1.44  
    1.45  declare unit.cases [nitpick_simp del]
    1.46  
    1.47 -lemma nat_case_def [nitpick_def, no_atp]:
    1.48 +lemma nat_case_def [nitpick_unfold, no_atp]:
    1.49  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.50  apply (rule eq_reflection)
    1.51  by (case_tac n) auto