killed most "no_atp", to make Sledgehammer more complete
authorblanchet
Fri Oct 18 10:43:20 2013 +0200 (2013-10-18)
changeset 5414797a8ff4e4ac9
parent 54146 97f69d44f732
child 54148 c8cc5ab4a863
killed most "no_atp", to make Sledgehammer more complete
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/Fields.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Groups.thy
src/HOL/Int.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Product_Type.thy
src/HOL/Record.thy
src/HOL/Relation.thy
src/HOL/Rings.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -1999,35 +1999,35 @@
     1.4    assumes fin_nonempty: "finite A" "A \<noteq> {}"
     1.5  begin
     1.6  
     1.7 -lemma Min_ge_iff [simp, no_atp]:
     1.8 +lemma Min_ge_iff [simp]:
     1.9    "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
    1.10    using fin_nonempty by (fact Min.bounded_iff)
    1.11  
    1.12 -lemma Max_le_iff [simp, no_atp]:
    1.13 +lemma Max_le_iff [simp]:
    1.14    "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
    1.15    using fin_nonempty by (fact Max.bounded_iff)
    1.16  
    1.17 -lemma Min_gr_iff [simp, no_atp]:
    1.18 +lemma Min_gr_iff [simp]:
    1.19    "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
    1.20    using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
    1.21  
    1.22 -lemma Max_less_iff [simp, no_atp]:
    1.23 +lemma Max_less_iff [simp]:
    1.24    "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
    1.25    using fin_nonempty by (induct rule: finite_ne_induct) simp_all
    1.26  
    1.27 -lemma Min_le_iff [no_atp]:
    1.28 +lemma Min_le_iff:
    1.29    "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
    1.30    using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
    1.31  
    1.32 -lemma Max_ge_iff [no_atp]:
    1.33 +lemma Max_ge_iff:
    1.34    "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
    1.35    using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
    1.36  
    1.37 -lemma Min_less_iff [no_atp]:
    1.38 +lemma Min_less_iff:
    1.39    "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
    1.40    using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
    1.41  
    1.42 -lemma Max_gr_iff [no_atp]:
    1.43 +lemma Max_gr_iff:
    1.44    "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
    1.45    using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
    1.46  
     2.1 --- a/src/HOL/Complete_Lattices.thy	Fri Oct 18 10:35:57 2013 +0200
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Fri Oct 18 10:43:20 2013 +0200
     2.3 @@ -93,12 +93,12 @@
     2.4  context complete_lattice
     2.5  begin
     2.6  
     2.7 -lemma INF_foundation_dual [no_atp]:
     2.8 +lemma INF_foundation_dual:
     2.9    "complete_lattice.SUPR Inf = INFI"
    2.10    by (simp add: fun_eq_iff INF_def
    2.11      complete_lattice.SUP_def [OF dual_complete_lattice])
    2.12  
    2.13 -lemma SUP_foundation_dual [no_atp]:
    2.14 +lemma SUP_foundation_dual:
    2.15    "complete_lattice.INFI Sup = SUPR"
    2.16    by (simp add: fun_eq_iff SUP_def
    2.17      complete_lattice.INF_def [OF dual_complete_lattice])
    2.18 @@ -306,7 +306,7 @@
    2.19    show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
    2.20  qed
    2.21  
    2.22 -lemma Inf_top_conv [simp, no_atp]:
    2.23 +lemma Inf_top_conv [simp]:
    2.24    "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.25    "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.26  proof -
    2.27 @@ -333,7 +333,7 @@
    2.28   "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    2.29    by (auto simp add: INF_def)
    2.30  
    2.31 -lemma Sup_bot_conv [simp, no_atp]:
    2.32 +lemma Sup_bot_conv [simp]:
    2.33    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
    2.34    "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
    2.35    using dual_complete_lattice
    2.36 @@ -769,7 +769,7 @@
    2.37      by (simp add: Inf_set_def image_def)
    2.38  qed
    2.39  
    2.40 -lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
    2.41 +lemma Inter_iff [simp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
    2.42    by (unfold Inter_eq) blast
    2.43  
    2.44  lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
    2.45 @@ -814,7 +814,7 @@
    2.46  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
    2.47    by (fact Inf_union_distrib)
    2.48  
    2.49 -lemma Inter_UNIV_conv [simp, no_atp]:
    2.50 +lemma Inter_UNIV_conv [simp]:
    2.51    "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
    2.52    "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
    2.53    by (fact Inf_top_conv)+
    2.54 @@ -952,7 +952,7 @@
    2.55      by (simp add: Sup_set_def image_def)
    2.56  qed
    2.57  
    2.58 -lemma Union_iff [simp, no_atp]:
    2.59 +lemma Union_iff [simp]:
    2.60    "A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
    2.61    by (unfold Union_eq) blast
    2.62  
    2.63 @@ -987,10 +987,10 @@
    2.64  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
    2.65    by (fact Sup_inter_less_eq)
    2.66  
    2.67 -lemma Union_empty_conv [no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    2.68 +lemma Union_empty_conv: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    2.69    by (fact Sup_bot_conv) (* already simp *)
    2.70  
    2.71 -lemma empty_Union_conv [no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    2.72 +lemma empty_Union_conv: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
    2.73    by (fact Sup_bot_conv) (* already simp *)
    2.74  
    2.75  lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
    2.76 @@ -1044,7 +1044,7 @@
    2.77    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
    2.78  *} -- {* to avoid eta-contraction of body *}
    2.79  
    2.80 -lemma UNION_eq [no_atp]:
    2.81 +lemma UNION_eq:
    2.82    "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
    2.83    by (auto simp add: SUP_def)
    2.84  
    2.85 @@ -1088,13 +1088,13 @@
    2.86  lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
    2.87    by (fact SUP_least)
    2.88  
    2.89 -lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    2.90 +lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
    2.91    by blast
    2.92  
    2.93  lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
    2.94    by blast
    2.95  
    2.96 -lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
    2.97 +lemma UN_empty: "(\<Union>x\<in>{}. B x) = {}"
    2.98    by (fact SUP_empty)
    2.99  
   2.100  lemma UN_empty2: "(\<Union>x\<in>A. {}) = {}"
   2.101 @@ -1126,7 +1126,7 @@
   2.102    "(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
   2.103    by (fact SUP_bot_conv)+ (* already simp *)
   2.104  
   2.105 -lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   2.106 +lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   2.107    by blast
   2.108  
   2.109  lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
   2.110 @@ -1248,7 +1248,7 @@
   2.111    "\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
   2.112    by auto
   2.113  
   2.114 -lemma UN_ball_bex_simps [simp, no_atp]:
   2.115 +lemma UN_ball_bex_simps [simp]:
   2.116    "\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
   2.117    "\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
   2.118    "\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
     3.1 --- a/src/HOL/Fields.thy	Fri Oct 18 10:35:57 2013 +0200
     3.2 +++ b/src/HOL/Fields.thy	Fri Oct 18 10:43:20 2013 +0200
     3.3 @@ -152,7 +152,7 @@
     3.4  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
     3.5    by (simp add: divide_inverse nonzero_inverse_minus_eq)
     3.6  
     3.7 -lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
     3.8 +lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
     3.9    by (simp add: divide_inverse)
    3.10  
    3.11  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
    3.12 @@ -252,7 +252,7 @@
    3.13     ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
    3.14  by (simp add: division_ring_inverse_add mult_ac)
    3.15  
    3.16 -lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
    3.17 +lemma nonzero_mult_divide_mult_cancel_left [simp]:
    3.18  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
    3.19  proof -
    3.20    have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    3.21 @@ -263,7 +263,7 @@
    3.22      finally show ?thesis by (simp add: divide_inverse)
    3.23  qed
    3.24  
    3.25 -lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
    3.26 +lemma nonzero_mult_divide_mult_cancel_right [simp]:
    3.27    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
    3.28  by (simp add: mult_commute [of _ c])
    3.29  
    3.30 @@ -275,7 +275,7 @@
    3.31    fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
    3.32    many proofs seem to need them.*}
    3.33  
    3.34 -lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
    3.35 +lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
    3.36  
    3.37  lemma add_frac_eq:
    3.38    assumes "y \<noteq> 0" and "z \<noteq> 0"
    3.39 @@ -291,27 +291,27 @@
    3.40  
    3.41  text{*Special Cancellation Simprules for Division*}
    3.42  
    3.43 -lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
    3.44 +lemma nonzero_mult_divide_cancel_right [simp]:
    3.45    "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
    3.46    using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
    3.47  
    3.48 -lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
    3.49 +lemma nonzero_mult_divide_cancel_left [simp]:
    3.50    "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
    3.51  using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
    3.52  
    3.53 -lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
    3.54 +lemma nonzero_divide_mult_cancel_right [simp]:
    3.55    "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
    3.56  using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
    3.57  
    3.58 -lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
    3.59 +lemma nonzero_divide_mult_cancel_left [simp]:
    3.60    "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
    3.61  using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
    3.62  
    3.63 -lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
    3.64 +lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
    3.65    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
    3.66  using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
    3.67  
    3.68 -lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
    3.69 +lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
    3.70    "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
    3.71  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
    3.72  
    3.73 @@ -383,18 +383,18 @@
    3.74  apply simp_all
    3.75  done
    3.76  
    3.77 -lemma divide_divide_eq_right [simp, no_atp]:
    3.78 +lemma divide_divide_eq_right [simp]:
    3.79    "a / (b / c) = (a * c) / b"
    3.80    by (simp add: divide_inverse mult_ac)
    3.81  
    3.82 -lemma divide_divide_eq_left [simp, no_atp]:
    3.83 +lemma divide_divide_eq_left [simp]:
    3.84    "(a / b) / c = a / (b * c)"
    3.85    by (simp add: divide_inverse mult_assoc)
    3.86  
    3.87  
    3.88  text {*Special Cancellation Simprules for Division*}
    3.89  
    3.90 -lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
    3.91 +lemma mult_divide_mult_cancel_left_if [simp]:
    3.92    shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
    3.93    by (simp add: mult_divide_mult_cancel_left)
    3.94  
    3.95 @@ -405,7 +405,7 @@
    3.96    "- (a / b) = a / - b"
    3.97    by (simp add: divide_inverse)
    3.98  
    3.99 -lemma divide_minus_right [simp, no_atp]:
   3.100 +lemma divide_minus_right [simp]:
   3.101    "a / - b = - (a / b)"
   3.102    by (simp add: divide_inverse)
   3.103  
   3.104 @@ -427,29 +427,29 @@
   3.105    "inverse x = 1 \<longleftrightarrow> x = 1"
   3.106    by (insert inverse_eq_iff_eq [of x 1], simp) 
   3.107  
   3.108 -lemma divide_eq_0_iff [simp, no_atp]:
   3.109 +lemma divide_eq_0_iff [simp]:
   3.110    "a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
   3.111    by (simp add: divide_inverse)
   3.112  
   3.113 -lemma divide_cancel_right [simp, no_atp]:
   3.114 +lemma divide_cancel_right [simp]:
   3.115    "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
   3.116    apply (cases "c=0", simp)
   3.117    apply (simp add: divide_inverse)
   3.118    done
   3.119  
   3.120 -lemma divide_cancel_left [simp, no_atp]:
   3.121 +lemma divide_cancel_left [simp]:
   3.122    "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 
   3.123    apply (cases "c=0", simp)
   3.124    apply (simp add: divide_inverse)
   3.125    done
   3.126  
   3.127 -lemma divide_eq_1_iff [simp, no_atp]:
   3.128 +lemma divide_eq_1_iff [simp]:
   3.129    "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   3.130    apply (cases "b=0", simp)
   3.131    apply (simp add: right_inverse_eq)
   3.132    done
   3.133  
   3.134 -lemma one_eq_divide_iff [simp, no_atp]:
   3.135 +lemma one_eq_divide_iff [simp]:
   3.136    "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   3.137    by (simp add: eq_commute [of 1])
   3.138  
   3.139 @@ -559,7 +559,7 @@
   3.140  done
   3.141  
   3.142  text{*Both premises are essential. Consider -1 and 1.*}
   3.143 -lemma inverse_less_iff_less [simp,no_atp]:
   3.144 +lemma inverse_less_iff_less [simp]:
   3.145    "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   3.146    by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   3.147  
   3.148 @@ -567,7 +567,7 @@
   3.149    "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
   3.150    by (force simp add: le_less less_imp_inverse_less)
   3.151  
   3.152 -lemma inverse_le_iff_le [simp,no_atp]:
   3.153 +lemma inverse_le_iff_le [simp]:
   3.154    "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   3.155    by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   3.156  
   3.157 @@ -601,7 +601,7 @@
   3.158  apply (simp add: nonzero_inverse_minus_eq) 
   3.159  done
   3.160  
   3.161 -lemma inverse_less_iff_less_neg [simp,no_atp]:
   3.162 +lemma inverse_less_iff_less_neg [simp]:
   3.163    "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
   3.164  apply (insert inverse_less_iff_less [of "-b" "-a"])
   3.165  apply (simp del: inverse_less_iff_less 
   3.166 @@ -612,7 +612,7 @@
   3.167    "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
   3.168    by (force simp add: le_less less_imp_inverse_less_neg)
   3.169  
   3.170 -lemma inverse_le_iff_le_neg [simp,no_atp]:
   3.171 +lemma inverse_le_iff_le_neg [simp]:
   3.172    "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   3.173    by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   3.174  
   3.175 @@ -713,11 +713,9 @@
   3.176  sign_simps} to @{text field_simps} because the former can lead to case
   3.177  explosions. *}
   3.178  
   3.179 -lemmas sign_simps [no_atp] = algebra_simps
   3.180 -  zero_less_mult_iff mult_less_0_iff
   3.181 +lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   3.182  
   3.183 -lemmas (in -) sign_simps [no_atp] = algebra_simps
   3.184 -  zero_less_mult_iff mult_less_0_iff
   3.185 +lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
   3.186  
   3.187  (* Only works once linear arithmetic is installed:
   3.188  text{*An example:*}
   3.189 @@ -998,13 +996,13 @@
   3.190  
   3.191  text{*Simplify expressions equated with 1*}
   3.192  
   3.193 -lemma zero_eq_1_divide_iff [simp,no_atp]:
   3.194 +lemma zero_eq_1_divide_iff [simp]:
   3.195       "(0 = 1/a) = (a = 0)"
   3.196  apply (cases "a=0", simp)
   3.197  apply (auto simp add: nonzero_eq_divide_eq)
   3.198  done
   3.199  
   3.200 -lemma one_divide_eq_0_iff [simp,no_atp]:
   3.201 +lemma one_divide_eq_0_iff [simp]:
   3.202       "(1/a = 0) = (a = 0)"
   3.203  apply (cases "a=0", simp)
   3.204  apply (insert zero_neq_one [THEN not_sym])
   3.205 @@ -1013,19 +1011,19 @@
   3.206  
   3.207  text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
   3.208  
   3.209 -lemma zero_le_divide_1_iff [simp, no_atp]:
   3.210 +lemma zero_le_divide_1_iff [simp]:
   3.211    "0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
   3.212    by (simp add: zero_le_divide_iff)
   3.213  
   3.214 -lemma zero_less_divide_1_iff [simp, no_atp]:
   3.215 +lemma zero_less_divide_1_iff [simp]:
   3.216    "0 < 1 / a \<longleftrightarrow> 0 < a"
   3.217    by (simp add: zero_less_divide_iff)
   3.218  
   3.219 -lemma divide_le_0_1_iff [simp, no_atp]:
   3.220 +lemma divide_le_0_1_iff [simp]:
   3.221    "1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
   3.222    by (simp add: divide_le_0_iff)
   3.223  
   3.224 -lemma divide_less_0_1_iff [simp, no_atp]:
   3.225 +lemma divide_less_0_1_iff [simp]:
   3.226    "1 / a < 0 \<longleftrightarrow> a < 0"
   3.227    by (simp add: divide_less_0_iff)
   3.228  
   3.229 @@ -1080,62 +1078,62 @@
   3.230  
   3.231  text{*Simplify quotients that are compared with the value 1.*}
   3.232  
   3.233 -lemma le_divide_eq_1 [no_atp]:
   3.234 +lemma le_divide_eq_1:
   3.235    "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   3.236  by (auto simp add: le_divide_eq)
   3.237  
   3.238 -lemma divide_le_eq_1 [no_atp]:
   3.239 +lemma divide_le_eq_1:
   3.240    "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   3.241  by (auto simp add: divide_le_eq)
   3.242  
   3.243 -lemma less_divide_eq_1 [no_atp]:
   3.244 +lemma less_divide_eq_1:
   3.245    "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   3.246  by (auto simp add: less_divide_eq)
   3.247  
   3.248 -lemma divide_less_eq_1 [no_atp]:
   3.249 +lemma divide_less_eq_1:
   3.250    "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   3.251  by (auto simp add: divide_less_eq)
   3.252  
   3.253  
   3.254  text {*Conditional Simplification Rules: No Case Splits*}
   3.255  
   3.256 -lemma le_divide_eq_1_pos [simp,no_atp]:
   3.257 +lemma le_divide_eq_1_pos [simp]:
   3.258    "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
   3.259  by (auto simp add: le_divide_eq)
   3.260  
   3.261 -lemma le_divide_eq_1_neg [simp,no_atp]:
   3.262 +lemma le_divide_eq_1_neg [simp]:
   3.263    "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
   3.264  by (auto simp add: le_divide_eq)
   3.265  
   3.266 -lemma divide_le_eq_1_pos [simp,no_atp]:
   3.267 +lemma divide_le_eq_1_pos [simp]:
   3.268    "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
   3.269  by (auto simp add: divide_le_eq)
   3.270  
   3.271 -lemma divide_le_eq_1_neg [simp,no_atp]:
   3.272 +lemma divide_le_eq_1_neg [simp]:
   3.273    "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
   3.274  by (auto simp add: divide_le_eq)
   3.275  
   3.276 -lemma less_divide_eq_1_pos [simp,no_atp]:
   3.277 +lemma less_divide_eq_1_pos [simp]:
   3.278    "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
   3.279  by (auto simp add: less_divide_eq)
   3.280  
   3.281 -lemma less_divide_eq_1_neg [simp,no_atp]:
   3.282 +lemma less_divide_eq_1_neg [simp]:
   3.283    "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
   3.284  by (auto simp add: less_divide_eq)
   3.285  
   3.286 -lemma divide_less_eq_1_pos [simp,no_atp]:
   3.287 +lemma divide_less_eq_1_pos [simp]:
   3.288    "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
   3.289  by (auto simp add: divide_less_eq)
   3.290  
   3.291 -lemma divide_less_eq_1_neg [simp,no_atp]:
   3.292 +lemma divide_less_eq_1_neg [simp]:
   3.293    "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
   3.294  by (auto simp add: divide_less_eq)
   3.295  
   3.296 -lemma eq_divide_eq_1 [simp,no_atp]:
   3.297 +lemma eq_divide_eq_1 [simp]:
   3.298    "(1 = b/a) = ((a \<noteq> 0 & a = b))"
   3.299  by (auto simp add: eq_divide_eq)
   3.300  
   3.301 -lemma divide_eq_eq_1 [simp,no_atp]:
   3.302 +lemma divide_eq_eq_1 [simp]:
   3.303    "(b/a = 1) = ((a \<noteq> 0 & a = b))"
   3.304  by (auto simp add: divide_eq_eq)
   3.305  
     4.1 --- a/src/HOL/Finite_Set.thy	Fri Oct 18 10:35:57 2013 +0200
     4.2 +++ b/src/HOL/Finite_Set.thy	Fri Oct 18 10:43:20 2013 +0200
     4.3 @@ -1620,8 +1620,7 @@
     4.4    show False by simp (blast dest: Suc_neq_Zero surjD)
     4.5  qed
     4.6  
     4.7 -(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
     4.8 -lemma infinite_UNIV_char_0 [no_atp]:
     4.9 +lemma infinite_UNIV_char_0:
    4.10    "\<not> finite (UNIV :: 'a::semiring_char_0 set)"
    4.11  proof
    4.12    assume "finite (UNIV :: 'a set)"
     5.1 --- a/src/HOL/Fun.thy	Fri Oct 18 10:35:57 2013 +0200
     5.2 +++ b/src/HOL/Fun.thy	Fri Oct 18 10:43:20 2013 +0200
     5.3 @@ -775,7 +775,7 @@
     5.4  
     5.5  subsection {* Cantor's Paradox *}
     5.6  
     5.7 -lemma Cantors_paradox [no_atp]:
     5.8 +lemma Cantors_paradox:
     5.9    "\<not>(\<exists>f. f ` A = Pow A)"
    5.10  proof clarify
    5.11    fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
     6.1 --- a/src/HOL/Groups.thy	Fri Oct 18 10:35:57 2013 +0200
     6.2 +++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
     6.3 @@ -1341,7 +1341,7 @@
     6.4  
     6.5  subsection {* Tools setup *}
     6.6  
     6.7 -lemma add_mono_thms_linordered_semiring [no_atp]:
     6.8 +lemma add_mono_thms_linordered_semiring:
     6.9    fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
    6.10    shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    6.11      and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    6.12 @@ -1349,7 +1349,7 @@
    6.13      and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
    6.14  by (rule add_mono, clarify+)+
    6.15  
    6.16 -lemma add_mono_thms_linordered_field [no_atp]:
    6.17 +lemma add_mono_thms_linordered_field:
    6.18    fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
    6.19    shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
    6.20      and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
     7.1 --- a/src/HOL/Int.thy	Fri Oct 18 10:35:57 2013 +0200
     7.2 +++ b/src/HOL/Int.thy	Fri Oct 18 10:43:20 2013 +0200
     7.3 @@ -450,7 +450,7 @@
     7.4        It is proved here because attribute @{text arith_split} is not available
     7.5        in theory @{text Rings}.
     7.6        But is it really better than just rewriting with @{text abs_if}?*}
     7.7 -lemma abs_split [arith_split,no_atp]:
     7.8 +lemma abs_split [arith_split, no_atp]:
     7.9       "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
    7.10  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    7.11  
    7.12 @@ -1158,32 +1158,32 @@
    7.13  
    7.14  text{*To Simplify Inequalities Where One Side is the Constant 1*}
    7.15  
    7.16 -lemma less_minus_iff_1 [simp,no_atp]:
    7.17 +lemma less_minus_iff_1 [simp]:
    7.18    fixes b::"'b::linordered_idom"
    7.19    shows "(1 < - b) = (b < -1)"
    7.20  by auto
    7.21  
    7.22 -lemma le_minus_iff_1 [simp,no_atp]:
    7.23 +lemma le_minus_iff_1 [simp]:
    7.24    fixes b::"'b::linordered_idom"
    7.25    shows "(1 \<le> - b) = (b \<le> -1)"
    7.26  by auto
    7.27  
    7.28 -lemma equation_minus_iff_1 [simp,no_atp]:
    7.29 +lemma equation_minus_iff_1 [simp]:
    7.30    fixes b::"'b::ring_1"
    7.31    shows "(1 = - b) = (b = -1)"
    7.32  by (subst equation_minus_iff, auto)
    7.33  
    7.34 -lemma minus_less_iff_1 [simp,no_atp]:
    7.35 +lemma minus_less_iff_1 [simp]:
    7.36    fixes a::"'b::linordered_idom"
    7.37    shows "(- a < 1) = (-1 < a)"
    7.38  by auto
    7.39  
    7.40 -lemma minus_le_iff_1 [simp,no_atp]:
    7.41 +lemma minus_le_iff_1 [simp]:
    7.42    fixes a::"'b::linordered_idom"
    7.43    shows "(- a \<le> 1) = (-1 \<le> a)"
    7.44  by auto
    7.45  
    7.46 -lemma minus_equation_iff_1 [simp,no_atp]:
    7.47 +lemma minus_equation_iff_1 [simp]:
    7.48    fixes a::"'b::ring_1"
    7.49    shows "(- a = 1) = (a = -1)"
    7.50  by (subst minus_equation_iff, auto)
     8.1 --- a/src/HOL/List.thy	Fri Oct 18 10:35:57 2013 +0200
     8.2 +++ b/src/HOL/List.thy	Fri Oct 18 10:43:20 2013 +0200
     8.3 @@ -902,7 +902,7 @@
     8.4  lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
     8.5  by (induct xs) auto
     8.6  
     8.7 -lemma append_eq_append_conv [simp, no_atp]:
     8.8 +lemma append_eq_append_conv [simp]:
     8.9   "length xs = length ys \<or> length us = length vs
    8.10   ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
    8.11  apply (induct xs arbitrary: ys)
    8.12 @@ -934,7 +934,7 @@
    8.13  lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
    8.14  using append_same_eq [of "[]"] by auto
    8.15  
    8.16 -lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    8.17 +lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    8.18  by (induct xs) auto
    8.19  
    8.20  lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
    8.21 @@ -1178,7 +1178,7 @@
    8.22  lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
    8.23  by (cases xs) auto
    8.24  
    8.25 -lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
    8.26 +lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
    8.27  apply (induct xs arbitrary: ys, force)
    8.28  apply (case_tac ys, simp, force)
    8.29  done
    8.30 @@ -5084,10 +5084,10 @@
    8.31    for A :: "'a set"
    8.32  where
    8.33      Nil [intro!, simp]: "[]: lists A"
    8.34 -  | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
    8.35 -
    8.36 -inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
    8.37 -inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
    8.38 +  | Cons [intro!, simp]: "[| a: A; l: lists A|] ==> a#l : lists A"
    8.39 +
    8.40 +inductive_cases listsE [elim!]: "x#l : lists A"
    8.41 +inductive_cases listspE [elim!]: "listsp A (x # l)"
    8.42  
    8.43  inductive_simps listsp_simps[code]:
    8.44    "listsp A []"
    8.45 @@ -5129,15 +5129,15 @@
    8.46  
    8.47  lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
    8.48  
    8.49 -lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    8.50 +lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    8.51  by (rule in_listsp_conv_set [THEN iffD1])
    8.52  
    8.53 -lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
    8.54 -
    8.55 -lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    8.56 +lemmas in_listsD [dest!] = in_listspD [to_set]
    8.57 +
    8.58 +lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    8.59  by (rule in_listsp_conv_set [THEN iffD2])
    8.60  
    8.61 -lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
    8.62 +lemmas in_listsI [intro!] = in_listspI [to_set]
    8.63  
    8.64  lemma lists_eq_set: "lists A = {xs. set xs <= A}"
    8.65  by auto
     9.1 --- a/src/HOL/Nat.thy	Fri Oct 18 10:35:57 2013 +0200
     9.2 +++ b/src/HOL/Nat.thy	Fri Oct 18 10:43:20 2013 +0200
     9.3 @@ -327,7 +327,7 @@
     9.4     apply auto
     9.5    done
     9.6  
     9.7 -lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
     9.8 +lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
     9.9    apply (rule trans)
    9.10    apply (rule_tac [2] mult_eq_1_iff, fastforce)
    9.11    done
    9.12 @@ -491,7 +491,7 @@
    9.13  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
    9.14    by (simp add: less_Suc_eq)
    9.15  
    9.16 -lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
    9.17 +lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
    9.18    unfolding One_nat_def by (rule less_Suc0)
    9.19  
    9.20  lemma Suc_mono: "m < n ==> Suc m < Suc n"
    9.21 @@ -659,7 +659,7 @@
    9.22  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
    9.23  by (fast intro: not0_implies_Suc)
    9.24  
    9.25 -lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
    9.26 +lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
    9.27  using neq0_conv by blast
    9.28  
    9.29  lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
    9.30 @@ -1396,10 +1396,10 @@
    9.31  
    9.32  text{*Special cases where either operand is zero*}
    9.33  
    9.34 -lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
    9.35 +lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
    9.36    by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
    9.37  
    9.38 -lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    9.39 +lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
    9.40    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
    9.41  
    9.42  end
    9.43 @@ -1432,7 +1432,7 @@
    9.44  
    9.45  text{*Special cases where either operand is zero*}
    9.46  
    9.47 -lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
    9.48 +lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
    9.49    by (rule of_nat_le_iff [of _ 0, simplified])
    9.50  
    9.51  lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
    10.1 --- a/src/HOL/Orderings.thy	Fri Oct 18 10:35:57 2013 +0200
    10.2 +++ b/src/HOL/Orderings.thy	Fri Oct 18 10:43:20 2013 +0200
    10.3 @@ -998,7 +998,7 @@
    10.4      (!!x y. x > y ==> f x > f y) ==> f a > c"
    10.5  by (subgoal_tac "f a > f b", force, force)
    10.6  
    10.7 -lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
    10.8 +lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
    10.9  
   10.10  (* 
   10.11    Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
    11.1 --- a/src/HOL/Power.thy	Fri Oct 18 10:35:57 2013 +0200
    11.2 +++ b/src/HOL/Power.thy	Fri Oct 18 10:43:20 2013 +0200
    11.3 @@ -530,7 +530,7 @@
    11.4    "abs ((-a) ^ n) = abs (a ^ n)"
    11.5    by (simp add: power_abs)
    11.6  
    11.7 -lemma zero_less_power_abs_iff [simp, no_atp]:
    11.8 +lemma zero_less_power_abs_iff [simp]:
    11.9    "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   11.10  proof (induct n)
   11.11    case 0 show ?case by simp
    12.1 --- a/src/HOL/Product_Type.thy	Fri Oct 18 10:35:57 2013 +0200
    12.2 +++ b/src/HOL/Product_Type.thy	Fri Oct 18 10:43:20 2013 +0200
    12.3 @@ -75,10 +75,10 @@
    12.4    f} rather than by @{term [source] "%u. f ()"}.
    12.5  *}
    12.6  
    12.7 -lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
    12.8 +lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
    12.9    by (rule ext) simp
   12.10  
   12.11 -lemma UNIV_unit [no_atp]:
   12.12 +lemma UNIV_unit:
   12.13    "UNIV = {()}" by auto
   12.14  
   12.15  instantiation unit :: default
   12.16 @@ -586,10 +586,10 @@
   12.17     to quite time-consuming computations (in particular for nested tuples) *)
   12.18  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
   12.19  
   12.20 -lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   12.21 +lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   12.22    by (rule ext) fast
   12.23  
   12.24 -lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   12.25 +lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   12.26    by (rule ext) fast
   12.27  
   12.28  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
    13.1 --- a/src/HOL/Record.thy	Fri Oct 18 10:35:57 2013 +0200
    13.2 +++ b/src/HOL/Record.thy	Fri Oct 18 10:43:20 2013 +0200
    13.3 @@ -399,7 +399,7 @@
    13.4  lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
    13.5    by simp
    13.6  
    13.7 -lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
    13.8 +lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
    13.9    by simp
   13.10  
   13.11  lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
    14.1 --- a/src/HOL/Relation.thy	Fri Oct 18 10:35:57 2013 +0200
    14.2 +++ b/src/HOL/Relation.thy	Fri Oct 18 10:43:20 2013 +0200
    14.3 @@ -478,7 +478,7 @@
    14.4  lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
    14.5    by (simp add: Id_on_def)
    14.6  
    14.7 -lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
    14.8 +lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A"
    14.9    by (rule Id_on_eqI) (rule refl)
   14.10  
   14.11  lemma Id_onE [elim!]:
   14.12 @@ -939,8 +939,6 @@
   14.13  where
   14.14    "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
   14.15  
   14.16 -declare Image_def [no_atp]
   14.17 -
   14.18  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   14.19    by (simp add: Image_def)
   14.20  
   14.21 @@ -950,7 +948,7 @@
   14.22  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   14.23    by (rule Image_iff [THEN trans]) simp
   14.24  
   14.25 -lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
   14.26 +lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
   14.27    by (unfold Image_def) blast
   14.28  
   14.29  lemma ImageE [elim!]:
    15.1 --- a/src/HOL/Rings.thy	Fri Oct 18 10:35:57 2013 +0200
    15.2 +++ b/src/HOL/Rings.thy	Fri Oct 18 10:43:20 2013 +0200
    15.3 @@ -127,7 +127,7 @@
    15.4    then show ?thesis ..
    15.5  qed
    15.6  
    15.7 -lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
    15.8 +lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
    15.9  by (auto intro: dvd_refl elim!: dvdE)
   15.10  
   15.11  lemma dvd_0_right [iff]: "a dvd 0"
   15.12 @@ -233,8 +233,8 @@
   15.13  by (rule minus_unique) (simp add: distrib_left [symmetric]) 
   15.14  
   15.15  text{*Extract signs from products*}
   15.16 -lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
   15.17 -lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
   15.18 +lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
   15.19 +lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
   15.20  
   15.21  lemma minus_mult_minus [simp]: "- a * - b = a * b"
   15.22  by simp
   15.23 @@ -248,7 +248,7 @@
   15.24  lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
   15.25  by (simp add: distrib_right diff_minus)
   15.26  
   15.27 -lemmas ring_distribs[no_atp] =
   15.28 +lemmas ring_distribs =
   15.29    distrib_left distrib_right left_diff_distrib right_diff_distrib
   15.30  
   15.31  lemma eq_add_iff1:
   15.32 @@ -261,7 +261,7 @@
   15.33  
   15.34  end
   15.35  
   15.36 -lemmas ring_distribs[no_atp] =
   15.37 +lemmas ring_distribs =
   15.38    distrib_left distrib_right left_diff_distrib right_diff_distrib
   15.39  
   15.40  class comm_ring = comm_semiring + ab_group_add
   15.41 @@ -336,7 +336,7 @@
   15.42  qed
   15.43  
   15.44  text{*Cancellation of equalities with a common factor*}
   15.45 -lemma mult_cancel_right [simp, no_atp]:
   15.46 +lemma mult_cancel_right [simp]:
   15.47    "a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
   15.48  proof -
   15.49    have "(a * c = b * c) = ((a - b) * c = 0)"
   15.50 @@ -344,7 +344,7 @@
   15.51    thus ?thesis by (simp add: disj_commute)
   15.52  qed
   15.53  
   15.54 -lemma mult_cancel_left [simp, no_atp]:
   15.55 +lemma mult_cancel_left [simp]:
   15.56    "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
   15.57  proof -
   15.58    have "(c * a = c * b) = (c * (a - b) = 0)"
   15.59 @@ -1048,7 +1048,7 @@
   15.60  
   15.61  text {* Simprules for comparisons where common factors can be cancelled. *}
   15.62  
   15.63 -lemmas mult_compare_simps[no_atp] =
   15.64 +lemmas mult_compare_simps =
   15.65      mult_le_cancel_right mult_le_cancel_left
   15.66      mult_le_cancel_right1 mult_le_cancel_right2
   15.67      mult_le_cancel_left1 mult_le_cancel_left2
    16.1 --- a/src/HOL/Set.thy	Fri Oct 18 10:35:57 2013 +0200
    16.2 +++ b/src/HOL/Set.thy	Fri Oct 18 10:43:20 2013 +0200
    16.3 @@ -87,7 +87,7 @@
    16.4    then show ?thesis by simp
    16.5  qed
    16.6  
    16.7 -lemma set_eq_iff [no_atp]:
    16.8 +lemma set_eq_iff:
    16.9    "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
   16.10    by (auto intro:set_eqI)
   16.11  
   16.12 @@ -495,7 +495,7 @@
   16.13    by (simp add: less_eq_set_def le_fun_def)
   16.14    -- {* Rule in Modus Ponens style. *}
   16.15  
   16.16 -lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   16.17 +lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
   16.18    -- {* The same, with reversed premises for use with @{text erule} --
   16.19        cf @{text rev_mp}. *}
   16.20    by (rule subsetD)
   16.21 @@ -504,13 +504,13 @@
   16.22    \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
   16.23  *}
   16.24  
   16.25 -lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   16.26 +lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
   16.27    -- {* Classical elimination rule. *}
   16.28    by (auto simp add: less_eq_set_def le_fun_def)
   16.29  
   16.30 -lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   16.31 -
   16.32 -lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   16.33 +lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
   16.34 +
   16.35 +lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
   16.36    by blast
   16.37  
   16.38  lemma subset_refl: "A \<subseteq> A"
   16.39 @@ -845,11 +845,11 @@
   16.40  
   16.41  subsubsection {* Singletons, using insert *}
   16.42  
   16.43 -lemma singletonI [intro!,no_atp]: "a : {a}"
   16.44 +lemma singletonI [intro!]: "a : {a}"
   16.45      -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   16.46    by (rule insertI1)
   16.47  
   16.48 -lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
   16.49 +lemma singletonD [dest!]: "b : {a} ==> b = a"
   16.50    by blast
   16.51  
   16.52  lemmas singletonE = singletonD [elim_format]
   16.53 @@ -860,11 +860,11 @@
   16.54  lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   16.55    by blast
   16.56  
   16.57 -lemma singleton_insert_inj_eq [iff,no_atp]:
   16.58 +lemma singleton_insert_inj_eq [iff]:
   16.59       "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   16.60    by blast
   16.61  
   16.62 -lemma singleton_insert_inj_eq' [iff,no_atp]:
   16.63 +lemma singleton_insert_inj_eq' [iff]:
   16.64       "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   16.65    by blast
   16.66  
   16.67 @@ -898,7 +898,7 @@
   16.68  *}
   16.69  
   16.70  definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
   16.71 -  image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
   16.72 +  image_def: "f ` A = {y. EX x:A. y = f(x)}"
   16.73  
   16.74  abbreviation
   16.75    range :: "('a => 'b) => 'b set" where -- "of function"
   16.76 @@ -930,7 +930,7 @@
   16.77  lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
   16.78    by blast
   16.79  
   16.80 -lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   16.81 +lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
   16.82    -- {* This rewrite rule would confuse users if made default. *}
   16.83    by blast
   16.84  
   16.85 @@ -1009,10 +1009,10 @@
   16.86  
   16.87  subsubsection {* The ``proper subset'' relation *}
   16.88  
   16.89 -lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   16.90 +lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   16.91    by (unfold less_le) blast
   16.92  
   16.93 -lemma psubsetE [elim!,no_atp]:
   16.94 +lemma psubsetE [elim!]:
   16.95      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   16.96    by (unfold less_le) blast
   16.97  
   16.98 @@ -1184,12 +1184,12 @@
   16.99  lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
  16.100    by blast
  16.101  
  16.102 -lemma insert_disjoint [simp,no_atp]:
  16.103 +lemma insert_disjoint [simp]:
  16.104   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  16.105   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
  16.106    by auto
  16.107  
  16.108 -lemma disjoint_insert [simp,no_atp]:
  16.109 +lemma disjoint_insert [simp]:
  16.110   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  16.111   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
  16.112    by auto
  16.113 @@ -1221,7 +1221,7 @@
  16.114  by blast
  16.115  
  16.116  
  16.117 -lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
  16.118 +lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
  16.119    -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
  16.120        with its implicit quantifier and conjunction.  Also image enjoys better
  16.121        equational properties than does the RHS. *}
  16.122 @@ -1244,7 +1244,7 @@
  16.123  
  16.124  text {* \medskip @{text range}. *}
  16.125  
  16.126 -lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
  16.127 +lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
  16.128    by auto
  16.129  
  16.130  lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
  16.131 @@ -1301,10 +1301,10 @@
  16.132  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
  16.133    by (fact inf_sup_distrib2)
  16.134  
  16.135 -lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  16.136 +lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  16.137    by (fact inf_eq_top_iff) (* already simp *)
  16.138  
  16.139 -lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  16.140 +lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  16.141    by (fact le_inf_iff)
  16.142  
  16.143  lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
  16.144 @@ -1395,7 +1395,7 @@
  16.145  lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
  16.146    by (fact sup_eq_bot_iff) (* FIXME: already simp *)
  16.147  
  16.148 -lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
  16.149 +lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
  16.150    by (fact le_sup_iff)
  16.151  
  16.152  lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
  16.153 @@ -1467,7 +1467,7 @@
  16.154  lemma Diff_eq: "A - B = A \<inter> (-B)"
  16.155    by blast
  16.156  
  16.157 -lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
  16.158 +lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
  16.159    by blast
  16.160  
  16.161  lemma Diff_cancel [simp]: "A - A = {}"
  16.162 @@ -1488,7 +1488,7 @@
  16.163  lemma Diff_UNIV [simp]: "A - UNIV = {}"
  16.164    by blast
  16.165  
  16.166 -lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
  16.167 +lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
  16.168    by blast
  16.169  
  16.170  lemma Diff_insert: "A - insert a B = A - B - {a}"
  16.171 @@ -1568,7 +1568,7 @@
  16.172  lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
  16.173    by (auto intro: bool_contrapos)
  16.174  
  16.175 -lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
  16.176 +lemma UNIV_bool: "UNIV = {False, True}"
  16.177    by (auto intro: bool_induct)
  16.178  
  16.179  text {* \medskip @{text Pow} *}
  16.180 @@ -1597,7 +1597,7 @@
  16.181  lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
  16.182    by blast
  16.183  
  16.184 -lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
  16.185 +lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
  16.186    by blast
  16.187  
  16.188  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
  16.189 @@ -1754,7 +1754,7 @@
  16.190    -- {* monotonicity *}
  16.191    by blast
  16.192  
  16.193 -lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  16.194 +lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
  16.195  by (blast intro: sym)
  16.196  
  16.197  lemma image_vimage_subset: "f ` (f -` A) <= A"
    17.1 --- a/src/HOL/Set_Interval.thy	Fri Oct 18 10:35:57 2013 +0200
    17.2 +++ b/src/HOL/Set_Interval.thy	Fri Oct 18 10:43:20 2013 +0200
    17.3 @@ -180,19 +180,19 @@
    17.4  context ord
    17.5  begin
    17.6  
    17.7 -lemma greaterThanLessThan_iff [simp,no_atp]:
    17.8 +lemma greaterThanLessThan_iff [simp]:
    17.9    "(i : {l<..<u}) = (l < i & i < u)"
   17.10  by (simp add: greaterThanLessThan_def)
   17.11  
   17.12 -lemma atLeastLessThan_iff [simp,no_atp]:
   17.13 +lemma atLeastLessThan_iff [simp]:
   17.14    "(i : {l..<u}) = (l <= i & i < u)"
   17.15  by (simp add: atLeastLessThan_def)
   17.16  
   17.17 -lemma greaterThanAtMost_iff [simp,no_atp]:
   17.18 +lemma greaterThanAtMost_iff [simp]:
   17.19    "(i : {l<..u}) = (l < i & i <= u)"
   17.20  by (simp add: greaterThanAtMost_def)
   17.21  
   17.22 -lemma atLeastAtMost_iff [simp,no_atp]:
   17.23 +lemma atLeastAtMost_iff [simp]:
   17.24    "(i : {l..u}) = (l <= i & i <= u)"
   17.25  by (simp add: atLeastAtMost_def)
   17.26  
   17.27 @@ -1196,7 +1196,7 @@
   17.28  
   17.29  subsubsection {* Some Subset Conditions *}
   17.30  
   17.31 -lemma ivl_subset [simp,no_atp]:
   17.32 +lemma ivl_subset [simp]:
   17.33   "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
   17.34  apply(auto simp:linorder_not_le)
   17.35  apply(rule ccontr)