inlined rules to free user-space from technical names
authorhaftmann
Wed Feb 18 22:46:47 2015 +0100 (2015-02-18)
changeset 595544044f53326c9
parent 59553 e87974cd9b86
child 59555 05573e5504a9
inlined rules to free user-space from technical names
src/HOL/Library/Float.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Semiring_Normalization.thy
     1.1 --- a/src/HOL/Library/Float.thy	Wed Feb 18 22:46:47 2015 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Feb 18 22:46:47 2015 +0100
     1.3 @@ -316,12 +316,10 @@
     1.4    case (less n)
     1.5    { fix m assume n: "n \<noteq> 0" "n = m * r"
     1.6      then have "\<bar>m \<bar> < \<bar>n\<bar>"
     1.7 -      by (metis abs_dvd_iff abs_ge_self assms comm_semiring_1_class.normalizing_semiring_rules(7)
     1.8 -                dvd_imp_le_int dvd_refl dvd_triv_right linorder_neq_iff linorder_not_le
     1.9 -                mult_eq_0_iff zdvd_mult_cancel1)
    1.10 +      using `1 < r` by (simp add: abs_mult)
    1.11      from less[OF this] n have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" by auto }
    1.12    then show ?case
    1.13 -    by (metis comm_semiring_1_class.normalizing_semiring_rules(12,7) dvdE power_0)
    1.14 +    by (metis dvd_def monoid_mult_class.mult.right_neutral mult.commute power_0)
    1.15  qed
    1.16  
    1.17  lemma mult_powr_eq_mult_powr_iff_asym:
     2.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 18 22:46:47 2015 +0100
     2.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 18 22:46:47 2015 +0100
     2.3 @@ -1263,8 +1263,7 @@
     2.4        case False
     2.5        hence "length (snd (rbtreeify_f n kvs)) = 
     2.6          length (snd (rbtreeify_f (Suc (2 * (n div 2))) kvs))"
     2.7 -        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7)
     2.8 -             mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
     2.9 +        by (simp add: mod_eq_0_iff_dvd)
    2.10        also from "1.prems" `\<not> n \<le> 1` obtain k v kvs' 
    2.11          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    2.12        also have "0 < n div 2" using `\<not> n \<le> 1` by(simp) 
    2.13 @@ -1328,8 +1327,7 @@
    2.14        case False
    2.15        hence "length (snd (rbtreeify_g n kvs)) = 
    2.16          length (snd (rbtreeify_g (Suc (2 * (n div 2))) kvs))"
    2.17 -        by(metis Suc_eq_plus1_left comm_semiring_1_class.normalizing_semiring_rules(7) 
    2.18 -            mod_2_not_eq_zero_eq_one_nat semiring_div_class.mod_div_equality')
    2.19 +        by (simp add: mod_eq_0_iff_dvd)
    2.20        also from "2.prems" `1 < n` obtain k v kvs'
    2.21          where kvs: "kvs = (k, v) # kvs'" by(cases kvs) auto
    2.22        also have "0 < n div 2" using `1 < n` by(simp)
     3.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:47 2015 +0100
     3.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Wed Feb 18 22:46:47 2015 +0100
     3.3 @@ -23,8 +23,8 @@
     3.4    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
     3.5      \<forall>x. abs (h x) \<le> c * abs (f x))
     3.6      \<longleftrightarrow> (\<exists>c. 0 < c \<and> (\<forall>x. abs(h x) \<le> c * abs (f x)))"
     3.7 -by (metis (no_types) abs_ge_zero
     3.8 -      comm_semiring_1_class.normalizing_semiring_rules(7) mult.comm_neutral
     3.9 +  by (metis (no_types) abs_ge_zero
    3.10 +      algebra_simps mult.comm_neutral
    3.11        mult_nonpos_nonneg not_leE order_trans zero_less_one)
    3.12  
    3.13  (*** Now various verions with an increasing shrink factor ***)
    3.14 @@ -131,8 +131,8 @@
    3.15  lemma bigo_elt_subset [intro]: "f : O(g) \<Longrightarrow> O(f) \<le> O(g)"
    3.16  apply (auto simp add: bigo_alt_def)
    3.17  apply (rule_tac x = "ca * c" in exI)
    3.18 -by (metis comm_semiring_1_class.normalizing_semiring_rules(7,19)
    3.19 -          mult_le_cancel_left_pos order_trans mult_pos_pos)
    3.20 +apply (metis algebra_simps mult_le_cancel_left_pos order_trans mult_pos_pos)
    3.21 +done
    3.22  
    3.23  lemma bigo_refl [intro]: "f : O(f)"
    3.24  unfolding bigo_def mem_Collect_eq
    3.25 @@ -232,9 +232,9 @@
    3.26  apply (rule set_minus_imp_plus)
    3.27  apply (rule bigo_bounded)
    3.28   apply (metis add_le_cancel_left diff_add_cancel diff_self minus_apply
    3.29 -              comm_semiring_1_class.normalizing_semiring_rules(24))
    3.30 +              algebra_simps)
    3.31  by (metis add_le_cancel_left diff_add_cancel func_plus le_fun_def
    3.32 -          comm_semiring_1_class.normalizing_semiring_rules(24))
    3.33 +          algebra_simps)
    3.34  
    3.35  lemma bigo_abs: "(\<lambda>x. abs(f x)) =o O(f)"
    3.36  apply (unfold bigo_def)
    3.37 @@ -339,9 +339,7 @@
    3.38      then have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) : f *o O(g)"
    3.39        by auto
    3.40      also have "f * ((\<lambda>x. (1\<Colon>'b) / f x) * h) = h"
    3.41 -      apply (simp add: func_times)
    3.42 -      by (metis (lifting, no_types) a eq_divide_imp ext
    3.43 -                comm_semiring_1_class.normalizing_semiring_rules(7))
    3.44 +      by (simp add: func_times fun_eq_iff a)
    3.45      finally show "h : f *o O(g)".
    3.46    qed
    3.47  qed
    3.48 @@ -368,9 +366,8 @@
    3.49  by (auto simp add: bigo_def fun_Compl_def)
    3.50  
    3.51  lemma bigo_minus2: "f : g +o O(h) \<Longrightarrow> -f : -g +o O(h)"
    3.52 -by (metis (no_types) bigo_elt_subset bigo_minus bigo_mult4 bigo_refl
    3.53 -          comm_semiring_1_class.normalizing_semiring_rules(11) minus_mult_left
    3.54 -          set_plus_mono_b)
    3.55 +by (metis (no_types, lifting) bigo_minus diff_minus_eq_add minus_add_distrib
    3.56 +    minus_minus set_minus_imp_plus set_plus_imp_minus)
    3.57  
    3.58  lemma bigo_minus3: "O(-f) = O(f)"
    3.59  by (metis bigo_elt_subset bigo_minus bigo_refl equalityI minus_minus)
     4.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Feb 18 22:46:47 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Feb 18 22:46:47 2015 +0100
     4.3 @@ -288,9 +288,8 @@
     4.4    thus ?thesis
     4.5    proof (intro bcontfunI)
     4.6      fix x assume "\<And>x. dist (f x) 0 \<le> y"
     4.7 -    thus "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
     4.8 -      by (metis abs_ge_zero comm_semiring_1_class.normalizing_semiring_rules(7) mult_right_mono
     4.9 -        norm_conv_dist norm_scaleR)
    4.10 +    then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y"
    4.11 +      by (metis norm_cmul_rule_thm norm_conv_dist)
    4.12    qed (simp add: continuous_intros)
    4.13  qed
    4.14  
     5.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Feb 18 22:46:47 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Feb 18 22:46:47 2015 +0100
     5.3 @@ -549,7 +549,8 @@
     5.4    "f complex_differentiable at (c * z) \<Longrightarrow> deriv (\<lambda>w. f (c * w)) z = c * deriv f (c * z)"
     5.5  apply (rule DERIV_imp_deriv)
     5.6  apply (simp add: DERIV_deriv_iff_complex_differentiable [symmetric])
     5.7 -apply (metis DERIV_chain' DERIV_cmult_Id comm_semiring_1_class.normalizing_semiring_rules(7))  
     5.8 +apply (drule DERIV_chain' [of "times c" c z UNIV f "deriv f (c * z)", OF DERIV_cmult_Id])
     5.9 +apply (simp add: algebra_simps)
    5.10  done
    5.11  
    5.12  subsection{*analyticity on a set*}
     6.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 18 22:46:47 2015 +0100
     6.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Feb 18 22:46:47 2015 +0100
     6.3 @@ -191,9 +191,7 @@
     6.4        apply (subst (asm) continuous_at_right_real_increasing)
     6.5        using mono_F apply force
     6.6        apply (drule_tac x = "epsilon / 2" in spec)
     6.7 -      using egt0 apply (auto simp add: field_simps)
     6.8 -      by (metis add_less_cancel_left comm_monoid_add_class.add.right_neutral 
     6.9 -        comm_semiring_1_class.normalizing_semiring_rules(24) mult_2 mult_2_right)
    6.10 +      using egt0 unfolding mult.commute [of 2] by force
    6.11      then obtain a' where a'lea [arith]: "a' > a" and 
    6.12        a_prop: "F a' - F a < epsilon / 2"
    6.13        by auto
     7.1 --- a/src/HOL/Semiring_Normalization.thy	Wed Feb 18 22:46:47 2015 +0100
     7.2 +++ b/src/HOL/Semiring_Normalization.thy	Wed Feb 18 22:46:47 2015 +0100
     7.3 @@ -72,63 +72,69 @@
     7.4  context comm_semiring_1
     7.5  begin
     7.6  
     7.7 -lemma normalizing_semiring_rules:
     7.8 -  "(a * m) + (b * m) = (a + b) * m"
     7.9 -  "(a * m) + m = (a + 1) * m"
    7.10 -  "m + (a * m) = (a + 1) * m"
    7.11 -  "m + m = (1 + 1) * m"
    7.12 -  "0 + a = a"
    7.13 -  "a + 0 = a"
    7.14 -  "a * b = b * a"
    7.15 -  "(a + b) * c = (a * c) + (b * c)"
    7.16 -  "0 * a = 0"
    7.17 -  "a * 0 = 0"
    7.18 -  "1 * a = a"
    7.19 -  "a * 1 = a"
    7.20 -  "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
    7.21 -  "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
    7.22 -  "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
    7.23 -  "(lx * ly) * rx = (lx * rx) * ly"
    7.24 -  "(lx * ly) * rx = lx * (ly * rx)"
    7.25 -  "lx * (rx * ry) = (lx * rx) * ry"
    7.26 -  "lx * (rx * ry) = rx * (lx * ry)"
    7.27 -  "(a + b) + (c + d) = (a + c) + (b + d)"
    7.28 -  "(a + b) + c = a + (b + c)"
    7.29 -  "a + (c + d) = c + (a + d)"
    7.30 -  "(a + b) + c = (a + c) + b"
    7.31 -  "a + c = c + a"
    7.32 -  "a + (c + d) = (a + c) + d"
    7.33 -  "(x ^ p) * (x ^ q) = x ^ (p + q)"
    7.34 -  "x * (x ^ q) = x ^ (Suc q)"
    7.35 -  "(x ^ q) * x = x ^ (Suc q)"
    7.36 -  "x * x = x\<^sup>2"
    7.37 -  "(x * y) ^ q = (x ^ q) * (y ^ q)"
    7.38 -  "(x ^ p) ^ q = x ^ (p * q)"
    7.39 -  "x ^ 0 = 1"
    7.40 -  "x ^ 1 = x"
    7.41 -  "x * (y + z) = (x * y) + (x * z)"
    7.42 -  "x ^ (Suc q) = x * (x ^ q)"
    7.43 -  "x ^ (2*n) = (x ^ n) * (x ^ n)"
    7.44 -  by (simp_all add: algebra_simps power_add power2_eq_square
    7.45 -    power_mult_distrib power_mult del: one_add_one)
    7.46 -
    7.47 -declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
    7.48 -  {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
    7.49 -    @{thms normalizing_semiring_rules}), ring = ([], []), field = ([], []), idom = [], ideal = []}\<close>
    7.50 +declaration \<open>
    7.51 +let
    7.52 +  val rules = @{lemma
    7.53 +    "(a * m) + (b * m) = (a + b) * m"
    7.54 +    "(a * m) + m = (a + 1) * m"
    7.55 +    "m + (a * m) = (a + 1) * m"
    7.56 +    "m + m = (1 + 1) * m"
    7.57 +    "0 + a = a"
    7.58 +    "a + 0 = a"
    7.59 +    "a * b = b * a"
    7.60 +    "(a + b) * c = (a * c) + (b * c)"
    7.61 +    "0 * a = 0"
    7.62 +    "a * 0 = 0"
    7.63 +    "1 * a = a"
    7.64 +    "a * 1 = a"
    7.65 +    "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
    7.66 +    "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
    7.67 +    "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
    7.68 +    "(lx * ly) * rx = (lx * rx) * ly"
    7.69 +    "(lx * ly) * rx = lx * (ly * rx)"
    7.70 +    "lx * (rx * ry) = (lx * rx) * ry"
    7.71 +    "lx * (rx * ry) = rx * (lx * ry)"
    7.72 +    "(a + b) + (c + d) = (a + c) + (b + d)"
    7.73 +    "(a + b) + c = a + (b + c)"
    7.74 +    "a + (c + d) = c + (a + d)"
    7.75 +    "(a + b) + c = (a + c) + b"
    7.76 +    "a + c = c + a"
    7.77 +    "a + (c + d) = (a + c) + d"
    7.78 +    "(x ^ p) * (x ^ q) = x ^ (p + q)"
    7.79 +    "x * (x ^ q) = x ^ (Suc q)"
    7.80 +    "(x ^ q) * x = x ^ (Suc q)"
    7.81 +    "x * x = x\<^sup>2"
    7.82 +    "(x * y) ^ q = (x ^ q) * (y ^ q)"
    7.83 +    "(x ^ p) ^ q = x ^ (p * q)"
    7.84 +    "x ^ 0 = 1"
    7.85 +    "x ^ 1 = x"
    7.86 +    "x * (y + z) = (x * y) + (x * z)"
    7.87 +    "x ^ (Suc q) = x * (x ^ q)"
    7.88 +    "x ^ (2*n) = (x ^ n) * (x ^ n)"
    7.89 +    by (simp_all add: algebra_simps power_add power2_eq_square
    7.90 +      power_mult_distrib power_mult del: one_add_one)}
    7.91 +in
    7.92 +  Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
    7.93 +    {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
    7.94 +      rules), ring = ([], []), field = ([], []), idom = [], ideal = []}
    7.95 +end\<close>
    7.96  
    7.97  end
    7.98  
    7.99  context comm_ring_1
   7.100  begin
   7.101  
   7.102 -lemma normalizing_ring_rules:
   7.103 -  "- x = (- 1) * x"
   7.104 -  "x - y = x + (- y)"
   7.105 -  by simp_all
   7.106 -
   7.107 -declaration \<open>Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
   7.108 -  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
   7.109 -    ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], @{thms normalizing_ring_rules}), field = ([], []), idom = [], ideal = []}\<close>
   7.110 +declaration \<open>
   7.111 +let
   7.112 +  val rules = @{lemma
   7.113 +    "- x = (- 1) * x"
   7.114 +    "x - y = x + (- y)"
   7.115 +    by simp_all}
   7.116 +in
   7.117 +  Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
   7.118 +    {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
   7.119 +      ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], rules), field = ([], []), idom = [], ideal = []}
   7.120 +end\<close>
   7.121  
   7.122  end
   7.123  
   7.124 @@ -155,23 +161,15 @@
   7.125  context field
   7.126  begin
   7.127  
   7.128 -lemmas normalizing_field_rules = divide_inverse inverse_eq_divide
   7.129 -
   7.130  declaration \<open>Semiring_Normalizer.declare @{thm field_axioms}
   7.131    {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms},
   7.132      ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms},
   7.133 -    field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms normalizing_field_rules}),
   7.134 +    field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms divide_inverse inverse_eq_divide}),
   7.135      idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms},
   7.136      ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close>
   7.137  
   7.138  end
   7.139  
   7.140 -hide_fact (open) normalizing_semiring_rules
   7.141 -
   7.142 -hide_fact (open) normalizing_ring_rules
   7.143 -
   7.144 -hide_fact (open) normalizing_field_rules
   7.145 -
   7.146  code_identifier
   7.147    code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   7.148