# HG changeset patch # User haftmann # Date 1273180317 -7200 # Node ID bfd7f5c3bf692d3605e9f04dc618fef5617b1d86 # Parent 41da7025e59cfb855527d9cbb73e3ee929b6c5d1 former free-floating field_comp_conv now in structure Normalizer diff -r 41da7025e59c -r bfd7f5c3bf69 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Thu May 06 23:11:57 2010 +0200 @@ -1222,7 +1222,7 @@ in (let val th = tryfind trivial_axiom (keq @ klep @ kltp) in - (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial) + (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv Normalizer.field_comp_conv) th, RealArith.Trivial) end) handle Failure _ => (let val proof = diff -r 41da7025e59c -r bfd7f5c3bf69 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Library/normarith.ML Thu May 06 23:11:57 2010 +0200 @@ -168,7 +168,7 @@ val real_poly_conv = Normalizer.semiring_normalize_wrapper ctxt (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) - in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) + in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (Normalizer.field_comp_conv then_conv real_poly_conv))) end; fun absc cv ct = case term_of ct of @@ -190,8 +190,8 @@ val apply_pth5 = rewr_conv @{thm pth_5}; val apply_pth6 = rewr_conv @{thm pth_6}; val apply_pth7 = rewrs_conv @{thms pth_7}; - val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); - val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); + val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Normalizer.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); + val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv Normalizer.field_comp_conv); val apply_ptha = rewr_conv @{thm pth_a}; val apply_pthb = rewrs_conv @{thms pth_b}; val apply_pthc = rewrs_conv @{thms pth_c}; @@ -204,7 +204,7 @@ | _ => error "headvector: non-canonical term" fun vector_cmul_conv ct = - ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv + ((apply_pth5 then_conv arg1_conv Normalizer.field_comp_conv) else_conv (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct fun vector_add_conv ct = apply_pth7 ct @@ -396,7 +396,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) - then_conv field_comp_conv + then_conv Normalizer.field_comp_conv then_conv nnf_conv fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); diff -r 41da7025e59c -r bfd7f5c3bf69 src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu May 06 23:11:57 2010 +0200 @@ -751,7 +751,7 @@ (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord in gen_real_arith ctxt - (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, + (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv, main,neg,add,mul, prover) end; diff -r 41da7025e59c -r bfd7f5c3bf69 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu May 06 23:11:57 2010 +0200 @@ -2231,7 +2231,7 @@ apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof fix z assume z:"z\{x - ?d..x + ?d}" have e:"e = setsum (\i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1 - by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) + by (metis eq_divide_imp times_divide_eq_left real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute) show "dist x z \ e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono) using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed hence k:"\y\{x - ?d..x + ?d}. f y \ k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption diff -r 41da7025e59c -r bfd7f5c3bf69 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu May 06 23:11:57 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu May 06 23:11:57 2010 +0200 @@ -810,7 +810,7 @@ guess k using real_lbound_gt_zero[OF d[THEN conjunct1] d'[THEN conjunct1]] .. note k=this show ?case apply(rule_tac x=k in exI,rule) defer proof(rule,rule) fix z assume as:"norm(z - y) < k" hence "norm (g z - g y - g' (z - y)) \ e / B * norm(g z - g y)" using d' k by auto - also have "\ \ e * norm(z - y)" unfolding mult_frac_num pos_divide_le_eq[OF `B>0`] + also have "\ \ e * norm(z - y)" unfolding times_divide_eq_left pos_divide_le_eq[OF `B>0`] using lem2[THEN spec[where x=z]] using k as using `e>0` by(auto simp add:field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (z - y)" by simp qed(insert k, auto) qed qed