src/HOL/Multivariate_Analysis/Integration.thy
changeset 36725 34c36a5cb808
parent 36587 534418d8d494
child 36778 739a9379e29b
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu May 06 23:37:07 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 07 09:59:24 2010 +0200
     1.3 @@ -2533,7 +2533,7 @@
     1.4            show "content x \<ge> 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le)
     1.5          qed have **:"norm (1::real) \<le> 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit]
     1.6          note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]]
     1.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)]
     1.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)]
     1.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"
    1.10            apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym])
    1.11            apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p'']
    1.12 @@ -4723,7 +4723,7 @@
    1.13    have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
    1.14      \<longrightarrow> norm(ig) < dia + e" 
    1.15    proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
    1.16 -      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
    1.17 +      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a
    1.18        apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
    1.19        apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
    1.20    qed note norm=this[rule_format]