--- a/src/HOL/Big_Operators.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Big_Operators.thy Fri Oct 18 10:43:20 2013 +0200
@@ -1999,35 +1999,35 @@
assumes fin_nonempty: "finite A" "A \<noteq> {}"
begin
-lemma Min_ge_iff [simp, no_atp]:
+lemma Min_ge_iff [simp]:
"x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
using fin_nonempty by (fact Min.bounded_iff)
-lemma Max_le_iff [simp, no_atp]:
+lemma Max_le_iff [simp]:
"Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
using fin_nonempty by (fact Max.bounded_iff)
-lemma Min_gr_iff [simp, no_atp]:
+lemma Min_gr_iff [simp]:
"x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
using fin_nonempty by (induct rule: finite_ne_induct) simp_all
-lemma Max_less_iff [simp, no_atp]:
+lemma Max_less_iff [simp]:
"Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
using fin_nonempty by (induct rule: finite_ne_induct) simp_all
-lemma Min_le_iff [no_atp]:
+lemma Min_le_iff:
"Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
-lemma Max_ge_iff [no_atp]:
+lemma Max_ge_iff:
"x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
-lemma Min_less_iff [no_atp]:
+lemma Min_less_iff:
"Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
-lemma Max_gr_iff [no_atp]:
+lemma Max_gr_iff:
"x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
--- a/src/HOL/Complete_Lattices.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Oct 18 10:43:20 2013 +0200
@@ -93,12 +93,12 @@
context complete_lattice
begin
-lemma INF_foundation_dual [no_atp]:
+lemma INF_foundation_dual:
"complete_lattice.SUPR Inf = INFI"
by (simp add: fun_eq_iff INF_def
complete_lattice.SUP_def [OF dual_complete_lattice])
-lemma SUP_foundation_dual [no_atp]:
+lemma SUP_foundation_dual:
"complete_lattice.INFI Sup = SUPR"
by (simp add: fun_eq_iff SUP_def
complete_lattice.INF_def [OF dual_complete_lattice])
@@ -306,7 +306,7 @@
show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
qed
-lemma Inf_top_conv [simp, no_atp]:
+lemma Inf_top_conv [simp]:
"\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
"\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
proof -
@@ -333,7 +333,7 @@
"\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
by (auto simp add: INF_def)
-lemma Sup_bot_conv [simp, no_atp]:
+lemma Sup_bot_conv [simp]:
"\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
"\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
using dual_complete_lattice
@@ -769,7 +769,7 @@
by (simp add: Inf_set_def image_def)
qed
-lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
+lemma Inter_iff [simp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
by (unfold Inter_eq) blast
lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
@@ -814,7 +814,7 @@
lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
by (fact Inf_union_distrib)
-lemma Inter_UNIV_conv [simp, no_atp]:
+lemma Inter_UNIV_conv [simp]:
"\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
"UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
by (fact Inf_top_conv)+
@@ -952,7 +952,7 @@
by (simp add: Sup_set_def image_def)
qed
-lemma Union_iff [simp, no_atp]:
+lemma Union_iff [simp]:
"A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
by (unfold Union_eq) blast
@@ -987,10 +987,10 @@
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
by (fact Sup_inter_less_eq)
-lemma Union_empty_conv [no_atp]: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv: "(\<Union>A = {}) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
by (fact Sup_bot_conv) (* already simp *)
-lemma empty_Union_conv [no_atp]: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv: "({} = \<Union>A) \<longleftrightarrow> (\<forall>x\<in>A. x = {})"
by (fact Sup_bot_conv) (* already simp *)
lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
@@ -1044,7 +1044,7 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
*} -- {* to avoid eta-contraction of body *}
-lemma UNION_eq [no_atp]:
+lemma UNION_eq:
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by (auto simp add: SUP_def)
@@ -1088,13 +1088,13 @@
lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
by (fact SUP_least)
-lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
by blast
lemma UN_insert_distrib: "u \<in> A \<Longrightarrow> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
-lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
+lemma UN_empty: "(\<Union>x\<in>{}. B x) = {}"
by (fact SUP_empty)
lemma UN_empty2: "(\<Union>x\<in>A. {}) = {}"
@@ -1126,7 +1126,7 @@
"(\<Union>x\<in>A. B x) = {} \<longleftrightarrow> (\<forall>x\<in>A. B x = {})"
by (fact SUP_bot_conv)+ (* already simp *)
-lemma Collect_ex_eq [no_atp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
by blast
lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
@@ -1248,7 +1248,7 @@
"\<And>A B f. (\<Inter>x\<in>f`A. B x) = (\<Inter>a\<in>A. B (f a))"
by auto
-lemma UN_ball_bex_simps [simp, no_atp]:
+lemma UN_ball_bex_simps [simp]:
"\<And>A P. (\<forall>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P x)"
"\<And>A B P. (\<forall>x\<in>UNION A B. P x) = (\<forall>a\<in>A. \<forall>x\<in> B a. P x)"
"\<And>A P. (\<exists>x\<in>\<Union>A. P x) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y. P x)"
--- a/src/HOL/Fields.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Fields.thy Fri Oct 18 10:43:20 2013 +0200
@@ -152,7 +152,7 @@
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
-lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
+lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
by (simp add: divide_inverse)
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -252,7 +252,7 @@
==> inverse a + inverse b = (a + b) * inverse a * inverse b"
by (simp add: division_ring_inverse_add mult_ac)
-lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_left [simp]:
assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
proof -
have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
@@ -263,7 +263,7 @@
finally show ?thesis by (simp add: divide_inverse)
qed
-lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_right [simp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
by (simp add: mult_commute [of _ c])
@@ -275,7 +275,7 @@
fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
many proofs seem to need them.*}
-lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
lemma add_frac_eq:
assumes "y \<noteq> 0" and "z \<noteq> 0"
@@ -291,27 +291,27 @@
text{*Special Cancellation Simprules for Division*}
-lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
+lemma nonzero_mult_divide_cancel_right [simp]:
"b \<noteq> 0 \<Longrightarrow> a * b / b = a"
using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
-lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
+lemma nonzero_mult_divide_cancel_left [simp]:
"a \<noteq> 0 \<Longrightarrow> a * b / a = b"
using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
-lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
+lemma nonzero_divide_mult_cancel_right [simp]:
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
-lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
+lemma nonzero_divide_mult_cancel_left [simp]:
"\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
-lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: mult_ac)
-lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
+lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
@@ -383,18 +383,18 @@
apply simp_all
done
-lemma divide_divide_eq_right [simp, no_atp]:
+lemma divide_divide_eq_right [simp]:
"a / (b / c) = (a * c) / b"
by (simp add: divide_inverse mult_ac)
-lemma divide_divide_eq_left [simp, no_atp]:
+lemma divide_divide_eq_left [simp]:
"(a / b) / c = a / (b * c)"
by (simp add: divide_inverse mult_assoc)
text {*Special Cancellation Simprules for Division*}
-lemma mult_divide_mult_cancel_left_if [simp,no_atp]:
+lemma mult_divide_mult_cancel_left_if [simp]:
shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
by (simp add: mult_divide_mult_cancel_left)
@@ -405,7 +405,7 @@
"- (a / b) = a / - b"
by (simp add: divide_inverse)
-lemma divide_minus_right [simp, no_atp]:
+lemma divide_minus_right [simp]:
"a / - b = - (a / b)"
by (simp add: divide_inverse)
@@ -427,29 +427,29 @@
"inverse x = 1 \<longleftrightarrow> x = 1"
by (insert inverse_eq_iff_eq [of x 1], simp)
-lemma divide_eq_0_iff [simp, no_atp]:
+lemma divide_eq_0_iff [simp]:
"a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
by (simp add: divide_inverse)
-lemma divide_cancel_right [simp, no_atp]:
+lemma divide_cancel_right [simp]:
"a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
done
-lemma divide_cancel_left [simp, no_atp]:
+lemma divide_cancel_left [simp]:
"c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
done
-lemma divide_eq_1_iff [simp, no_atp]:
+lemma divide_eq_1_iff [simp]:
"a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
apply (cases "b=0", simp)
apply (simp add: right_inverse_eq)
done
-lemma one_eq_divide_iff [simp, no_atp]:
+lemma one_eq_divide_iff [simp]:
"1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
by (simp add: eq_commute [of 1])
@@ -559,7 +559,7 @@
done
text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,no_atp]:
+lemma inverse_less_iff_less [simp]:
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
@@ -567,7 +567,7 @@
"a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
by (force simp add: le_less less_imp_inverse_less)
-lemma inverse_le_iff_le [simp,no_atp]:
+lemma inverse_le_iff_le [simp]:
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
@@ -601,7 +601,7 @@
apply (simp add: nonzero_inverse_minus_eq)
done
-lemma inverse_less_iff_less_neg [simp,no_atp]:
+lemma inverse_less_iff_less_neg [simp]:
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
apply (insert inverse_less_iff_less [of "-b" "-a"])
apply (simp del: inverse_less_iff_less
@@ -612,7 +612,7 @@
"a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
by (force simp add: le_less less_imp_inverse_less_neg)
-lemma inverse_le_iff_le_neg [simp,no_atp]:
+lemma inverse_le_iff_le_neg [simp]:
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
@@ -713,11 +713,9 @@
sign_simps} to @{text field_simps} because the former can lead to case
explosions. *}
-lemmas sign_simps [no_atp] = algebra_simps
- zero_less_mult_iff mult_less_0_iff
+lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
-lemmas (in -) sign_simps [no_atp] = algebra_simps
- zero_less_mult_iff mult_less_0_iff
+lemmas (in -) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
(* Only works once linear arithmetic is installed:
text{*An example:*}
@@ -998,13 +996,13 @@
text{*Simplify expressions equated with 1*}
-lemma zero_eq_1_divide_iff [simp,no_atp]:
+lemma zero_eq_1_divide_iff [simp]:
"(0 = 1/a) = (a = 0)"
apply (cases "a=0", simp)
apply (auto simp add: nonzero_eq_divide_eq)
done
-lemma one_divide_eq_0_iff [simp,no_atp]:
+lemma one_divide_eq_0_iff [simp]:
"(1/a = 0) = (a = 0)"
apply (cases "a=0", simp)
apply (insert zero_neq_one [THEN not_sym])
@@ -1013,19 +1011,19 @@
text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
-lemma zero_le_divide_1_iff [simp, no_atp]:
+lemma zero_le_divide_1_iff [simp]:
"0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a"
by (simp add: zero_le_divide_iff)
-lemma zero_less_divide_1_iff [simp, no_atp]:
+lemma zero_less_divide_1_iff [simp]:
"0 < 1 / a \<longleftrightarrow> 0 < a"
by (simp add: zero_less_divide_iff)
-lemma divide_le_0_1_iff [simp, no_atp]:
+lemma divide_le_0_1_iff [simp]:
"1 / a \<le> 0 \<longleftrightarrow> a \<le> 0"
by (simp add: divide_le_0_iff)
-lemma divide_less_0_1_iff [simp, no_atp]:
+lemma divide_less_0_1_iff [simp]:
"1 / a < 0 \<longleftrightarrow> a < 0"
by (simp add: divide_less_0_iff)
@@ -1080,62 +1078,62 @@
text{*Simplify quotients that are compared with the value 1.*}
-lemma le_divide_eq_1 [no_atp]:
+lemma le_divide_eq_1:
"(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
by (auto simp add: le_divide_eq)
-lemma divide_le_eq_1 [no_atp]:
+lemma divide_le_eq_1:
"(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
by (auto simp add: divide_le_eq)
-lemma less_divide_eq_1 [no_atp]:
+lemma less_divide_eq_1:
"(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
by (auto simp add: less_divide_eq)
-lemma divide_less_eq_1 [no_atp]:
+lemma divide_less_eq_1:
"(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
text {*Conditional Simplification Rules: No Case Splits*}
-lemma le_divide_eq_1_pos [simp,no_atp]:
+lemma le_divide_eq_1_pos [simp]:
"0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
by (auto simp add: le_divide_eq)
-lemma le_divide_eq_1_neg [simp,no_atp]:
+lemma le_divide_eq_1_neg [simp]:
"a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
by (auto simp add: le_divide_eq)
-lemma divide_le_eq_1_pos [simp,no_atp]:
+lemma divide_le_eq_1_pos [simp]:
"0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
by (auto simp add: divide_le_eq)
-lemma divide_le_eq_1_neg [simp,no_atp]:
+lemma divide_le_eq_1_neg [simp]:
"a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
by (auto simp add: divide_le_eq)
-lemma less_divide_eq_1_pos [simp,no_atp]:
+lemma less_divide_eq_1_pos [simp]:
"0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
by (auto simp add: less_divide_eq)
-lemma less_divide_eq_1_neg [simp,no_atp]:
+lemma less_divide_eq_1_neg [simp]:
"a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
by (auto simp add: less_divide_eq)
-lemma divide_less_eq_1_pos [simp,no_atp]:
+lemma divide_less_eq_1_pos [simp]:
"0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
by (auto simp add: divide_less_eq)
-lemma divide_less_eq_1_neg [simp,no_atp]:
+lemma divide_less_eq_1_neg [simp]:
"a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
by (auto simp add: divide_less_eq)
-lemma eq_divide_eq_1 [simp,no_atp]:
+lemma eq_divide_eq_1 [simp]:
"(1 = b/a) = ((a \<noteq> 0 & a = b))"
by (auto simp add: eq_divide_eq)
-lemma divide_eq_eq_1 [simp,no_atp]:
+lemma divide_eq_eq_1 [simp]:
"(b/a = 1) = ((a \<noteq> 0 & a = b))"
by (auto simp add: divide_eq_eq)
--- a/src/HOL/Finite_Set.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Finite_Set.thy Fri Oct 18 10:43:20 2013 +0200
@@ -1620,8 +1620,7 @@
show False by simp (blast dest: Suc_neq_Zero surjD)
qed
-(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
-lemma infinite_UNIV_char_0 [no_atp]:
+lemma infinite_UNIV_char_0:
"\<not> finite (UNIV :: 'a::semiring_char_0 set)"
proof
assume "finite (UNIV :: 'a set)"
--- a/src/HOL/Fun.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Fun.thy Fri Oct 18 10:43:20 2013 +0200
@@ -775,7 +775,7 @@
subsection {* Cantor's Paradox *}
-lemma Cantors_paradox [no_atp]:
+lemma Cantors_paradox:
"\<not>(\<exists>f. f ` A = Pow A)"
proof clarify
fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast
--- a/src/HOL/Groups.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Groups.thy Fri Oct 18 10:43:20 2013 +0200
@@ -1341,7 +1341,7 @@
subsection {* Tools setup *}
-lemma add_mono_thms_linordered_semiring [no_atp]:
+lemma add_mono_thms_linordered_semiring:
fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
@@ -1349,7 +1349,7 @@
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
by (rule add_mono, clarify+)+
-lemma add_mono_thms_linordered_field [no_atp]:
+lemma add_mono_thms_linordered_field:
fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"
--- a/src/HOL/Int.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Int.thy Fri Oct 18 10:43:20 2013 +0200
@@ -450,7 +450,7 @@
It is proved here because attribute @{text arith_split} is not available
in theory @{text Rings}.
But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split,no_atp]:
+lemma abs_split [arith_split, no_atp]:
"P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
@@ -1158,32 +1158,32 @@
text{*To Simplify Inequalities Where One Side is the Constant 1*}
-lemma less_minus_iff_1 [simp,no_atp]:
+lemma less_minus_iff_1 [simp]:
fixes b::"'b::linordered_idom"
shows "(1 < - b) = (b < -1)"
by auto
-lemma le_minus_iff_1 [simp,no_atp]:
+lemma le_minus_iff_1 [simp]:
fixes b::"'b::linordered_idom"
shows "(1 \<le> - b) = (b \<le> -1)"
by auto
-lemma equation_minus_iff_1 [simp,no_atp]:
+lemma equation_minus_iff_1 [simp]:
fixes b::"'b::ring_1"
shows "(1 = - b) = (b = -1)"
by (subst equation_minus_iff, auto)
-lemma minus_less_iff_1 [simp,no_atp]:
+lemma minus_less_iff_1 [simp]:
fixes a::"'b::linordered_idom"
shows "(- a < 1) = (-1 < a)"
by auto
-lemma minus_le_iff_1 [simp,no_atp]:
+lemma minus_le_iff_1 [simp]:
fixes a::"'b::linordered_idom"
shows "(- a \<le> 1) = (-1 \<le> a)"
by auto
-lemma minus_equation_iff_1 [simp,no_atp]:
+lemma minus_equation_iff_1 [simp]:
fixes a::"'b::ring_1"
shows "(- a = 1) = (a = -1)"
by (subst minus_equation_iff, auto)
--- a/src/HOL/List.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/List.thy Fri Oct 18 10:43:20 2013 +0200
@@ -902,7 +902,7 @@
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
by (induct xs) auto
-lemma append_eq_append_conv [simp, no_atp]:
+lemma append_eq_append_conv [simp]:
"length xs = length ys \<or> length us = length vs
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
apply (induct xs arbitrary: ys)
@@ -934,7 +934,7 @@
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
using append_same_eq [of "[]"] by auto
-lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
by (induct xs) auto
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
@@ -1178,7 +1178,7 @@
lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
by (cases xs) auto
-lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
+lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
apply (induct xs arbitrary: ys, force)
apply (case_tac ys, simp, force)
done
@@ -5084,10 +5084,10 @@
for A :: "'a set"
where
Nil [intro!, simp]: "[]: lists A"
- | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
-inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
+ | Cons [intro!, simp]: "[| a: A; l: lists A|] ==> a#l : lists A"
+
+inductive_cases listsE [elim!]: "x#l : lists A"
+inductive_cases listspE [elim!]: "listsp A (x # l)"
inductive_simps listsp_simps[code]:
"listsp A []"
@@ -5129,15 +5129,15 @@
lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
-lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
by (rule in_listsp_conv_set [THEN iffD1])
-lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
-
-lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemmas in_listsD [dest!] = in_listspD [to_set]
+
+lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
by (rule in_listsp_conv_set [THEN iffD2])
-lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
+lemmas in_listsI [intro!] = in_listspI [to_set]
lemma lists_eq_set: "lists A = {xs. set xs <= A}"
by auto
--- a/src/HOL/Nat.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Nat.thy Fri Oct 18 10:43:20 2013 +0200
@@ -327,7 +327,7 @@
apply auto
done
-lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
+lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastforce)
done
@@ -491,7 +491,7 @@
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
@@ -659,7 +659,7 @@
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
by (fast intro: not0_implies_Suc)
-lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
using neq0_conv by blast
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
@@ -1396,10 +1396,10 @@
text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
-lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
end
@@ -1432,7 +1432,7 @@
text{*Special cases where either operand is zero*}
-lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
by (rule of_nat_le_iff [of _ 0, simplified])
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
--- a/src/HOL/Orderings.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Orderings.thy Fri Oct 18 10:43:20 2013 +0200
@@ -998,7 +998,7 @@
(!!x y. x > y ==> f x > f y) ==> f a > c"
by (subgoal_tac "f a > f b", force, force)
-lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9 [no_atp]
+lemmas xtrans = xt1 xt2 xt3 xt4 xt5 xt6 xt7 xt8 xt9
(*
Since "a >= b" abbreviates "b <= a", the abbreviation "..." stands
--- a/src/HOL/Power.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Power.thy Fri Oct 18 10:43:20 2013 +0200
@@ -530,7 +530,7 @@
"abs ((-a) ^ n) = abs (a ^ n)"
by (simp add: power_abs)
-lemma zero_less_power_abs_iff [simp, no_atp]:
+lemma zero_less_power_abs_iff [simp]:
"0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
proof (induct n)
case 0 show ?case by simp
--- a/src/HOL/Product_Type.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Product_Type.thy Fri Oct 18 10:43:20 2013 +0200
@@ -75,10 +75,10 @@
f} rather than by @{term [source] "%u. f ()"}.
*}
-lemma unit_abs_eta_conv [simp, no_atp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
by (rule ext) simp
-lemma UNIV_unit [no_atp]:
+lemma UNIV_unit:
"UNIV = {()}" by auto
instantiation unit :: default
@@ -586,10 +586,10 @@
to quite time-consuming computations (in particular for nested tuples) *)
setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
-lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp, no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
by (rule ext) fast
-lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp, no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
by (rule ext) fast
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
--- a/src/HOL/Record.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Record.thy Fri Oct 18 10:43:20 2013 +0200
@@ -399,7 +399,7 @@
lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
by simp
-lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
by simp
lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
--- a/src/HOL/Relation.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Relation.thy Fri Oct 18 10:43:20 2013 +0200
@@ -478,7 +478,7 @@
lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
by (simp add: Id_on_def)
-lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
+lemma Id_onI [intro!]: "a : A ==> (a, a) : Id_on A"
by (rule Id_on_eqI) (rule refl)
lemma Id_onE [elim!]:
@@ -939,8 +939,6 @@
where
"r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
-declare Image_def [no_atp]
-
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
by (simp add: Image_def)
@@ -950,7 +948,7 @@
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
by (rule Image_iff [THEN trans]) simp
-lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
by (unfold Image_def) blast
lemma ImageE [elim!]:
--- a/src/HOL/Rings.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Rings.thy Fri Oct 18 10:43:20 2013 +0200
@@ -127,7 +127,7 @@
then show ?thesis ..
qed
-lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
+lemma dvd_0_left_iff [simp]: "0 dvd a \<longleftrightarrow> a = 0"
by (auto intro: dvd_refl elim!: dvdE)
lemma dvd_0_right [iff]: "a dvd 0"
@@ -233,8 +233,8 @@
by (rule minus_unique) (simp add: distrib_left [symmetric])
text{*Extract signs from products*}
-lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
lemma minus_mult_minus [simp]: "- a * - b = a * b"
by simp
@@ -248,7 +248,7 @@
lemma left_diff_distrib[algebra_simps, field_simps]: "(a - b) * c = a * c - b * c"
by (simp add: distrib_right diff_minus)
-lemmas ring_distribs[no_atp] =
+lemmas ring_distribs =
distrib_left distrib_right left_diff_distrib right_diff_distrib
lemma eq_add_iff1:
@@ -261,7 +261,7 @@
end
-lemmas ring_distribs[no_atp] =
+lemmas ring_distribs =
distrib_left distrib_right left_diff_distrib right_diff_distrib
class comm_ring = comm_semiring + ab_group_add
@@ -336,7 +336,7 @@
qed
text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp, no_atp]:
+lemma mult_cancel_right [simp]:
"a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
proof -
have "(a * c = b * c) = ((a - b) * c = 0)"
@@ -344,7 +344,7 @@
thus ?thesis by (simp add: disj_commute)
qed
-lemma mult_cancel_left [simp, no_atp]:
+lemma mult_cancel_left [simp]:
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
proof -
have "(c * a = c * b) = (c * (a - b) = 0)"
@@ -1048,7 +1048,7 @@
text {* Simprules for comparisons where common factors can be cancelled. *}
-lemmas mult_compare_simps[no_atp] =
+lemmas mult_compare_simps =
mult_le_cancel_right mult_le_cancel_left
mult_le_cancel_right1 mult_le_cancel_right2
mult_le_cancel_left1 mult_le_cancel_left2
--- a/src/HOL/Set.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Set.thy Fri Oct 18 10:43:20 2013 +0200
@@ -87,7 +87,7 @@
then show ?thesis by simp
qed
-lemma set_eq_iff [no_atp]:
+lemma set_eq_iff:
"A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
by (auto intro:set_eqI)
@@ -495,7 +495,7 @@
by (simp add: less_eq_set_def le_fun_def)
-- {* Rule in Modus Ponens style. *}
-lemma rev_subsetD [no_atp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
-- {* The same, with reversed premises for use with @{text erule} --
cf @{text rev_mp}. *}
by (rule subsetD)
@@ -504,13 +504,13 @@
\medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
*}
-lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
by (auto simp add: less_eq_set_def le_fun_def)
-lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
-
-lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma subset_eq: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+
+lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
lemma subset_refl: "A \<subseteq> A"
@@ -845,11 +845,11 @@
subsubsection {* Singletons, using insert *}
-lemma singletonI [intro!,no_atp]: "a : {a}"
+lemma singletonI [intro!]: "a : {a}"
-- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
by (rule insertI1)
-lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
+lemma singletonD [dest!]: "b : {a} ==> b = a"
by blast
lemmas singletonE = singletonD [elim_format]
@@ -860,11 +860,11 @@
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
by blast
-lemma singleton_insert_inj_eq [iff,no_atp]:
+lemma singleton_insert_inj_eq [iff]:
"({b} = insert a A) = (a = b & A \<subseteq> {b})"
by blast
-lemma singleton_insert_inj_eq' [iff,no_atp]:
+lemma singleton_insert_inj_eq' [iff]:
"(insert a A = {b}) = (a = b & A \<subseteq> {b})"
by blast
@@ -898,7 +898,7 @@
*}
definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
- image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
+ image_def: "f ` A = {y. EX x:A. y = f(x)}"
abbreviation
range :: "('a => 'b) => 'b set" where -- "of function"
@@ -930,7 +930,7 @@
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
by blast
-lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
-- {* This rewrite rule would confuse users if made default. *}
by blast
@@ -1009,10 +1009,10 @@
subsubsection {* The ``proper subset'' relation *}
-lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
+lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
by (unfold less_le) blast
-lemma psubsetE [elim!,no_atp]:
+lemma psubsetE [elim!]:
"[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
by (unfold less_le) blast
@@ -1184,12 +1184,12 @@
lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
by blast
-lemma insert_disjoint [simp,no_atp]:
+lemma insert_disjoint [simp]:
"(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
"({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
by auto
-lemma disjoint_insert [simp,no_atp]:
+lemma disjoint_insert [simp]:
"(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
"({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
by auto
@@ -1221,7 +1221,7 @@
by blast
-lemma image_Collect [no_atp]: "f ` {x. P x} = {f x | x. P x}"
+lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
-- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
with its implicit quantifier and conjunction. Also image enjoys better
equational properties than does the RHS. *}
@@ -1244,7 +1244,7 @@
text {* \medskip @{text range}. *}
-lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
+lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
by auto
lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
@@ -1301,10 +1301,10 @@
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
by (fact inf_sup_distrib2)
-lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by (fact inf_eq_top_iff) (* already simp *)
-lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
by (fact le_inf_iff)
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1395,7 +1395,7 @@
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
by (fact sup_eq_bot_iff) (* FIXME: already simp *)
-lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
by (fact le_sup_iff)
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1467,7 +1467,7 @@
lemma Diff_eq: "A - B = A \<inter> (-B)"
by blast
-lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
+lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
by blast
lemma Diff_cancel [simp]: "A - A = {}"
@@ -1488,7 +1488,7 @@
lemma Diff_UNIV [simp]: "A - UNIV = {}"
by blast
-lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
+lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
by blast
lemma Diff_insert: "A - insert a B = A - B - {a}"
@@ -1568,7 +1568,7 @@
lemma ex_bool_eq: "(\<exists>b. P b) \<longleftrightarrow> P True \<or> P False"
by (auto intro: bool_contrapos)
-lemma UNIV_bool [no_atp]: "UNIV = {False, True}"
+lemma UNIV_bool: "UNIV = {False, True}"
by (auto intro: bool_induct)
text {* \medskip @{text Pow} *}
@@ -1597,7 +1597,7 @@
lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
by blast
-lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
by blast
lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
@@ -1754,7 +1754,7 @@
-- {* monotonicity *}
by blast
-lemma vimage_image_eq [no_atp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
by (blast intro: sym)
lemma image_vimage_subset: "f ` (f -` A) <= A"
--- a/src/HOL/Set_Interval.thy Fri Oct 18 10:35:57 2013 +0200
+++ b/src/HOL/Set_Interval.thy Fri Oct 18 10:43:20 2013 +0200
@@ -180,19 +180,19 @@
context ord
begin
-lemma greaterThanLessThan_iff [simp,no_atp]:
+lemma greaterThanLessThan_iff [simp]:
"(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-lemma atLeastLessThan_iff [simp,no_atp]:
+lemma atLeastLessThan_iff [simp]:
"(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-lemma greaterThanAtMost_iff [simp,no_atp]:
+lemma greaterThanAtMost_iff [simp]:
"(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-lemma atLeastAtMost_iff [simp,no_atp]:
+lemma atLeastAtMost_iff [simp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
@@ -1196,7 +1196,7 @@
subsubsection {* Some Subset Conditions *}
-lemma ivl_subset [simp,no_atp]:
+lemma ivl_subset [simp]:
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
apply(auto simp:linorder_not_le)
apply(rule ccontr)