# HG changeset patch
# User paulson
# Date 1187175176 -7200
# Node ID 7619080e49f0de6de218b1e7eaee9b85df53ac24
# Parent  066bb557570f9f23ad5da521eb2bd042dea16c7b
ATP blacklisting is now in theory data, attribute noatp

diff -r 066bb557570f -r 7619080e49f0 src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -193,19 +193,19 @@
 text{*These are actually for fields, like real: but where else to put them?*}
 lemmas zero_less_divide_iff_number_of =
     zero_less_divide_iff [of "number_of w", standard]
-declare zero_less_divide_iff_number_of [simp]
+declare zero_less_divide_iff_number_of [simp,noatp]
 
 lemmas divide_less_0_iff_number_of =
     divide_less_0_iff [of "number_of w", standard]
-declare divide_less_0_iff_number_of [simp]
+declare divide_less_0_iff_number_of [simp,noatp]
 
 lemmas zero_le_divide_iff_number_of =
     zero_le_divide_iff [of "number_of w", standard]
-declare zero_le_divide_iff_number_of [simp]
+declare zero_le_divide_iff_number_of [simp,noatp]
 
 lemmas divide_le_0_iff_number_of =
     divide_le_0_iff [of "number_of w", standard]
-declare divide_le_0_iff_number_of [simp]
+declare divide_le_0_iff_number_of [simp,noatp]
 
 
 (****
@@ -249,58 +249,58 @@
 into the literal.*}
 lemmas less_minus_iff_number_of =
     less_minus_iff [of "number_of v", standard]
-declare less_minus_iff_number_of [simp]
+declare less_minus_iff_number_of [simp,noatp]
 
 lemmas le_minus_iff_number_of =
     le_minus_iff [of "number_of v", standard]
-declare le_minus_iff_number_of [simp]
+declare le_minus_iff_number_of [simp,noatp]
 
 lemmas equation_minus_iff_number_of =
     equation_minus_iff [of "number_of v", standard]
-declare equation_minus_iff_number_of [simp]
+declare equation_minus_iff_number_of [simp,noatp]
 
 
 lemmas minus_less_iff_number_of =
     minus_less_iff [of _ "number_of v", standard]
-declare minus_less_iff_number_of [simp]
+declare minus_less_iff_number_of [simp,noatp]
 
 lemmas minus_le_iff_number_of =
     minus_le_iff [of _ "number_of v", standard]
-declare minus_le_iff_number_of [simp]
+declare minus_le_iff_number_of [simp,noatp]
 
 lemmas minus_equation_iff_number_of =
     minus_equation_iff [of _ "number_of v", standard]
-declare minus_equation_iff_number_of [simp]
+declare minus_equation_iff_number_of [simp,noatp]
 
 
 text{*To Simplify Inequalities Where One Side is the Constant 1*}
 
-lemma less_minus_iff_1 [simp]:
+lemma less_minus_iff_1 [simp,noatp]:
   fixes b::"'b::{ordered_idom,number_ring}"
   shows "(1 < - b) = (b < -1)"
 by auto
 
-lemma le_minus_iff_1 [simp]:
+lemma le_minus_iff_1 [simp,noatp]:
   fixes b::"'b::{ordered_idom,number_ring}"
   shows "(1 \<le> - b) = (b \<le> -1)"
 by auto
 
-lemma equation_minus_iff_1 [simp]:
+lemma equation_minus_iff_1 [simp,noatp]:
   fixes b::"'b::number_ring"
   shows "(1 = - b) = (b = -1)"
 by (subst equation_minus_iff, auto)
 
-lemma minus_less_iff_1 [simp]:
+lemma minus_less_iff_1 [simp,noatp]:
   fixes a::"'b::{ordered_idom,number_ring}"
   shows "(- a < 1) = (-1 < a)"
 by auto
 
-lemma minus_le_iff_1 [simp]:
+lemma minus_le_iff_1 [simp,noatp]:
   fixes a::"'b::{ordered_idom,number_ring}"
   shows "(- a \<le> 1) = (-1 \<le> a)"
 by auto
 
-lemma minus_equation_iff_1 [simp]:
+lemma minus_equation_iff_1 [simp,noatp]:
   fixes a::"'b::number_ring"
   shows "(- a = 1) = (a = -1)"
 by (subst minus_equation_iff, auto)
