# HG changeset patch
# User webertj
# Date 1156900748 -7200
# Node ID 07ec5737605151433c921ad20ae544a145aa7734
# Parent  eef4e9081beabd817bd96938afde8e349f914d2c
lin_arith_prover: splitting reverted because of performance loss

diff -r eef4e9081bea -r 07ec57376051 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -327,6 +327,7 @@
 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 eef4e9081bea -r 07ec57376051 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -513,7 +513,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)
+        by (simp cong: R.finsum_cong add: Pi_def) arith
       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 eef4e9081bea -r 07ec57376051 src/HOL/Algebra/poly/LongDiv.ML
--- a/src/HOL/Algebra/poly/LongDiv.ML	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 30 03:19:08 2006 +0200
@@ -24,8 +24,6 @@
 
 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}) |] \
@@ -279,5 +277,3 @@
 by (rtac long_div_quo_unique 1);
 by (REPEAT (atac 1));
 qed "long_div_rem_unique";
-
-fast_arith_split_limit := 9;  (* FIXME *)
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -187,8 +187,6 @@
     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 -
@@ -228,8 +226,6 @@
     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)
 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -764,10 +764,8 @@
 apply (subgoal_tac "0 < v")
  prefer 2 apply arith
 apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
+apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
 apply (simp add: power2_eq_square)
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-apply (rule_tac lemma_sqrt_hcomplex_capprox, auto)
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 done
 
 lemma CFinite_HFinite_iff:
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Divides.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -710,7 +710,7 @@
   apply (rule iffI)
   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
 prefer 3; apply assumption
-  apply (simp_all add: quorem_def)
+  apply (simp_all add: quorem_def) apply arith
   apply (rule conjI)
   apply (rule_tac P="%x. n * (m div n) \<le> x" in
     subst [OF mod_div_equality [of _ n]])
diff -r eef4e9081bea -r 07ec57376051 src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -111,8 +111,6 @@
 apply(erule Ex_first_occurrence)
 done
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-
 lemma Graph2: 
   "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
 apply (unfold Reach_def)
@@ -128,7 +126,6 @@
  apply(case_tac "j=R")
   apply(erule_tac x = "Suc i" in allE)
   apply simp
-  apply arith
  apply (force simp add:nth_list_update)
 apply simp
 apply(erule exE)
@@ -156,7 +153,6 @@
 apply simp
 apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
  prefer 2 apply arith
-apply simp
 apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
  prefer 2 apply arith
 apply simp
@@ -177,26 +173,19 @@
  prefer 2 apply arith
  apply(drule_tac n = "Suc nata" in Compl_lemma)
  apply clarify
+ ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
  apply force
+ ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
 apply(drule leI)
 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
  apply(erule_tac x = "m - (Suc nata)" in allE)
  apply(case_tac "m")
   apply simp
  apply simp
- apply(subgoal_tac "natb - nata < Suc natb")
-  prefer 2 apply(erule thin_rl)+ apply arith
- apply simp
- apply(case_tac "length path")
-  apply force
-apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
 apply simp
-apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
-apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
-apply simp
-apply arith
 done
 
+
 subsubsection{* Graph 3 *}
 
 lemma Graph3: 
@@ -254,8 +243,6 @@
   apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
     prefer 2 apply arith
    apply simp
-  apply(erule mp)
-  apply arith
 --{* T is a root *}
  apply(case_tac "m=0")
   apply force
@@ -282,8 +269,6 @@
 apply(force simp add: nth_list_update)
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 subsubsection{* Graph 4 *}
 
 lemma Graph4: 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -329,7 +329,7 @@
 apply(rule_tac x=0 in exI,simp)
 done
 
-lemma Basic_sound:
+lemma Basic_sound: 
   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
   stable pre rely; stable post rely\<rbrakk>
   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
@@ -369,15 +369,16 @@
 apply(drule_tac s="Some (Basic f)" in sym,simp)
 apply(case_tac "x!Suc j",simp)
 apply(rule ctran.elims,simp)
-       apply(simp_all)
+apply(simp_all)
 apply(drule_tac c=sa in subsetD,simp)
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
-  apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
- apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
+  apply arith+
 apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Await rule *}
@@ -496,7 +497,7 @@
 apply(drule_tac s="Some (Await b P)" in sym,simp)
 apply(case_tac "x!Suc j",simp)
 apply(rule ctran.elims,simp)
-       apply(simp_all)
+apply(simp_all)
 apply(drule Star_imp_cptn) 
 apply clarify
 apply(erule_tac x=sa in allE)
@@ -510,17 +511,16 @@
 apply simp
 apply clarify
 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
-  apply(case_tac x,simp+)
+ apply(case_tac x,simp+)
  apply(erule_tac x=i in allE)
- apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
+ apply arith+
 apply(case_tac x)
- apply(simp add:last_length)+
+apply(simp add:last_length)+
 done
 
 subsubsection{* Soundness of the Conditional rule *}
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-
 lemma Cond_sound: 
   "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
   \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
@@ -537,7 +537,6 @@
     apply(simp add:assum_def)
    apply(simp add:assum_def)
   apply(erule_tac m="length x" in etran_or_ctran,simp+)
-  apply(case_tac x,simp+)
  apply(case_tac x, (simp add:last_length)+)
 apply(erule exE)
 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
@@ -549,18 +548,7 @@
  apply(erule_tac x="sa" in allE)
  apply(drule_tac c="drop (Suc m) x" in subsetD)
   apply simp
-  apply(rule conjI)
-   apply force
   apply clarify
-  apply(subgoal_tac "(Suc m) + i \<le> length x")
-   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
-    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
-    apply arith
-   apply arith
-  apply arith
  apply simp
  apply clarify
  apply(case_tac "i\<le>m")
@@ -569,52 +557,34 @@
    apply(erule_tac x=i in allE, erule impE, assumption)
    apply simp+
  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
-  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule mp)
-    apply arith
-   apply arith
-  apply arith
-  apply(case_tac "length (drop (Suc m) x)",simp)
-  apply(erule_tac x="sa" in allE)
-  back
-  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
-   apply(rule conjI)
-    apply force
-   apply clarify
-   apply(subgoal_tac "(Suc m) + i \<le> length x")
-    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
-     apply(rotate_tac -2)
-     apply simp
-     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
-     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
-      apply simp
-     apply arith
-    apply arith
-   apply arith
-  apply simp
-  apply clarify
-  apply(case_tac "i\<le>m")
-   apply(drule le_imp_less_or_eq)
-   apply(erule disjE)
-    apply(erule_tac x=i in allE, erule impE, assumption)
-    apply simp
+ apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+   apply(rotate_tac -2)
    apply simp
-  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
-  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
-   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
-    apply(rotate_tac -2)
-    apply simp
-    apply(erule mp)
-   apply arith
   apply arith
  apply arith
+apply(case_tac "length (drop (Suc m) x)",simp)
+apply(erule_tac x="sa" in allE)
+back
+apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
+ apply clarify
+apply simp
+apply clarify
+apply(case_tac "i\<le>m")
+ apply(drule le_imp_less_or_eq)
+ apply(erule disjE)
+  apply(erule_tac x=i in allE, erule impE, assumption)
+  apply simp
+ apply simp
+apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
+apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
+ apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
+  apply(rotate_tac -2)
+  apply simp
+ apply arith
+apply arith
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 subsubsection{* Soundness of the Sequential rule *}
 
 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
@@ -656,7 +626,6 @@
  apply(simp add:lift_def)
 apply simp
 done
-
 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
 
 lemma Seq_sound2 [rule_format]: 
@@ -714,7 +683,6 @@
   apply simp+
 apply(simp add:lift_def)
 done
-
 (*
 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
 apply(simp only:last_length [THEN sym])
@@ -737,8 +705,6 @@
 apply simp
 done
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-
 lemma Seq_sound: 
   "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
   \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
@@ -862,8 +828,6 @@
       apply simp
       apply(erule mp)
       apply(case_tac ys,simp+)
-     apply arith
-    apply arith
    apply force
   apply arith
  apply force
@@ -877,8 +841,6 @@
  apply(case_tac ys,simp+)
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 subsubsection{* Soundness of the While rule *}
 
 lemma last_append[rule_format]:
@@ -924,8 +886,6 @@
 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
 done
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-
 lemma While_sound_aux [rule_format]: 
   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
@@ -1092,8 +1052,6 @@
 apply simp
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 lemma While_sound: 
   "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
     \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -173,10 +173,7 @@
  prefer 2 apply assumption
 apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
  prefer 2 apply arith
-apply (drule_tac x = "psize D - Suc n" in spec)
-ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
-apply simp
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
+apply (drule_tac x = "psize D - Suc n" in spec, simp) 
 done
 
 lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
@@ -439,8 +436,6 @@
 apply (simp add: right_diff_distrib)
 done
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-
 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
              ==> Integral(a,b) f' (f(b) - f(a))"
 apply (drule order_le_imp_less_or_eq, auto) 
@@ -472,7 +467,6 @@
           fine_def)
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
 by simp
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -2239,7 +2239,7 @@
   thus ?thesis by simp
 qed
 
-ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
+ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
 
 lemma LIMSEQ_SEQ_conv2:
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
@@ -2321,7 +2321,7 @@
   ultimately show False by simp
 qed
 
-ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma LIMSEQ_SEQ_conv:
   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -394,7 +394,7 @@
   apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
   apply force
   apply assumption
-  apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
+  apply (simp add: power2_eq_square mult_compare_simps)
   apply (rule mult_imp_div_pos_less)
   apply (rule mult_pos_pos, assumption, assumption)
   apply (subgoal_tac "xa * xa = abs xa * abs xa")
@@ -408,7 +408,6 @@
   apply (subst diff_minus [THEN sym])+
   apply (subst ln_div [THEN sym])
   apply arith
-  apply assumption
   apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq 
     add_divide_distrib power2_eq_square)
   apply (rule mult_pos_pos, assumption)+
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -329,7 +329,7 @@
 apply (rule InfinitesimalI)
 apply (drule HFiniteD, clarify)
 apply (simp only: abs_mult)
-apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp)
+apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp add: split_if)
 apply (subgoal_tac "0 < r / t")
 apply (rule mult_strict_mono)
 apply (simp add: InfinitesimalD SReal_divide)
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -426,6 +426,7 @@
      "\<forall>p2. length (p1 +++ p2) =
              (if (length p1 < length p2) then length p2 else length p1)"
 apply (induct "p1", simp_all)
+apply arith
 done
 
 lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -323,8 +323,6 @@
 
 lemmas sumr_geometric = geometric_sum [where 'a = real]
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: needed because otherwise a premise gets simplified away *)
-
 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
 apply (case_tac "x = 1")
 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
@@ -335,8 +333,6 @@
 apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
-
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
 
 lemma summable_convergent_sumr_iff:
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -400,6 +400,8 @@
 apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
 apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
 apply (auto simp add: mult_assoc power_abs abs_mult)
+ prefer 2
+ apply (drule_tac x = 0 in spec, force)
 apply (auto simp add: power_abs mult_ac)
 apply (rule_tac a2 = "z ^ n" 
        in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
@@ -576,6 +578,8 @@
 
 text{* FIXME: Long proofs*}
 
+ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proofs *)
+
 lemma termdiffs_aux:
      "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
     ==> (\<lambda>h. \<Sum>n. c n *
@@ -589,56 +593,53 @@
      and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
                              - (real n * (x ^ (n - Suc 0))))" 
        in lemma_termdiff5)
-  -- "3 subgoals"
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
-  apply (auto simp add: add_commute)
- apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
-  apply (rule_tac [2] x = K in powser_insidea, auto)
- apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
-  apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
- apply (simp add: diffs_def mult_assoc [symmetric])
- apply (subgoal_tac
-         "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
-               = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
-  apply (auto simp add: abs_mult)
-   apply (drule diffs_equiv)
-   apply (drule sums_summable)
-   apply (simp_all add: diffs_def)
- apply (simp add: diffs_def mult_ac)
- apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
-  apply auto
+apply (auto simp add: add_commute)
+apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
+apply (rule_tac [2] x = K in powser_insidea, auto)
+apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
+apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
+apply (simp add: diffs_def mult_assoc [symmetric])
+apply (subgoal_tac
+        "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
+              = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
+apply (auto simp add: abs_mult)
+apply (drule diffs_equiv)
+apply (drule sums_summable)
+apply (simp_all add: diffs_def) 
+apply (simp add: diffs_def mult_ac)
+apply (subgoal_tac " (%n. real n * (real (Suc n) * (\<bar>c (Suc n)\<bar> * (r ^ (n - Suc 0))))) = (%n. diffs (%m. real (m - Suc 0) * \<bar>c m\<bar> * inverse r) n * (r ^ n))")
+apply auto
   prefer 2
   apply (rule ext)
-  apply (simp add: diffs_def)
+  apply (simp add: diffs_def) 
   apply (case_tac "n", auto)
 txt{*23*}
    apply (drule abs_ge_zero [THEN order_le_less_trans])
-   apply (simp add: mult_ac)
+   apply (simp add: mult_ac) 
   apply (drule abs_ge_zero [THEN order_le_less_trans])
-  apply (simp add: mult_ac)
+  apply (simp add: mult_ac) 
  apply (drule diffs_equiv)
  apply (drule sums_summable)
- apply (subgoal_tac
-           "summable
-             (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
-                  r ^ (n - Suc 0)) =
-            summable
-             (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
-  apply simp
- apply (rule_tac f = summable in arg_cong, rule ext)
+apply (subgoal_tac
+          "summable
+            (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
+                 r ^ (n - Suc 0)) =
+           summable
+            (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
+apply simp 
+apply (rule_tac f = summable in arg_cong, rule ext)
 txt{*33*}
- apply (case_tac "n", auto)
- apply (case_tac "nat", auto)
- apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
+apply (case_tac "n", auto)
+apply (case_tac "nat", auto)
+apply (drule abs_ge_zero [THEN order_le_less_trans], auto) 
 apply (drule abs_ge_zero [THEN order_le_less_trans])
 apply (simp add: mult_assoc)
 apply (rule mult_left_mono)
- prefer 2 apply arith
+ prefer 2 apply arith 
 apply (subst add_commute)
 apply (simp (no_asm) add: mult_assoc [symmetric])
 apply (rule lemma_termdiff3)
-  apply (auto intro: abs_triangle_ineq [THEN order_trans])
-apply arith
+apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
 done
 
 ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
@@ -655,7 +656,7 @@
 apply (simp add: LIM_def, safe)
 apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
 apply (auto simp add: less_diff_eq)
-apply (frule abs_triangle_ineq [THEN order_le_less_trans])
+apply (drule abs_triangle_ineq [THEN order_le_less_trans])
 apply (rule_tac y = 0 in order_le_less_trans, auto)
 apply (subgoal_tac " (%n. (c n) * (x ^ n)) sums (\<Sum>n. (c n) * (x ^ n)) & (%n. (c n) * ((x + xa) ^ n)) sums (\<Sum>n. (c n) * ( (x + xa) ^ n))")
 apply (auto intro!: summable_sums)
@@ -667,11 +668,11 @@
 apply (simp add: diff_def divide_inverse add_ac mult_ac)
 apply (rule LIM_zero_cancel)
 apply (rule_tac g = "%h. \<Sum>n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) - (real n * (x ^ (n - Suc 0))))" in LIM_trans)
- prefer 2 apply (blast intro: termdiffs_aux)
+ prefer 2 apply (blast intro: termdiffs_aux) 
 apply (simp add: LIM_def, safe)
 apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
 apply (auto simp add: less_diff_eq)
-apply (frule abs_triangle_ineq [THEN order_le_less_trans])
+apply (drule abs_triangle_ineq [THEN order_le_less_trans])
 apply (rule_tac y = 0 in order_le_less_trans, auto)
 apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
 apply (rule_tac [2] powser_inside, auto)
@@ -2580,5 +2581,5 @@
 apply (drule_tac [3] LIM_fun_gt_zero)
 apply force+
 done
-
+  
 end 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -221,7 +221,7 @@
   by simp
 
 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
-  by simp
+  by (simp, arith)
 
 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   by (simp add: max_def)
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -387,7 +387,7 @@
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
   have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (simp add: congruent_def)
+    by (simp add: congruent_def) arith
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Isar_examples/HoareEx.thy
--- a/src/HOL/Isar_examples/HoareEx.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -317,6 +317,7 @@
       apply simp
      apply clarsimp
     apply clarsimp
+   apply arith
    prefer 2
    apply clarsimp
   apply (clarsimp simp: nat_distrib)
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -934,10 +934,11 @@
   apply (subst Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply (case_tac "j + int u < 0")
-  apply simp
+  apply (simp, arith)
   apply (case_tac "i + int v < 0")
+  apply (simp add: neg_def, arith)
   apply (simp add: neg_def)
-  apply (simp add: neg_def)
+  apply arith
   done
 
 lemma Rep_take_columns[simp]:
diff -r eef4e9081bea -r 07ec57376051 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -338,12 +338,17 @@
     apply (subst Rep_matrix_mult)
     apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
     apply (simp_all)
+    apply (intro strip, rule conjI)
     apply (intro strip)
+    apply (drule_tac max_helper)
+    apply (simp)
+    apply (auto)
     apply (rule zero_imp_mult_zero)
     apply (rule disjI2)
     apply (rule nrows)
     apply (rule order_trans[of _ 1])
-    apply auto
+    apply (simp)
+    apply (simp)
     done
 qed
 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -968,14 +968,14 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply fast
 
 (* case exit Loop *)
@@ -1003,7 +1003,7 @@
 apply fast
 apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply simp
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply (rule progression_refl)
 
 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -663,7 +663,7 @@
   (* show P x of bspec *)
 apply simp
   apply (subgoal_tac "length mt_pre \<le> pc'")
-  apply (simp add: nth_append)
+  apply (simp add: nth_append) apply arith
 
   (* subgoals *)
 apply (simp add: eff_def xcpt_eff_def)
@@ -965,6 +965,7 @@
 apply (simp only:)
 apply (rule check_type_mono) apply assumption
 apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
+apply arith
 apply (simp add: nth_append)
 
 apply (erule conjE)+
@@ -1282,7 +1283,6 @@
   apply auto
   done
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
 
 lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; 
   max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
@@ -1319,7 +1319,6 @@
 apply (simp add: max_def)
   done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; 
   0 \<le> (int pc + i);  nat (int pc + i) < max_pc;
@@ -1644,7 +1643,7 @@
 done
 
 
-ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
+
 
 lemma wt_method_compTpExpr_Exprs_corresp: "
   \<lbrakk> jmb = (pns,lvars,blk,res); 
@@ -1923,7 +1922,6 @@
 
 done
 
-ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 
 lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
   wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
diff -r eef4e9081bea -r 07ec57376051 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -175,6 +175,11 @@
      apply (rule_tac [!] funprod_zgcd)
      apply safe
      apply simp_all
+   apply (subgoal_tac "i<n")
+    prefer 2
+    apply arith
+   apply (case_tac [2] i)
+    apply simp_all
   done
 
 lemma x_sol_lin_aux:
diff -r eef4e9081bea -r 07ec57376051 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -72,6 +72,7 @@
    apply (simp add: fib.Suc_Suc mod_Suc)
   apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
                    mod_Suc zmult_int [symmetric])
+  apply (presburger (no_abs))
   done
 
 text{*We now obtain a version for the natural numbers via the coercion 
diff -r eef4e9081bea -r 07ec57376051 src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -193,8 +193,6 @@
   then show ?thesis by auto
 qed
 
-ML {* fast_arith_split_limit := 0; *} (*FIXME*)
-
 lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
     (p * b \<noteq> q * a)"
 proof
@@ -236,8 +234,6 @@
   with q_g_2 show False by auto
 qed
 
-ML {* fast_arith_split_limit := 9; *} (*FIXME*)
-
 lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)