lin_arith_prover splits certain operators (e.g. min, max, abs)
authorwebertj
Wed Aug 02 16:50:41 2006 +0200 (2006-08-02)
changeset 2028249c312eaaa11
parent 20281 16733b31e1cf
child 20283 81b7832b29a3
lin_arith_prover splits certain operators (e.g. min, max, abs)
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/LongDiv.ML
src/HOL/Algebra/poly/UnivPoly2.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Aug 02 13:48:21 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 02 16:50:41 2006 +0200
     1.3 @@ -326,7 +326,6 @@
     1.4  apply (subst times_binomial_minus1_eq, simp, simp)
     1.5  apply (subst exponent_mult_add, simp)
     1.6  apply (simp (no_asm_simp) add: zero_less_binomial_iff)
     1.7 -apply arith
     1.8  apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
     1.9  done
    1.10  
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 13:48:21 2006 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 16:50:41 2006 +0200
     2.3 @@ -511,7 +511,7 @@
     2.4        have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
     2.5          by (simp cong: R.finsum_cong add: Pi_def)
     2.6        from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
     2.7 -        by (simp cong: R.finsum_cong add: Pi_def) arith
     2.8 +        by (simp cong: R.finsum_cong add: Pi_def)
     2.9        have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
    2.10          by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
    2.11        show ?thesis
     3.1 --- a/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 02 13:48:21 2006 +0200
     3.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 02 16:50:41 2006 +0200
     3.3 @@ -24,6 +24,8 @@
     3.4  
     3.5  val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma";
     3.6  
     3.7 +fast_arith_split_limit := 0;  (* FIXME: rewrite proofs *)
     3.8 +
     3.9  Goal
    3.10    "!! f::(nat=>'a::ring). \
    3.11  \    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
    3.12 @@ -277,3 +279,5 @@
    3.13  by (rtac long_div_quo_unique 1);
    3.14  by (REPEAT (atac 1));
    3.15  qed "long_div_rem_unique";
    3.16 +
    3.17 +fast_arith_split_limit := 9;  (* FIXME *)
     4.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 13:48:21 2006 +0200
     4.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 16:50:41 2006 +0200
     4.3 @@ -187,6 +187,8 @@
     4.4      by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
     4.5  qed
     4.6  
     4.7 +ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
     4.8 +
     4.9  lemma coeff_mult [simp]:
    4.10    "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
    4.11  proof -
    4.12 @@ -226,6 +228,8 @@
    4.13      by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
    4.14  qed
    4.15  
    4.16 +ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    4.17 +
    4.18  lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
    4.19  by (unfold up_uminus_def) (simp add: ring_simps)
    4.20