--- a/src/HOL/Big_Operators.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Big_Operators.thy Thu Mar 18 12:58:52 2010 +0100
@@ -1534,12 +1534,12 @@
from assms show ?thesis by (simp add: Max_def fold1_belowI)
qed
-lemma Min_ge_iff [simp, noatp]:
+lemma Min_ge_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
using assms by (simp add: Min_def min_max.below_fold1_iff)
-lemma Max_le_iff [simp, noatp]:
+lemma Max_le_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
proof -
@@ -1548,12 +1548,12 @@
from assms show ?thesis by (simp add: Max_def below_fold1_iff)
qed
-lemma Min_gr_iff [simp, noatp]:
+lemma Min_gr_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
using assms by (simp add: Min_def strict_below_fold1_iff)
-lemma Max_less_iff [simp, noatp]:
+lemma Max_less_iff [simp, no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
proof -
@@ -1563,12 +1563,12 @@
by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
qed
-lemma Min_le_iff [noatp]:
+lemma Min_le_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
using assms by (simp add: Min_def fold1_below_iff)
-lemma Max_ge_iff [noatp]:
+lemma Max_ge_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
proof -
@@ -1578,12 +1578,12 @@
by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
qed
-lemma Min_less_iff [noatp]:
+lemma Min_less_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
using assms by (simp add: Min_def fold1_strict_below_iff)
-lemma Max_gr_iff [noatp]:
+lemma Max_gr_iff [no_atp]:
assumes "finite A" and "A \<noteq> {}"
shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
proof -
--- a/src/HOL/Complete_Lattice.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy Thu Mar 18 12:58:52 2010 +0100
@@ -231,7 +231,7 @@
by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
qed
-lemma Union_iff [simp, noatp]:
+lemma Union_iff [simp, no_atp]:
"A \<in> \<Union>C \<longleftrightarrow> (\<exists>X\<in>C. A\<in>X)"
by (unfold Union_eq) blast
@@ -269,10 +269,10 @@
lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
by blast
-lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp,no_atp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
by blast
-lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv [simp,no_atp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
by blast
lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
@@ -332,7 +332,7 @@
"\<Union>S = (\<Union>x\<in>S. x)"
by (simp add: UNION_eq_Union_image image_def)
-lemma UNION_def [noatp]:
+lemma UNION_def [no_atp]:
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
by (auto simp add: UNION_eq_Union_image Union_eq)
@@ -368,13 +368,13 @@
lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
by (iprover intro: subsetI elim: UN_E dest: subsetD)
-lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+lemma Collect_bex_eq [no_atp]: "{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 ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
by blast
-lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
+lemma UN_empty [simp,no_atp]: "(\<Union>x\<in>{}. B x) = {}"
by blast
lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
@@ -412,7 +412,7 @@
"((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
by blast+
-lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+lemma Collect_ex_eq [no_atp]: "{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) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
@@ -467,7 +467,7 @@
by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
-lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
+lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
by (unfold Inter_eq) blast
lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
@@ -515,7 +515,7 @@
lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
by blast
-lemma Inter_UNIV_conv [simp,noatp]:
+lemma Inter_UNIV_conv [simp,no_atp]:
"(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
"(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
by blast+
@@ -724,7 +724,7 @@
"!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
by auto
-lemma ball_simps [simp,noatp]:
+lemma ball_simps [simp,no_atp]:
"!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
"!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
"!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
@@ -739,7 +739,7 @@
"!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
by auto
-lemma bex_simps [simp,noatp]:
+lemma bex_simps [simp,no_atp]:
"!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
"!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
"!!P. (EX x:{}. P x) = False"
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Mar 18 12:58:52 2010 +0100
@@ -19,9 +19,9 @@
context linorder
begin
-lemma less_not_permute[noatp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
+lemma less_not_permute[no_atp]: "\<not> (x < y \<and> y < x)" by (simp add: not_less linear)
-lemma gather_simps[noatp]:
+lemma gather_simps[no_atp]:
shows
"(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> x < u \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> (insert u U). x < y) \<and> P x)"
and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x \<and> P x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y) \<and> P x)"
@@ -29,61 +29,61 @@
and "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y) \<and> l < x) \<longleftrightarrow> (\<exists>x. (\<forall>y \<in> (insert l L). y < x) \<and> (\<forall>y \<in> U. x < y))" by auto
lemma
- gather_start[noatp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
+ gather_start[no_atp]: "(\<exists>x. P x) \<equiv> (\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y\<in> {}. x < y) \<and> P x)"
by simp
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*}
-lemma minf_lt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
-lemma minf_gt[noatp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
+lemma minf_lt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (x < t \<longleftrightarrow> True)" by auto
+lemma minf_gt[no_atp]: "\<exists>z . \<forall>x. x < z \<longrightarrow> (t < x \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma minf_le[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma minf_ge[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
+lemma minf_le[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<le> t \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma minf_ge[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (t \<le> x \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
-lemma minf_eq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma minf_neq[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma minf_P[noatp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma minf_eq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma minf_neq[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma minf_P[no_atp]: "\<exists>z. \<forall>x. x < z \<longrightarrow> (P \<longleftrightarrow> P)" by blast
text{* Theorems for @{text "\<exists>z. \<forall>x. x < z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"}*}
-lemma pinf_gt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
-lemma pinf_lt[noatp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
+lemma pinf_gt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (t < x \<longleftrightarrow> True)" by auto
+lemma pinf_lt[no_atp]: "\<exists>z . \<forall>x. z < x \<longrightarrow> (x < t \<longleftrightarrow> False)"
by (simp add: not_less) (rule exI[where x="t"], auto simp add: less_le)
-lemma pinf_ge[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
-lemma pinf_le[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
+lemma pinf_ge[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (t \<le> x \<longleftrightarrow> True)" by (auto simp add: less_le)
+lemma pinf_le[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<le> t \<longleftrightarrow> False)"
by (auto simp add: less_le not_less not_le)
-lemma pinf_eq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
-lemma pinf_neq[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
-lemma pinf_P[noatp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
+lemma pinf_eq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x = t \<longleftrightarrow> False)" by auto
+lemma pinf_neq[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (x \<noteq> t \<longleftrightarrow> True)" by auto
+lemma pinf_P[no_atp]: "\<exists>z. \<forall>x. z < x \<longrightarrow> (P \<longleftrightarrow> P)" by blast
-lemma nmi_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
+lemma nmi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x < t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t < x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)"
by (auto simp add: le_less)
-lemma nmi_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_neq[noatp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_conj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
+lemma nmi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x\<le> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> t\<le> x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_neq[no_atp]: "t \<in> U \<Longrightarrow>\<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
+lemma nmi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
\<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma nmi_disj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
+lemma nmi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x) ;
\<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. u \<le> x)\<rbrakk> \<Longrightarrow>
\<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. u \<le> x)" by auto
-lemma npi_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x < t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
-lemma npi_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<le> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_neq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u )" by auto
-lemma npi_P[noatp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_conj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+lemma npi_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x < t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by (auto simp add: le_less)
+lemma npi_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t < x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x \<le> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> t \<le> x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>False \<and> x = t \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x. \<not>True \<and> x \<noteq> t \<longrightarrow> (\<exists> u\<in> U. x \<le> u )" by auto
+lemma npi_P[no_atp]: "\<forall> x. ~P \<and> P \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
+lemma npi_conj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
\<Longrightarrow> \<forall>x. \<not>(P1' \<and> P2') \<and> (P1 x \<and> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma npi_disj[noatp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+lemma npi_disj[no_atp]: "\<lbrakk>\<forall>x. \<not>P1' \<and> P1 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u) ; \<forall>x. \<not>P2' \<and> P2 x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
\<Longrightarrow> \<forall>x. \<not>(P1' \<or> P2') \<and> (P1 x \<or> P2 x) \<longrightarrow> (\<exists> u\<in> U. x \<le> u)" by auto
-lemma lin_dense_lt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
+lemma lin_dense_lt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t < u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x < t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y < t)"
proof(clarsimp)
fix x l u y assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x"
and xu: "x<u" and px: "x < t" and ly: "l<y" and yu:"y < u"
@@ -96,7 +96,7 @@
thus "y < t" using tny by (simp add: less_le)
qed
-lemma lin_dense_gt[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
+lemma lin_dense_gt[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l < x \<and> x < u \<and> t < x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t < y)"
proof(clarsimp)
fix x l u y
assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
@@ -109,7 +109,7 @@
thus "t < y" using tny by (simp add:less_le)
qed
-lemma lin_dense_le[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
+lemma lin_dense_le[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<le> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<le> t)"
proof(clarsimp)
fix x l u y
assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
@@ -122,7 +122,7 @@
hence "\<not> t < y" by auto thus "y \<le> t" by (simp add: not_less)
qed
-lemma lin_dense_ge[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
+lemma lin_dense_ge[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> t \<le> x \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> t \<le> y)"
proof(clarsimp)
fix x l u y
assume tU: "t \<in> U" and noU: "\<forall>t. l < t \<and> t < u \<longrightarrow> t \<notin> U" and lx: "l < x" and xu: "x<u"
@@ -134,11 +134,11 @@
with tU noU have "False" by auto}
hence "\<not> y<t" by auto thus "t \<le> y" by (simp add: not_less)
qed
-lemma lin_dense_eq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)" by auto
-lemma lin_dense_neq[noatp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)" by auto
-lemma lin_dense_P[noatp]: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)" by auto
+lemma lin_dense_eq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x = t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y= t)" by auto
+lemma lin_dense_neq[no_atp]: "t \<in> U \<Longrightarrow> \<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> x \<noteq> t \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> y\<noteq> t)" by auto
+lemma lin_dense_P[no_atp]: "\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P)" by auto
-lemma lin_dense_conj[noatp]:
+lemma lin_dense_conj[no_atp]:
"\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
@@ -146,7 +146,7 @@
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> (P1 x \<and> P2 x)
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<and> P2 y))"
by blast
-lemma lin_dense_disj[noatp]:
+lemma lin_dense_disj[no_atp]:
"\<lbrakk>\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P1 x
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> P1 y) ;
\<forall>x l u. (\<forall> t. l < t \<and> t< u \<longrightarrow> t \<notin> U) \<and> l< x \<and> x < u \<and> P2 x
@@ -155,11 +155,11 @@
\<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
by blast
-lemma npmibnd[noatp]: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
+lemma npmibnd[no_atp]: "\<lbrakk>\<forall>x. \<not> MP \<and> P x \<longrightarrow> (\<exists> u\<in> U. u \<le> x); \<forall>x. \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. x \<le> u)\<rbrakk>
\<Longrightarrow> \<forall>x. \<not> MP \<and> \<not>PP \<and> P x \<longrightarrow> (\<exists> u\<in> U. \<exists> u' \<in> U. u \<le> x \<and> x \<le> u')"
by auto
-lemma finite_set_intervals[noatp]:
+lemma finite_set_intervals[no_atp]:
assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
shows "\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a \<le> x \<and> x \<le> b \<and> P x"
@@ -191,7 +191,7 @@
from ainS binS noy ax xb px show ?thesis by blast
qed
-lemma finite_set_intervals2[noatp]:
+lemma finite_set_intervals2[no_atp]:
assumes px: "P x" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S"
and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"
shows "(\<exists> s\<in> S. P s) \<or> (\<exists> a \<in> S. \<exists> b \<in> S. (\<forall> y. a < y \<and> y < b \<longrightarrow> y \<notin> S) \<and> a < x \<and> x < b \<and> P x)"
@@ -215,7 +215,7 @@
"{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
by (auto dest: dense)
-lemma dlo_qe_bnds[noatp]:
+lemma dlo_qe_bnds[no_atp]:
assumes ne: "L \<noteq> {}" and neU: "U \<noteq> {}" and fL: "finite L" and fU: "finite U"
shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> (\<forall> l \<in> L. \<forall>u \<in> U. l < u)"
proof (simp only: atomize_eq, rule iffI)
@@ -239,7 +239,7 @@
ultimately show "\<exists>x. (\<forall>y\<in>L. y < x) \<and> (\<forall>y\<in>U. x < y)" by auto
qed
-lemma dlo_qe_noub[noatp]:
+lemma dlo_qe_noub[no_atp]:
assumes ne: "L \<noteq> {}" and fL: "finite L"
shows "(\<exists>x. (\<forall>y \<in> L. y < x) \<and> (\<forall>y \<in> {}. x < y)) \<equiv> True"
proof(simp add: atomize_eq)
@@ -249,7 +249,7 @@
thus "\<exists>x. \<forall>y\<in>L. y < x" by blast
qed
-lemma dlo_qe_nolb[noatp]:
+lemma dlo_qe_nolb[no_atp]:
assumes ne: "U \<noteq> {}" and fU: "finite U"
shows "(\<exists>x. (\<forall>y \<in> {}. y < x) \<and> (\<forall>y \<in> U. x < y)) \<equiv> True"
proof(simp add: atomize_eq)
@@ -259,14 +259,14 @@
thus "\<exists>x. \<forall>y\<in>U. x < y" by blast
qed
-lemma exists_neq[noatp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
+lemma exists_neq[no_atp]: "\<exists>(x::'a). x \<noteq> t" "\<exists>(x::'a). t \<noteq> x"
using gt_ex[of t] by auto
-lemmas dlo_simps[noatp] = order_refl less_irrefl not_less not_le exists_neq
+lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq
le_less neq_iff linear less_not_permute
-lemma axiom[noatp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
-lemma atoms[noatp]:
+lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
and "TERM (op = :: 'a \<Rightarrow> _)" .
@@ -277,21 +277,21 @@
end
(* FIXME: Move to HOL -- together with the conj_aci_rule in langford.ML *)
-lemma dnf[noatp]:
+lemma dnf[no_atp]:
"(P & (Q | R)) = ((P&Q) | (P&R))"
"((Q | R) & P) = ((Q&P) | (R&P))"
by blast+
-lemmas weak_dnf_simps[noatp] = simp_thms dnf
+lemmas weak_dnf_simps[no_atp] = simp_thms dnf
-lemma nnf_simps[noatp]:
+lemma nnf_simps[no_atp]:
"(\<not>(P \<and> Q)) = (\<not>P \<or> \<not>Q)" "(\<not>(P \<or> Q)) = (\<not>P \<and> \<not>Q)" "(P \<longrightarrow> Q) = (\<not>P \<or> Q)"
"(P = Q) = ((P \<and> Q) \<or> (\<not>P \<and> \<not> Q))" "(\<not> \<not>(P)) = P"
by blast+
-lemma ex_distrib[noatp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
+lemma ex_distrib[no_atp]: "(\<exists>x. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x. P x) \<or> (\<exists>x. Q x))" by blast
-lemmas dnf_simps[noatp] = weak_dnf_simps nnf_simps ex_distrib
+lemmas dnf_simps[no_atp] = weak_dnf_simps nnf_simps ex_distrib
use "~~/src/HOL/Tools/Qelim/langford.ML"
method_setup dlo = {*
@@ -316,10 +316,10 @@
locale linorder_no_ub = linorder_stupid_syntax +
assumes gt_ex: "\<exists>y. less x y"
begin
-lemma ge_ex[noatp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
+lemma ge_ex[no_atp]: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
text {* Theorems for @{text "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>+\<infinity>\<^esub>)"} *}
-lemma pinf_conj[noatp]:
+lemma pinf_conj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
@@ -335,7 +335,7 @@
thus ?thesis by blast
qed
-lemma pinf_disj[noatp]:
+lemma pinf_disj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. z1 \<sqsubset> x \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. z2 \<sqsubset> x \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
@@ -351,7 +351,7 @@
thus ?thesis by blast
qed
-lemma pinf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma pinf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
proof-
from ex obtain z where z: "\<forall>x. z \<sqsubset> x \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
from gt_ex obtain x where x: "z \<sqsubset> x" by blast
@@ -365,11 +365,11 @@
locale linorder_no_lb = linorder_stupid_syntax +
assumes lt_ex: "\<exists>y. less y x"
begin
-lemma le_ex[noatp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
+lemma le_ex[no_atp]: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
text {* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"} *}
-lemma minf_conj[noatp]:
+lemma minf_conj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<and> P2 x) \<longleftrightarrow> (P1' \<and> P2'))"
@@ -384,7 +384,7 @@
thus ?thesis by blast
qed
-lemma minf_disj[noatp]:
+lemma minf_disj[no_atp]:
assumes ex1: "\<exists>z1. \<forall>x. x \<sqsubset> z1 \<longrightarrow> (P1 x \<longleftrightarrow> P1')"
and ex2: "\<exists>z2. \<forall>x. x \<sqsubset> z2 \<longrightarrow> (P2 x \<longleftrightarrow> P2')"
shows "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> ((P1 x \<or> P2 x) \<longleftrightarrow> (P1' \<or> P2'))"
@@ -399,7 +399,7 @@
thus ?thesis by blast
qed
-lemma minf_ex[noatp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
+lemma minf_ex[no_atp]: assumes ex:"\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" and p1: P1 shows "\<exists> x. P x"
proof-
from ex obtain z where z: "\<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P1)" by blast
from lt_ex obtain x where x: "x \<sqsubset> z" by blast
@@ -422,7 +422,7 @@
context constr_dense_linorder
begin
-lemma rinf_U[noatp]:
+lemma rinf_U[no_atp]:
assumes fU: "finite U"
and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
@@ -465,7 +465,7 @@
ultimately show ?thesis by blast
qed
-theorem fr_eq[noatp]:
+theorem fr_eq[no_atp]:
assumes fU: "finite U"
and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
\<longrightarrow> (\<forall> y. l \<sqsubset> y \<and> y \<sqsubset> u \<longrightarrow> P y )"
@@ -493,16 +493,16 @@
ultimately have "?E = ?D" by blast thus "?E \<equiv> ?D" by simp
qed
-lemmas minf_thms[noatp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
-lemmas pinf_thms[noatp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
+lemmas minf_thms[no_atp] = minf_conj minf_disj minf_eq minf_neq minf_lt minf_le minf_gt minf_ge minf_P
+lemmas pinf_thms[no_atp] = pinf_conj pinf_disj pinf_eq pinf_neq pinf_lt pinf_le pinf_gt pinf_ge pinf_P
-lemmas nmi_thms[noatp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
-lemmas npi_thms[noatp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
-lemmas lin_dense_thms[noatp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
+lemmas nmi_thms[no_atp] = nmi_conj nmi_disj nmi_eq nmi_neq nmi_lt nmi_le nmi_gt nmi_ge nmi_P
+lemmas npi_thms[no_atp] = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
+lemmas lin_dense_thms[no_atp] = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
-lemma ferrack_axiom[noatp]: "constr_dense_linorder less_eq less between"
+lemma ferrack_axiom[no_atp]: "constr_dense_linorder less_eq less between"
by (rule constr_dense_linorder_axioms)
-lemma atoms[noatp]:
+lemma atoms[no_atp]:
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
and "TERM (op = :: 'a \<Rightarrow> _)" .
--- a/src/HOL/Fields.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Fields.thy Thu Mar 18 12:58:52 2010 +0100
@@ -65,7 +65,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, noatp]:
+lemma nonzero_mult_divide_mult_cancel_left [simp, no_atp]:
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)"
@@ -76,7 +76,7 @@
finally show ?thesis by (simp add: divide_inverse)
qed
-lemma nonzero_mult_divide_mult_cancel_right [simp, noatp]:
+lemma nonzero_mult_divide_mult_cancel_right [simp, no_atp]:
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
by (simp add: mult_commute [of _ c])
@@ -90,7 +90,7 @@
by (simp add: divide_inverse mult_ac)
text {* These are later declared as simp rules. *}
-lemmas times_divide_eq [noatp] = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
lemma add_frac_eq:
assumes "y \<noteq> 0" and "z \<noteq> 0"
@@ -106,27 +106,27 @@
text{*Special Cancellation Simprules for Division*}
-lemma nonzero_mult_divide_cancel_right [simp, noatp]:
+lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
"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, noatp]:
+lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
"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, noatp]:
+lemma nonzero_divide_mult_cancel_right [simp, no_atp]:
"\<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, noatp]:
+lemma nonzero_divide_mult_cancel_left [simp, no_atp]:
"\<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, noatp]:
+lemma nonzero_mult_divide_mult_cancel_left2 [simp, no_atp]:
"\<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, noatp]:
+lemma nonzero_mult_divide_mult_cancel_right2 [simp, no_atp]:
"\<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)
@@ -139,7 +139,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, noatp]: "(-a) / b = - (a / b)"
+lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
by (simp add: divide_inverse)
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -183,7 +183,7 @@
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
by (erule subst, simp)
-lemmas field_eq_simps[noatp] = algebra_simps
+lemmas field_eq_simps[no_atp] = algebra_simps
(* pull / out*)
add_divide_eq_iff divide_add_eq_iff
diff_divide_eq_iff divide_diff_eq_iff
@@ -292,18 +292,18 @@
apply simp_all
done
-lemma divide_divide_eq_right [simp,noatp]:
+lemma divide_divide_eq_right [simp,no_atp]:
"a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
by (simp add: divide_inverse mult_ac)
-lemma divide_divide_eq_left [simp,noatp]:
+lemma divide_divide_eq_left [simp,no_atp]:
"(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
by (simp add: divide_inverse mult_assoc)
subsubsection{*Special Cancellation Simprules for Division*}
-lemma mult_divide_mult_cancel_left_if[simp,noatp]:
+lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
fixes c :: "'a :: {field,division_by_zero}"
shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
by (simp add: mult_divide_mult_cancel_left)
@@ -314,7 +314,7 @@
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
by (simp add: divide_inverse)
-lemma divide_minus_right [simp, noatp]:
+lemma divide_minus_right [simp, no_atp]:
"a / -(b::'a::{field,division_by_zero}) = -(a / b)"
by (simp add: divide_inverse)
@@ -440,7 +440,7 @@
done
text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,noatp]:
+lemma inverse_less_iff_less [simp,no_atp]:
"[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
@@ -448,7 +448,7 @@
"[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
by (force simp add: order_le_less less_imp_inverse_less)
-lemma inverse_le_iff_le [simp,noatp]:
+lemma inverse_le_iff_le [simp,no_atp]:
"[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
@@ -482,7 +482,7 @@
apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
done
-lemma inverse_less_iff_less_neg [simp,noatp]:
+lemma inverse_less_iff_less_neg [simp,no_atp]:
"[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
apply (insert inverse_less_iff_less [of "-b" "-a"])
apply (simp del: inverse_less_iff_less
@@ -493,7 +493,7 @@
"[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
by (force simp add: order_le_less less_imp_inverse_less_neg)
-lemma inverse_le_iff_le_neg [simp,noatp]:
+lemma inverse_le_iff_le_neg [simp,no_atp]:
"[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
@@ -665,7 +665,7 @@
(for inequations). Can be too aggressive and is therefore separate from the
more benign @{text algebra_simps}. *}
-lemmas field_simps[noatp] = field_eq_simps
+lemmas field_simps[no_atp] = field_eq_simps
(* multiply ineqn *)
pos_divide_less_eq neg_divide_less_eq
pos_less_divide_eq neg_less_divide_eq
@@ -677,7 +677,7 @@
sign_simps} to @{text field_simps} because the former can lead to case
explosions. *}
-lemmas sign_simps[noatp] = group_simps
+lemmas sign_simps[no_atp] = group_simps
zero_less_mult_iff mult_less_0_iff
(* Only works once linear arithmetic is installed:
@@ -716,7 +716,7 @@
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
by (simp add: divide_inverse mult_le_0_iff)
-lemma divide_eq_0_iff [simp,noatp]:
+lemma divide_eq_0_iff [simp,no_atp]:
"(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
by (simp add: divide_inverse)
@@ -756,13 +756,13 @@
subsection{*Cancellation Laws for Division*}
-lemma divide_cancel_right [simp,noatp]:
+lemma divide_cancel_right [simp,no_atp]:
"(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
done
-lemma divide_cancel_left [simp,noatp]:
+lemma divide_cancel_left [simp,no_atp]:
"(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
apply (cases "c=0", simp)
apply (simp add: divide_inverse)
@@ -772,23 +772,23 @@
subsection {* Division and the Number One *}
text{*Simplify expressions equated with 1*}
-lemma divide_eq_1_iff [simp,noatp]:
+lemma divide_eq_1_iff [simp,no_atp]:
"(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
apply (cases "b=0", simp)
apply (simp add: right_inverse_eq)
done
-lemma one_eq_divide_iff [simp,noatp]:
+lemma one_eq_divide_iff [simp,no_atp]:
"(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
by (simp add: eq_commute [of 1])
-lemma zero_eq_1_divide_iff [simp,noatp]:
+lemma zero_eq_1_divide_iff [simp,no_atp]:
"((0::'a::{linordered_field,division_by_zero}) = 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,noatp]:
+lemma one_divide_eq_0_iff [simp,no_atp]:
"(1/a = (0::'a::{linordered_field,division_by_zero})) = (a = 0)"
apply (cases "a=0", simp)
apply (insert zero_neq_one [THEN not_sym])
@@ -801,10 +801,10 @@
lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
-declare zero_less_divide_1_iff [simp,noatp]
-declare divide_less_0_1_iff [simp,noatp]
-declare zero_le_divide_1_iff [simp,noatp]
-declare divide_le_0_1_iff [simp,noatp]
+declare zero_less_divide_1_iff [simp,no_atp]
+declare divide_less_0_1_iff [simp,no_atp]
+declare zero_le_divide_1_iff [simp,no_atp]
+declare divide_le_0_1_iff [simp,no_atp]
subsection {* Ordering Rules for Division *}
@@ -853,22 +853,22 @@
text{*Simplify quotients that are compared with the value 1.*}
-lemma le_divide_eq_1 [noatp]:
+lemma le_divide_eq_1 [no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(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 [noatp]:
+lemma divide_le_eq_1 [no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(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 [noatp]:
+lemma less_divide_eq_1 [no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
by (auto simp add: less_divide_eq)
-lemma divide_less_eq_1 [noatp]:
+lemma divide_less_eq_1 [no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
@@ -876,52 +876,52 @@
subsection{*Conditional Simplification Rules: No Case Splits*}
-lemma le_divide_eq_1_pos [simp,noatp]:
+lemma le_divide_eq_1_pos [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
by (auto simp add: le_divide_eq)
-lemma le_divide_eq_1_neg [simp,noatp]:
+lemma le_divide_eq_1_neg [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
by (auto simp add: le_divide_eq)
-lemma divide_le_eq_1_pos [simp,noatp]:
+lemma divide_le_eq_1_pos [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
by (auto simp add: divide_le_eq)
-lemma divide_le_eq_1_neg [simp,noatp]:
+lemma divide_le_eq_1_neg [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
by (auto simp add: divide_le_eq)
-lemma less_divide_eq_1_pos [simp,noatp]:
+lemma less_divide_eq_1_pos [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
by (auto simp add: less_divide_eq)
-lemma less_divide_eq_1_neg [simp,noatp]:
+lemma less_divide_eq_1_neg [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
by (auto simp add: less_divide_eq)
-lemma divide_less_eq_1_pos [simp,noatp]:
+lemma divide_less_eq_1_pos [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
by (auto simp add: divide_less_eq)
-lemma divide_less_eq_1_neg [simp,noatp]:
+lemma divide_less_eq_1_neg [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
by (auto simp add: divide_less_eq)
-lemma eq_divide_eq_1 [simp,noatp]:
+lemma eq_divide_eq_1 [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
by (auto simp add: eq_divide_eq)
-lemma divide_eq_eq_1 [simp,noatp]:
+lemma divide_eq_eq_1 [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
by (auto simp add: divide_eq_eq)
--- a/src/HOL/Finite_Set.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Finite_Set.thy Thu Mar 18 12:58:52 2010 +0100
@@ -524,13 +524,13 @@
end
-lemma UNIV_unit [noatp]:
+lemma UNIV_unit [no_atp]:
"UNIV = {()}" by auto
instance unit :: finite proof
qed (simp add: UNIV_unit)
-lemma UNIV_bool [noatp]:
+lemma UNIV_bool [no_atp]:
"UNIV = {False, True}" by auto
instance bool :: finite proof
@@ -1779,7 +1779,7 @@
"card A > 0 \<Longrightarrow> finite A"
by (rule ccontr) simp
-lemma card_0_eq [simp, noatp]:
+lemma card_0_eq [simp, no_atp]:
"finite A \<Longrightarrow> card A = 0 \<longleftrightarrow> A = {}"
by (auto dest: mk_disjoint_insert)
@@ -2109,8 +2109,8 @@
show False by simp (blast dest: Suc_neq_Zero surjD)
qed
-(* Often leads to bogus ATP proofs because of reduced type information, hence noatp *)
-lemma infinite_UNIV_char_0[noatp]:
+(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *)
+lemma infinite_UNIV_char_0[no_atp]:
"\<not> finite (UNIV::'a::semiring_char_0 set)"
proof
assume "finite (UNIV::'a set)"
--- a/src/HOL/Groups.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Groups.thy Thu Mar 18 12:58:52 2010 +0100
@@ -437,7 +437,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, noatp]: "a - b = 0 \<longleftrightarrow> a = b"
+lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (simp add: algebra_simps)
end
@@ -772,12 +772,12 @@
by (simp add: algebra_simps)
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps[noatp] = algebra_simps
+lemmas group_simps[no_atp] = algebra_simps
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps[noatp] = algebra_simps
+lemmas group_simps[no_atp] = algebra_simps
class linordered_ab_semigroup_add =
linorder + ordered_ab_semigroup_add
@@ -1054,7 +1054,7 @@
lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
by simp
-lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
+lemma abs_0_eq [simp, no_atp]: "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
@@ -1201,7 +1201,7 @@
subsection {* Tools setup *}
-lemma add_mono_thms_linordered_semiring [noatp]:
+lemma add_mono_thms_linordered_semiring [no_atp]:
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"
@@ -1209,7 +1209,7 @@
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
by (rule add_mono, clarify+)+
-lemma add_mono_thms_linordered_field [noatp]:
+lemma add_mono_thms_linordered_field [no_atp]:
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"
@@ -1220,8 +1220,8 @@
add_less_le_mono add_le_less_mono add_strict_mono)
text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
-lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
+lemmas diff_less_0_iff_less [simp, no_atp] = less_iff_diff_less_0 [symmetric]
+lemmas diff_le_0_iff_le [simp, no_atp] = le_iff_diff_le_0 [symmetric]
ML {*
structure ab_group_add_cancel = Abel_Cancel
--- a/src/HOL/HOL.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/HOL.thy Thu Mar 18 12:58:52 2010 +0100
@@ -23,7 +23,6 @@
"~~/src/Tools/coherent.ML"
"~~/src/Tools/eqsubst.ML"
"~~/src/Provers/quantifier1.ML"
- "Tools/res_blacklist.ML"
("Tools/simpdata.ML")
"~~/src/Tools/random_word.ML"
"~~/src/Tools/atomize_elim.ML"
@@ -35,8 +34,6 @@
setup {* Intuitionistic.method_setup @{binding iprover} *}
-setup Res_Blacklist.setup
-
subsection {* Primitive logic *}
@@ -794,6 +791,25 @@
subsection {* Package setup *}
+subsubsection {* Sledgehammer setup *}
+
+text {*
+Theorems blacklisted to Sledgehammer. These theorems typically produce clauses
+that are prolific (match too many equality or membership literals) and relate to
+seldom-used facts. Some duplicate other rules.
+*}
+
+ML {*
+structure No_ATPs = Named_Thms
+(
+ val name = "no_atp"
+ val description = "theorems that should be avoided by Sledgehammer"
+)
+*}
+
+setup {* No_ATPs.setup *}
+
+
subsubsection {* Classical Reasoner setup *}
lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
@@ -1041,7 +1057,7 @@
lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
-declare All_def [noatp]
+declare All_def [no_atp]
lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
@@ -1088,7 +1104,7 @@
lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
by (simplesubst split_if, blast)
-lemmas if_splits [noatp] = split_if split_if_asm
+lemmas if_splits [no_atp] = split_if split_if_asm
lemma if_cancel: "(if c then x else x) = x"
by (simplesubst split_if, blast)
--- a/src/HOL/Int.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Int.thy Thu Mar 18 12:58:52 2010 +0100
@@ -86,7 +86,7 @@
text{*Reduces equality on abstractions to equality on representatives:
@{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
-declare Abs_Integ_inject [simp,noatp] Abs_Integ_inverse [simp,noatp]
+declare Abs_Integ_inject [simp,no_atp] Abs_Integ_inverse [simp,no_atp]
text{*Case analysis on the representation of an integer as an equivalence
class of pairs of naturals.*}
@@ -522,7 +522,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,noatp]:
+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)
@@ -1874,16 +1874,16 @@
text{*These are actually for fields, like real: but where else to put them?*}
-lemmas zero_less_divide_iff_number_of [simp, noatp] =
+lemmas zero_less_divide_iff_number_of [simp, no_atp] =
zero_less_divide_iff [of "number_of w", standard]
-lemmas divide_less_0_iff_number_of [simp, noatp] =
+lemmas divide_less_0_iff_number_of [simp, no_atp] =
divide_less_0_iff [of "number_of w", standard]
-lemmas zero_le_divide_iff_number_of [simp, noatp] =
+lemmas zero_le_divide_iff_number_of [simp, no_atp] =
zero_le_divide_iff [of "number_of w", standard]
-lemmas divide_le_0_iff_number_of [simp, noatp] =
+lemmas divide_le_0_iff_number_of [simp, no_atp] =
divide_le_0_iff [of "number_of w", standard]
@@ -1896,53 +1896,53 @@
text {*These laws simplify inequalities, moving unary minus from a term
into the literal.*}
-lemmas less_minus_iff_number_of [simp, noatp] =
+lemmas less_minus_iff_number_of [simp, no_atp] =
less_minus_iff [of "number_of v", standard]
-lemmas le_minus_iff_number_of [simp, noatp] =
+lemmas le_minus_iff_number_of [simp, no_atp] =
le_minus_iff [of "number_of v", standard]
-lemmas equation_minus_iff_number_of [simp, noatp] =
+lemmas equation_minus_iff_number_of [simp, no_atp] =
equation_minus_iff [of "number_of v", standard]
-lemmas minus_less_iff_number_of [simp, noatp] =
+lemmas minus_less_iff_number_of [simp, no_atp] =
minus_less_iff [of _ "number_of v", standard]
-lemmas minus_le_iff_number_of [simp, noatp] =
+lemmas minus_le_iff_number_of [simp, no_atp] =
minus_le_iff [of _ "number_of v", standard]
-lemmas minus_equation_iff_number_of [simp, noatp] =
+lemmas minus_equation_iff_number_of [simp, no_atp] =
minus_equation_iff [of _ "number_of v", standard]
text{*To Simplify Inequalities Where One Side is the Constant 1*}
-lemma less_minus_iff_1 [simp,noatp]:
+lemma less_minus_iff_1 [simp,no_atp]:
fixes b::"'b::{linordered_idom,number_ring}"
shows "(1 < - b) = (b < -1)"
by auto
-lemma le_minus_iff_1 [simp,noatp]:
+lemma le_minus_iff_1 [simp,no_atp]:
fixes b::"'b::{linordered_idom,number_ring}"
shows "(1 \<le> - b) = (b \<le> -1)"
by auto
-lemma equation_minus_iff_1 [simp,noatp]:
+lemma equation_minus_iff_1 [simp,no_atp]:
fixes b::"'b::number_ring"
shows "(1 = - b) = (b = -1)"
by (subst equation_minus_iff, auto)
-lemma minus_less_iff_1 [simp,noatp]:
+lemma minus_less_iff_1 [simp,no_atp]:
fixes a::"'b::{linordered_idom,number_ring}"
shows "(- a < 1) = (-1 < a)"
by auto
-lemma minus_le_iff_1 [simp,noatp]:
+lemma minus_le_iff_1 [simp,no_atp]:
fixes a::"'b::{linordered_idom,number_ring}"
shows "(- a \<le> 1) = (-1 \<le> a)"
by auto
-lemma minus_equation_iff_1 [simp,noatp]:
+lemma minus_equation_iff_1 [simp,no_atp]:
fixes a::"'b::number_ring"
shows "(- a = 1) = (a = -1)"
by (subst minus_equation_iff, auto)
@@ -1950,16 +1950,16 @@
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
-lemmas mult_less_cancel_left_number_of [simp, noatp] =
+lemmas mult_less_cancel_left_number_of [simp, no_atp] =
mult_less_cancel_left [of "number_of v", standard]
-lemmas mult_less_cancel_right_number_of [simp, noatp] =
+lemmas mult_less_cancel_right_number_of [simp, no_atp] =
mult_less_cancel_right [of _ "number_of v", standard]
-lemmas mult_le_cancel_left_number_of [simp, noatp] =
+lemmas mult_le_cancel_left_number_of [simp, no_atp] =
mult_le_cancel_left [of "number_of v", standard]
-lemmas mult_le_cancel_right_number_of [simp, noatp] =
+lemmas mult_le_cancel_right_number_of [simp, no_atp] =
mult_le_cancel_right [of _ "number_of v", standard]
--- a/src/HOL/IsaMakefile Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 18 12:58:52 2010 +0100
@@ -314,7 +314,6 @@
Tools/Quotient/quotient_term.ML \
Tools/Quotient/quotient_typ.ML \
Tools/recdef.ML \
- Tools/res_blacklist.ML \
Tools/Sledgehammer/metis_tactics.ML \
Tools/Sledgehammer/sledgehammer_fact_filter.ML \
Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
--- a/src/HOL/Library/Lattice_Algebras.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy Thu Mar 18 12:58:52 2010 +0100
@@ -163,16 +163,16 @@
lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
-lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
+lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x"
by (simp add: pprt_def sup_aci sup_absorb1)
-lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
+lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
by (simp add: nprt_def inf_aci inf_absorb1)
-lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
+lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
by (simp add: pprt_def sup_aci sup_absorb2)
-lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
+lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
by (simp add: nprt_def inf_aci inf_absorb2)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
@@ -197,10 +197,10 @@
apply (erule sup_0_imp_0)
done
-lemma inf_0_eq_0 [simp, noatp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
+lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
by (rule, erule inf_0_imp_0) simp
-lemma sup_0_eq_0 [simp, noatp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
+lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
by (rule, erule sup_0_imp_0) simp
lemma zero_le_double_add_iff_zero_le_single_add [simp]:
@@ -295,10 +295,10 @@
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
unfolding le_iff_inf by (simp add: nprt_def inf_commute)
-lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
+lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
-lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
+lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
end
--- a/src/HOL/List.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/List.thy Thu Mar 18 12:58:52 2010 +0100
@@ -582,7 +582,7 @@
lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
by (induct xs) auto
-lemma append_eq_append_conv [simp, noatp]:
+lemma append_eq_append_conv [simp, no_atp]:
"length xs = length ys \<or> length us = length vs
==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
apply (induct xs arbitrary: ys)
@@ -614,7 +614,7 @@
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
using append_same_eq [of "[]"] by auto
-lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp,no_atp]: "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)"
@@ -3928,10 +3928,10 @@
for A :: "'a set"
where
Nil [intro!]: "[]: lists A"
- | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
-
-inductive_cases listsE [elim!,noatp]: "x#l : lists A"
-inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
+ | Cons [intro!,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)"
lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
@@ -3966,15 +3966,15 @@
lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
-lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
by (rule in_listsp_conv_set [THEN iffD1])
-lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
-
-lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+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"
by (rule in_listsp_conv_set [THEN iffD2])
-lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
+lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
lemma lists_UNIV [simp]: "lists UNIV = UNIV"
by auto
--- a/src/HOL/Nat.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Nat.thy Thu Mar 18 12:58:52 2010 +0100
@@ -320,7 +320,7 @@
apply auto
done
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
+lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastsimp)
done
@@ -480,7 +480,7 @@
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff, no_atp]: "(n < (1::nat)) = (n = 0)"
unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
@@ -648,7 +648,7 @@
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
by (fast intro: not0_implies_Suc)
-lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff,no_atp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
using neq0_conv by blast
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
@@ -1279,10 +1279,10 @@
text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
+lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
-lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
+lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
lemma inj_of_nat: "inj of_nat"
@@ -1327,7 +1327,7 @@
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
by (rule of_nat_le_iff [of 0, simplified])
-lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
+lemma of_nat_le_0_iff [simp, no_atp]: "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 Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Orderings.thy Thu Mar 18 12:58:52 2010 +0100
@@ -293,11 +293,11 @@
"max x y < z \<longleftrightarrow> x < z \<and> y < z"
unfolding max_def le_less using less_linear by (auto intro: less_trans)
-lemma split_min [noatp]:
+lemma split_min [no_atp]:
"P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
by (simp add: min_def)
-lemma split_max [noatp]:
+lemma split_max [no_atp]:
"P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
by (simp add: max_def)
--- a/src/HOL/Power.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Power.thy Thu Mar 18 12:58:52 2010 +0100
@@ -334,7 +334,7 @@
"abs ((-a) ^ n) = abs (a ^ n)"
by (simp add: power_abs)
-lemma zero_less_power_abs_iff [simp, noatp]:
+lemma zero_less_power_abs_iff [simp, no_atp]:
"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 Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 18 12:58:52 2010 +0100
@@ -46,7 +46,7 @@
where
"() = Abs_unit True"
-lemma unit_eq [noatp]: "u = ()"
+lemma unit_eq [no_atp]: "u = ()"
by (induct u) (simp add: unit_def Unity_def)
text {*
@@ -78,7 +78,7 @@
f} rather than by @{term [source] "%u. f ()"}.
*}
-lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f"
by (rule ext) simp
instantiation unit :: default
@@ -497,7 +497,7 @@
lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)"
by (subst surjective_pairing, rule split_conv)
-lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
+lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
-- {* For use with @{text split} and the Simplifier. *}
by (insert surj_pair [of p], clarify, simp)
@@ -508,7 +508,7 @@
current goal contains one of those constants.
*}
-lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
+lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
by (subst split_split, simp)
@@ -582,10 +582,10 @@
Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
*}
-lemma split_eta_SetCompr [simp,noatp]: "(%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,noatp]: "(%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)"
@@ -947,11 +947,11 @@
-- {* Suggested by Pierre Chartier *}
by blast
-lemma split_paired_Ball_Sigma [simp,noatp]:
+lemma split_paired_Ball_Sigma [simp,no_atp]:
"(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
by blast
-lemma split_paired_Bex_Sigma [simp,noatp]:
+lemma split_paired_Bex_Sigma [simp,no_atp]:
"(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
by blast
--- a/src/HOL/Relation.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Relation.thy Thu Mar 18 12:58:52 2010 +0100
@@ -121,7 +121,7 @@
lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A"
by (simp add: Id_on_def)
-lemma Id_onI [intro!,noatp]: "a : A ==> (a, a) : Id_on A"
+lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A"
by (rule Id_on_eqI) (rule refl)
lemma Id_onE [elim!]:
@@ -361,7 +361,7 @@
subsection {* Domain *}
-declare Domain_def [noatp]
+declare Domain_def [no_atp]
lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
by (unfold Domain_def) blast
@@ -484,7 +484,7 @@
subsection {* Image of a set under a relation *}
-declare Image_def [noatp]
+declare Image_def [no_atp]
lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
by (simp add: Image_def)
@@ -495,7 +495,7 @@
lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
by (rule Image_iff [THEN trans]) simp
-lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro,no_atp]: "(a, b) : r ==> a : A ==> b : r``A"
by (unfold Image_def) blast
lemma ImageE [elim!]:
--- a/src/HOL/Rings.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Rings.thy Thu Mar 18 12:58:52 2010 +0100
@@ -127,7 +127,7 @@
then show ?thesis ..
qed
-lemma dvd_0_left_iff [noatp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
+lemma dvd_0_left_iff [no_atp, simp]: "0 dvd a \<longleftrightarrow> a = 0"
by (auto intro: dvd_refl elim!: dvdE)
lemma dvd_0_right [iff]: "a dvd 0"
@@ -221,8 +221,8 @@
by (rule minus_unique) (simp add: right_distrib [symmetric])
text{*Extract signs from products*}
-lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp, no_atp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp,no_atp] = minus_mult_right [symmetric]
lemma minus_mult_minus [simp]: "- a * - b = a * b"
by simp
@@ -236,11 +236,11 @@
lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
by (simp add: left_distrib diff_minus)
-lemmas ring_distribs[noatp] =
+lemmas ring_distribs[no_atp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
lemma eq_add_iff1:
"a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -252,7 +252,7 @@
end
-lemmas ring_distribs[noatp] =
+lemmas ring_distribs[no_atp] =
right_distrib left_distrib left_diff_distrib right_diff_distrib
class comm_ring = comm_semiring + ab_group_add
@@ -319,7 +319,7 @@
qed
text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp, noatp]:
+lemma mult_cancel_right [simp, no_atp]:
"a * c = b * c \<longleftrightarrow> c = 0 \<or> a = b"
proof -
have "(a * c = b * c) = ((a - b) * c = 0)"
@@ -327,7 +327,7 @@
thus ?thesis by (simp add: disj_commute)
qed
-lemma mult_cancel_left [simp, noatp]:
+lemma mult_cancel_left [simp, no_atp]:
"c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b"
proof -
have "(c * a = c * b) = (c * (a - b) = 0)"
@@ -743,7 +743,7 @@
subclass ordered_ab_group_add ..
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
lemma less_add_iff1:
"a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
@@ -950,7 +950,7 @@
end
text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps[noatp] = algebra_simps
+lemmas ring_simps[no_atp] = algebra_simps
lemmas mult_sign_intros =
mult_nonneg_nonneg mult_nonneg_nonpos
@@ -1099,7 +1099,7 @@
text {* Simprules for comparisons where common factors can be cancelled. *}
-lemmas mult_compare_simps[noatp] =
+lemmas mult_compare_simps[no_atp] =
mult_le_cancel_right mult_le_cancel_left
mult_le_cancel_right1 mult_le_cancel_right2
mult_le_cancel_left1 mult_le_cancel_left2
@@ -1180,7 +1180,7 @@
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
-lemmas eq_minus_self_iff[noatp] = equal_neg_zero
+lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
--- a/src/HOL/Set.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Set.thy Thu Mar 18 12:58:52 2010 +0100
@@ -462,7 +462,7 @@
unfolding mem_def by (erule le_funE, erule le_boolE)
-- {* Rule in Modus Ponens style. *}
-lemma rev_subsetD [noatp,intro?]: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
+lemma rev_subsetD [no_atp,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)
@@ -471,13 +471,13 @@
\medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
*}
-lemma subsetCE [noatp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
+lemma subsetCE [no_atp,elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
unfolding mem_def by (blast dest: le_funE le_boolE)
-lemma subset_eq [noatp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
+lemma subset_eq [no_atp]: "A \<le> B = (\<forall>x\<in>A. x \<in> B)" by blast
-lemma contra_subsetD [noatp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
+lemma contra_subsetD [no_atp]: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
lemma subset_refl [simp]: "A \<subseteq> A"
@@ -791,11 +791,11 @@
subsubsection {* Singletons, using insert *}
-lemma singletonI [intro!,noatp]: "a : {a}"
+lemma singletonI [intro!,no_atp]: "a : {a}"
-- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
by (rule insertI1)
-lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
+lemma singletonD [dest!,no_atp]: "b : {a} ==> b = a"
by blast
lemmas singletonE = singletonD [elim_format]
@@ -806,11 +806,11 @@
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
by blast
-lemma singleton_insert_inj_eq [iff,noatp]:
+lemma singleton_insert_inj_eq [iff,no_atp]:
"({b} = insert a A) = (a = b & A \<subseteq> {b})"
by blast
-lemma singleton_insert_inj_eq' [iff,noatp]:
+lemma singleton_insert_inj_eq' [iff,no_atp]:
"(insert a A = {b}) = (a = b & A \<subseteq> {b})"
by blast
@@ -837,7 +837,7 @@
*}
definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
- image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
+ image_def [no_atp]: "f ` A = {y. EX x:A. y = f(x)}"
abbreviation
range :: "('a => 'b) => 'b set" where -- "of function"
@@ -942,10 +942,10 @@
subsubsection {* The ``proper subset'' relation *}
-lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
+lemma psubsetI [intro!,no_atp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
by (unfold less_le) blast
-lemma psubsetE [elim!,noatp]:
+lemma psubsetE [elim!,no_atp]:
"[|A \<subset> B; [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
by (unfold less_le) blast
@@ -1102,12 +1102,12 @@
lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
by blast
-lemma insert_disjoint [simp,noatp]:
+lemma insert_disjoint [simp,no_atp]:
"(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,noatp]:
+lemma disjoint_insert [simp,no_atp]:
"(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
@@ -1139,7 +1139,7 @@
by blast
-lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
+lemma image_Collect [no_atp]: "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. *}
@@ -1156,7 +1156,7 @@
text {* \medskip @{text range}. *}
-lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
+lemma full_SetCompr_eq [no_atp]: "{u. \<exists>x. u = f x} = range f"
by auto
lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
@@ -1213,7 +1213,7 @@
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
by blast
-lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by blast
lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
@@ -1376,7 +1376,7 @@
lemma Diff_eq: "A - B = A \<inter> (-B)"
by blast
-lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
+lemma Diff_eq_empty_iff [simp,no_atp]: "(A - B = {}) = (A \<subseteq> B)"
by blast
lemma Diff_cancel [simp]: "A - A = {}"
@@ -1397,7 +1397,7 @@
lemma Diff_UNIV [simp]: "A - UNIV = {}"
by blast
-lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
+lemma Diff_insert0 [simp,no_atp]: "x \<notin> A ==> A - insert x B = A - B"
by blast
lemma Diff_insert: "A - insert a B = A - B - {a}"
@@ -1639,7 +1639,7 @@
-- {* monotonicity *}
by blast
-lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq [no_atp]: "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/SetInterval.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/SetInterval.thy Thu Mar 18 12:58:52 2010 +0100
@@ -165,19 +165,19 @@
context ord
begin
-lemma greaterThanLessThan_iff [simp,noatp]:
+lemma greaterThanLessThan_iff [simp,no_atp]:
"(i : {l<..<u}) = (l < i & i < u)"
by (simp add: greaterThanLessThan_def)
-lemma atLeastLessThan_iff [simp,noatp]:
+lemma atLeastLessThan_iff [simp,no_atp]:
"(i : {l..<u}) = (l <= i & i < u)"
by (simp add: atLeastLessThan_def)
-lemma greaterThanAtMost_iff [simp,noatp]:
+lemma greaterThanAtMost_iff [simp,no_atp]:
"(i : {l<..u}) = (l < i & i <= u)"
by (simp add: greaterThanAtMost_def)
-lemma atLeastAtMost_iff [simp,noatp]:
+lemma atLeastAtMost_iff [simp,no_atp]:
"(i : {l..u}) = (l <= i & i <= u)"
by (simp add: atLeastAtMost_def)
@@ -844,7 +844,7 @@
subsubsection {* Some Subset Conditions *}
-lemma ivl_subset [simp,noatp]:
+lemma ivl_subset [simp,no_atp]:
"({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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Mar 18 12:58:52 2010 +0100
@@ -412,10 +412,11 @@
fun name_thm_pairs ctxt =
let
val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
- fun blacklisted (_, th) =
- run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
+ val blacklist =
+ if run_blacklist_filter then No_ATPs.get ctxt |> map Thm.prop_of else []
+ fun is_blacklisted (_, th) = member (op =) blacklist (Thm.prop_of th)
in
- filter_out blacklisted
+ filter_out is_blacklisted
(fold add_single_names singles (fold add_multi_names mults []))
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Mar 18 12:58:52 2010 +0100
@@ -326,7 +326,7 @@
val multi_base_blacklist =
["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
- "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "noatp" *)
+ "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *)
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
--- a/src/HOL/Tools/res_blacklist.ML Wed Mar 17 19:37:44 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: HOL/Tools/res_blacklist.ML
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Author: Makarius
-
-Theorems blacklisted to sledgehammer. These theorems typically
-produce clauses that are prolific (match too many equality or
-membership literals) and relate to seldom-used facts. Some duplicate
-other rules.
-*)
-
-signature RES_BLACKLIST =
-sig
- val setup: theory -> theory
- val blacklisted: Proof.context -> thm -> bool
- val add: attribute
- val del: attribute
-end;
-
-structure Res_Blacklist: RES_BLACKLIST =
-struct
-
-structure Data = Generic_Data
-(
- type T = thm Termtab.table;
- val empty = Termtab.empty;
- val extend = I;
- fun merge tabs = Termtab.merge (K true) tabs;
-);
-
-fun blacklisted ctxt th =
- Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
-
-fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
-fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
-
-val add = Thm.declaration_attribute add_thm;
-val del = Thm.declaration_attribute del_thm;
-
-val setup =
- Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
- PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
-
-end;
--- a/src/HOL/Wellfounded.thy Wed Mar 17 19:37:44 2010 +0100
+++ b/src/HOL/Wellfounded.thy Thu Mar 18 12:58:52 2010 +0100
@@ -908,7 +908,7 @@
lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
by (induct n) simp_all
-declare "prod.size" [noatp]
+declare "prod.size" [no_atp]
lemma [code]:
"size (P :: 'a Predicate.pred) = 0" by (cases P) simp