lin_arith_prover: splitting reverted because of performance loss
authorwebertj
Wed Aug 30 03:19:08 2006 +0200 (2006-08-30)
changeset 2043207ec57376051
parent 20431 eef4e9081bea
child 20433 55471f940e5c
lin_arith_prover: splitting reverted because of performance loss
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/LongDiv.ML
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Complex/NSCA.thy
src/HOL/Divides.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/Ln.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Integ/IntDef.thy
src/HOL/Isar_examples/HoareEx.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Tue Aug 29 21:43:34 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Aug 30 03:19:08 2006 +0200
     1.3 @@ -327,6 +327,7 @@
     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	Tue Aug 29 21:43:34 2006 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Aug 30 03:19:08 2006 +0200
     2.3 @@ -513,7 +513,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)
     2.8 +        by (simp cong: R.finsum_cong add: Pi_def) arith
     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	Tue Aug 29 21:43:34 2006 +0200
     3.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML	Wed Aug 30 03:19:08 2006 +0200
     3.3 @@ -24,8 +24,6 @@
     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 @@ -279,5 +277,3 @@
    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	Tue Aug 29 21:43:34 2006 +0200
     4.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Aug 30 03:19:08 2006 +0200
     4.3 @@ -187,8 +187,6 @@
     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 @@ -228,8 +226,6 @@
    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  
     5.1 --- a/src/HOL/Complex/NSCA.thy	Tue Aug 29 21:43:34 2006 +0200
     5.2 +++ b/src/HOL/Complex/NSCA.thy	Wed Aug 30 03:19:08 2006 +0200
     5.3 @@ -764,10 +764,8 @@
     5.4  apply (subgoal_tac "0 < v")
     5.5   prefer 2 apply arith
     5.6  apply (subgoal_tac "sqrt (abs (Y x) ^ 2 + abs (Z x) ^ 2) < 2*u + 2*v")
     5.7 +apply (rule_tac [2] lemma_sqrt_hcomplex_capprox, auto)
     5.8  apply (simp add: power2_eq_square)
     5.9 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
    5.10 -apply (rule_tac lemma_sqrt_hcomplex_capprox, auto)
    5.11 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    5.12  done
    5.13  
    5.14  lemma CFinite_HFinite_iff:
     6.1 --- a/src/HOL/Divides.thy	Tue Aug 29 21:43:34 2006 +0200
     6.2 +++ b/src/HOL/Divides.thy	Wed Aug 30 03:19:08 2006 +0200
     6.3 @@ -710,7 +710,7 @@
     6.4    apply (rule iffI)
     6.5    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
     6.6  prefer 3; apply assumption
     6.7 -  apply (simp_all add: quorem_def)
     6.8 +  apply (simp_all add: quorem_def) apply arith
     6.9    apply (rule conjI)
    6.10    apply (rule_tac P="%x. n * (m div n) \<le> x" in
    6.11      subst [OF mod_div_equality [of _ n]])
     7.1 --- a/src/HOL/HoareParallel/Graph.thy	Tue Aug 29 21:43:34 2006 +0200
     7.2 +++ b/src/HOL/HoareParallel/Graph.thy	Wed Aug 30 03:19:08 2006 +0200
     7.3 @@ -111,8 +111,6 @@
     7.4  apply(erule Ex_first_occurrence)
     7.5  done
     7.6  
     7.7 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
     7.8 -
     7.9  lemma Graph2: 
    7.10    "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
    7.11  apply (unfold Reach_def)
    7.12 @@ -128,7 +126,6 @@
    7.13   apply(case_tac "j=R")
    7.14    apply(erule_tac x = "Suc i" in allE)
    7.15    apply simp
    7.16 -  apply arith
    7.17   apply (force simp add:nth_list_update)
    7.18  apply simp
    7.19  apply(erule exE)
    7.20 @@ -156,7 +153,6 @@
    7.21  apply simp
    7.22  apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
    7.23   prefer 2 apply arith
    7.24 -apply simp
    7.25  apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
    7.26   prefer 2 apply arith
    7.27  apply simp
    7.28 @@ -177,26 +173,19 @@
    7.29   prefer 2 apply arith
    7.30   apply(drule_tac n = "Suc nata" in Compl_lemma)
    7.31   apply clarify
    7.32 + ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
    7.33   apply force
    7.34 + ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
    7.35  apply(drule leI)
    7.36  apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
    7.37   apply(erule_tac x = "m - (Suc nata)" in allE)
    7.38   apply(case_tac "m")
    7.39    apply simp
    7.40   apply simp
    7.41 - apply(subgoal_tac "natb - nata < Suc natb")
    7.42 -  prefer 2 apply(erule thin_rl)+ apply arith
    7.43 - apply simp
    7.44 - apply(case_tac "length path")
    7.45 -  apply force
    7.46 -apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
    7.47  apply simp
    7.48 -apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
    7.49 -apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
    7.50 -apply simp
    7.51 -apply arith
    7.52  done
    7.53  
    7.54 +
    7.55  subsubsection{* Graph 3 *}
    7.56  
    7.57  lemma Graph3: 
    7.58 @@ -254,8 +243,6 @@
    7.59    apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
    7.60      prefer 2 apply arith
    7.61     apply simp
    7.62 -  apply(erule mp)
    7.63 -  apply arith
    7.64  --{* T is a root *}
    7.65   apply(case_tac "m=0")
    7.66    apply force
    7.67 @@ -282,8 +269,6 @@
    7.68  apply(force simp add: nth_list_update)
    7.69  done
    7.70  
    7.71 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    7.72 -
    7.73  subsubsection{* Graph 4 *}
    7.74  
    7.75  lemma Graph4: 
     8.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Aug 29 21:43:34 2006 +0200
     8.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Aug 30 03:19:08 2006 +0200
     8.3 @@ -329,7 +329,7 @@
     8.4  apply(rule_tac x=0 in exI,simp)
     8.5  done
     8.6  
     8.7 -lemma Basic_sound:
     8.8 +lemma Basic_sound: 
     8.9    " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; 
    8.10    stable pre rely; stable post rely\<rbrakk>
    8.11    \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
    8.12 @@ -369,15 +369,16 @@
    8.13  apply(drule_tac s="Some (Basic f)" in sym,simp)
    8.14  apply(case_tac "x!Suc j",simp)
    8.15  apply(rule ctran.elims,simp)
    8.16 -       apply(simp_all)
    8.17 +apply(simp_all)
    8.18  apply(drule_tac c=sa in subsetD,simp)
    8.19  apply clarify
    8.20  apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
    8.21 -  apply(case_tac x,simp+)
    8.22 + apply(case_tac x,simp+)
    8.23   apply(erule_tac x=i in allE)
    8.24 - apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
    8.25 +apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
    8.26 +  apply arith+
    8.27  apply(case_tac x)
    8.28 - apply(simp add:last_length)+
    8.29 +apply(simp add:last_length)+
    8.30  done
    8.31  
    8.32  subsubsection{* Soundness of the Await rule *}
    8.33 @@ -496,7 +497,7 @@
    8.34  apply(drule_tac s="Some (Await b P)" in sym,simp)
    8.35  apply(case_tac "x!Suc j",simp)
    8.36  apply(rule ctran.elims,simp)
    8.37 -       apply(simp_all)
    8.38 +apply(simp_all)
    8.39  apply(drule Star_imp_cptn) 
    8.40  apply clarify
    8.41  apply(erule_tac x=sa in allE)
    8.42 @@ -510,17 +511,16 @@
    8.43  apply simp
    8.44  apply clarify
    8.45  apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all)
    8.46 -  apply(case_tac x,simp+)
    8.47 + apply(case_tac x,simp+)
    8.48   apply(erule_tac x=i in allE)
    8.49 - apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
    8.50 +apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
    8.51 + apply arith+
    8.52  apply(case_tac x)
    8.53 - apply(simp add:last_length)+
    8.54 +apply(simp add:last_length)+
    8.55  done
    8.56  
    8.57  subsubsection{* Soundness of the Conditional rule *}
    8.58  
    8.59 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
    8.60 -
    8.61  lemma Cond_sound: 
    8.62    "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; 
    8.63    \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk>
    8.64 @@ -537,7 +537,6 @@
    8.65      apply(simp add:assum_def)
    8.66     apply(simp add:assum_def)
    8.67    apply(erule_tac m="length x" in etran_or_ctran,simp+)
    8.68 -  apply(case_tac x,simp+)
    8.69   apply(case_tac x, (simp add:last_length)+)
    8.70  apply(erule exE)
    8.71  apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
    8.72 @@ -549,18 +548,7 @@
    8.73   apply(erule_tac x="sa" in allE)
    8.74   apply(drule_tac c="drop (Suc m) x" in subsetD)
    8.75    apply simp
    8.76 -  apply(rule conjI)
    8.77 -   apply force
    8.78    apply clarify
    8.79 -  apply(subgoal_tac "(Suc m) + i \<le> length x")
    8.80 -   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
    8.81 -    apply(rotate_tac -2)
    8.82 -    apply simp
    8.83 -    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
    8.84 -    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
    8.85 -    apply arith
    8.86 -   apply arith
    8.87 -  apply arith
    8.88   apply simp
    8.89   apply clarify
    8.90   apply(case_tac "i\<le>m")
    8.91 @@ -569,52 +557,34 @@
    8.92     apply(erule_tac x=i in allE, erule impE, assumption)
    8.93     apply simp+
    8.94   apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
    8.95 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
    8.96 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
    8.97 -    apply(rotate_tac -2)
    8.98 -    apply simp
    8.99 -    apply(erule mp)
   8.100 -    apply arith
   8.101 -   apply arith
   8.102 -  apply arith
   8.103 -  apply(case_tac "length (drop (Suc m) x)",simp)
   8.104 -  apply(erule_tac x="sa" in allE)
   8.105 -  back
   8.106 -  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
   8.107 -   apply(rule conjI)
   8.108 -    apply force
   8.109 -   apply clarify
   8.110 -   apply(subgoal_tac "(Suc m) + i \<le> length x")
   8.111 -    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
   8.112 -     apply(rotate_tac -2)
   8.113 -     apply simp
   8.114 -     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
   8.115 -     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
   8.116 -      apply simp
   8.117 -     apply arith
   8.118 -    apply arith
   8.119 -   apply arith
   8.120 -  apply simp
   8.121 -  apply clarify
   8.122 -  apply(case_tac "i\<le>m")
   8.123 -   apply(drule le_imp_less_or_eq)
   8.124 -   apply(erule disjE)
   8.125 -    apply(erule_tac x=i in allE, erule impE, assumption)
   8.126 -    apply simp
   8.127 + apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   8.128 +  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   8.129 +   apply(rotate_tac -2)
   8.130     apply simp
   8.131 -  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   8.132 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   8.133 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   8.134 -    apply(rotate_tac -2)
   8.135 -    apply simp
   8.136 -    apply(erule mp)
   8.137 -   apply arith
   8.138    apply arith
   8.139   apply arith
   8.140 +apply(case_tac "length (drop (Suc m) x)",simp)
   8.141 +apply(erule_tac x="sa" in allE)
   8.142 +back
   8.143 +apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
   8.144 + apply clarify
   8.145 +apply simp
   8.146 +apply clarify
   8.147 +apply(case_tac "i\<le>m")
   8.148 + apply(drule le_imp_less_or_eq)
   8.149 + apply(erule disjE)
   8.150 +  apply(erule_tac x=i in allE, erule impE, assumption)
   8.151 +  apply simp
   8.152 + apply simp
   8.153 +apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   8.154 +apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   8.155 + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   8.156 +  apply(rotate_tac -2)
   8.157 +  apply simp
   8.158 + apply arith
   8.159 +apply arith
   8.160  done
   8.161  
   8.162 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   8.163 -
   8.164  subsubsection{* Soundness of the Sequential rule *}
   8.165  
   8.166  inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t"
   8.167 @@ -656,7 +626,6 @@
   8.168   apply(simp add:lift_def)
   8.169  apply simp
   8.170  done
   8.171 -
   8.172  declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del]
   8.173  
   8.174  lemma Seq_sound2 [rule_format]: 
   8.175 @@ -714,7 +683,6 @@
   8.176    apply simp+
   8.177  apply(simp add:lift_def)
   8.178  done
   8.179 -
   8.180  (*
   8.181  lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None"
   8.182  apply(simp only:last_length [THEN sym])
   8.183 @@ -737,8 +705,6 @@
   8.184  apply simp
   8.185  done
   8.186  
   8.187 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
   8.188 -
   8.189  lemma Seq_sound: 
   8.190    "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk>
   8.191    \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]"
   8.192 @@ -862,8 +828,6 @@
   8.193        apply simp
   8.194        apply(erule mp)
   8.195        apply(case_tac ys,simp+)
   8.196 -     apply arith
   8.197 -    apply arith
   8.198     apply force
   8.199    apply arith
   8.200   apply force
   8.201 @@ -877,8 +841,6 @@
   8.202   apply(case_tac ys,simp+)
   8.203  done
   8.204  
   8.205 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   8.206 -
   8.207  subsubsection{* Soundness of the While rule *}
   8.208  
   8.209  lemma last_append[rule_format]:
   8.210 @@ -924,8 +886,6 @@
   8.211  apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps)
   8.212  done
   8.213  
   8.214 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
   8.215 -
   8.216  lemma While_sound_aux [rule_format]: 
   8.217    "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
   8.218     stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk> 
   8.219 @@ -1092,8 +1052,6 @@
   8.220  apply simp
   8.221  done
   8.222  
   8.223 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   8.224 -
   8.225  lemma While_sound: 
   8.226    "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely;
   8.227      \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk>
     9.1 --- a/src/HOL/Hyperreal/Integration.thy	Tue Aug 29 21:43:34 2006 +0200
     9.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Aug 30 03:19:08 2006 +0200
     9.3 @@ -173,10 +173,7 @@
     9.4   prefer 2 apply assumption
     9.5  apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
     9.6   prefer 2 apply arith
     9.7 -apply (drule_tac x = "psize D - Suc n" in spec)
     9.8 -ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
     9.9 -apply simp
    9.10 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    9.11 +apply (drule_tac x = "psize D - Suc n" in spec, simp) 
    9.12  done
    9.13  
    9.14  lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
    9.15 @@ -439,8 +436,6 @@
    9.16  apply (simp add: right_diff_distrib)
    9.17  done
    9.18  
    9.19 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
    9.20 -
    9.21  lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
    9.22               ==> Integral(a,b) f' (f(b) - f(a))"
    9.23  apply (drule order_le_imp_less_or_eq, auto) 
    9.24 @@ -472,7 +467,6 @@
    9.25            fine_def)
    9.26  done
    9.27  
    9.28 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
    9.29  
    9.30  lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
    9.31  by simp
    10.1 --- a/src/HOL/Hyperreal/Lim.thy	Tue Aug 29 21:43:34 2006 +0200
    10.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 30 03:19:08 2006 +0200
    10.3 @@ -2239,7 +2239,7 @@
    10.4    thus ?thesis by simp
    10.5  qed
    10.6  
    10.7 -ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
    10.8 +ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
    10.9  
   10.10  lemma LIMSEQ_SEQ_conv2:
   10.11    assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   10.12 @@ -2321,7 +2321,7 @@
   10.13    ultimately show False by simp
   10.14  qed
   10.15  
   10.16 -ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
   10.17 +ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   10.18  
   10.19  lemma LIMSEQ_SEQ_conv:
   10.20    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
    11.1 --- a/src/HOL/Hyperreal/Ln.thy	Tue Aug 29 21:43:34 2006 +0200
    11.2 +++ b/src/HOL/Hyperreal/Ln.thy	Wed Aug 30 03:19:08 2006 +0200
    11.3 @@ -394,7 +394,7 @@
    11.4    apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
    11.5    apply force
    11.6    apply assumption
    11.7 -  apply (simp (asm_lr) add: power2_eq_square mult_compare_simps)
    11.8 +  apply (simp add: power2_eq_square mult_compare_simps)
    11.9    apply (rule mult_imp_div_pos_less)
   11.10    apply (rule mult_pos_pos, assumption, assumption)
   11.11    apply (subgoal_tac "xa * xa = abs xa * abs xa")
   11.12 @@ -408,7 +408,6 @@
   11.13    apply (subst diff_minus [THEN sym])+
   11.14    apply (subst ln_div [THEN sym])
   11.15    apply arith
   11.16 -  apply assumption
   11.17    apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq 
   11.18      add_divide_distrib power2_eq_square)
   11.19    apply (rule mult_pos_pos, assumption)+
    12.1 --- a/src/HOL/Hyperreal/NSA.thy	Tue Aug 29 21:43:34 2006 +0200
    12.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Aug 30 03:19:08 2006 +0200
    12.3 @@ -329,7 +329,7 @@
    12.4  apply (rule InfinitesimalI)
    12.5  apply (drule HFiniteD, clarify)
    12.6  apply (simp only: abs_mult)
    12.7 -apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp)
    12.8 +apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp add: split_if)
    12.9  apply (subgoal_tac "0 < r / t")
   12.10  apply (rule mult_strict_mono)
   12.11  apply (simp add: InfinitesimalD SReal_divide)
    13.1 --- a/src/HOL/Hyperreal/Poly.thy	Tue Aug 29 21:43:34 2006 +0200
    13.2 +++ b/src/HOL/Hyperreal/Poly.thy	Wed Aug 30 03:19:08 2006 +0200
    13.3 @@ -426,6 +426,7 @@
    13.4       "\<forall>p2. length (p1 +++ p2) =
    13.5               (if (length p1 < length p2) then length p2 else length p1)"
    13.6  apply (induct "p1", simp_all)
    13.7 +apply arith
    13.8  done
    13.9  
   13.10  lemma poly_root_mult_length: "length([a,b] *** p) = Suc (length p)"
    14.1 --- a/src/HOL/Hyperreal/Series.thy	Tue Aug 29 21:43:34 2006 +0200
    14.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Aug 30 03:19:08 2006 +0200
    14.3 @@ -323,8 +323,6 @@
    14.4  
    14.5  lemmas sumr_geometric = geometric_sum [where 'a = real]
    14.6  
    14.7 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: needed because otherwise a premise gets simplified away *)
    14.8 -
    14.9  lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))"
   14.10  apply (case_tac "x = 1")
   14.11  apply (auto dest!: LIMSEQ_rabs_realpow_zero2 
   14.12 @@ -335,8 +333,6 @@
   14.13  apply (auto intro: LIMSEQ_const simp add: diff_minus minus_divide_right LIMSEQ_rabs_realpow_zero2)
   14.14  done
   14.15  
   14.16 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   14.17 -
   14.18  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
   14.19  
   14.20  lemma summable_convergent_sumr_iff:
    15.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Tue Aug 29 21:43:34 2006 +0200
    15.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Aug 30 03:19:08 2006 +0200
    15.3 @@ -400,6 +400,8 @@
    15.4  apply (subgoal_tac "0 < \<bar>x ^ n\<bar> ")
    15.5  apply (rule_tac c="\<bar>x ^ n\<bar>" in mult_right_le_imp_le) 
    15.6  apply (auto simp add: mult_assoc power_abs abs_mult)
    15.7 + prefer 2
    15.8 + apply (drule_tac x = 0 in spec, force)
    15.9  apply (auto simp add: power_abs mult_ac)
   15.10  apply (rule_tac a2 = "z ^ n" 
   15.11         in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
   15.12 @@ -576,6 +578,8 @@
   15.13  
   15.14  text{* FIXME: Long proofs*}
   15.15  
   15.16 +ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proofs *)
   15.17 +
   15.18  lemma termdiffs_aux:
   15.19       "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
   15.20      ==> (\<lambda>h. \<Sum>n. c n *
   15.21 @@ -589,56 +593,53 @@
   15.22       and g = "%h n. c (n) * ((( ((x + h) ^ n) - (x ^ n)) * inverse h) 
   15.23                               - (real n * (x ^ (n - Suc 0))))" 
   15.24         in lemma_termdiff5)
   15.25 -  -- "3 subgoals"
   15.26 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
   15.27 -  apply (auto simp add: add_commute)
   15.28 - apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
   15.29 -  apply (rule_tac [2] x = K in powser_insidea, auto)
   15.30 - apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
   15.31 -  apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
   15.32 - apply (simp add: diffs_def mult_assoc [symmetric])
   15.33 - apply (subgoal_tac
   15.34 -         "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
   15.35 -               = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
   15.36 -  apply (auto simp add: abs_mult)
   15.37 -   apply (drule diffs_equiv)
   15.38 -   apply (drule sums_summable)
   15.39 -   apply (simp_all add: diffs_def)
   15.40 - apply (simp add: diffs_def mult_ac)
   15.41 - 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))")
   15.42 -  apply auto
   15.43 +apply (auto simp add: add_commute)
   15.44 +apply (subgoal_tac "summable (%n. \<bar>diffs (diffs c) n\<bar> * (r ^ n))")
   15.45 +apply (rule_tac [2] x = K in powser_insidea, auto)
   15.46 +apply (subgoal_tac [2] "\<bar>r\<bar> = r", auto)
   15.47 +apply (rule_tac [2] y1 = "\<bar>x\<bar>" in order_trans [THEN abs_of_nonneg], auto)
   15.48 +apply (simp add: diffs_def mult_assoc [symmetric])
   15.49 +apply (subgoal_tac
   15.50 +        "\<forall>n. real (Suc n) * real (Suc (Suc n)) * \<bar>c (Suc (Suc n))\<bar> * (r ^ n) 
   15.51 +              = diffs (diffs (%n. \<bar>c n\<bar>)) n * (r ^ n) ") 
   15.52 +apply (auto simp add: abs_mult)
   15.53 +apply (drule diffs_equiv)
   15.54 +apply (drule sums_summable)
   15.55 +apply (simp_all add: diffs_def) 
   15.56 +apply (simp add: diffs_def mult_ac)
   15.57 +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))")
   15.58 +apply auto
   15.59    prefer 2
   15.60    apply (rule ext)
   15.61 -  apply (simp add: diffs_def)
   15.62 +  apply (simp add: diffs_def) 
   15.63    apply (case_tac "n", auto)
   15.64  txt{*23*}
   15.65     apply (drule abs_ge_zero [THEN order_le_less_trans])
   15.66 -   apply (simp add: mult_ac)
   15.67 +   apply (simp add: mult_ac) 
   15.68    apply (drule abs_ge_zero [THEN order_le_less_trans])
   15.69 -  apply (simp add: mult_ac)
   15.70 +  apply (simp add: mult_ac) 
   15.71   apply (drule diffs_equiv)
   15.72   apply (drule sums_summable)
   15.73 - apply (subgoal_tac
   15.74 -           "summable
   15.75 -             (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
   15.76 -                  r ^ (n - Suc 0)) =
   15.77 -            summable
   15.78 -             (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
   15.79 -  apply simp
   15.80 - apply (rule_tac f = summable in arg_cong, rule ext)
   15.81 +apply (subgoal_tac
   15.82 +          "summable
   15.83 +            (\<lambda>n. real n * (real (n - Suc 0) * \<bar>c n\<bar> * inverse r) *
   15.84 +                 r ^ (n - Suc 0)) =
   15.85 +           summable
   15.86 +            (\<lambda>n. real n * (\<bar>c n\<bar> * (real (n - Suc 0) * r ^ (n - 2))))")
   15.87 +apply simp 
   15.88 +apply (rule_tac f = summable in arg_cong, rule ext)
   15.89  txt{*33*}
   15.90 - apply (case_tac "n", auto)
   15.91 - apply (case_tac "nat", auto)
   15.92 - apply (drule abs_ge_zero [THEN order_le_less_trans], auto)
   15.93 +apply (case_tac "n", auto)
   15.94 +apply (case_tac "nat", auto)
   15.95 +apply (drule abs_ge_zero [THEN order_le_less_trans], auto) 
   15.96  apply (drule abs_ge_zero [THEN order_le_less_trans])
   15.97  apply (simp add: mult_assoc)
   15.98  apply (rule mult_left_mono)
   15.99 - prefer 2 apply arith
  15.100 + prefer 2 apply arith 
  15.101  apply (subst add_commute)
  15.102  apply (simp (no_asm) add: mult_assoc [symmetric])
  15.103  apply (rule lemma_termdiff3)
  15.104 -  apply (auto intro: abs_triangle_ineq [THEN order_trans])
  15.105 -apply arith
  15.106 +apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
  15.107  done
  15.108  
  15.109  ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
  15.110 @@ -655,7 +656,7 @@
  15.111  apply (simp add: LIM_def, safe)
  15.112  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
  15.113  apply (auto simp add: less_diff_eq)
  15.114 -apply (frule abs_triangle_ineq [THEN order_le_less_trans])
  15.115 +apply (drule abs_triangle_ineq [THEN order_le_less_trans])
  15.116  apply (rule_tac y = 0 in order_le_less_trans, auto)
  15.117  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))")
  15.118  apply (auto intro!: summable_sums)
  15.119 @@ -667,11 +668,11 @@
  15.120  apply (simp add: diff_def divide_inverse add_ac mult_ac)
  15.121  apply (rule LIM_zero_cancel)
  15.122  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)
  15.123 - prefer 2 apply (blast intro: termdiffs_aux)
  15.124 + prefer 2 apply (blast intro: termdiffs_aux) 
  15.125  apply (simp add: LIM_def, safe)
  15.126  apply (rule_tac x = "\<bar>K\<bar> - \<bar>x\<bar>" in exI)
  15.127  apply (auto simp add: less_diff_eq)
  15.128 -apply (frule abs_triangle_ineq [THEN order_le_less_trans])
  15.129 +apply (drule abs_triangle_ineq [THEN order_le_less_trans])
  15.130  apply (rule_tac y = 0 in order_le_less_trans, auto)
  15.131  apply (subgoal_tac "summable (%n. (diffs c) (n) * (x ^ n))")
  15.132  apply (rule_tac [2] powser_inside, auto)
  15.133 @@ -2580,5 +2581,5 @@
  15.134  apply (drule_tac [3] LIM_fun_gt_zero)
  15.135  apply force+
  15.136  done
  15.137 -
  15.138 +  
  15.139  end 
    16.1 --- a/src/HOL/Import/HOL4Compat.thy	Tue Aug 29 21:43:34 2006 +0200
    16.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Aug 30 03:19:08 2006 +0200
    16.3 @@ -221,7 +221,7 @@
    16.4    by simp
    16.5  
    16.6  lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
    16.7 -  by simp
    16.8 +  by (simp, arith)
    16.9  
   16.10  lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   16.11    by (simp add: max_def)
    17.1 --- a/src/HOL/Integ/IntDef.thy	Tue Aug 29 21:43:34 2006 +0200
    17.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Aug 30 03:19:08 2006 +0200
    17.3 @@ -387,7 +387,7 @@
    17.4  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    17.5  proof -
    17.6    have "(\<lambda>(x,y). {x-y}) respects intrel"
    17.7 -    by (simp add: congruent_def)
    17.8 +    by (simp add: congruent_def) arith
    17.9    thus ?thesis
   17.10      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   17.11  qed
    18.1 --- a/src/HOL/Isar_examples/HoareEx.thy	Tue Aug 29 21:43:34 2006 +0200
    18.2 +++ b/src/HOL/Isar_examples/HoareEx.thy	Wed Aug 30 03:19:08 2006 +0200
    18.3 @@ -317,6 +317,7 @@
    18.4        apply simp
    18.5       apply clarsimp
    18.6      apply clarsimp
    18.7 +   apply arith
    18.8     prefer 2
    18.9     apply clarsimp
   18.10    apply (clarsimp simp: nat_distrib)
    19.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Tue Aug 29 21:43:34 2006 +0200
    19.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Aug 30 03:19:08 2006 +0200
    19.3 @@ -934,10 +934,11 @@
    19.4    apply (subst Rep_matrix_inject[symmetric])
    19.5    apply (rule ext)+
    19.6    apply (case_tac "j + int u < 0")
    19.7 -  apply simp
    19.8 +  apply (simp, arith)
    19.9    apply (case_tac "i + int v < 0")
   19.10 +  apply (simp add: neg_def, arith)
   19.11    apply (simp add: neg_def)
   19.12 -  apply (simp add: neg_def)
   19.13 +  apply arith
   19.14    done
   19.15  
   19.16  lemma Rep_take_columns[simp]:
    20.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Tue Aug 29 21:43:34 2006 +0200
    20.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 30 03:19:08 2006 +0200
    20.3 @@ -338,12 +338,17 @@
    20.4      apply (subst Rep_matrix_mult)
    20.5      apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
    20.6      apply (simp_all)
    20.7 +    apply (intro strip, rule conjI)
    20.8      apply (intro strip)
    20.9 +    apply (drule_tac max_helper)
   20.10 +    apply (simp)
   20.11 +    apply (auto)
   20.12      apply (rule zero_imp_mult_zero)
   20.13      apply (rule disjI2)
   20.14      apply (rule nrows)
   20.15      apply (rule order_trans[of _ 1])
   20.16 -    apply auto
   20.17 +    apply (simp)
   20.18 +    apply (simp)
   20.19      done
   20.20  qed
   20.21  
    21.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Aug 29 21:43:34 2006 +0200
    21.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Wed Aug 30 03:19:08 2006 +0200
    21.3 @@ -968,14 +968,14 @@
    21.4  apply fast
    21.5  apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
    21.6  apply (simp, rule conjI, (rule HOL.refl)+)
    21.7 -apply simp
    21.8 +apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
    21.9  apply (rule progression_refl)
   21.10  
   21.11   (* case b= False *)
   21.12  apply simp
   21.13  apply (rule_tac ?instrs1.0 = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
   21.14  apply (simp, rule conjI, (rule HOL.refl)+)
   21.15 -apply simp
   21.16 +apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   21.17  apply fast
   21.18  
   21.19  (* case exit Loop *)
   21.20 @@ -1003,7 +1003,7 @@
   21.21  apply fast
   21.22  apply (rule_tac ?instrs1.0 = "[]" in jump_fwd_progression)
   21.23  apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
   21.24 -apply simp
   21.25 +apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
   21.26  apply (rule progression_refl)
   21.27  
   21.28  
    22.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Aug 29 21:43:34 2006 +0200
    22.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Aug 30 03:19:08 2006 +0200
    22.3 @@ -663,7 +663,7 @@
    22.4    (* show P x of bspec *)
    22.5  apply simp
    22.6    apply (subgoal_tac "length mt_pre \<le> pc'")
    22.7 -  apply (simp add: nth_append)
    22.8 +  apply (simp add: nth_append) apply arith
    22.9  
   22.10    (* subgoals *)
   22.11  apply (simp add: eff_def xcpt_eff_def)
   22.12 @@ -965,6 +965,7 @@
   22.13  apply (simp only:)
   22.14  apply (rule check_type_mono) apply assumption
   22.15  apply (simp (no_asm_simp)  add: max_ssize_def max_of_list_append max_ac)
   22.16 +apply arith
   22.17  apply (simp add: nth_append)
   22.18  
   22.19  apply (erule conjE)+
   22.20 @@ -1282,7 +1283,6 @@
   22.21    apply auto
   22.22    done
   22.23  
   22.24 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
   22.25  
   22.26  lemma bc_mt_corresp_Invoke: "\<lbrakk> wf_prog wf_mb G; 
   22.27    max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
   22.28 @@ -1319,7 +1319,6 @@
   22.29  apply (simp add: max_def)
   22.30    done
   22.31  
   22.32 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   22.33  
   22.34  lemma wt_instr_Ifcmpeq: "\<lbrakk>Suc pc < max_pc; 
   22.35    0 \<le> (int pc + i);  nat (int pc + i) < max_pc;
   22.36 @@ -1644,7 +1643,7 @@
   22.37  done
   22.38  
   22.39  
   22.40 -ML {* fast_arith_split_limit := 0; *}  (* FIXME: rewrite proof *)
   22.41 +
   22.42  
   22.43  lemma wt_method_compTpExpr_Exprs_corresp: "
   22.44    \<lbrakk> jmb = (pns,lvars,blk,res); 
   22.45 @@ -1923,7 +1922,6 @@
   22.46  
   22.47  done
   22.48  
   22.49 -ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   22.50  
   22.51  lemmas wt_method_compTpExpr_corresp [rule_format (no_asm)] = 
   22.52    wt_method_compTpExpr_Exprs_corresp [THEN conjunct1]
    23.1 --- a/src/HOL/NumberTheory/Chinese.thy	Tue Aug 29 21:43:34 2006 +0200
    23.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Wed Aug 30 03:19:08 2006 +0200
    23.3 @@ -175,6 +175,11 @@
    23.4       apply (rule_tac [!] funprod_zgcd)
    23.5       apply safe
    23.6       apply simp_all
    23.7 +   apply (subgoal_tac "i<n")
    23.8 +    prefer 2
    23.9 +    apply arith
   23.10 +   apply (case_tac [2] i)
   23.11 +    apply simp_all
   23.12    done
   23.13  
   23.14  lemma x_sol_lin_aux:
    24.1 --- a/src/HOL/NumberTheory/Fib.thy	Tue Aug 29 21:43:34 2006 +0200
    24.2 +++ b/src/HOL/NumberTheory/Fib.thy	Wed Aug 30 03:19:08 2006 +0200
    24.3 @@ -72,6 +72,7 @@
    24.4     apply (simp add: fib.Suc_Suc mod_Suc)
    24.5    apply (simp add: fib.Suc_Suc add_mult_distrib add_mult_distrib2
    24.6                     mod_Suc zmult_int [symmetric])
    24.7 +  apply (presburger (no_abs))
    24.8    done
    24.9  
   24.10  text{*We now obtain a version for the natural numbers via the coercion 
    25.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Aug 29 21:43:34 2006 +0200
    25.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Aug 30 03:19:08 2006 +0200
    25.3 @@ -193,8 +193,6 @@
    25.4    then show ?thesis by auto
    25.5  qed
    25.6  
    25.7 -ML {* fast_arith_split_limit := 0; *} (*FIXME*)
    25.8 -
    25.9  lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
   25.10      (p * b \<noteq> q * a)"
   25.11  proof
   25.12 @@ -236,8 +234,6 @@
   25.13    with q_g_2 show False by auto
   25.14  qed
   25.15  
   25.16 -ML {* fast_arith_split_limit := 9; *} (*FIXME*)
   25.17 -
   25.18  lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   25.19    using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
   25.20