ATP blacklisting is now in theory data, attribute noatp
authorpaulson
Wed Aug 15 12:52:56 2007 +0200 (2007-08-15)
changeset 242867619080e49f0
parent 24285 066bb557570f
child 24287 c857dac06da6
ATP blacklisting is now in theory data, attribute noatp
src/HOL/Arith_Tools.thy
src/HOL/Datatype.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/IntDef.thy
src/HOL/IntDiv.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/OrderedGroup.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Ring_and_Field.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Arith_Tools.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Arith_Tools.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -193,19 +193,19 @@
     1.4  text{*These are actually for fields, like real: but where else to put them?*}
     1.5  lemmas zero_less_divide_iff_number_of =
     1.6      zero_less_divide_iff [of "number_of w", standard]
     1.7 -declare zero_less_divide_iff_number_of [simp]
     1.8 +declare zero_less_divide_iff_number_of [simp,noatp]
     1.9  
    1.10  lemmas divide_less_0_iff_number_of =
    1.11      divide_less_0_iff [of "number_of w", standard]
    1.12 -declare divide_less_0_iff_number_of [simp]
    1.13 +declare divide_less_0_iff_number_of [simp,noatp]
    1.14  
    1.15  lemmas zero_le_divide_iff_number_of =
    1.16      zero_le_divide_iff [of "number_of w", standard]
    1.17 -declare zero_le_divide_iff_number_of [simp]
    1.18 +declare zero_le_divide_iff_number_of [simp,noatp]
    1.19  
    1.20  lemmas divide_le_0_iff_number_of =
    1.21      divide_le_0_iff [of "number_of w", standard]
    1.22 -declare divide_le_0_iff_number_of [simp]
    1.23 +declare divide_le_0_iff_number_of [simp,noatp]
    1.24  
    1.25  
    1.26  (****
    1.27 @@ -249,58 +249,58 @@
    1.28  into the literal.*}
    1.29  lemmas less_minus_iff_number_of =
    1.30      less_minus_iff [of "number_of v", standard]
    1.31 -declare less_minus_iff_number_of [simp]
    1.32 +declare less_minus_iff_number_of [simp,noatp]
    1.33  
    1.34  lemmas le_minus_iff_number_of =
    1.35      le_minus_iff [of "number_of v", standard]
    1.36 -declare le_minus_iff_number_of [simp]
    1.37 +declare le_minus_iff_number_of [simp,noatp]
    1.38  
    1.39  lemmas equation_minus_iff_number_of =
    1.40      equation_minus_iff [of "number_of v", standard]
    1.41 -declare equation_minus_iff_number_of [simp]
    1.42 +declare equation_minus_iff_number_of [simp,noatp]
    1.43  
    1.44  
    1.45  lemmas minus_less_iff_number_of =
    1.46      minus_less_iff [of _ "number_of v", standard]
    1.47 -declare minus_less_iff_number_of [simp]
    1.48 +declare minus_less_iff_number_of [simp,noatp]
    1.49  
    1.50  lemmas minus_le_iff_number_of =
    1.51      minus_le_iff [of _ "number_of v", standard]
    1.52 -declare minus_le_iff_number_of [simp]
    1.53 +declare minus_le_iff_number_of [simp,noatp]
    1.54  
    1.55  lemmas minus_equation_iff_number_of =
    1.56      minus_equation_iff [of _ "number_of v", standard]
    1.57 -declare minus_equation_iff_number_of [simp]
    1.58 +declare minus_equation_iff_number_of [simp,noatp]
    1.59  
    1.60  
    1.61  text{*To Simplify Inequalities Where One Side is the Constant 1*}
    1.62  
    1.63 -lemma less_minus_iff_1 [simp]:
    1.64 +lemma less_minus_iff_1 [simp,noatp]:
    1.65    fixes b::"'b::{ordered_idom,number_ring}"
    1.66    shows "(1 < - b) = (b < -1)"
    1.67  by auto
    1.68  
    1.69 -lemma le_minus_iff_1 [simp]:
    1.70 +lemma le_minus_iff_1 [simp,noatp]:
    1.71    fixes b::"'b::{ordered_idom,number_ring}"
    1.72    shows "(1 \<le> - b) = (b \<le> -1)"
    1.73  by auto
    1.74  
    1.75 -lemma equation_minus_iff_1 [simp]:
    1.76 +lemma equation_minus_iff_1 [simp,noatp]:
    1.77    fixes b::"'b::number_ring"
    1.78    shows "(1 = - b) = (b = -1)"
    1.79  by (subst equation_minus_iff, auto)
    1.80  
    1.81 -lemma minus_less_iff_1 [simp]:
    1.82 +lemma minus_less_iff_1 [simp,noatp]:
    1.83    fixes a::"'b::{ordered_idom,number_ring}"
    1.84    shows "(- a < 1) = (-1 < a)"
    1.85  by auto
    1.86  
    1.87 -lemma minus_le_iff_1 [simp]:
    1.88 +lemma minus_le_iff_1 [simp,noatp]:
    1.89    fixes a::"'b::{ordered_idom,number_ring}"
    1.90    shows "(- a \<le> 1) = (-1 \<le> a)"
    1.91  by auto
    1.92  
    1.93 -lemma minus_equation_iff_1 [simp]:
    1.94 +lemma minus_equation_iff_1 [simp,noatp]:
    1.95    fixes a::"'b::number_ring"
    1.96    shows "(- a = 1) = (a = -1)"
    1.97  by (subst minus_equation_iff, auto)
    1.98 @@ -310,19 +310,19 @@
    1.99  
   1.100  lemmas mult_less_cancel_left_number_of =
   1.101      mult_less_cancel_left [of "number_of v", standard]
   1.102 -declare mult_less_cancel_left_number_of [simp]
   1.103 +declare mult_less_cancel_left_number_of [simp,noatp]
   1.104  
   1.105  lemmas mult_less_cancel_right_number_of =
   1.106      mult_less_cancel_right [of _ "number_of v", standard]
   1.107 -declare mult_less_cancel_right_number_of [simp]
   1.108 +declare mult_less_cancel_right_number_of [simp,noatp]
   1.109  
   1.110  lemmas mult_le_cancel_left_number_of =
   1.111      mult_le_cancel_left [of "number_of v", standard]
   1.112 -declare mult_le_cancel_left_number_of [simp]
   1.113 +declare mult_le_cancel_left_number_of [simp,noatp]
   1.114  
   1.115  lemmas mult_le_cancel_right_number_of =
   1.116      mult_le_cancel_right [of _ "number_of v", standard]
   1.117 -declare mult_le_cancel_right_number_of [simp]
   1.118 +declare mult_le_cancel_right_number_of [simp,noatp]
   1.119  
   1.120  
   1.121  text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
     2.1 --- a/src/HOL/Datatype.thy	Wed Aug 15 09:02:11 2007 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Wed Aug 15 12:52:56 2007 +0200
     2.3 @@ -556,6 +556,8 @@
     2.4    inject Pair_eq
     2.5    induction prod_induct
     2.6  
     2.7 +declare prod.size [noatp]
     2.8 +
     2.9  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
    2.10  
    2.11  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
     3.1 --- a/src/HOL/Divides.thy	Wed Aug 15 09:02:11 2007 +0200
     3.2 +++ b/src/HOL/Divides.thy	Wed Aug 15 12:52:56 2007 +0200
     3.3 @@ -483,6 +483,8 @@
     3.4  lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
     3.5    by (blast intro: dvd_0_left)
     3.6  
     3.7 +declare dvd_0_left_iff [noatp]
     3.8 +
     3.9  lemma dvd_1_left [iff]: "Suc 0 dvd k"
    3.10    unfolding dvd_def by simp
    3.11  
     4.1 --- a/src/HOL/Finite_Set.thy	Wed Aug 15 09:02:11 2007 +0200
     4.2 +++ b/src/HOL/Finite_Set.thy	Wed Aug 15 12:52:56 2007 +0200
     4.3 @@ -1507,7 +1507,7 @@
     4.4  lemma card_empty [simp]: "card {} = 0"
     4.5    by (simp add: card_def)
     4.6  
     4.7 -lemma card_infinite [simp]: "~ finite A ==> card A = 0"
     4.8 +lemma card_infinite [simp,noatp]: "~ finite A ==> card A = 0"
     4.9    by (simp add: card_def)
    4.10  
    4.11  lemma card_eq_setsum: "card A = setsum (%x. 1) A"
    4.12 @@ -1521,7 +1521,7 @@
    4.13      "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
    4.14    by (simp add: insert_absorb)
    4.15  
    4.16 -lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})"
    4.17 +lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})"
    4.18    apply auto
    4.19    apply (drule_tac a = x in mk_disjoint_insert, clarify, auto)
    4.20    done
    4.21 @@ -2034,7 +2034,7 @@
    4.22    then show ?thesis by (simp add: below_def)
    4.23  qed
    4.24  
    4.25 -lemma below_f_conv [simp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    4.26 +lemma below_f_conv [simp,noatp]: "x \<sqsubseteq> y \<cdot> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    4.27  proof
    4.28    assume "x \<sqsubseteq> y \<cdot> z"
    4.29    hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
    4.30 @@ -2099,7 +2099,7 @@
    4.31    qed
    4.32  qed
    4.33  
    4.34 -lemma strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
    4.35 +lemma strict_below_f_conv[simp,noatp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
    4.36  apply(simp add: strict_below_def)
    4.37  using lin[of y z] by (auto simp:below_def ACI)
    4.38  
    4.39 @@ -2575,12 +2575,12 @@
    4.40  lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def]
    4.41  lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def]
    4.42  
    4.43 -lemma Min_in [simp]:
    4.44 +lemma Min_in [simp,noatp]:
    4.45    shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
    4.46    using ACf.fold1_in [OF ACf_min]
    4.47    by (fastsimp simp: Min_def min_def)
    4.48  
    4.49 -lemma Max_in [simp]:
    4.50 +lemma Max_in [simp,noatp]:
    4.51    shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
    4.52    using ACf.fold1_in [OF ACf_max]
    4.53    by (fastsimp simp: Max_def max_def)
    4.54 @@ -2591,41 +2591,41 @@
    4.55  lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<^loc>\<le> Max N"
    4.56    by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max])
    4.57  
    4.58 -lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
    4.59 +lemma Min_le [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x"
    4.60    by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min])
    4.61  
    4.62 -lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
    4.63 +lemma Max_ge [simp,noatp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A"
    4.64    by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max])
    4.65  
    4.66 -lemma Min_ge_iff [simp]:
    4.67 +lemma Min_ge_iff [simp,noatp]:
    4.68    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>\<le> a)"
    4.69    by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min])
    4.70  
    4.71 -lemma Max_le_iff [simp]:
    4.72 +lemma Max_le_iff [simp,noatp]:
    4.73    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>\<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>\<le> x)"
    4.74    by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max])
    4.75  
    4.76 -lemma Min_gr_iff [simp]:
    4.77 +lemma Min_gr_iff [simp,noatp]:
    4.78    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<^loc>< a)"
    4.79    by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min])
    4.80  
    4.81 -lemma Max_less_iff [simp]:
    4.82 +lemma Max_less_iff [simp,noatp]:
    4.83    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A \<^loc>< x \<longleftrightarrow> (\<forall>a\<in>A. a \<^loc>< x)"
    4.84    by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max])
    4.85  
    4.86 -lemma Min_le_iff:
    4.87 +lemma Min_le_iff [noatp]:
    4.88    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>\<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>\<le> x)"
    4.89    by (simp add: Min_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_min])
    4.90  
    4.91 -lemma Max_ge_iff:
    4.92 +lemma Max_ge_iff [noatp]:
    4.93    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>\<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>\<le> a)"
    4.94    by (simp add: Max_def ACIfSLlin.fold1_below_iff [OF ACIfSLlin_max])
    4.95  
    4.96 -lemma Min_less_iff:
    4.97 +lemma Min_less_iff [noatp]:
    4.98    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<^loc>< x \<longleftrightarrow> (\<exists>a\<in>A. a \<^loc>< x)"
    4.99    by (simp add: Min_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_min])
   4.100  
   4.101 -lemma Max_gr_iff:
   4.102 +lemma Max_gr_iff [noatp]:
   4.103    "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> x \<^loc>< Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<^loc>< a)"
   4.104    by (simp add: Max_def ACIfSLlin.fold1_strict_below_iff [OF ACIfSLlin_max])
   4.105  
     5.1 --- a/src/HOL/Fun.thy	Wed Aug 15 09:02:11 2007 +0200
     5.2 +++ b/src/HOL/Fun.thy	Wed Aug 15 12:52:56 2007 +0200
     5.3 @@ -268,7 +268,7 @@
     5.4  lemma vimage_id [simp]: "id -` A = A"
     5.5  by (simp add: id_def)
     5.6  
     5.7 -lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
     5.8 +lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
     5.9  by (blast intro: sym)
    5.10  
    5.11  lemma image_vimage_subset: "f ` (f -` A) <= A"
     6.1 --- a/src/HOL/HOL.thy	Wed Aug 15 09:02:11 2007 +0200
     6.2 +++ b/src/HOL/HOL.thy	Wed Aug 15 12:52:56 2007 +0200
     6.3 @@ -935,8 +935,14 @@
     6.4    (Scan.succeed ("claset", "Classical.local_claset_of (ML_Context.the_local_context ())"));
     6.5  
     6.6  structure ResAtpset = NamedThmsFun(val name = "atp" val description = "ATP rules");
     6.7 +
     6.8 +structure ResBlacklist = NamedThmsFun(val name = "noatp" val description = "Theorems blacklisted for ATP");
     6.9  *}
    6.10  
    6.11 +(*ResBlacklist holds theorems blacklisted to sledgehammer. 
    6.12 +  These theorems typically produce clauses that are prolific (match too many equality or
    6.13 +  membership literals) and relate to seldom-used facts. Some duplicate other rules.*)
    6.14 +
    6.15  setup {*
    6.16  let
    6.17    (*prevent substitution on bool*)
    6.18 @@ -948,6 +954,7 @@
    6.19    #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    6.20    #> Classical.setup
    6.21    #> ResAtpset.setup
    6.22 +  #> ResBlacklist.setup
    6.23  end
    6.24  *}
    6.25  
    6.26 @@ -1136,6 +1143,8 @@
    6.27  lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
    6.28  lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))" by blast
    6.29  
    6.30 +declare All_def [noatp]
    6.31 +
    6.32  lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
    6.33  lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
    6.34  
    6.35 @@ -1181,7 +1190,7 @@
    6.36  lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    6.37  by (simplesubst split_if, blast)
    6.38  
    6.39 -lemmas if_splits = split_if split_if_asm
    6.40 +lemmas if_splits [noatp] = split_if split_if_asm
    6.41  
    6.42  lemma if_cancel: "(if c then x else x) = x"
    6.43  by (simplesubst split_if, blast)
     7.1 --- a/src/HOL/IntDef.thy	Wed Aug 15 09:02:11 2007 +0200
     7.2 +++ b/src/HOL/IntDef.thy	Wed Aug 15 12:52:56 2007 +0200
     7.3 @@ -71,7 +71,7 @@
     7.4  
     7.5  text{*Reduces equality on abstractions to equality on representatives:
     7.6    @{prop "\<lbrakk>x \<in> Integ; y \<in> Integ\<rbrakk> \<Longrightarrow> (Abs_Integ x = Abs_Integ y) = (x=y)"} *}
     7.7 -declare Abs_Integ_inject [simp]  Abs_Integ_inverse [simp]
     7.8 +declare Abs_Integ_inject [simp,noatp]  Abs_Integ_inverse [simp,noatp]
     7.9  
    7.10  text{*Case analysis on the representation of an integer as an equivalence
    7.11        class of pairs of naturals.*}
    7.12 @@ -371,7 +371,7 @@
    7.13        It is proved here because attribute @{text arith_split} is not available
    7.14        in theory @{text Ring_and_Field}.
    7.15        But is it really better than just rewriting with @{text abs_if}?*}
    7.16 -lemma abs_split [arith_split]:
    7.17 +lemma abs_split [arith_split,noatp]:
    7.18       "P(abs(a::'a::ordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
    7.19  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    7.20  
     8.1 --- a/src/HOL/IntDiv.thy	Wed Aug 15 09:02:11 2007 +0200
     8.2 +++ b/src/HOL/IntDiv.thy	Wed Aug 15 12:52:56 2007 +0200
     8.3 @@ -1082,7 +1082,7 @@
     8.4  lemma zdvd_0_right [iff]: "(m::int) dvd 0"
     8.5    by (simp add: dvd_def)
     8.6  
     8.7 -lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"
     8.8 +lemma zdvd_0_left [iff,noatp]: "(0 dvd (m::int)) = (m = 0)"
     8.9    by (simp add: dvd_def)
    8.10  
    8.11  lemma zdvd_1_left [iff]: "1 dvd (m::int)"
     9.1 --- a/src/HOL/List.thy	Wed Aug 15 09:02:11 2007 +0200
     9.2 +++ b/src/HOL/List.thy	Wed Aug 15 12:52:56 2007 +0200
     9.3 @@ -436,7 +436,7 @@
     9.4  lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
     9.5  by (induct xs) auto
     9.6  
     9.7 -lemma append_eq_append_conv [simp]:
     9.8 +lemma append_eq_append_conv [simp,noatp]:
     9.9   "!!ys. length xs = length ys \<or> length us = length vs
    9.10   ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
    9.11  apply (induct xs)
    9.12 @@ -469,7 +469,7 @@
    9.13  lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
    9.14  using append_same_eq [of "[]"] by auto
    9.15  
    9.16 -lemma hd_Cons_tl [simp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    9.17 +lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
    9.18  by (induct xs) auto
    9.19  
    9.20  lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
    9.21 @@ -2391,10 +2391,10 @@
    9.22    for A :: "'a set"
    9.23  where
    9.24      Nil [intro!]: "[]: lists A"
    9.25 -  | Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A"
    9.26 -
    9.27 -inductive_cases listsE [elim!]: "x#l : lists A"
    9.28 -inductive_cases listspE [elim!]: "listsp A (x # l)"
    9.29 +  | Cons [intro!,noatp]: "[| a: A;l: lists A|] ==> a#l : lists A"
    9.30 +
    9.31 +inductive_cases listsE [elim!,noatp]: "x#l : lists A"
    9.32 +inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
    9.33  
    9.34  lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
    9.35    by (clarify, erule listsp.induct, blast+)
    9.36 @@ -2429,15 +2429,15 @@
    9.37  
    9.38  lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
    9.39  
    9.40 -lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    9.41 +lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
    9.42  by (rule in_listsp_conv_set [THEN iffD1])
    9.43  
    9.44 -lemmas in_listsD [dest!] = in_listspD [to_set]
    9.45 -
    9.46 -lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    9.47 +lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
    9.48 +
    9.49 +lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
    9.50  by (rule in_listsp_conv_set [THEN iffD2])
    9.51  
    9.52 -lemmas in_listsI [intro!] = in_listspI [to_set]
    9.53 +lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
    9.54  
    9.55  lemma lists_UNIV [simp]: "lists UNIV = UNIV"
    9.56  by auto
    10.1 --- a/src/HOL/Nat.thy	Wed Aug 15 09:02:11 2007 +0200
    10.2 +++ b/src/HOL/Nat.thy	Wed Aug 15 12:52:56 2007 +0200
    10.3 @@ -241,7 +241,7 @@
    10.4  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
    10.5    by (blast elim!: less_SucE intro: less_trans)
    10.6  
    10.7 -lemma less_one [iff]: "(n < (1::nat)) = (n = 0)"
    10.8 +lemma less_one [iff,noatp]: "(n < (1::nat)) = (n = 0)"
    10.9    by (simp add: less_Suc_eq)
   10.10  
   10.11  lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
   10.12 @@ -516,7 +516,7 @@
   10.13  lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   10.14    by (fast intro: not0_implies_Suc)
   10.15  
   10.16 -lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   10.17 +lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   10.18    apply (rule iffI)
   10.19    apply (rule ccontr)
   10.20    apply simp_all
   10.21 @@ -1012,7 +1012,7 @@
   10.22     apply auto
   10.23    done
   10.24  
   10.25 -lemma one_eq_mult_iff [simp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
   10.26 +lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
   10.27    apply (rule trans)
   10.28    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   10.29    done
   10.30 @@ -1332,7 +1332,7 @@
   10.31  text{*Special cases where either operand is zero*}
   10.32  lemma of_nat_0_le_iff [simp]: "(0::'a::ordered_semidom) \<le> of_nat n"
   10.33    by (rule of_nat_le_iff [of 0, simplified])
   10.34 -lemma of_nat_le_0_iff [simp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
   10.35 +lemma of_nat_le_0_iff [simp,noatp]: "(of_nat m \<le> (0::'a::ordered_semidom)) = (m = 0)"
   10.36    by (rule of_nat_le_iff [of _ 0, simplified])
   10.37  
   10.38  text{*Class for unital semirings with characteristic zero.
   10.39 @@ -1347,9 +1347,9 @@
   10.40  by intro_classes (simp add: order_eq_iff)
   10.41  
   10.42  text{*Special cases where either operand is zero*}
   10.43 -lemma of_nat_0_eq_iff [simp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
   10.44 +lemma of_nat_0_eq_iff [simp,noatp]: "((0::'a::semiring_char_0) = of_nat n) = (0 = n)"
   10.45    by (rule of_nat_eq_iff [of 0, simplified])
   10.46 -lemma of_nat_eq_0_iff [simp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   10.47 +lemma of_nat_eq_0_iff [simp,noatp]: "(of_nat m = (0::'a::semiring_char_0)) = (m = 0)"
   10.48    by (rule of_nat_eq_iff [of _ 0, simplified])
   10.49  
   10.50  lemma inj_of_nat: "inj (of_nat :: nat \<Rightarrow> 'a::semiring_char_0)"
    11.1 --- a/src/HOL/OrderedGroup.thy	Wed Aug 15 09:02:11 2007 +0200
    11.2 +++ b/src/HOL/OrderedGroup.thy	Wed Aug 15 12:52:56 2007 +0200
    11.3 @@ -711,16 +711,16 @@
    11.4  lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def)
    11.5  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
    11.6  
    11.7 -lemma pprt_eq_id[simp]: "0 <= x \<Longrightarrow> pprt x = x"
    11.8 +lemma pprt_eq_id[simp,noatp]: "0 <= x \<Longrightarrow> pprt x = x"
    11.9    by (simp add: pprt_def le_iff_sup sup_aci)
   11.10  
   11.11 -lemma nprt_eq_id[simp]: "x <= 0 \<Longrightarrow> nprt x = x"
   11.12 +lemma nprt_eq_id[simp,noatp]: "x <= 0 \<Longrightarrow> nprt x = x"
   11.13    by (simp add: nprt_def le_iff_inf inf_aci)
   11.14  
   11.15 -lemma pprt_eq_0[simp]: "x <= 0 \<Longrightarrow> pprt x = 0"
   11.16 +lemma pprt_eq_0[simp,noatp]: "x <= 0 \<Longrightarrow> pprt x = 0"
   11.17    by (simp add: pprt_def le_iff_sup sup_aci)
   11.18  
   11.19 -lemma nprt_eq_0[simp]: "0 <= x \<Longrightarrow> nprt x = 0"
   11.20 +lemma nprt_eq_0[simp,noatp]: "0 <= x \<Longrightarrow> nprt x = 0"
   11.21    by (simp add: nprt_def le_iff_inf inf_aci)
   11.22  
   11.23  lemma sup_0_imp_0: "sup a (-a) = 0 \<Longrightarrow> a = (0::'a::lordered_ab_group)"
   11.24 @@ -745,10 +745,10 @@
   11.25  apply (erule sup_0_imp_0)
   11.26  done
   11.27  
   11.28 -lemma inf_0_eq_0[simp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   11.29 +lemma inf_0_eq_0[simp,noatp]: "(inf a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   11.30  by (auto, erule inf_0_imp_0)
   11.31  
   11.32 -lemma sup_0_eq_0[simp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   11.33 +lemma sup_0_eq_0[simp,noatp]: "(sup a (-a) = 0) = (a = (0::'a::lordered_ab_group))"
   11.34  by (auto, erule sup_0_imp_0)
   11.35  
   11.36  lemma zero_le_double_add_iff_zero_le_single_add[simp]: "(0 \<le> a + a) = (0 \<le> (a::'a::lordered_ab_group))"
   11.37 @@ -798,6 +798,8 @@
   11.38    thus ?thesis by simp
   11.39  qed
   11.40  
   11.41 +declare abs_0_eq [noatp] (*essentially the same as the other one*)
   11.42 +
   11.43  lemma neg_inf_eq_sup[simp]: "- inf a (b::_::lordered_ab_group) = sup (-a) (-b)"
   11.44  by (simp add: inf_eq_neg_sup)
   11.45  
   11.46 @@ -883,10 +885,10 @@
   11.47  lemma zero_le_iff_nprt_id: "(a \<le> 0) = (nprt a = a)"
   11.48  by (simp add: le_iff_inf nprt_def inf_commute)
   11.49  
   11.50 -lemma pprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
   11.51 +lemma pprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> pprt a <= pprt b"
   11.52    by (simp add: le_iff_sup pprt_def sup_aci)
   11.53  
   11.54 -lemma nprt_mono[simp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   11.55 +lemma nprt_mono[simp,noatp]: "(a::_::lordered_ab_group) <= b \<Longrightarrow> nprt a <= nprt b"
   11.56    by (simp add: le_iff_inf nprt_def inf_aci)
   11.57  
   11.58  lemma pprt_neg: "pprt (-x) = - nprt x"
   11.59 @@ -1063,7 +1065,7 @@
   11.60  lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric]
   11.61  lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric]
   11.62  declare diff_less_0_iff_less [simp]
   11.63 -declare diff_eq_0_iff_eq [simp]
   11.64 +declare diff_eq_0_iff_eq [simp,noatp]
   11.65  declare diff_le_0_iff_le [simp]
   11.66  
   11.67  ML {*
    12.1 --- a/src/HOL/Orderings.thy	Wed Aug 15 09:02:11 2007 +0200
    12.2 +++ b/src/HOL/Orderings.thy	Wed Aug 15 12:52:56 2007 +0200
    12.3 @@ -225,11 +225,11 @@
    12.4    "max x y \<^loc>< z \<longleftrightarrow> x \<^loc>< z \<and> y \<^loc>< z"
    12.5  unfolding max_def le_less using less_linear by (auto intro: less_trans)
    12.6  
    12.7 -lemma split_min:
    12.8 +lemma split_min [noatp]:
    12.9    "P (min i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P i) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P j)"
   12.10  by (simp add: min_def)
   12.11  
   12.12 -lemma split_max:
   12.13 +lemma split_max [noatp]:
   12.14    "P (max i j) \<longleftrightarrow> (i \<^loc>\<le> j \<longrightarrow> P j) \<and> (\<not> i \<^loc>\<le> j \<longrightarrow> P i)"
   12.15  by (simp add: max_def)
   12.16  
    13.1 --- a/src/HOL/Power.thy	Wed Aug 15 09:02:11 2007 +0200
    13.2 +++ b/src/HOL/Power.thy	Wed Aug 15 12:52:56 2007 +0200
    13.3 @@ -183,7 +183,7 @@
    13.4  apply (auto simp add: power_Suc abs_mult)
    13.5  done
    13.6  
    13.7 -lemma zero_less_power_abs_iff [simp]:
    13.8 +lemma zero_less_power_abs_iff [simp,noatp]:
    13.9       "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
   13.10  proof (induct "n")
   13.11    case 0
    14.1 --- a/src/HOL/Product_Type.thy	Wed Aug 15 09:02:11 2007 +0200
    14.2 +++ b/src/HOL/Product_Type.thy	Wed Aug 15 12:52:56 2007 +0200
    14.3 @@ -22,7 +22,7 @@
    14.4    Unity :: unit    ("'(')")
    14.5    "() == Abs_unit True"
    14.6  
    14.7 -lemma unit_eq: "u = ()"
    14.8 +lemma unit_eq [noatp]: "u = ()"
    14.9    by (induct u) (simp add: unit_def Unity_def)
   14.10  
   14.11  text {*
   14.12 @@ -46,7 +46,7 @@
   14.13  lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P"
   14.14    by (rule triv_forall_equality)
   14.15  
   14.16 -lemma unit_induct [induct type: unit]: "P () ==> P x"
   14.17 +lemma unit_induct [noatp,induct type: unit]: "P () ==> P x"
   14.18    by simp
   14.19  
   14.20  text {*
   14.21 @@ -55,7 +55,7 @@
   14.22    f} rather than by @{term [source] "%u. f ()"}.
   14.23  *}
   14.24  
   14.25 -lemma unit_abs_eta_conv [simp]: "(%u::unit. f ()) = f"
   14.26 +lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   14.27    by (rule ext) simp
   14.28  
   14.29  
   14.30 @@ -443,7 +443,7 @@
   14.31  lemma split_beta: "(%(x, y). P x y) z = P (fst z) (snd z)"
   14.32    by (subst surjective_pairing, rule split_conv)
   14.33  
   14.34 -lemma split_split: "R (split c p) = (ALL x y. p = (x, y) --> R (c x y))"
   14.35 +lemma split_split [noatp]: "R(split c p) = (ALL x y. p = (x, y) --> R(c x y))"
   14.36    -- {* For use with @{text split} and the Simplifier. *}
   14.37    by (insert surj_pair [of p], clarify, simp)
   14.38  
   14.39 @@ -454,7 +454,7 @@
   14.40    current goal contains one of those constants.
   14.41  *}
   14.42  
   14.43 -lemma split_split_asm: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   14.44 +lemma split_split_asm [noatp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))"
   14.45  by (subst split_split, simp)
   14.46  
   14.47  
   14.48 @@ -525,10 +525,10 @@
   14.49  change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac));
   14.50  *}
   14.51  
   14.52 -lemma split_eta_SetCompr [simp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   14.53 +lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   14.54    by (rule ext) fast
   14.55  
   14.56 -lemma split_eta_SetCompr2 [simp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   14.57 +lemma split_eta_SetCompr2 [simp,noatp]: "(%u. EX x y. u = (x, y) & P x y) = split P"
   14.58    by (rule ext) fast
   14.59  
   14.60  lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)"
   14.61 @@ -696,11 +696,11 @@
   14.62    -- {* Suggested by Pierre Chartier *}
   14.63    by blast
   14.64  
   14.65 -lemma split_paired_Ball_Sigma [simp]:
   14.66 +lemma split_paired_Ball_Sigma [simp,noatp]:
   14.67      "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   14.68    by blast
   14.69  
   14.70 -lemma split_paired_Bex_Sigma [simp]:
   14.71 +lemma split_paired_Bex_Sigma [simp,noatp]:
   14.72      "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   14.73    by blast
   14.74  
    15.1 --- a/src/HOL/Relation.thy	Wed Aug 15 09:02:11 2007 +0200
    15.2 +++ b/src/HOL/Relation.thy	Wed Aug 15 12:52:56 2007 +0200
    15.3 @@ -112,7 +112,7 @@
    15.4  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    15.5    by (simp add: diag_def)
    15.6  
    15.7 -lemma diagI [intro!]: "a : A ==> (a, a) : diag A"
    15.8 +lemma diagI [intro!,noatp]: "a : A ==> (a, a) : diag A"
    15.9    by (rule diag_eqI) (rule refl)
   15.10  
   15.11  lemma diagE [elim!]:
   15.12 @@ -325,6 +325,8 @@
   15.13  
   15.14  subsection {* Domain *}
   15.15  
   15.16 +declare Domain_def [noatp]
   15.17 +
   15.18  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   15.19    by (unfold Domain_def) blast
   15.20  
   15.21 @@ -411,6 +413,8 @@
   15.22  
   15.23  subsection {* Image of a set under a relation *}
   15.24  
   15.25 +declare Image_def [noatp]
   15.26 +
   15.27  lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   15.28    by (simp add: Image_def)
   15.29  
   15.30 @@ -420,7 +424,7 @@
   15.31  lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   15.32    by (rule Image_iff [THEN trans]) simp
   15.33  
   15.34 -lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
   15.35 +lemma ImageI [intro,noatp]: "(a, b) : r ==> a : A ==> b : r``A"
   15.36    by (unfold Image_def) blast
   15.37  
   15.38  lemma ImageE [elim!]:
    16.1 --- a/src/HOL/Ring_and_Field.thy	Wed Aug 15 09:02:11 2007 +0200
    16.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Aug 15 12:52:56 2007 +0200
    16.3 @@ -660,7 +660,7 @@
    16.4  qed  
    16.5  
    16.6  text{*Cancellation of equalities with a common factor*}
    16.7 -lemma mult_cancel_right [simp]:
    16.8 +lemma mult_cancel_right [simp,noatp]:
    16.9    fixes a b c :: "'a::ring_no_zero_divisors"
   16.10    shows "(a * c = b * c) = (c = 0 \<or> a = b)"
   16.11  proof -
   16.12 @@ -670,7 +670,7 @@
   16.13      by (simp add: disj_commute)
   16.14  qed
   16.15  
   16.16 -lemma mult_cancel_left [simp]:
   16.17 +lemma mult_cancel_left [simp,noatp]:
   16.18    fixes a b c :: "'a::ring_no_zero_divisors"
   16.19    shows "(c * a = c * b) = (c = 0 \<or> a = b)"
   16.20  proof -
   16.21 @@ -1029,11 +1029,11 @@
   16.22  
   16.23  lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
   16.24  
   16.25 -lemma divide_divide_eq_right [simp]:
   16.26 +lemma divide_divide_eq_right [simp,noatp]:
   16.27    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
   16.28  by (simp add: divide_inverse mult_ac)
   16.29  
   16.30 -lemma divide_divide_eq_left [simp]:
   16.31 +lemma divide_divide_eq_left [simp,noatp]:
   16.32    "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
   16.33  by (simp add: divide_inverse mult_assoc)
   16.34  
   16.35 @@ -1309,7 +1309,7 @@
   16.36  done
   16.37  
   16.38  text{*Both premises are essential. Consider -1 and 1.*}
   16.39 -lemma inverse_less_iff_less [simp]:
   16.40 +lemma inverse_less_iff_less [simp,noatp]:
   16.41    "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   16.42  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
   16.43  
   16.44 @@ -1317,7 +1317,7 @@
   16.45    "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   16.46  by (force simp add: order_le_less less_imp_inverse_less)
   16.47  
   16.48 -lemma inverse_le_iff_le [simp]:
   16.49 +lemma inverse_le_iff_le [simp,noatp]:
   16.50   "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   16.51  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
   16.52  
   16.53 @@ -1351,7 +1351,7 @@
   16.54  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
   16.55  done
   16.56  
   16.57 -lemma inverse_less_iff_less_neg [simp]:
   16.58 +lemma inverse_less_iff_less_neg [simp,noatp]:
   16.59    "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
   16.60  apply (insert inverse_less_iff_less [of "-b" "-a"])
   16.61  apply (simp del: inverse_less_iff_less 
   16.62 @@ -1362,7 +1362,7 @@
   16.63    "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
   16.64  by (force simp add: order_le_less less_imp_inverse_less_neg)
   16.65  
   16.66 -lemma inverse_le_iff_le_neg [simp]:
   16.67 +lemma inverse_le_iff_le_neg [simp,noatp]:
   16.68   "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
   16.69  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
   16.70  
   16.71 @@ -1585,7 +1585,7 @@
   16.72        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
   16.73  by (simp add: divide_inverse mult_le_0_iff)
   16.74  
   16.75 -lemma divide_eq_0_iff [simp]:
   16.76 +lemma divide_eq_0_iff [simp,noatp]:
   16.77       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
   16.78  by (simp add: divide_inverse)
   16.79  
   16.80 @@ -1625,13 +1625,13 @@
   16.81  
   16.82  subsection{*Cancellation Laws for Division*}
   16.83  
   16.84 -lemma divide_cancel_right [simp]:
   16.85 +lemma divide_cancel_right [simp,noatp]:
   16.86       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
   16.87  apply (cases "c=0", simp)
   16.88  apply (simp add: divide_inverse)
   16.89  done
   16.90  
   16.91 -lemma divide_cancel_left [simp]:
   16.92 +lemma divide_cancel_left [simp,noatp]:
   16.93       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
   16.94  apply (cases "c=0", simp)
   16.95  apply (simp add: divide_inverse)
   16.96 @@ -1641,23 +1641,23 @@
   16.97  subsection {* Division and the Number One *}
   16.98  
   16.99  text{*Simplify expressions equated with 1*}
  16.100 -lemma divide_eq_1_iff [simp]:
  16.101 +lemma divide_eq_1_iff [simp,noatp]:
  16.102       "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  16.103  apply (cases "b=0", simp)
  16.104  apply (simp add: right_inverse_eq)
  16.105  done
  16.106  
  16.107 -lemma one_eq_divide_iff [simp]:
  16.108 +lemma one_eq_divide_iff [simp,noatp]:
  16.109       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
  16.110  by (simp add: eq_commute [of 1])
  16.111  
  16.112 -lemma zero_eq_1_divide_iff [simp]:
  16.113 +lemma zero_eq_1_divide_iff [simp,noatp]:
  16.114       "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
  16.115  apply (cases "a=0", simp)
  16.116  apply (auto simp add: nonzero_eq_divide_eq)
  16.117  done
  16.118  
  16.119 -lemma one_divide_eq_0_iff [simp]:
  16.120 +lemma one_divide_eq_0_iff [simp,noatp]:
  16.121       "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
  16.122  apply (cases "a=0", simp)
  16.123  apply (insert zero_neq_one [THEN not_sym])
  16.124 @@ -1671,9 +1671,9 @@
  16.125  lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
  16.126  
  16.127  declare zero_less_divide_1_iff [simp]
  16.128 -declare divide_less_0_1_iff [simp]
  16.129 +declare divide_less_0_1_iff [simp,noatp]
  16.130  declare zero_le_divide_1_iff [simp]
  16.131 -declare divide_le_0_1_iff [simp]
  16.132 +declare divide_le_0_1_iff [simp,noatp]
  16.133  
  16.134  
  16.135  subsection {* Ordering Rules for Division *}
  16.136 @@ -1722,22 +1722,22 @@
  16.137  
  16.138  text{*Simplify quotients that are compared with the value 1.*}
  16.139  
  16.140 -lemma le_divide_eq_1:
  16.141 +lemma le_divide_eq_1 [noatp]:
  16.142    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.143    shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
  16.144  by (auto simp add: le_divide_eq)
  16.145  
  16.146 -lemma divide_le_eq_1:
  16.147 +lemma divide_le_eq_1 [noatp]:
  16.148    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.149    shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
  16.150  by (auto simp add: divide_le_eq)
  16.151  
  16.152 -lemma less_divide_eq_1:
  16.153 +lemma less_divide_eq_1 [noatp]:
  16.154    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.155    shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
  16.156  by (auto simp add: less_divide_eq)
  16.157  
  16.158 -lemma divide_less_eq_1:
  16.159 +lemma divide_less_eq_1 [noatp]:
  16.160    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.161    shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
  16.162  by (auto simp add: divide_less_eq)
  16.163 @@ -1745,52 +1745,52 @@
  16.164  
  16.165  subsection{*Conditional Simplification Rules: No Case Splits*}
  16.166  
  16.167 -lemma le_divide_eq_1_pos [simp]:
  16.168 +lemma le_divide_eq_1_pos [simp,noatp]:
  16.169    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.170    shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
  16.171  by (auto simp add: le_divide_eq)
  16.172  
  16.173 -lemma le_divide_eq_1_neg [simp]:
  16.174 +lemma le_divide_eq_1_neg [simp,noatp]:
  16.175    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.176    shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
  16.177  by (auto simp add: le_divide_eq)
  16.178  
  16.179 -lemma divide_le_eq_1_pos [simp]:
  16.180 +lemma divide_le_eq_1_pos [simp,noatp]:
  16.181    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.182    shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
  16.183  by (auto simp add: divide_le_eq)
  16.184  
  16.185 -lemma divide_le_eq_1_neg [simp]:
  16.186 +lemma divide_le_eq_1_neg [simp,noatp]:
  16.187    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.188    shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
  16.189  by (auto simp add: divide_le_eq)
  16.190  
  16.191 -lemma less_divide_eq_1_pos [simp]:
  16.192 +lemma less_divide_eq_1_pos [simp,noatp]:
  16.193    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.194    shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
  16.195  by (auto simp add: less_divide_eq)
  16.196  
  16.197 -lemma less_divide_eq_1_neg [simp]:
  16.198 +lemma less_divide_eq_1_neg [simp,noatp]:
  16.199    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.200    shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
  16.201  by (auto simp add: less_divide_eq)
  16.202  
  16.203 -lemma divide_less_eq_1_pos [simp]:
  16.204 +lemma divide_less_eq_1_pos [simp,noatp]:
  16.205    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.206    shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
  16.207  by (auto simp add: divide_less_eq)
  16.208  
  16.209 -lemma divide_less_eq_1_neg [simp]:
  16.210 +lemma divide_less_eq_1_neg [simp,noatp]:
  16.211    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.212    shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
  16.213  by (auto simp add: divide_less_eq)
  16.214  
  16.215 -lemma eq_divide_eq_1 [simp]:
  16.216 +lemma eq_divide_eq_1 [simp,noatp]:
  16.217    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.218    shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
  16.219  by (auto simp add: eq_divide_eq)
  16.220  
  16.221 -lemma divide_eq_eq_1 [simp]:
  16.222 +lemma divide_eq_eq_1 [simp,noatp]:
  16.223    fixes a :: "'a :: {ordered_field,division_by_zero}"
  16.224    shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
  16.225  by (auto simp add: divide_eq_eq)
    17.1 --- a/src/HOL/Set.thy	Wed Aug 15 09:02:11 2007 +0200
    17.2 +++ b/src/HOL/Set.thy	Wed Aug 15 12:52:56 2007 +0200
    17.3 @@ -775,11 +775,11 @@
    17.4  
    17.5  subsubsection {* Singletons, using insert *}
    17.6  
    17.7 -lemma singletonI [intro!]: "a : {a}"
    17.8 +lemma singletonI [intro!,noatp]: "a : {a}"
    17.9      -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
   17.10    by (rule insertI1)
   17.11  
   17.12 -lemma singletonD [dest!]: "b : {a} ==> b = a"
   17.13 +lemma singletonD [dest!,noatp]: "b : {a} ==> b = a"
   17.14    by blast
   17.15  
   17.16  lemmas singletonE = singletonD [elim_format]
   17.17 @@ -790,10 +790,12 @@
   17.18  lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
   17.19    by blast
   17.20  
   17.21 -lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   17.22 +lemma singleton_insert_inj_eq [iff,noatp]:
   17.23 +     "({b} = insert a A) = (a = b & A \<subseteq> {b})"
   17.24    by blast
   17.25  
   17.26 -lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   17.27 +lemma singleton_insert_inj_eq' [iff,noatp]:
   17.28 +     "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
   17.29    by blast
   17.30  
   17.31  lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
   17.32 @@ -818,6 +820,8 @@
   17.33    @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
   17.34  *}
   17.35  
   17.36 +declare UNION_def [noatp]
   17.37 +
   17.38  lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
   17.39    by (unfold UNION_def) blast
   17.40  
   17.41 @@ -858,7 +862,7 @@
   17.42  
   17.43  subsubsection {* Union *}
   17.44  
   17.45 -lemma Union_iff [simp]: "(A : Union C) = (EX X:C. A:X)"
   17.46 +lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)"
   17.47    by (unfold Union_def) blast
   17.48  
   17.49  lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C"
   17.50 @@ -872,7 +876,7 @@
   17.51  
   17.52  subsubsection {* Inter *}
   17.53  
   17.54 -lemma Inter_iff [simp]: "(A : Inter C) = (ALL X:C. A:X)"
   17.55 +lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
   17.56    by (unfold Inter_def) blast
   17.57  
   17.58  lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
   17.59 @@ -897,6 +901,8 @@
   17.60    not have the syntactic form of @{term "f x"}.
   17.61  *}
   17.62  
   17.63 +declare image_def [noatp]
   17.64 +
   17.65  lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
   17.66    by (unfold image_def) blast
   17.67  
   17.68 @@ -996,10 +1002,10 @@
   17.69  
   17.70  subsubsection {* The ``proper subset'' relation *}
   17.71  
   17.72 -lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   17.73 +lemma psubsetI [intro!,noatp]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
   17.74    by (unfold psubset_def) blast
   17.75  
   17.76 -lemma psubsetE [elim!]: 
   17.77 +lemma psubsetE [elim!,noatp]: 
   17.78      "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
   17.79    by (unfold psubset_def) blast
   17.80  
   17.81 @@ -1164,10 +1170,10 @@
   17.82  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
   17.83    by blast
   17.84  
   17.85 -lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   17.86 +lemma Collect_ex_eq [noatp]: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
   17.87    by blast
   17.88  
   17.89 -lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   17.90 +lemma Collect_bex_eq [noatp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
   17.91    by blast
   17.92  
   17.93  
   17.94 @@ -1211,12 +1217,12 @@
   17.95  lemma insert_inter_insert[simp]: "insert a A \<inter> insert a B = insert a (A \<inter> B)"
   17.96    by blast
   17.97  
   17.98 -lemma insert_disjoint[simp]:
   17.99 +lemma insert_disjoint [simp,noatp]:
  17.100   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
  17.101   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
  17.102    by auto
  17.103  
  17.104 -lemma disjoint_insert[simp]:
  17.105 +lemma disjoint_insert [simp,noatp]:
  17.106   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
  17.107   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
  17.108    by auto
  17.109 @@ -1245,7 +1251,7 @@
  17.110    by blast
  17.111  
  17.112  
  17.113 -lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
  17.114 +lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
  17.115    -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
  17.116        with its implicit quantifier and conjunction.  Also image enjoys better
  17.117        equational properties than does the RHS. *}
  17.118 @@ -1262,7 +1268,7 @@
  17.119  
  17.120  text {* \medskip @{text range}. *}
  17.121  
  17.122 -lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
  17.123 +lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
  17.124    by auto
  17.125  
  17.126  lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
  17.127 @@ -1322,7 +1328,7 @@
  17.128  lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
  17.129    by blast
  17.130  
  17.131 -lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  17.132 +lemma Int_UNIV [simp,noatp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
  17.133    by blast
  17.134  
  17.135  lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
  17.136 @@ -1479,10 +1485,10 @@
  17.137  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
  17.138    by blast
  17.139  
  17.140 -lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
  17.141 +lemma Union_empty_conv [simp,noatp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
  17.142    by blast
  17.143  
  17.144 -lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
  17.145 +lemma empty_Union_conv [simp,noatp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
  17.146    by blast
  17.147  
  17.148  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
  17.149 @@ -1506,7 +1512,7 @@
  17.150  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
  17.151    by blast
  17.152  
  17.153 -lemma Inter_UNIV_conv [simp]:
  17.154 +lemma Inter_UNIV_conv [simp,noatp]:
  17.155    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
  17.156    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
  17.157    by blast+
  17.158 @@ -1517,7 +1523,7 @@
  17.159  
  17.160    Basic identities: *}
  17.161  
  17.162 -lemma UN_empty [simp]: "(\<Union>x\<in>{}. B x) = {}"
  17.163 +lemma UN_empty [simp,noatp]: "(\<Union>x\<in>{}. B x) = {}"
  17.164    by blast
  17.165  
  17.166  lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
  17.167 @@ -1657,7 +1663,7 @@
  17.168  lemma Diff_eq: "A - B = A \<inter> (-B)"
  17.169    by blast
  17.170  
  17.171 -lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
  17.172 +lemma Diff_eq_empty_iff [simp,noatp]: "(A - B = {}) = (A \<subseteq> B)"
  17.173    by blast
  17.174  
  17.175  lemma Diff_cancel [simp]: "A - A = {}"
  17.176 @@ -1678,7 +1684,7 @@
  17.177  lemma Diff_UNIV [simp]: "A - UNIV = {}"
  17.178    by blast
  17.179  
  17.180 -lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
  17.181 +lemma Diff_insert0 [simp,noatp]: "x \<notin> A ==> A - insert x B = A - B"
  17.182    by blast
  17.183  
  17.184  lemma Diff_insert: "A - insert a B = A - B - {a}"
  17.185 @@ -1850,7 +1856,7 @@
  17.186    "!!A B f. (INT x:f`A. B x)    = (INT a:A. B (f a))"
  17.187    by auto
  17.188  
  17.189 -lemma ball_simps [simp]:
  17.190 +lemma ball_simps [simp,noatp]:
  17.191    "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
  17.192    "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
  17.193    "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
  17.194 @@ -1865,7 +1871,7 @@
  17.195    "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
  17.196    by auto
  17.197  
  17.198 -lemma bex_simps [simp]:
  17.199 +lemma bex_simps [simp,noatp]:
  17.200    "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
  17.201    "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
  17.202    "!!P. (EX x:{}. P x) = False"
    18.1 --- a/src/HOL/SetInterval.thy	Wed Aug 15 09:02:11 2007 +0200
    18.2 +++ b/src/HOL/SetInterval.thy	Wed Aug 15 12:52:56 2007 +0200
    18.3 @@ -153,19 +153,19 @@
    18.4  
    18.5  subsection {*Two-sided intervals*}
    18.6  
    18.7 -lemma greaterThanLessThan_iff [simp]:
    18.8 +lemma greaterThanLessThan_iff [simp,noatp]:
    18.9    "(i : {l<..<u}) = (l < i & i < u)"
   18.10  by (simp add: greaterThanLessThan_def)
   18.11  
   18.12 -lemma atLeastLessThan_iff [simp]:
   18.13 +lemma atLeastLessThan_iff [simp,noatp]:
   18.14    "(i : {l..<u}) = (l <= i & i < u)"
   18.15  by (simp add: atLeastLessThan_def)
   18.16  
   18.17 -lemma greaterThanAtMost_iff [simp]:
   18.18 +lemma greaterThanAtMost_iff [simp,noatp]:
   18.19    "(i : {l<..u}) = (l < i & i <= u)"
   18.20  by (simp add: greaterThanAtMost_def)
   18.21  
   18.22 -lemma atLeastAtMost_iff [simp]:
   18.23 +lemma atLeastAtMost_iff [simp,noatp]:
   18.24    "(i : {l..u}) = (l <= i & i <= u)"
   18.25  by (simp add: atLeastAtMost_def)
   18.26  
   18.27 @@ -569,7 +569,7 @@
   18.28  
   18.29  subsubsection {* Some Subset Conditions *}
   18.30  
   18.31 -lemma ivl_subset[simp]:
   18.32 +lemma ivl_subset [simp,noatp]:
   18.33   "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
   18.34  apply(auto simp:linorder_not_le)
   18.35  apply(rule ccontr)
    19.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 15 09:02:11 2007 +0200
    19.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 15 12:52:56 2007 +0200
    19.3 @@ -260,152 +260,6 @@
    19.4    or identified with ATPset (which however is too big currently)*)
    19.5  val whitelist = [subsetI];
    19.6  
    19.7 -(*Names of theorems and theorem lists to be blacklisted.
    19.8 -
    19.9 -  These theorems typically produce clauses that are prolific (match too many equality or
   19.10 -  membership literals) and relate to seldom-used facts. Some duplicate other rules.
   19.11 -  FIXME: this blacklist needs to be maintained using theory data and added to using
   19.12 -  an attribute.*)
   19.13 -val blacklist = 
   19.14 -  ["Datatype.prod.size",
   19.15 -   "Divides.dvd_0_left_iff",
   19.16 -   "Finite_Set.card_0_eq",
   19.17 -   "Finite_Set.card_infinite",
   19.18 -   "Finite_Set.Max_ge",
   19.19 -   "Finite_Set.Max_in",
   19.20 -   "Finite_Set.Max_le_iff",
   19.21 -   "Finite_Set.Max_less_iff",
   19.22 -   "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   19.23 -   "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   19.24 -   "Finite_Set.Min_ge_iff",
   19.25 -   "Finite_Set.Min_gr_iff",
   19.26 -   "Finite_Set.Min_in",
   19.27 -   "Finite_Set.Min_le",
   19.28 -   "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   19.29 -   "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   19.30 -   "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   19.31 -   "HOL.split_if_asm",     (*splitting theorem*)
   19.32 -   "HOL.split_if",         (*splitting theorem*)
   19.33 -   "HOL.All_def",          (*far worse than useless!!*)
   19.34 -   "IntDef.abs_split",
   19.35 -   "IntDef.Integ.Abs_Integ_inject",
   19.36 -   "IntDef.Integ.Abs_Integ_inverse",
   19.37 -   "IntDiv.zdvd_0_left",
   19.38 -   "List.append_eq_append_conv",
   19.39 -   "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   19.40 -   "List.in_listsD",
   19.41 -   "List.in_listsI",
   19.42 -   "List.lists.Cons",
   19.43 -   "List.listsE",
   19.44 -   "Nat.less_one", (*not directional? obscure*)
   19.45 -   "Nat.not_gr0",
   19.46 -   "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   19.47 -   "Nat.of_nat_0_eq_iff",
   19.48 -   "Nat.of_nat_eq_0_iff",
   19.49 -   "Nat.of_nat_le_0_iff",
   19.50 -   "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   19.51 -   "NatSimprocs.divide_less_0_iff_number_of",
   19.52 -   "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   19.53 -   "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   19.54 -   "NatSimprocs.le_minus_iff_1", (*not directional*)
   19.55 -   "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   19.56 -   "NatSimprocs.less_minus_iff_1", (*not directional*)
   19.57 -   "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   19.58 -   "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   19.59 -   "NatSimprocs.minus_le_iff_1", (*not directional*)
   19.60 -   "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   19.61 -   "NatSimprocs.minus_less_iff_1", (*not directional*)
   19.62 -   "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   19.63 -   "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   19.64 -   "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   19.65 -   "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   19.66 -   "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   19.67 -   "NatSimprocs.zero_less_divide_iff_number_of",
   19.68 -   "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   19.69 -   "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   19.70 -   "OrderedGroup.sup_0_eq_0",
   19.71 -   "OrderedGroup.inf_0_eq_0",
   19.72 -   "OrderedGroup.pprt_eq_0",   (*obscure*)
   19.73 -   "OrderedGroup.pprt_eq_id",   (*obscure*)
   19.74 -   "OrderedGroup.pprt_mono",   (*obscure*)
   19.75 -   "Orderings.split_max",      (*splitting theorem*)
   19.76 -   "Orderings.split_min",      (*splitting theorem*)
   19.77 -   "Power.zero_less_power_abs_iff",
   19.78 -   "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   19.79 -   "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   19.80 -   "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   19.81 -   "Product_Type.split_split_asm",             (*splitting theorem*)
   19.82 -   "Product_Type.split_split",                 (*splitting theorem*)
   19.83 -   "Product_Type.unit_abs_eta_conv",
   19.84 -   "Product_Type.unit_induct",
   19.85 -   "Relation.diagI",
   19.86 -   "Relation.Domain_def",   (*involves an existential quantifier*)
   19.87 -   "Relation.Image_def",   (*involves an existential quantifier*)
   19.88 -   "Relation.ImageI",
   19.89 -   "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   19.90 -   "Ring_and_Field.divide_cancel_right",
   19.91 -   "Ring_and_Field.divide_divide_eq_left",
   19.92 -   "Ring_and_Field.divide_divide_eq_right",
   19.93 -   "Ring_and_Field.divide_eq_0_iff",
   19.94 -   "Ring_and_Field.divide_eq_1_iff",
   19.95 -   "Ring_and_Field.divide_eq_eq_1",
   19.96 -   "Ring_and_Field.divide_le_0_1_iff",
   19.97 -   "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   19.98 -   "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   19.99 -   "Ring_and_Field.divide_less_0_1_iff",
  19.100 -   "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
  19.101 -   "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
  19.102 -   "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
  19.103 -   "Ring_and_Field.field_mult_cancel_left",
  19.104 -   "Ring_and_Field.field_mult_cancel_right",
  19.105 -   "Ring_and_Field.inverse_le_iff_le_neg",
  19.106 -   "Ring_and_Field.inverse_le_iff_le",
  19.107 -   "Ring_and_Field.inverse_less_iff_less_neg",
  19.108 -   "Ring_and_Field.inverse_less_iff_less",
  19.109 -   "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
  19.110 -   "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
  19.111 -   "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
  19.112 -   "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
  19.113 -   "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
  19.114 -   "Set.ball_simps", "Set.bex_simps",  (*quantifier rewriting: useless*)
  19.115 -   "Set.Collect_bex_eq",   (*involves an existential quantifier*)
  19.116 -   "Set.Collect_ex_eq",   (*involves an existential quantifier*)
  19.117 -   "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
  19.118 -   "Set.Diff_insert0",
  19.119 -   "Set.empty_Union_conv",   (*redundant with paramodulation*)
  19.120 -   "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
  19.121 -   "Set.image_Collect",      (*involves Collect and a boolean variable...*)
  19.122 -   "Set.image_def",          (*involves an existential quantifier*)
  19.123 -   "Set.disjoint_insert", "Set.insert_disjoint",
  19.124 -   "Set.Int_UNIV",  (*redundant with paramodulation*)
  19.125 -   "Set.Inter_UNIV_conv",
  19.126 -   "Set.Inter_iff", (*We already have InterI, InterE*)
  19.127 -   "Set.psubsetE",    (*too prolific and obscure*)
  19.128 -   "Set.psubsetI",
  19.129 -   "Set.singleton_insert_inj_eq'",
  19.130 -   "Set.singleton_insert_inj_eq",
  19.131 -   "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
  19.132 -   "Set.singletonI",
  19.133 -   "Set.Un_empty", (*redundant with paramodulation*)
  19.134 -   "Set.UNION_def",   (*involves an existential quantifier*)
  19.135 -   "Set.Union_empty_conv", (*redundant with paramodulation*)
  19.136 -   "Set.Union_iff",              (*We already have UnionI, UnionE*)
  19.137 -   "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
  19.138 -   "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
  19.139 -   "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
  19.140 -   "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
  19.141 -   "SetInterval.ivl_subset"];  (*excessive case analysis*)
  19.142 -
  19.143 -(*These might be prolific but are probably OK, and min and max are basic.
  19.144 -   "Orderings.max_less_iff_conj",
  19.145 -   "Orderings.min_less_iff_conj",
  19.146 -   "Orderings.min_max.below_inf.below_inf_conv",
  19.147 -   "Orderings.min_max.below_sup.above_sup_conv",
  19.148 -Very prolific and somewhat obscure:
  19.149 -   "Set.InterD",
  19.150 -   "Set.UnionI",
  19.151 -*)
  19.152 -
  19.153  (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
  19.154  
  19.155  (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
  19.156 @@ -473,9 +327,7 @@
  19.157  
  19.158  fun all_valid_thms ctxt =
  19.159    let
  19.160 -    val banned_tab = foldl setinsert Symtab.empty blacklist
  19.161 -    fun blacklisted s = !run_blacklist_filter andalso
  19.162 -                        (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
  19.163 +    fun blacklisted s = !run_blacklist_filter andalso is_package_def s
  19.164  
  19.165      fun extern_valid space (name, ths) =
  19.166        let
  19.167 @@ -514,10 +366,16 @@
  19.168  
  19.169  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
  19.170  
  19.171 -(*The single theorems go BEFORE the multiple ones*)
  19.172 +(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
  19.173  fun name_thm_pairs ctxt =
  19.174    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
  19.175 -  in  foldl add_single_names  (foldl add_multi_names [] mults) singles end;
  19.176 +      val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
  19.177 +      fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
  19.178 +  in
  19.179 +      app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
  19.180 +      filter (not o blacklisted o #2)
  19.181 +        (foldl add_single_names (foldl add_multi_names [] mults) singles)
  19.182 +  end;
  19.183  
  19.184  fun check_named ("",th) = (warning ("No name for theorem " ^ string_of_thm th); false)
  19.185    | check_named (_,th) = true;