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