# HG changeset patch
# User haftmann
# Date 1424296007 -3600
# Node ID 4044f53326c9ee76650e7d2dfea90dc9658b4e20
# Parent  e87974cd9b868f987c30f605f4b5456e3988f97a
inlined rules to free user-space from technical names

diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Library/Float.thy
--- 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:
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Library/RBT_Impl.thy
--- 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)
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Metis_Examples/Big_O.thy
--- 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)
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
--- 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
 
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- 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*}
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Probability/Lebesgue_Measure.thy
--- 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
diff -r e87974cd9b86 -r 4044f53326c9 src/HOL/Semiring_Normalization.thy
--- 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