# HG changeset patch
# User webertj
# Date 1154530241 -7200
# Node ID 49c312eaaa1103d0f538b595e33f4693a9ba38e7
# Parent  16733b31e1cf7026daef7820307ae88c89732f04
lin_arith_prover splits certain operators (e.g. min, max, abs)

diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 02 16:50:41 2006 +0200
@@ -326,7 +326,6 @@
 apply (subst times_binomial_minus1_eq, simp, simp)
 apply (subst exponent_mult_add, simp)
 apply (simp (no_asm_simp) add: zero_less_binomial_iff)
-apply arith
 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
 done
 
diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 02 16:50:41 2006 +0200
@@ -511,7 +511,7 @@
       have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
         by (simp cong: R.finsum_cong add: Pi_def)
       from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
-        by (simp cong: R.finsum_cong add: Pi_def) arith
+        by (simp cong: R.finsum_cong add: Pi_def)
       have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
         by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
       show ?thesis
diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 02 16:50:41 2006 +0200
@@ -24,6 +24,8 @@
 
 val SUM_shrink_below_lemma = thm "SUM_shrink_below_lemma";
 
+fast_arith_split_limit := 0;  (* FIXME: rewrite proofs *)
+
 Goal
   "!! f::(nat=>'a::ring). \
 \    [| m <= n; !!i. i < m ==> f i = 0; P (setsum (%i. f (i+m)) {..n-m}) |] \
@@ -277,3 +279,5 @@
 by (rtac long_div_quo_unique 1);
 by (REPEAT (atac 1));
 qed "long_div_rem_unique";
+
+fast_arith_split_limit := 9;  (* FIXME *)
diff -r 16733b31e1cf -r 49c312eaaa11 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 13:48:21 2006 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 02 16:50:41 2006 +0200
@@ -187,6 +187,8 @@
     by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP)
 qed
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 lemma coeff_mult [simp]:
   "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)"
 proof -
@@ -226,6 +228,8 @@
     by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP)
 qed
 
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+
 lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)"
 by (unfold up_uminus_def) (simp add: ring_simps)