--- 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 "="}) *}
--- 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"
--- 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
--- 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])
--- 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"
--- 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)
--- 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)
--- 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)"
--- 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
--- 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)"
--- 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 {*
--- 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)
--- 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
--- 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
--- 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!]:
--- 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)
--- 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"
--- 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)
--- 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;