prefix normalizing replaces class_semiring
authorhaftmann
Fri May 07 09:59:24 2010 +0200 (2010-05-07)
changeset 3672534c36a5cb808
parent 36724 5779d9fbedd0
child 36726 47ba1770da8e
prefix normalizing replaces class_semiring
src/HOL/Metis_Examples/BT.thy
src/HOL/Metis_Examples/BigO.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Probability/Lebesgue.thy
     1.1 --- a/src/HOL/Metis_Examples/BT.thy	Thu May 06 23:37:07 2010 +0200
     1.2 +++ b/src/HOL/Metis_Examples/BT.thy	Fri May 07 09:59:24 2010 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4    case Lf thus ?case by (metis reflect.simps(1))
     1.5  next
     1.6    case (Br a t1 t2) thus ?case
     1.7 -    by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
     1.8 +    by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
     1.9  qed
    1.10  
    1.11  declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
     2.1 --- a/src/HOL/Metis_Examples/BigO.thy	Thu May 06 23:37:07 2010 +0200
     2.2 +++ b/src/HOL/Metis_Examples/BigO.thy	Fri May 07 09:59:24 2010 +0200
     2.3 @@ -41,7 +41,7 @@
     2.4    fix c :: 'a and x :: 'b
     2.5    assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
     2.6    have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
     2.7 -  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
     2.8 +  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
     2.9    have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
    2.10    have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
    2.11      by (metis abs_mult)
    2.12 @@ -70,7 +70,7 @@
    2.13  proof -
    2.14    fix c :: 'a and x :: 'b
    2.15    assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
    2.16 -  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
    2.17 +  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
    2.18    have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
    2.19      by (metis abs_mult)
    2.20    have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
    2.21 @@ -92,7 +92,7 @@
    2.22  proof -
    2.23    fix c :: 'a and x :: 'b
    2.24    assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
    2.25 -  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
    2.26 +  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
    2.27    have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
    2.28    hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
    2.29    hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
    2.30 @@ -111,7 +111,7 @@
    2.31  proof -
    2.32    fix c :: 'a and x :: 'b
    2.33    assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
    2.34 -  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
    2.35 +  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1)
    2.36    hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
    2.37      by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
    2.38    hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
    2.39 @@ -145,12 +145,12 @@
    2.40  declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
    2.41  lemma bigo_refl [intro]: "f : O(f)"
    2.42  apply (auto simp add: bigo_def)
    2.43 -by (metis class_semiring.mul_1 order_refl)
    2.44 +by (metis normalizing.mul_1 order_refl)
    2.45  
    2.46  declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
    2.47  lemma bigo_zero: "0 : O(g)"
    2.48  apply (auto simp add: bigo_def func_zero)
    2.49 -by (metis class_semiring.mul_0 order_refl)
    2.50 +by (metis normalizing.mul_0 order_refl)
    2.51  
    2.52  lemma bigo_zero2: "O(%x.0) = {%x.0}"
    2.53    apply (auto simp add: bigo_def) 
    2.54 @@ -307,7 +307,7 @@
    2.55   apply (auto simp add: diff_minus fun_Compl_def func_plus)
    2.56   prefer 2
    2.57   apply (drule_tac x = x in spec)+
    2.58 - apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
    2.59 + apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
    2.60  proof -
    2.61    fix x :: 'a
    2.62    assume "\<forall>x. lb x \<le> f x"
    2.63 @@ -318,13 +318,13 @@
    2.64  lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
    2.65  apply (unfold bigo_def)
    2.66  apply auto
    2.67 -by (metis class_semiring.mul_1 order_refl)
    2.68 +by (metis normalizing.mul_1 order_refl)
    2.69  
    2.70  declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
    2.71  lemma bigo_abs2: "f =o O(%x. abs(f x))"
    2.72  apply (unfold bigo_def)
    2.73  apply auto
    2.74 -by (metis class_semiring.mul_1 order_refl)
    2.75 +by (metis normalizing.mul_1 order_refl)
    2.76   
    2.77  lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
    2.78  proof -
     3.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu May 06 23:37:07 2010 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri May 07 09:59:24 2010 +0200
     3.3 @@ -1877,7 +1877,7 @@
     3.4        using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
     3.5        unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
     3.6        apply (rule mult_left_le_imp_le[of "1 - u"])
     3.7 -      unfolding class_semiring.mul_a using `u<1` by auto
     3.8 +      unfolding normalizing.mul_a using `u<1` by auto
     3.9      thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
    3.10        using as unfolding scaleR_scaleR by auto qed auto
    3.11    thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
     4.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu May 06 23:37:07 2010 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri May 07 09:59:24 2010 +0200
     4.3 @@ -698,7 +698,7 @@
     4.4      unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
     4.5    then guess x .. note x=this
     4.6    show ?thesis proof(cases "f a = f b")
     4.7 -    case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules)
     4.8 +    case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:normalizing.semiring_rules)
     4.9      also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
    4.10      also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
    4.11      also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
     5.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu May 06 23:37:07 2010 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 07 09:59:24 2010 +0200
     5.3 @@ -2533,7 +2533,7 @@
     5.4            show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
     5.5          qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
     5.6          note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
     5.7 -        note this[unfolded real_scaleR_def real_norm_def class_semiring.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
     5.8 +        note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)]
     5.9          from this[unfolded abs_of_nonneg[OF *]] show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x $ k - c\<bar> \<le> d})) < e"
    5.10            apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
    5.11            apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
    5.12 @@ -4723,7 +4723,7 @@
    5.13    have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
    5.14      \<longrightarrow> norm(ig) < dia + e" 
    5.15    proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
    5.16 -      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
    5.17 +      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
    5.18        apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
    5.19        apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
    5.20    qed note norm=this[rule_format]
     6.1 --- a/src/HOL/Probability/Lebesgue.thy	Thu May 06 23:37:07 2010 +0200
     6.2 +++ b/src/HOL/Probability/Lebesgue.thy	Fri May 07 09:59:24 2010 +0200
     6.3 @@ -938,17 +938,17 @@
     6.4    proof safe
     6.5      fix t assume t: "t \<in> space M"
     6.6      { fix m n :: nat assume "m \<le> n"
     6.7 -      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto
     6.8 +      hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto
     6.9        have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \<le> real (natfloor (f t * 2 ^ n))"
    6.10          apply (subst *)
    6.11 -        apply (subst class_semiring.mul_a)
    6.12 +        apply (subst normalizing.mul_a)
    6.13          apply (subst real_of_nat_le_iff)
    6.14          apply (rule le_mult_natfloor)
    6.15          using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg)
    6.16        hence "real (natfloor (f t * 2^m)) * 2^n \<le> real (natfloor (f t * 2^n)) * 2^m"
    6.17          apply (subst *)
    6.18 -        apply (subst (3) class_semiring.mul_c)
    6.19 -        apply (subst class_semiring.mul_a)
    6.20 +        apply (subst (3) normalizing.mul_c)
    6.21 +        apply (subst normalizing.mul_a)
    6.22          by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) }
    6.23      thus "incseq (\<lambda>n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def
    6.24        by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)