@@ -310,19 +310,19 @@
 
 lemmas mult_less_cancel_left_number_of =
     mult_less_cancel_left [of "number_of v", standard]
-declare mult_less_cancel_left_number_of [simp]
+declare mult_less_cancel_left_number_of [simp,noatp]
 
 lemmas mult_less_cancel_right_number_of =
     mult_less_cancel_right [of _ "number_of v", standard]
-declare mult_less_cancel_right_number_of [simp]
+declare mult_less_cancel_right_number_of [simp,noatp]
 
 lemmas mult_le_cancel_left_number_of =
     mult_le_cancel_left [of "number_of v", standard]
-declare mult_le_cancel_left_number_of [simp]
+declare mult_le_cancel_left_number_of [simp,noatp]
 
 lemmas mult_le_cancel_right_number_of =
     mult_le_cancel_right [of _ "number_of v", standard]
-declare mult_le_cancel_right_number_of [simp]
+declare mult_le_cancel_right_number_of [simp,noatp]
 
 
 text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Datatype.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -556,6 +556,8 @@
   inject Pair_eq
   induction prod_induct
 
+declare prod.size [noatp]
+
 lemmas prod_caseI = prod.cases [THEN iffD2, standard]
 
 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -483,6 +483,8 @@
 lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
   by (blast intro: dvd_0_left)
 
+declare dvd_0_left_iff [noatp]
+
 lemma dvd_1_left [iff]: "Suc 0 dvd k"
   unfolding dvd_def by simp
 
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -1507,7 +1507,7 @@
 lemma card_empty [simp]: "card {} = 0"
   by (simp add: card_def)
 
-lemma card_infinite [simp]: "~ finite A ==> card A = 0"
+lemma card_infinite [simp,noatp]: "~ finite A ==> card A = 0"
   by (simp add: card_def)
 
 lemma card_eq_setsum: "card A = setsum (%x. 1) A"
@@ -1521,7 +1521,7 @@
     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
   by (simp add: insert_absorb)
 
-lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
+lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
   apply auto
   apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
   done
@@ -2034,7 +2034,7 @@
   then show ?thesis by (simp add: below_def)
 qed
 
