killed more "no_atp"s
authorblanchet
Fri Oct 18 10:43:21 2013 +0200 (2013-10-18)
changeset 54148c8cc5ab4a863
parent 54147 97a8ff4e4ac9
child 54149 70456a8f5e6e
killed more "no_atp"s
src/HOL/ATP.thy
src/HOL/Enum.thy
src/HOL/Finite_Set.thy
src/HOL/Groups.thy
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Nitpick.thy
     1.1 --- a/src/HOL/ATP.thy	Fri Oct 18 10:43:20 2013 +0200
     1.2 +++ b/src/HOL/ATP.thy	Fri Oct 18 10:43:21 2013 +0200
     1.3 @@ -18,34 +18,34 @@
     1.4  
     1.5  subsection {* Higher-order reasoning helpers *}
     1.6  
     1.7 -definition fFalse :: bool where [no_atp]:
     1.8 +definition fFalse :: bool where
     1.9  "fFalse \<longleftrightarrow> False"
    1.10  
    1.11 -definition fTrue :: bool where [no_atp]:
    1.12 +definition fTrue :: bool where
    1.13  "fTrue \<longleftrightarrow> True"
    1.14  
    1.15 -definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
    1.16 +definition fNot :: "bool \<Rightarrow> bool" where
    1.17  "fNot P \<longleftrightarrow> \<not> P"
    1.18  
    1.19 -definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.20 +definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
    1.21  "fComp P = (\<lambda>x. \<not> P x)"
    1.22  
    1.23 -definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.24 +definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.25  "fconj P Q \<longleftrightarrow> P \<and> Q"
    1.26  
    1.27 -definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.28 +definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.29  "fdisj P Q \<longleftrightarrow> P \<or> Q"
    1.30  
    1.31 -definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
    1.32 +definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
    1.33  "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
    1.34  
    1.35 -definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
    1.36 +definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
    1.37  "fequal x y \<longleftrightarrow> (x = y)"
    1.38  
    1.39 -definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.40 +definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.41  "fAll P \<longleftrightarrow> All P"
    1.42  
    1.43 -definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
    1.44 +definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.45  "fEx P \<longleftrightarrow> Ex P"
    1.46  
    1.47  lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
     2.1 --- a/src/HOL/Enum.thy	Fri Oct 18 10:43:20 2013 +0200
     2.2 +++ b/src/HOL/Enum.thy	Fri Oct 18 10:43:21 2013 +0200
     2.3 @@ -156,11 +156,11 @@
     2.4    "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
     2.5    by (auto intro: imageI in_enum)
     2.6  
     2.7 -lemma tranclp_unfold [code, no_atp]:
     2.8 +lemma tranclp_unfold [code]:
     2.9    "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
    2.10    by (simp add: trancl_def)
    2.11  
    2.12 -lemma rtranclp_rtrancl_eq [code, no_atp]:
    2.13 +lemma rtranclp_rtrancl_eq [code]:
    2.14    "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
    2.15    by (simp add: rtrancl_def)
    2.16  
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:21 2013 +0200
     3.3 @@ -1188,7 +1188,7 @@
     3.4    "card A > 0 \<Longrightarrow> finite A"
     3.5    by (rule ccontr) simp
     3.6  
     3.7 -lemma card_0_eq [simp, no_atp]:
     3.8 +lemma card_0_eq [simp]:
     3.9    "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
    3.10    by (auto dest: mk_disjoint_insert)
    3.11  
     4.1 --- a/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
     4.2 +++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:21 2013 +0200
     4.3 @@ -517,7 +517,7 @@
     4.4  
     4.5  (* FIXME: duplicates right_minus_eq from class group_add *)
     4.6  (* but only this one is declared as a simp rule. *)
     4.7 -lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
     4.8 +lemma diff_eq_0_iff_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
     4.9    by (rule right_minus_eq)
    4.10  
    4.11  lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
    4.12 @@ -896,7 +896,7 @@
    4.13  lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
    4.14  by (auto simp add: le_less minus_less_iff)
    4.15  
    4.16 -lemma diff_less_0_iff_less [simp, no_atp]:
    4.17 +lemma diff_less_0_iff_less [simp]:
    4.18    "a - b < 0 \<longleftrightarrow> a < b"
    4.19  proof -
    4.20    have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
    4.21 @@ -924,7 +924,7 @@
    4.22  lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
    4.23  by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
    4.24  
    4.25 -lemma diff_le_0_iff_le [simp, no_atp]:
    4.26 +lemma diff_le_0_iff_le [simp]:
    4.27    "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
    4.28    by (simp add: algebra_simps)
    4.29  
    4.30 @@ -1231,7 +1231,7 @@
    4.31  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
    4.32  by simp
    4.33  
    4.34 -lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    4.35 +lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
    4.36  proof -
    4.37    have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
    4.38    thus ?thesis by simp
     5.1 --- a/src/HOL/Meson.thy	Fri Oct 18 10:43:20 2013 +0200
     5.2 +++ b/src/HOL/Meson.thy	Fri Oct 18 10:43:21 2013 +0200
     5.3 @@ -132,45 +132,45 @@
     5.4  text{* Combinator translation helpers *}
     5.5  
     5.6  definition COMBI :: "'a \<Rightarrow> 'a" where
     5.7 -[no_atp]: "COMBI P = P"
     5.8 +"COMBI P = P"
     5.9  
    5.10  definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
    5.11 -[no_atp]: "COMBK P Q = P"
    5.12 +"COMBK P Q = P"
    5.13  
    5.14 -definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
    5.15 +definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    5.16  "COMBB P Q R = P (Q R)"
    5.17  
    5.18  definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    5.19 -[no_atp]: "COMBC P Q R = P R Q"
    5.20 +"COMBC P Q R = P R Q"
    5.21  
    5.22  definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
    5.23 -[no_atp]: "COMBS P Q R = P R (Q R)"
    5.24 +"COMBS P Q R = P R (Q R)"
    5.25  
    5.26 -lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    5.27 +lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
    5.28  apply (rule eq_reflection)
    5.29  apply (rule ext) 
    5.30  apply (simp add: COMBS_def) 
    5.31  done
    5.32  
    5.33 -lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
    5.34 +lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
    5.35  apply (rule eq_reflection)
    5.36  apply (rule ext) 
    5.37  apply (simp add: COMBI_def) 
    5.38  done
    5.39  
    5.40 -lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
    5.41 +lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
    5.42  apply (rule eq_reflection)
    5.43  apply (rule ext) 
    5.44  apply (simp add: COMBK_def) 
    5.45  done
    5.46  
    5.47 -lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    5.48 +lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
    5.49  apply (rule eq_reflection)
    5.50  apply (rule ext) 
    5.51  apply (simp add: COMBB_def) 
    5.52  done
    5.53  
    5.54 -lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    5.55 +lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
    5.56  apply (rule eq_reflection)
    5.57  apply (rule ext) 
    5.58  apply (simp add: COMBC_def) 
    5.59 @@ -180,7 +180,7 @@
    5.60  subsection {* Skolemization helpers *}
    5.61  
    5.62  definition skolem :: "'a \<Rightarrow> 'a" where
    5.63 -[no_atp]: "skolem = (\<lambda>x. x)"
    5.64 +"skolem = (\<lambda>x. x)"
    5.65  
    5.66  lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
    5.67  unfolding skolem_def COMBK_def by (rule refl)
     6.1 --- a/src/HOL/Metis.thy	Fri Oct 18 10:43:20 2013 +0200
     6.2 +++ b/src/HOL/Metis.thy	Fri Oct 18 10:43:21 2013 +0200
     6.3 @@ -16,7 +16,7 @@
     6.4  subsection {* Literal selection and lambda-lifting helpers *}
     6.5  
     6.6  definition select :: "'a \<Rightarrow> 'a" where
     6.7 -[no_atp]: "select = (\<lambda>x. x)"
     6.8 +"select = (\<lambda>x. x)"
     6.9  
    6.10  lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
    6.11  by (cut_tac atomize_not [of "\<not> A"]) simp
    6.12 @@ -30,7 +30,7 @@
    6.13  lemma select_FalseI: "False \<Longrightarrow> select False" by simp
    6.14  
    6.15  definition lambda :: "'a \<Rightarrow> 'a" where
    6.16 -[no_atp]: "lambda = (\<lambda>x. x)"
    6.17 +"lambda = (\<lambda>x. x)"
    6.18  
    6.19  lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
    6.20  unfolding lambda_def by assumption
     7.1 --- a/src/HOL/Nitpick.thy	Fri Oct 18 10:43:20 2013 +0200
     7.2 +++ b/src/HOL/Nitpick.thy	Fri Oct 18 10:43:21 2013 +0200
     7.3 @@ -33,7 +33,7 @@
     7.4  Alternative definitions.
     7.5  *}
     7.6  
     7.7 -lemma Ex1_unfold [nitpick_unfold, no_atp]:
     7.8 +lemma Ex1_unfold [nitpick_unfold]:
     7.9  "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
    7.10  apply (rule eq_reflection)
    7.11  apply (simp add: Ex1_def set_eq_iff)
    7.12 @@ -46,18 +46,18 @@
    7.13   apply (erule_tac x = y in allE)
    7.14  by auto
    7.15  
    7.16 -lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    7.17 +lemma rtrancl_unfold [nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
    7.18    by (simp only: rtrancl_trancl_reflcl)
    7.19  
    7.20 -lemma rtranclp_unfold [nitpick_unfold, no_atp]:
    7.21 +lemma rtranclp_unfold [nitpick_unfold]:
    7.22  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
    7.23  by (rule eq_reflection) (auto dest: rtranclpD)
    7.24  
    7.25 -lemma tranclp_unfold [nitpick_unfold, no_atp]:
    7.26 +lemma tranclp_unfold [nitpick_unfold]:
    7.27  "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
    7.28  by (simp add: trancl_def)
    7.29  
    7.30 -lemma [nitpick_simp, no_atp]:
    7.31 +lemma [nitpick_simp]:
    7.32  "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
    7.33  by (cases n) auto
    7.34  
    7.35 @@ -85,18 +85,18 @@
    7.36  \textit{specialize} optimization.
    7.37  *}
    7.38  
    7.39 -lemma The_psimp [nitpick_psimp, no_atp]:
    7.40 +lemma The_psimp [nitpick_psimp]:
    7.41    "P = (op =) x \<Longrightarrow> The P = x"
    7.42    by auto
    7.43  
    7.44 -lemma Eps_psimp [nitpick_psimp, no_atp]:
    7.45 +lemma Eps_psimp [nitpick_psimp]:
    7.46  "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
    7.47  apply (cases "P (Eps P)")
    7.48   apply auto
    7.49  apply (erule contrapos_np)
    7.50  by (rule someI)
    7.51  
    7.52 -lemma unit_case_unfold [nitpick_unfold, no_atp]:
    7.53 +lemma unit_case_unfold [nitpick_unfold]:
    7.54  "unit_case x u \<equiv> x"
    7.55  apply (subgoal_tac "u = ()")
    7.56   apply (simp only: unit.cases)
    7.57 @@ -104,14 +104,14 @@
    7.58  
    7.59  declare unit.cases [nitpick_simp del]
    7.60  
    7.61 -lemma nat_case_unfold [nitpick_unfold, no_atp]:
    7.62 +lemma nat_case_unfold [nitpick_unfold]:
    7.63  "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
    7.64  apply (rule eq_reflection)
    7.65  by (cases n) auto
    7.66  
    7.67  declare nat.cases [nitpick_simp del]
    7.68  
    7.69 -lemma list_size_simp [nitpick_simp, no_atp]:
    7.70 +lemma list_size_simp [nitpick_simp]:
    7.71  "list_size f xs = (if xs = [] then 0
    7.72                     else Suc (f (hd xs) + list_size f (tl xs)))"
    7.73  "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"