add "no_atp"s to Nitpick lemmas
authorblanchet
Fri May 14 15:27:07 2010 +0200 (2010-05-14)
changeset 36918e65f8d253fd1
parent 36917 8674cdb0b8cc
child 36919 182774d56bd2
child 36920 62e4af74a70a
child 36922 12f87df9c1a5
add "no_atp"s to Nitpick lemmas
src/HOL/Nitpick.thy
     1.1 --- a/src/HOL/Nitpick.thy	Fri May 14 15:26:26 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Fri May 14 15:27:07 2010 +0200
     1.3 @@ -52,11 +52,11 @@
     1.4  Alternative definitions.
     1.5  *}
     1.6  
     1.7 -lemma If_def [nitpick_def]:
     1.8 +lemma If_def [nitpick_def, no_atp]:
     1.9  "(if P then Q else R) \<equiv> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
    1.10  by (rule eq_reflection) (rule if_bool_eq_conj)
    1.11  
    1.12 -lemma Ex1_def [nitpick_def]:
    1.13 +lemma Ex1_def [nitpick_def, no_atp]:
    1.14  "Ex1 P \<equiv> \<exists>x. P = {x}"
    1.15  apply (rule eq_reflection)
    1.16  apply (simp add: Ex1_def expand_set_eq)
    1.17 @@ -69,14 +69,14 @@
    1.18   apply (erule_tac x = y in allE)
    1.19  by (auto simp: mem_def)
    1.20  
    1.21 -lemma rtrancl_def [nitpick_def]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.22 +lemma rtrancl_def [nitpick_def, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    1.23  by simp
    1.24  
    1.25 -lemma rtranclp_def [nitpick_def]:
    1.26 +lemma rtranclp_def [nitpick_def, no_atp]:
    1.27  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    1.28  by (rule eq_reflection) (auto dest: rtranclpD)
    1.29  
    1.30 -lemma tranclp_def [nitpick_def]:
    1.31 +lemma tranclp_def [nitpick_def, no_atp]:
    1.32  "tranclp r a b \<equiv> trancl (split r) (a, b)"
    1.33  by (simp add: trancl_def Collect_def mem_def)
    1.34  
    1.35 @@ -110,18 +110,18 @@
    1.36  \textit{special\_level} optimization.
    1.37  *}
    1.38  
    1.39 -lemma The_psimp [nitpick_psimp]:
    1.40 +lemma The_psimp [nitpick_psimp, no_atp]:
    1.41  "P = {x} \<Longrightarrow> The P = x"
    1.42  by (subgoal_tac "{x} = (\<lambda>y. y = x)") (auto simp: mem_def)
    1.43  
    1.44 -lemma Eps_psimp [nitpick_psimp]:
    1.45 +lemma Eps_psimp [nitpick_psimp, no_atp]:
    1.46  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
    1.47  apply (case_tac "P (Eps P)")
    1.48   apply auto
    1.49  apply (erule contrapos_np)
    1.50  by (rule someI)
    1.51  
    1.52 -lemma unit_case_def [nitpick_def]:
    1.53 +lemma unit_case_def [nitpick_def, no_atp]:
    1.54  "unit_case x u \<equiv> x"
    1.55  apply (subgoal_tac "u = ()")
    1.56   apply (simp only: unit.cases)
    1.57 @@ -129,14 +129,14 @@
    1.58  
    1.59  declare unit.cases [nitpick_simp del]
    1.60  
    1.61 -lemma nat_case_def [nitpick_def]:
    1.62 +lemma nat_case_def [nitpick_def, no_atp]:
    1.63  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    1.64  apply (rule eq_reflection)
    1.65  by (case_tac n) auto
    1.66  
    1.67  declare nat.cases [nitpick_simp del]
    1.68  
    1.69 -lemma list_size_simp [nitpick_simp]:
    1.70 +lemma list_size_simp [nitpick_simp, no_atp]:
    1.71  "list_size f xs = (if xs = [] then 0
    1.72                     else Suc (f (hd xs) + list_size f (tl xs)))"
    1.73  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"