-lemma below_f_conv [simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
+lemma below_f_conv [simp,noatp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
 proof
   assume "x \<sqsubseteq> y \<cdot> z"
   hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
@@ -2099,7 +2099,7 @@
   qed
 qed
 
-lemma strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
+lemma strict_below_f_conv[simp,noatp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
 apply(simp add: strict_below_def)
 using lin[of y z] by (auto simp:below_def ACI)
 
@@ -2575,12 +2575,12 @@
 lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def]
 lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def]
 
-lemma Min_in [simp]:
+lemma Min_in [simp,noatp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
   using ACf.fold1_in [OF ACf_min]
   by (fastsimp simp: Min_def min_def)
 
-lemma Max_in [simp]:
+lemma Max_in [simp,noatp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
   using ACf.fold1_in [OF ACf_max]
   by (fastsimp simp: Max_def max_def)
@@ -2591,41 +2591,41 @@
 lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<^loc>\<le> Max N"
   by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
 
-lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
+lemma Min_le [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
   by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
 
-lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
+lemma Max_ge [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
   by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
 
-lemma Min_ge_iff [simp]:
+lemma Min_ge_iff [simp,noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>\<le> a)"
   by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
 
-lemma Max_le_iff [simp]:
+lemma Max_le_iff [simp,noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>\<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>\<le> x)"
   by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
 
-lemma Min_gr_iff [simp]:
+lemma Min_gr_iff [simp,noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>< a)"
   by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
 
-lemma Max_less_iff [simp]:
+lemma Max_less_iff [simp,noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>< x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>< x)"
   by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
 
-lemma Min_le_iff:
+lemma Min_le_iff [noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>\<le> x)"
   by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
 
-lemma Max_ge_iff:
+lemma Max_ge_iff [noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>\<le> a)"
   by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
 
-lemma Min_less_iff:
+lemma Min_less_iff [noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>< x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>< x)"
   by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
 
-lemma Max_gr_iff:
+lemma Max_gr_iff [noatp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>< a)"
   by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
 
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -268,7 +268,7 @@
 lemma vimage_id [simp]: "id -` A = A"
 by (simp add: id_def)
 
-lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
+lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
 by (blast intro: sym)
 
 lemma image_vimage_subset: "f ` (f -` A) <= A"
diff -r 066bb557570f -r 7619080e49f0 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -935,8 +935,14 @@
   (Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())"));
 
 structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
+
+structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
 *}
 
+(*ResBlacklist holds 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.*)
+
 setup {*
 let
   (*prevent substitution on bool*)
@@ -948,6 +954,7 @@
   #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
   #> Classical.setup
   #> ResAtpset.setup
+  #> ResBlacklist.setup
 end
 *}
 
@@ -1136,6 +1143,8 @@
 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]
+
 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
 
@@ -1181,7 +1190,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 = split_if split_if_asm
+lemmas if_splits [noatp] = split_if split_if_asm
 
 lemma if_cancel: "(if c then x else x) = x"
 by (simplesubst split_if, blast)
diff -r 066bb557570f -r 7619080e49f0 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/IntDef.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -71,7 +71,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]  Abs_Integ_inverse [simp]
+declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
 
 text{*Case analysis on the representation of an integer as an equivalence
       class of pairs of naturals.*}
@@ -371,7 +371,7 @@
       It is proved here because attribute @{text arith_split} is not available
       in theory @{text Ring_and_Field}.
       But is it really better than just rewriting with @{text abs_if}?*}
-lemma abs_split [arith_split]:
+lemma abs_split [arith_split,noatp]:
      "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
diff -r 066bb557570f -r 7619080e49f0 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/IntDiv.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -1082,7 +1082,7 @@
 lemma zdvd_0_right [iff]: "(m::int) dvd 0"
   by (simp add: dvd_def)
 
-lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
+lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
   by (simp add: dvd_def)
 
 lemma zdvd_1_left [iff]: "1 dvd (m::int)"
diff -r 066bb557570f -r 7619080e49f0 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/List.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -436,7 +436,7 @@
 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
 by (induct xs) auto
 
-lemma append_eq_append_conv [simp]:
+lemma append_eq_append_conv [simp,noatp]:
  "!!ys. length xs = length ys \<or> length us = length vs
  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
 apply (induct xs)
@@ -469,7 +469,7 @@
 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
 using append_same_eq [of "[]"] by auto
 
-lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl [simp,noatp]: "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)"
@@ -2391,10 +2391,10 @@
   for A :: "'a set"
 where
     Nil [intro!]: "[]: lists A"
-  | Cons [intro!]: "[| 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)"
+  | 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)"
 
 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
   by (clarify, erule listsp.induct, blast+)
@@ -2429,15 +2429,15 @@
 
 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
 
-lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
 by (rule in_listsp_conv_set [THEN iffD1])
 
-lemmas in_listsD [dest!] = in_listspD [to_set]
-
-lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
+
+lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
 by (rule in_listsp_conv_set [THEN iffD2])
 
-lemmas in_listsI [intro!] = in_listspI [to_set]
+lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
 
 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
 by auto
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Nat.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -241,7 +241,7 @@
 lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
   by (blast elim!: less_SucE intro: less_trans)
 
-lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
+lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
   by (simp add: less_Suc_eq)
 
 lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
@@ -516,7 +516,7 @@
 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   by (fast intro: not0_implies_Suc)
 
-lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
+lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   apply (rule iffI)
   apply (rule ccontr)
   apply simp_all
@@ -1012,7 +1012,7 @@
    apply auto
   done
 
-lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
+lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
   apply (rule trans)
   apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   done
@@ -1332,7 +1332,7 @@
 text{*Special cases where either operand is zero*}
 lemma of_nat_0_le_iff [simp]: "(0::'a::ordered_semidom) \<le> of_nat n"
   by (rule of_nat_le_iff [of 0, simplified])
-lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
+lemma of_nat_le_0_iff [simp,noatp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
 text{*Class for unital semirings with characteristic zero.
@@ -1347,9 +1347,9 @@
 by intro_classes (simp add: order_eq_iff)
 
 text{*Special cases where either operand is zero*}
-lemma of_nat_0_eq_iff [simp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
+lemma of_nat_0_eq_iff [simp,noatp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
   by (rule of_nat_eq_iff [of 0, simplified])
-lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
+lemma of_nat_eq_0_iff [simp,noatp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   by (rule of_nat_eq_iff [of _ 0, simplified])
 
 lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
diff -r 066bb557570f -r 7619080e49f0 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -711,16 +711,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]: "0 <= x \<Longrightarrow> pprt x = x"
+lemma pprt_eq_id[simp,noatp]: "0 <= x \<Longrightarrow> pprt x = x"
   by (simp add: pprt_def le_iff_sup sup_aci)
 
-lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
+lemma nprt_eq_id[simp,noatp]: "x <= 0 \<Longrightarrow> nprt x = x"
   by (simp add: nprt_def le_iff_inf inf_aci)
 
-lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
+lemma pprt_eq_0[simp,noatp]: "x <= 0 \<Longrightarrow> pprt x = 0"
   by (simp add: pprt_def le_iff_sup sup_aci)
 
-lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
+lemma nprt_eq_0[simp,noatp]: "0 <= x \<Longrightarrow> nprt x = 0"
   by (simp add: nprt_def le_iff_inf inf_aci)
 
 lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
@@ -745,10 +745,10 @@
 apply (erule sup_0_imp_0)
 done
 
-lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
+lemma inf_0_eq_0[simp,noatp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
 by (auto, erule inf_0_imp_0)
 
-lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
+lemma sup_0_eq_0[simp,noatp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
 by (auto, erule sup_0_imp_0)
 
 lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
@@ -798,6 +798,8 @@
   thus ?thesis by simp
 qed
 
+declare abs_0_eq [noatp] (*essentially the same as the other one*)
+
 lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
 by (simp add: inf_eq_neg_sup)
 
@@ -883,10 +885,10 @@
 lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
 by (simp add: le_iff_inf nprt_def inf_commute)
 
-lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
+lemma pprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
   by (simp add: le_iff_sup pprt_def sup_aci)
 
-lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
+lemma nprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   by (simp add: le_iff_inf nprt_def inf_aci)
 
 lemma pprt_neg: "pprt (-x) = - nprt x"
@@ -1063,7 +1065,7 @@
 lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
 lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]
 declare diff_less_0_iff_less [simp]
-declare diff_eq_0_iff_eq [simp]
+declare diff_eq_0_iff_eq [simp,noatp]
 declare diff_le_0_iff_le [simp]
 
 ML {*
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Orderings.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -225,11 +225,11 @@
   "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
 unfolding max_def le_less using less_linear by (auto intro: less_trans)
 
-lemma split_min:
+lemma split_min [noatp]:
   "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
 by (simp add: min_def)
 
-lemma split_max:
+lemma split_max [noatp]:
   "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
 by (simp add: max_def)
 
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Power.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -183,7 +183,7 @@
 apply (auto simp add: power_Suc abs_mult)
 done
 
-lemma zero_less_power_abs_iff [simp]:
+lemma zero_less_power_abs_iff [simp,noatp]:
      "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
 proof (induct "n")
   case 0
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -22,7 +22,7 @@
   Unity :: unit    ("'(')")
   "() == Abs_unit True"
 
-lemma unit_eq: "u = ()"
+lemma unit_eq [noatp]: "u = ()"
   by (induct u) (simp add: unit_def Unity_def)
 
 text {*
@@ -46,7 +46,7 @@
 lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
   by (rule triv_forall_equality)
 
-lemma unit_induct [induct type: unit]: "P () ==> P x"
+lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
   by simp
 
 text {*
@@ -55,7 +55,7 @@
   f} rather than by @{term [source] "%u. f ()"}.
 *}
 
-lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
+lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
 
@@ -443,7 +443,7 @@
 lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   by (subst surjective_pairing, rule split_conv)
 
-lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
+lemma split_split [noatp]: "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)
 
@@ -454,7 +454,7 @@
   current goal contains one of those constants.
 *}
 
-lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
+lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
 by (subst split_split, simp)
 
 
@@ -525,10 +525,10 @@
 change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
 *}
 
-lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
+lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
 
-lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
+lemma split_eta_SetCompr2 [simp,noatp]: "(%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)"
@@ -696,11 +696,11 @@
   -- {* Suggested by Pierre Chartier *}
   by blast
 
-lemma split_paired_Ball_Sigma [simp]:
+lemma split_paired_Ball_Sigma [simp,noatp]:
     "(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]:
+lemma split_paired_Bex_Sigma [simp,noatp]:
     "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   by blast
 
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Relation.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -112,7 +112,7 @@
 lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
   by (simp add: diag_def)
 
-lemma diagI [intro!]: "a : A ==> (a, a) : diag A"
+lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
   by (rule diag_eqI) (rule refl)
 
 lemma diagE [elim!]:
@@ -325,6 +325,8 @@
 
 subsection {* Domain *}
 
+declare Domain_def [noatp]
+
 lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   by (unfold Domain_def) blast
 
@@ -411,6 +413,8 @@
 
 subsection {* Image of a set under a relation *}
 
+declare Image_def [noatp]
+
 lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   by (simp add: Image_def)
 
@@ -420,7 +424,7 @@
 lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   by (rule Image_iff [THEN trans]) simp
 
-lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
+lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
   by (unfold Image_def) blast
 
 lemma ImageE [elim!]:
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -660,7 +660,7 @@
 qed  
 
 text{*Cancellation of equalities with a common factor*}
-lemma mult_cancel_right [simp]:
+lemma mult_cancel_right [simp,noatp]:
   fixes a b c :: "'a::ring_no_zero_divisors"
   shows "(a * c = b * c) = (c = 0 \<or> a = b)"
 proof -
@@ -670,7 +670,7 @@
     by (simp add: disj_commute)
 qed
 
-lemma mult_cancel_left [simp]:
+lemma mult_cancel_left [simp,noatp]:
   fixes a b c :: "'a::ring_no_zero_divisors"
   shows "(c * a = c * b) = (c = 0 \<or> a = b)"
 proof -
@@ -1029,11 +1029,11 @@
 
 lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
 
-lemma divide_divide_eq_right [simp]:
+lemma divide_divide_eq_right [simp,noatp]:
   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
 by (simp add: divide_inverse mult_ac)
 
-lemma divide_divide_eq_left [simp]:
+lemma divide_divide_eq_left [simp,noatp]:
   "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
 by (simp add: divide_inverse mult_assoc)
 
@@ -1309,7 +1309,7 @@
 done
 
 text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp]:
+lemma inverse_less_iff_less [simp,noatp]:
   "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
 by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
 
@@ -1317,7 +1317,7 @@
   "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
 by (force simp add: order_le_less less_imp_inverse_less)
 
-lemma inverse_le_iff_le [simp]:
+lemma inverse_le_iff_le [simp,noatp]:
  "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
 by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
 
@@ -1351,7 +1351,7 @@
 apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
 done
 
-lemma inverse_less_iff_less_neg [simp]:
+lemma inverse_less_iff_less_neg [simp,noatp]:
   "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
 apply (insert inverse_less_iff_less [of "-b" "-a"])
 apply (simp del: inverse_less_iff_less 
@@ -1362,7 +1362,7 @@
   "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
 by (force simp add: order_le_less less_imp_inverse_less_neg)
 
-lemma inverse_le_iff_le_neg [simp]:
+lemma inverse_le_iff_le_neg [simp,noatp]:
  "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
 by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
@@ -1585,7 +1585,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]:
+lemma divide_eq_0_iff [simp,noatp]:
      "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
 by (simp add: divide_inverse)
 
@@ -1625,13 +1625,13 @@
 
 subsection{*Cancellation Laws for Division*}
 
-lemma divide_cancel_right [simp]:
+lemma divide_cancel_right [simp,noatp]:
      "(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]:
+lemma divide_cancel_left [simp,noatp]:
      "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
 apply (cases "c=0", simp)
 apply (simp add: divide_inverse)
@@ -1641,23 +1641,23 @@
 subsection {* Division and the Number One *}
 
 text{*Simplify expressions equated with 1*}
-lemma divide_eq_1_iff [simp]:
+lemma divide_eq_1_iff [simp,noatp]:
      "(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]:
+lemma one_eq_divide_iff [simp,noatp]:
      "(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]:
+lemma zero_eq_1_divide_iff [simp,noatp]:
      "((0::'a::{ordered_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]:
+lemma one_divide_eq_0_iff [simp,noatp]:
      "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
 apply (cases "a=0", simp)
 apply (insert zero_neq_one [THEN not_sym])
@@ -1671,9 +1671,9 @@
 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
 
 declare zero_less_divide_1_iff [simp]
-declare divide_less_0_1_iff [simp]
+declare divide_less_0_1_iff [simp,noatp]
 declare zero_le_divide_1_iff [simp]
-declare divide_le_0_1_iff [simp]
+declare divide_le_0_1_iff [simp,noatp]
 
 
 subsection {* Ordering Rules for Division *}
@@ -1722,22 +1722,22 @@
 
 text{*Simplify quotients that are compared with the value 1.*}
 
-lemma le_divide_eq_1:
+lemma le_divide_eq_1 [noatp]:
   fixes a :: "'a :: {ordered_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:
+lemma divide_le_eq_1 [noatp]:
   fixes a :: "'a :: {ordered_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:
+lemma less_divide_eq_1 [noatp]:
   fixes a :: "'a :: {ordered_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:
+lemma divide_less_eq_1 [noatp]:
   fixes a :: "'a :: {ordered_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)
@@ -1745,52 +1745,52 @@
 
 subsection{*Conditional Simplification Rules: No Case Splits*}
 
-lemma le_divide_eq_1_pos [simp]:
+lemma le_divide_eq_1_pos [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma le_divide_eq_1_neg [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma divide_le_eq_1_pos [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma divide_le_eq_1_neg [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma less_divide_eq_1_pos [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma less_divide_eq_1_neg [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma divide_less_eq_1_pos [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma divide_less_eq_1_neg [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma eq_divide_eq_1 [simp,noatp]:
   fixes a :: "'a :: {ordered_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]:
+lemma divide_eq_eq_1 [simp,noatp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
   shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Set.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -775,11 +775,11 @@
 
 subsubsection {* Singletons, using insert *}
 
-lemma singletonI [intro!]: "a : {a}"
+lemma singletonI [intro!,noatp]: "a : {a}"
     -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   by (rule insertI1)
 
-lemma singletonD [dest!]: "b : {a} ==> b = a"
+lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
   by blast
 
 lemmas singletonE = singletonD [elim_format]
@@ -790,10 +790,12 @@
 lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   by blast
 
-lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \<subseteq> {b})"
+lemma singleton_insert_inj_eq [iff,noatp]:
+     "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   by blast
 
-lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
+lemma singleton_insert_inj_eq' [iff,noatp]:
+     "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   by blast
 
 lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
@@ -818,6 +820,8 @@
   @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
 *}
 
+declare UNION_def [noatp]
+
 lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   by (unfold UNION_def) blast
 
@@ -858,7 +862,7 @@
 
 subsubsection {* Union *}
 
-lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"
+lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
   by (unfold Union_def) blast
 
 lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
@@ -872,7 +876,7 @@
 
 subsubsection {* Inter *}
 
-lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"
+lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
   by (unfold Inter_def) blast
 
 lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
@@ -897,6 +901,8 @@
   not have the syntactic form of @{term "f x"}.
 *}
 
+declare image_def [noatp]
+
 lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   by (unfold image_def) blast
 
@@ -996,10 +1002,10 @@
 
 subsubsection {* The ``proper subset'' relation *}
 
-lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
+lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   by (unfold psubset_def) blast
 
-lemma psubsetE [elim!]: 
+lemma psubsetE [elim!,noatp]: 
     "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   by (unfold psubset_def) blast
 
@@ -1164,10 +1170,10 @@
 lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   by blast
 
-lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   by blast
 
-lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   by blast
 
 
@@ -1211,12 +1217,12 @@
 lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   by blast
 
-lemma insert_disjoint[simp]:
+lemma insert_disjoint [simp,noatp]:
  "(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]:
+lemma disjoint_insert [simp,noatp]:
  "(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
@@ -1245,7 +1251,7 @@
   by blast
 
 
-lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
+lemma image_Collect [noatp]: "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. *}
@@ -1262,7 +1268,7 @@
 
 text {* \medskip @{text range}. *}
 
-lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
+lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
   by auto
 
 lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
@@ -1322,7 +1328,7 @@
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   by blast
 
-lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+lemma Int_UNIV [simp,noatp]: "(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)"
@@ -1479,10 +1485,10 @@
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   by blast
 
-lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   by blast
 
-lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   by blast
 
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
@@ -1506,7 +1512,7 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
-lemma Inter_UNIV_conv [simp]:
+lemma Inter_UNIV_conv [simp,noatp]:
   "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   by blast+
@@ -1517,7 +1523,7 @@
 
   Basic identities: *}
 
-lemma UN_empty [simp]: "(\<Union>x\<in>{}. B x) = {}"
+lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
   by blast
 
 lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
@@ -1657,7 +1663,7 @@
 lemma Diff_eq: "A - B = A \<inter> (-B)"
   by blast
 
-lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
+lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
   by blast
 
 lemma Diff_cancel [simp]: "A - A = {}"
@@ -1678,7 +1684,7 @@
 lemma Diff_UNIV [simp]: "A - UNIV = {}"
   by blast
 
-lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
+lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
   by blast
 
 lemma Diff_insert: "A - insert a B = A - B - {a}"
@@ -1850,7 +1856,7 @@
   "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
   by auto
 
-lemma ball_simps [simp]:
+lemma ball_simps [simp,noatp]:
   "!!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))"
@@ -1865,7 +1871,7 @@
   "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
   by auto
 
-lemma bex_simps [simp]:
+lemma bex_simps [simp,noatp]:
   "!!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"
diff -r 066bb557570f -r 7619080e49f0 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/SetInterval.thy	Wed Aug 15 12:52:56 2007 +0200
@@ -153,19 +153,19 @@
 
 subsection {*Two-sided intervals*}
 
-lemma greaterThanLessThan_iff [simp]:
+lemma greaterThanLessThan_iff [simp,noatp]:
   "(i : {l<..<u}) = (l < i & i < u)"
 by (simp add: greaterThanLessThan_def)
 
-lemma atLeastLessThan_iff [simp]:
+lemma atLeastLessThan_iff [simp,noatp]:
   "(i : {l..<u}) = (l <= i & i < u)"
 by (simp add: atLeastLessThan_def)
 
-lemma greaterThanAtMost_iff [simp]:
+lemma greaterThanAtMost_iff [simp,noatp]:
   "(i : {l<..u}) = (l < i & i <= u)"
 by (simp add: greaterThanAtMost_def)
 
-lemma atLeastAtMost_iff [simp]:
+lemma atLeastAtMost_iff [simp,noatp]:
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
@@ -569,7 +569,7 @@
 
 subsubsection {* Some Subset Conditions *}
 
-lemma ivl_subset[simp]:
+lemma ivl_subset [simp,noatp]:
  "({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)
diff -r 066bb557570f -r 7619080e49f0 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Aug 15 09:02:11 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Aug 15 12:52:56 2007 +0200
@@ -260,152 +260,6 @@
   or identified with ATPset (which however is too big currently)*)
 val whitelist = [subsetI];
 
-(*Names of theorems and theorem lists to be blacklisted.
-
-  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.
-  FIXME: this blacklist needs to be maintained using theory data and added to using
-  an attribute.*)
-val blacklist = 
-  ["Datatype.prod.size",
-   "Divides.dvd_0_left_iff",
-   "Finite_Set.card_0_eq",
-   "Finite_Set.card_infinite",
-   "Finite_Set.Max_ge",
-   "Finite_Set.Max_in",
-   "Finite_Set.Max_le_iff",
-   "Finite_Set.Max_less_iff",
-   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
-   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
-   "Finite_Set.Min_ge_iff",
-   "Finite_Set.Min_gr_iff",
-   "Finite_Set.Min_in",
-   "Finite_Set.Min_le",
-   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
-   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
-   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
-   "HOL.split_if_asm",     (*splitting theorem*)
-   "HOL.split_if",         (*splitting theorem*)
-   "HOL.All_def",          (*far worse than useless!!*)
-   "IntDef.abs_split",
-   "IntDef.Integ.Abs_Integ_inject",
-   "IntDef.Integ.Abs_Integ_inverse",
-   "IntDiv.zdvd_0_left",
-   "List.append_eq_append_conv",
-   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
-   "List.in_listsD",
-   "List.in_listsI",
-   "List.lists.Cons",
-   "List.listsE",
-   "Nat.less_one", (*not directional? obscure*)
-   "Nat.not_gr0",
-   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
-   "Nat.of_nat_0_eq_iff",
-   "Nat.of_nat_eq_0_iff",
-   "Nat.of_nat_le_0_iff",
-   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
-   "NatSimprocs.divide_less_0_iff_number_of",
-   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
-   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
-   "NatSimprocs.le_minus_iff_1", (*not directional*)
-   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
-   "NatSimprocs.less_minus_iff_1", (*not directional*)
-   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
-   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
-   "NatSimprocs.minus_le_iff_1", (*not directional*)
-   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
-   "NatSimprocs.minus_less_iff_1", (*not directional*)
-   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
-   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
-   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
-   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
-   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
-   "NatSimprocs.zero_less_divide_iff_number_of",
-   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
-   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
-   "OrderedGroup.sup_0_eq_0",
-   "OrderedGroup.inf_0_eq_0",
-   "OrderedGroup.pprt_eq_0",   (*obscure*)
-   "OrderedGroup.pprt_eq_id",   (*obscure*)
-   "OrderedGroup.pprt_mono",   (*obscure*)
-   "Orderings.split_max",      (*splitting theorem*)
-   "Orderings.split_min",      (*splitting theorem*)
-   "Power.zero_less_power_abs_iff",
-   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
-   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
-   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
-   "Product_Type.split_split_asm",             (*splitting theorem*)
-   "Product_Type.split_split",                 (*splitting theorem*)
-   "Product_Type.unit_abs_eta_conv",
-   "Product_Type.unit_induct",
-   "Relation.diagI",
-   "Relation.Domain_def",   (*involves an existential quantifier*)
-   "Relation.Image_def",   (*involves an existential quantifier*)
-   "Relation.ImageI",
-   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
-   "Ring_and_Field.divide_cancel_right",
-   "Ring_and_Field.divide_divide_eq_left",
-   "Ring_and_Field.divide_divide_eq_right",
-   "Ring_and_Field.divide_eq_0_iff",
-   "Ring_and_Field.divide_eq_1_iff",
-   "Ring_and_Field.divide_eq_eq_1",
-   "Ring_and_Field.divide_le_0_1_iff",
-   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
-   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
-   "Ring_and_Field.divide_less_0_1_iff",
-   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
-   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
-   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
-   "Ring_and_Field.field_mult_cancel_left",
-   "Ring_and_Field.field_mult_cancel_right",
-   "Ring_and_Field.inverse_le_iff_le_neg",
-   "Ring_and_Field.inverse_le_iff_le",
-   "Ring_and_Field.inverse_less_iff_less_neg",
-   "Ring_and_Field.inverse_less_iff_less",
-   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
-   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
-   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
-   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
-   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
-   "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
-   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
-   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
-   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
-   "Set.Diff_insert0",
-   "Set.empty_Union_conv",   (*redundant with paramodulation*)
-   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
-   "Set.image_Collect",      (*involves Collect and a boolean variable...*)
-   "Set.image_def",          (*involves an existential quantifier*)
-   "Set.disjoint_insert", "Set.insert_disjoint",
-   "Set.Int_UNIV",  (*redundant with paramodulation*)
-   "Set.Inter_UNIV_conv",
-   "Set.Inter_iff", (*We already have InterI, InterE*)
-   "Set.psubsetE",    (*too prolific and obscure*)
-   "Set.psubsetI",
-   "Set.singleton_insert_inj_eq'",
-   "Set.singleton_insert_inj_eq",
-   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
-   "Set.singletonI",
-   "Set.Un_empty", (*redundant with paramodulation*)
-   "Set.UNION_def",   (*involves an existential quantifier*)
-   "Set.Union_empty_conv", (*redundant with paramodulation*)
-   "Set.Union_iff",              (*We already have UnionI, UnionE*)
-   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
-   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
-   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
-   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
-   "SetInterval.ivl_subset"];  (*excessive case analysis*)
-
-(*These might be prolific but are probably OK, and min and max are basic.
-   "Orderings.max_less_iff_conj",
-   "Orderings.min_less_iff_conj",
-   "Orderings.min_max.below_inf.below_inf_conv",
-   "Orderings.min_max.below_sup.above_sup_conv",
-Very prolific and somewhat obscure:
-   "Set.InterD",
-   "Set.UnionI",
-*)
-
 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
 
 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
@@ -473,9 +327,7 @@
 
 fun all_valid_thms ctxt =
   let
-    val banned_tab = foldl setinsert Symtab.empty blacklist
-    fun blacklisted s = !run_blacklist_filter andalso
-                        (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
+    fun blacklisted s = !run_blacklist_filter andalso is_package_def s
 
     fun extern_valid space (name, ths) =
       let
@@ -514,10 +366,16 @@
 
 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
 
-(*The single theorems go BEFORE the multiple ones*)
+(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
 fun name_thm_pairs ctxt =
   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
-  in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
+      val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
+      fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
+  in
+      app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
+      filter (not o blacklisted o #2)
+        (foldl add_single_names (foldl add_multi_names [] mults) singles)
+  end;
 
 fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
   | check_named (_,th) = true;