# HG changeset patch # User haftmann # Date 1273219164 -7200 # Node ID 34c36a5cb808b56e1bad36a5355474f9d8ae546f # Parent 5779d9fbedd0171522efafb6986b876e090178f2 prefix normalizing replaces class_semiring diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Metis_Examples/BT.thy --- a/src/HOL/Metis_Examples/BT.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Metis_Examples/BT.thy Fri May 07 09:59:24 2010 +0200 @@ -88,7 +88,7 @@ case Lf thus ?case by (metis reflect.simps(1)) next case (Br a t1 t2) thus ?case - by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) + by (metis normalizing.semiring_rules(24) n_nodes.simps(2) reflect.simps(2)) qed declare [[ atp_problem_prefix = "BT__depth_reflect" ]] diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Metis_Examples/BigO.thy --- a/src/HOL/Metis_Examples/BigO.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Metis_Examples/BigO.thy Fri May 07 09:59:24 2010 +0200 @@ -41,7 +41,7 @@ fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" have F1: "\x\<^isub>1\'a\linordered_idom. 0 \ \x\<^isub>1\" by (metis abs_ge_zero) - have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F2: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F3: "\x\<^isub>1 x\<^isub>3. x\<^isub>3 \ \h x\<^isub>1\ \ x\<^isub>3 \ c * \f x\<^isub>1\" by (metis A1 order_trans) have F4: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) @@ -70,7 +70,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>2 x\<^isub>3\'a\linordered_idom. \x\<^isub>3\ * \x\<^isub>2\ = \x\<^isub>3 * x\<^isub>2\" by (metis abs_mult) have "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_mult_pos abs_one) @@ -92,7 +92,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have F1: "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) have F2: "\x\<^isub>3 x\<^isub>1\'a\linordered_idom. 0 \ x\<^isub>1 \ \x\<^isub>3 * x\<^isub>1\ = \x\<^isub>3\ * x\<^isub>1" by (metis abs_mult_pos) hence "\x\<^isub>1\0. \x\<^isub>1\'a\linordered_idom\ = x\<^isub>1" by (metis F1 abs_one) hence "\x\<^isub>3. 0 \ \f x\<^isub>3\ \ c * \f x\<^isub>3\ = \c\ * \f x\<^isub>3\" by (metis F2 A1 abs_ge_zero order_trans) @@ -111,7 +111,7 @@ proof - fix c :: 'a and x :: 'b assume A1: "\x. \h x\ \ c * \f x\" - have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1) + have "\x\<^isub>1\'a\linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis normalizing.mul_1) hence "\x\<^isub>3. \c * \f x\<^isub>3\\ = c * \f x\<^isub>3\" by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one) hence "\h x\ \ \c * f x\" by (metis A1 abs_ge_zero abs_mult_pos abs_mult) @@ -145,12 +145,12 @@ declare [[ atp_problem_prefix = "BigO__bigo_refl" ]] lemma bigo_refl [intro]: "f : O(f)" apply (auto simp add: bigo_def) -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_zero" ]] lemma bigo_zero: "0 : O(g)" apply (auto simp add: bigo_def func_zero) -by (metis class_semiring.mul_0 order_refl) +by (metis normalizing.mul_0 order_refl) lemma bigo_zero2: "O(%x.0) = {%x.0}" apply (auto simp add: bigo_def) @@ -307,7 +307,7 @@ apply (auto simp add: diff_minus fun_Compl_def func_plus) prefer 2 apply (drule_tac x = x in spec)+ - apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) + apply (metis add_right_mono normalizing.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans) proof - fix x :: 'a assume "\x. lb x \ f x" @@ -318,13 +318,13 @@ lemma bigo_abs: "(%x. abs(f x)) =o O(f)" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]] lemma bigo_abs2: "f =o O(%x. abs(f x))" apply (unfold bigo_def) apply auto -by (metis class_semiring.mul_1 order_refl) +by (metis normalizing.mul_1 order_refl) lemma bigo_abs3: "O(f) = O(%x. abs(f x))" proof - diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri May 07 09:59:24 2010 +0200 @@ -1877,7 +1877,7 @@ using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR apply (rule mult_left_le_imp_le[of "1 - u"]) - unfolding class_semiring.mul_a using `u<1` by auto + unfolding normalizing.mul_a using `u<1` by auto thus "y \ s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u] using as unfolding scaleR_scaleR by auto qed auto thus "u *\<^sub>R x \ s - frontier s" using frontier_def and interior_subset by auto qed diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri May 07 09:59:24 2010 +0200 @@ -698,7 +698,7 @@ unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto then guess x .. note x=this show ?thesis proof(cases "f a = f b") - 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) + 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) also have "\ = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by auto also have "\ \ norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz) diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri May 07 09:59:24 2010 +0200 @@ -2533,7 +2533,7 @@ show "content x \ 0" unfolding as snd_conv * interval_doublesplit by(rule content_pos_le) qed have **:"norm (1::real) \ 1" by auto note division_doublesplit[OF p'',unfolded interval_doublesplit] note dsum_bound[OF this **,unfolded interval_doublesplit[THEN sym]] - 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)] + note this[unfolded real_scaleR_def real_norm_def normalizing.semiring_rules, of k c d] note le_less_trans[OF this d(2)] from this[unfolded abs_of_nonneg[OF *]] show "(\ka\snd ` p. content (ka \ {x. \x $ k - c\ \ d})) < e" apply(subst vsum_nonzero_image_lemma[of "snd ` p" content "{}", unfolded o_def,THEN sym]) apply(rule finite_imageI p' content_empty)+ unfolding forall_in_division[OF p''] @@ -4723,7 +4723,7 @@ have "\e sg dsa dia ig. norm(sg) \ dsa \ abs(dsa - dia) < e / 2 \ norm(sg - ig) < e / 2 \ norm(ig) < dia + e" proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) - apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a + apply(subst real_sum_of_halves[of e,THEN sym]) unfolding normalizing.add_a apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith qed note norm=this[rule_format] diff -r 5779d9fbedd0 -r 34c36a5cb808 src/HOL/Probability/Lebesgue.thy --- a/src/HOL/Probability/Lebesgue.thy Thu May 06 23:37:07 2010 +0200 +++ b/src/HOL/Probability/Lebesgue.thy Fri May 07 09:59:24 2010 +0200 @@ -938,17 +938,17 @@ proof safe fix t assume t: "t \ space M" { fix m n :: nat assume "m \ n" - hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding class_semiring.mul_pwr by auto + hence *: "(2::real)^n = 2^m * 2^(n - m)" unfolding normalizing.mul_pwr by auto have "real (natfloor (f t * 2^m) * natfloor (2^(n-m))) \ real (natfloor (f t * 2 ^ n))" apply (subst *) - apply (subst class_semiring.mul_a) + apply (subst normalizing.mul_a) apply (subst real_of_nat_le_iff) apply (rule le_mult_natfloor) using nonneg[OF t] by (auto intro!: mult_nonneg_nonneg) hence "real (natfloor (f t * 2^m)) * 2^n \ real (natfloor (f t * 2^n)) * 2^m" apply (subst *) - apply (subst (3) class_semiring.mul_c) - apply (subst class_semiring.mul_a) + apply (subst (3) normalizing.mul_c) + apply (subst normalizing.mul_a) by (auto intro: mult_right_mono simp: natfloor_power real_of_nat_power[symmetric]) } thus "incseq (\n. ?u n t)" unfolding u_at_t[OF t] unfolding incseq_def by (auto simp add: le_divide_eq divide_le_eq less_divide_eq)