--- a/src/HOL/Library/Float.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Library/Float.thy Wed Feb 18 22:46:47 2015 +0100
@@ -316,12 +316,10 @@
case (less n)
{ fix m assume n: "n \<noteq> 0" "n = m * r"
then have "\<bar>m \<bar> < \<bar>n\<bar>"
- by (metis abs_dvd_iff abs_ge_self assms comm_semiring_1_class.normalizing_semiring_rules(7)
- dvd_imp_le_int dvd_refl dvd_triv_right linorder_neq_iff linorder_not_le
- mult_eq_0_iff zdvd_mult_cancel1)
+ using `1 < r` by (simp add: abs_mult)
from less[OF this] n have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" by auto }
then show ?case
- by (metis comm_semiring_1_class.normalizing_semiring_rules(12,7) dvdE power_0)
+ by (metis dvd_def monoid_mult_class.mult.right_neutral mult.commute power_0)
qed
lemma mult_powr_eq_mult_powr_iff_asym:
--- a/src/HOL/Library/RBT_Impl.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Library/RBT_Impl.thy Wed Feb 18 22:46:47 2015 +0100
@@ -1263,8 +1263,7 @@
case False
hence "length (snd (rbtreeify_f n kvs)) =
length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
- by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
- mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
+ by (simp add: mod_eq_0_iff_dvd)
also from "1.prems" `\<not> n \<le> 1` obtain k v kvs'
where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
also have "0 < n div 2" using `\<not> n \<le> 1` by(simp)
@@ -1328,8 +1327,7 @@
case False
hence "length (snd (rbtreeify_g n kvs)) =
length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
- by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
- mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
+ by (simp add: mod_eq_0_iff_dvd)
also from "2.prems" `1 < n` obtain k v kvs'
where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
also have "0 < n div 2" using `1 < n` by(simp)
--- a/src/HOL/Metis_Examples/Big_O.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy Wed Feb 18 22:46:47 2015 +0100
@@ -23,8 +23,8 @@
"(\<exists>c\<Colon>'a\<Colon>linordered_idom.
\<forall>x. abs (h x) \<le> c * abs (f x))
\<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
-by (metis (no_types) abs_ge_zero
- comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
+ by (metis (no_types) abs_ge_zero
+ algebra_simps mult.comm_neutral
mult_nonpos_nonneg not_leE order_trans zero_less_one)
(*** Now various verions with an increasing shrink factor ***)
@@ -131,8 +131,8 @@
lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
apply (auto simp add: bigo_alt_def)
apply (rule_tac x = "ca * c" in exI)
-by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19)
- mult_le_cancel_left_pos order_trans mult_pos_pos)
+apply (metis algebra_simps mult_le_cancel_left_pos order_trans mult_pos_pos)
+done
lemma bigo_refl [intro]: "f : O(f)"
unfolding bigo_def mem_Collect_eq
@@ -232,9 +232,9 @@
apply (rule set_minus_imp_plus)
apply (rule bigo_bounded)
apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
- comm_semiring_1_class.normalizing_semiring_rules(24))
+ algebra_simps)
by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
- comm_semiring_1_class.normalizing_semiring_rules(24))
+ algebra_simps)
lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
apply (unfold bigo_def)
@@ -339,9 +339,7 @@
then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
by auto
also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
- apply (simp add: func_times)
- by (metis (lifting, no_types) a eq_divide_imp ext
- comm_semiring_1_class.normalizing_semiring_rules(7))
+ by (simp add: func_times fun_eq_iff a)
finally show "h : f *o O(g)".
qed
qed
@@ -368,9 +366,8 @@
by (auto simp add: bigo_def fun_Compl_def)
lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
-by (metis (no_types) bigo_elt_subset bigo_minus bigo_mult4 bigo_refl
- comm_semiring_1_class.normalizing_semiring_rules(11) minus_mult_left
- set_plus_mono_b)
+by (metis (no_types, lifting) bigo_minus diff_minus_eq_add minus_add_distrib
+ minus_minus set_minus_imp_plus set_plus_imp_minus)
lemma bigo_minus3: "O(-f) = O(f)"
by (metis bigo_elt_subset bigo_minus bigo_refl equalityI minus_minus)
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Feb 18 22:46:47 2015 +0100
@@ -288,9 +288,8 @@
thus ?thesis
proof (intro bcontfunI)
fix x assume "\<And>x. dist (f x) 0 \<le> y"
- thus "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
- by (metis abs_ge_zero comm_semiring_1_class.normalizing_semiring_rules(7) mult_right_mono
- norm_conv_dist norm_scaleR)
+ then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
+ by (metis norm_cmul_rule_thm norm_conv_dist)
qed (simp add: continuous_intros)
qed
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Feb 18 22:46:47 2015 +0100
@@ -549,7 +549,8 @@
"f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
apply (rule DERIV_imp_deriv)
apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
-apply (metis DERIV_chain' DERIV_cmult_Id comm_semiring_1_class.normalizing_semiring_rules(7))
+apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
+apply (simp add: algebra_simps)
done
subsection{*analyticity on a set*}
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Feb 18 22:46:47 2015 +0100
@@ -191,9 +191,7 @@
apply (subst (asm) continuous_at_right_real_increasing)
using mono_F apply force
apply (drule_tac x = "epsilon / 2" in spec)
- using egt0 apply (auto simp add: field_simps)
- by (metis add_less_cancel_left comm_monoid_add_class.add.right_neutral
- comm_semiring_1_class.normalizing_semiring_rules(24) mult_2 mult_2_right)
+ using egt0 unfolding mult.commute [of 2] by force
then obtain a' where a'lea [arith]: "a' > a" and
a_prop: "F a' - F a < epsilon / 2"
by auto
--- a/src/HOL/Semiring_Normalization.thy Wed Feb 18 22:46:47 2015 +0100
+++ b/src/HOL/Semiring_Normalization.thy Wed Feb 18 22:46:47 2015 +0100
@@ -72,63 +72,69 @@
context comm_semiring_1
begin
-lemma normalizing_semiring_rules:
- "(a * m) + (b * m) = (a + b) * m"
- "(a * m) + m = (a + 1) * m"
- "m + (a * m) = (a + 1) * m"
- "m + m = (1 + 1) * m"
- "0 + a = a"
- "a + 0 = a"
- "a * b = b * a"
- "(a + b) * c = (a * c) + (b * c)"
- "0 * a = 0"
- "a * 0 = 0"
- "1 * a = a"
- "a * 1 = a"
- "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
- "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
- "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
- "(lx * ly) * rx = (lx * rx) * ly"
- "(lx * ly) * rx = lx * (ly * rx)"
- "lx * (rx * ry) = (lx * rx) * ry"
- "lx * (rx * ry) = rx * (lx * ry)"
- "(a + b) + (c + d) = (a + c) + (b + d)"
- "(a + b) + c = a + (b + c)"
- "a + (c + d) = c + (a + d)"
- "(a + b) + c = (a + c) + b"
- "a + c = c + a"
- "a + (c + d) = (a + c) + d"
- "(x ^ p) * (x ^ q) = x ^ (p + q)"
- "x * (x ^ q) = x ^ (Suc q)"
- "(x ^ q) * x = x ^ (Suc q)"
- "x * x = x\<^sup>2"
- "(x * y) ^ q = (x ^ q) * (y ^ q)"
- "(x ^ p) ^ q = x ^ (p * q)"
- "x ^ 0 = 1"
- "x ^ 1 = x"
- "x * (y + z) = (x * y) + (x * z)"
- "x ^ (Suc q) = x * (x ^ q)"
- "x ^ (2*n) = (x ^ n) * (x ^ n)"
- by (simp_all add: algebra_simps power_add power2_eq_square
- power_mult_distrib power_mult del: one_add_one)
-
-declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
- {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
- @{thms normalizing_semiring_rules}), ring = ([], []), field = ([], []), idom = [], ideal = []}\<close>
+declaration \<open>
+let
+ val rules = @{lemma
+ "(a * m) + (b * m) = (a + b) * m"
+ "(a * m) + m = (a + 1) * m"
+ "m + (a * m) = (a + 1) * m"
+ "m + m = (1 + 1) * m"
+ "0 + a = a"
+ "a + 0 = a"
+ "a * b = b * a"
+ "(a + b) * c = (a * c) + (b * c)"
+ "0 * a = 0"
+ "a * 0 = 0"
+ "1 * a = a"
+ "a * 1 = a"
+ "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
+ "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
+ "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
+ "(lx * ly) * rx = (lx * rx) * ly"
+ "(lx * ly) * rx = lx * (ly * rx)"
+ "lx * (rx * ry) = (lx * rx) * ry"
+ "lx * (rx * ry) = rx * (lx * ry)"
+ "(a + b) + (c + d) = (a + c) + (b + d)"
+ "(a + b) + c = a + (b + c)"
+ "a + (c + d) = c + (a + d)"
+ "(a + b) + c = (a + c) + b"
+ "a + c = c + a"
+ "a + (c + d) = (a + c) + d"
+ "(x ^ p) * (x ^ q) = x ^ (p + q)"
+ "x * (x ^ q) = x ^ (Suc q)"
+ "(x ^ q) * x = x ^ (Suc q)"
+ "x * x = x\<^sup>2"
+ "(x * y) ^ q = (x ^ q) * (y ^ q)"
+ "(x ^ p) ^ q = x ^ (p * q)"
+ "x ^ 0 = 1"
+ "x ^ 1 = x"
+ "x * (y + z) = (x * y) + (x * z)"
+ "x ^ (Suc q) = x * (x ^ q)"
+ "x ^ (2*n) = (x ^ n) * (x ^ n)"
+ by (simp_all add: algebra_simps power_add power2_eq_square
+ power_mult_distrib power_mult del: one_add_one)}
+in
+ Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
+ {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
+ rules), ring = ([], []), field = ([], []), idom = [], ideal = []}
+end\<close>
end
context comm_ring_1
begin
-lemma normalizing_ring_rules:
- "- x = (- 1) * x"
- "x - y = x + (- y)"
- by simp_all
-
-declaration \<open>Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
- {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
- ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], @{thms normalizing_ring_rules}), field = ([], []), idom = [], ideal = []}\<close>
+declaration \<open>
+let
+ val rules = @{lemma
+ "- x = (- 1) * x"
+ "x - y = x + (- y)"
+ by simp_all}
+in
+ Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
+ {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
+ ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], rules), field = ([], []), idom = [], ideal = []}
+end\<close>
end
@@ -155,23 +161,15 @@
context field
begin
-lemmas normalizing_field_rules = divide_inverse inverse_eq_divide
-
declaration \<open>Semiring_Normalizer.declare @{thm field_axioms}
{semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms},
ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms},
- field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms normalizing_field_rules}),
+ field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms divide_inverse inverse_eq_divide}),
idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms},
ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close>
end
-hide_fact (open) normalizing_semiring_rules
-
-hide_fact (open) normalizing_ring_rules
-
-hide_fact (open) normalizing_field_rules
-
code_identifier
code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith