# HG changeset patch
# User blanchet
# Date 1382085801 -7200
# Node ID c8cc5ab4a863ca9902f0f305cb378ca102e7eb58
# Parent  97a8ff4e4ac95ff4d7991359c3963f538b089cde
killed more "no_atp"s

diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/ATP.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -18,34 +18,34 @@
 
 subsection {* Higher-order reasoning helpers *}
 
-definition fFalse :: bool where [no_atp]:
+definition fFalse :: bool where
 "fFalse \<longleftrightarrow> False"
 
-definition fTrue :: bool where [no_atp]:
+definition fTrue :: bool where
 "fTrue \<longleftrightarrow> True"
 
-definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
+definition fNot :: "bool \<Rightarrow> bool" where
 "fNot P \<longleftrightarrow> \<not> P"
 
-definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+definition fComp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
 "fComp P = (\<lambda>x. \<not> P x)"
 
-definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fconj P Q \<longleftrightarrow> P \<and> Q"
 
-definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fdisj P Q \<longleftrightarrow> P \<or> Q"
 
-definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
+definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
 "fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
 
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 "fequal x y \<longleftrightarrow> (x = y)"
 
-definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fAll P \<longleftrightarrow> All P"
 
-definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
+definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where
 "fEx P \<longleftrightarrow> Ex P"
 
 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Enum.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -156,11 +156,11 @@
   "Id = image (\<lambda>x. (x, x)) (set Enum.enum)"
   by (auto intro: imageI in_enum)
 
-lemma tranclp_unfold [code, no_atp]:
+lemma tranclp_unfold [code]:
   "tranclp r a b \<longleftrightarrow> (a, b) \<in> trancl {(x, y). r x y}"
   by (simp add: trancl_def)
 
-lemma rtranclp_rtrancl_eq [code, no_atp]:
+lemma rtranclp_rtrancl_eq [code]:
   "rtranclp r x y \<longleftrightarrow> (x, y) \<in> rtrancl {(x, y). r x y}"
   by (simp add: rtrancl_def)
 
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -1188,7 +1188,7 @@
   "card A > 0 \<Longrightarrow> finite A"
   by (rule ccontr) simp
 
-lemma card_0_eq [simp, no_atp]:
+lemma card_0_eq [simp]:
   "finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
   by (auto dest: mk_disjoint_insert)
 
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -517,7 +517,7 @@
 
 (* FIXME: duplicates right_minus_eq from class group_add *)
 (* but only this one is declared as a simp rule. *)
-lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
+lemma diff_eq_0_iff_eq [simp]: "a - b = 0 \<longleftrightarrow> a = b"
   by (rule right_minus_eq)
 
 lemma add_diff_cancel_left: "(c + a) - (c + b) = a - b"
@@ -896,7 +896,7 @@
 lemma minus_le_iff: "- a \<le> b \<longleftrightarrow> - b \<le> a"
 by (auto simp add: le_less minus_less_iff)
 
-lemma diff_less_0_iff_less [simp, no_atp]:
+lemma diff_less_0_iff_less [simp]:
   "a - b < 0 \<longleftrightarrow> a < b"
 proof -
   have "a - b < 0 \<longleftrightarrow> a + (- b) < b + (- b)" by (simp add: diff_minus)
@@ -924,7 +924,7 @@
 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c"
 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel)
 
-lemma diff_le_0_iff_le [simp, no_atp]:
+lemma diff_le_0_iff_le [simp]:
   "a - b \<le> 0 \<longleftrightarrow> a \<le> b"
   by (simp add: algebra_simps)
 
@@ -1231,7 +1231,7 @@
 lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
 by simp
 
-lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
+lemma abs_0_eq [simp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
 proof -
   have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   thus ?thesis by simp
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Meson.thy
--- a/src/HOL/Meson.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Meson.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -132,45 +132,45 @@
 text{* Combinator translation helpers *}
 
 definition COMBI :: "'a \<Rightarrow> 'a" where
-[no_atp]: "COMBI P = P"
+"COMBI P = P"
 
 definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
-[no_atp]: "COMBK P Q = P"
+"COMBK P Q = P"
 
-definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
+definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
 "COMBB P Q R = P (Q R)"
 
 definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBC P Q R = P R Q"
+"COMBC P Q R = P R Q"
 
 definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBS P Q R = P R (Q R)"
+"COMBS P Q R = P R (Q R)"
 
-lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
+lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBS_def) 
 done
 
-lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
+lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBI_def) 
 done
 
-lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
+lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBK_def) 
 done
 
-lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
+lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBB_def) 
 done
 
-lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
+lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBC_def) 
@@ -180,7 +180,7 @@
 subsection {* Skolemization helpers *}
 
 definition skolem :: "'a \<Rightarrow> 'a" where
-[no_atp]: "skolem = (\<lambda>x. x)"
+"skolem = (\<lambda>x. x)"
 
 lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
 unfolding skolem_def COMBK_def by (rule refl)
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Metis.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -16,7 +16,7 @@
 subsection {* Literal selection and lambda-lifting helpers *}
 
 definition select :: "'a \<Rightarrow> 'a" where
-[no_atp]: "select = (\<lambda>x. x)"
+"select = (\<lambda>x. x)"
 
 lemma not_atomize: "(\<not> A \<Longrightarrow> False) \<equiv> Trueprop A"
 by (cut_tac atomize_not [of "\<not> A"]) simp
@@ -30,7 +30,7 @@
 lemma select_FalseI: "False \<Longrightarrow> select False" by simp
 
 definition lambda :: "'a \<Rightarrow> 'a" where
-[no_atp]: "lambda = (\<lambda>x. x)"
+"lambda = (\<lambda>x. x)"
 
 lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
 unfolding lambda_def by assumption
diff -r 97a8ff4e4ac9 -r c8cc5ab4a863 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Fri Oct 18 10:43:20 2013 +0200
+++ b/src/HOL/Nitpick.thy	Fri Oct 18 10:43:21 2013 +0200
@@ -33,7 +33,7 @@
 Alternative definitions.
 *}
 
-lemma Ex1_unfold [nitpick_unfold, no_atp]:
+lemma Ex1_unfold [nitpick_unfold]:
 "Ex1 P \<equiv> \<exists>x. {x. P x} = {x}"
 apply (rule eq_reflection)
 apply (simp add: Ex1_def set_eq_iff)
@@ -46,18 +46,18 @@
  apply (erule_tac x = y in allE)
 by auto
 
-lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
+lemma rtrancl_unfold [nitpick_unfold]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
   by (simp only: rtrancl_trancl_reflcl)
 
-lemma rtranclp_unfold [nitpick_unfold, no_atp]:
+lemma rtranclp_unfold [nitpick_unfold]:
 "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
 by (rule eq_reflection) (auto dest: rtranclpD)
 
-lemma tranclp_unfold [nitpick_unfold, no_atp]:
+lemma tranclp_unfold [nitpick_unfold]:
 "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
 by (simp add: trancl_def)
 
-lemma [nitpick_simp, no_atp]:
+lemma [nitpick_simp]:
 "of_nat n = (if n = 0 then 0 else 1 + of_nat (n - 1))"
 by (cases n) auto
 
@@ -85,18 +85,18 @@
 \textit{specialize} optimization.
 *}
 
-lemma The_psimp [nitpick_psimp, no_atp]:
+lemma The_psimp [nitpick_psimp]:
   "P = (op =) x \<Longrightarrow> The P = x"
   by auto
 
-lemma Eps_psimp [nitpick_psimp, no_atp]:
+lemma Eps_psimp [nitpick_psimp]:
 "\<lbrakk>P x; \<not> P y; Eps P = y\<rbrakk> \<Longrightarrow> Eps P = x"
 apply (cases "P (Eps P)")
  apply auto
 apply (erule contrapos_np)
 by (rule someI)
 
-lemma unit_case_unfold [nitpick_unfold, no_atp]:
+lemma unit_case_unfold [nitpick_unfold]:
 "unit_case x u \<equiv> x"
 apply (subgoal_tac "u = ()")
  apply (simp only: unit.cases)
@@ -104,14 +104,14 @@
 
 declare unit.cases [nitpick_simp del]
 
-lemma nat_case_unfold [nitpick_unfold, no_atp]:
+lemma nat_case_unfold [nitpick_unfold]:
 "nat_case x f n \<equiv> if n = 0 then x else f (n - 1)"
 apply (rule eq_reflection)
 by (cases n) auto
 
 declare nat.cases [nitpick_simp del]
 
-lemma list_size_simp [nitpick_simp, no_atp]:
+lemma list_size_simp [nitpick_simp]:
 "list_size f xs = (if xs = [] then 0
                    else Suc (f (hd xs) + list_size f (tl xs)))"
 "size xs = (if xs = [] then 0 else Suc (size (tl xs)))"