# HG changeset patch
# User webertj
# Date 1153934584 -7200
# Node ID 25b068a99d2b22319c1962c8946ab5c35523b9eb
# Parent  f30b733850602ad56f7b539acbade6f151f9d286
linear arithmetic splits certain operators (e.g. min, max, abs)

diff -r f30b73385060 -r 25b068a99d2b NEWS
--- a/NEWS	Wed Jul 26 13:31:07 2006 +0200
+++ b/NEWS	Wed Jul 26 19:23:04 2006 +0200
@@ -510,6 +510,12 @@
   (i.e. a boolean expression) by compiling it to ML. The goal is
   "proved" (via the oracle "Evaluation") if it evaluates to True.
 
+* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
+when invoked by the simplifier.  This results in the simplifier being more
+powerful on arithmetic goals.
+INCOMPATIBILTY: rewrite proofs.  Set fast_arith_split_limit to 0 to obtain
+the old behavior.
+
 * Support for hex (0x20) and binary (0b1001) numerals. 
 
 *** HOL-Algebra ***
diff -r f30b73385060 -r 25b068a99d2b doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -90,19 +90,10 @@
 
 \noindent
 The inclusion remains to be proved. After unfolding some definitions, 
-we are left with simple arithmetic:
+we are left with simple arithmetic that is dispatched automatically.
 *}
 
-apply (clarify, simp add: measure_def inv_image_def)
-
-txt{*
-@{subgoals[display,indent=0,margin=65]}
-
-\noindent
-And that is dispatched automatically:
-*}
-
-by arith
+by (clarify, simp add: measure_def inv_image_def)
 
 text{*\noindent
 
diff -r f30b73385060 -r 25b068a99d2b doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 13:31:07 2006 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 19:23:04 2006 +0200
@@ -119,22 +119,11 @@
 
 \noindent
 The inclusion remains to be proved. After unfolding some definitions, 
-we are left with simple arithmetic:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
-\end{isabelle}
-
-\noindent
-And that is dispatched automatically:%
+we are left with simple arithmetic that is dispatched automatically.%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{by}\isamarkupfalse%
-\ arith%
+\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -972,13 +972,13 @@
     next
       case (Suc j)
       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
-        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg])
       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
-        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg])
       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
         using Suc by (auto intro!: funcset_mem [OF Rf])
       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
-        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
+        using Suc by (auto intro!: funcset_mem [OF Rg])
       have R11: "g 0 \<in> carrier R"
         using Suc by (auto intro!: funcset_mem [OF Rg])
       from Suc show ?case
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -231,7 +231,7 @@
 "greatest_msg other = 0"
 
 lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
-by (induct X, auto, arith+)
+by (induct X, auto)
 
 subsubsection{*sets of keys*}
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Auth/Guard/Guard_Public.thy
--- a/src/HOL/Auth/Guard/Guard_Public.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -95,7 +95,7 @@
 apply (induct evs, auto simp: initState.simps)
 apply (drule used_sub_parts_used, safe)
 apply (drule greatest_msg_is_greatest, arith)
-by (simp, arith)
+by simp
 
 subsubsection{*function giving a new nonce*}
 
@@ -171,4 +171,4 @@
 apply (frule_tac A=A in priK_analz_iff_bad)
 by (simp add: knows_decomp)+
 
-end
\ No newline at end of file
+end
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1421,7 +1421,6 @@
 apply (drule finite_subset)
 apply (erule finite_imageI)
 apply auto
-apply arith
 done
 
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Binomial.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -33,9 +33,8 @@
 by simp
 
 lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
-apply (induct "n", auto)
-apply (erule allE)
-apply (erule mp, arith)
+apply (induct "n")
+apply auto
 done
 
 declare binomial_0 [simp del] binomial_Suc [simp del]
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -178,7 +178,7 @@
 apply (simp add: CInfinitesimal_hcmod_iff star_of_def
             Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod,  blast)
 apply (drule_tac x = r in spec, clarify)
-apply (drule FreeUltrafilterNat_all, ultra, arith)
+apply (drule FreeUltrafilterNat_all, ultra)
 done
 
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -710,8 +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 arith
+  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 f30b73385060 -r 25b068a99d2b src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -126,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)
@@ -154,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
@@ -175,24 +173,16 @@
  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
 
 
@@ -253,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
diff -r f30b73385060 -r 25b068a99d2b src/HOL/HoareParallel/OG_Examples.thy
--- a/src/HOL/HoareParallel/OG_Examples.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -298,7 +298,6 @@
 --{* 98 verification conditions *}
 apply auto 
 --{* auto takes about 3 minutes !! *}
-apply arith+
 done
 
 text {* Easier Version: without AWAIT.  Apt and Olderog. page 256: *}
@@ -332,7 +331,6 @@
 --{* 20 vc *}
 apply auto
 --{* auto takes aprox. 2 minutes. *}
-apply arith+
 done
 
 subsection {* Producer/Consumer *}
diff -r f30b73385060 -r 25b068a99d2b src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -361,11 +361,8 @@
 apply clarify
 apply(frule_tac j=0 and k="j" and p=pre in stability)
       apply simp_all
-    apply arith
   apply(erule_tac x=i in allE,simp)
  apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
-  apply arith
- apply arith
 apply(case_tac "x!j")
 apply clarify
 apply simp
@@ -492,11 +489,8 @@
 apply(simp add:assum_def)
 apply clarify
 apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
-   apply arith
   apply(erule_tac x=i in allE,simp)
  apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
-  apply arith
- apply arith
 apply(case_tac "x!j")
 apply clarify
 apply simp
@@ -543,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)
@@ -555,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")
@@ -575,49 +557,33 @@
    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
- done  
+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
 
 subsubsection{* Soundness of the Sequential rule *}
 
@@ -862,8 +828,6 @@
       apply simp
       apply(erule mp)
       apply(case_tac ys,simp+)
-     apply arith
-    apply arith
    apply force
   apply arith
  apply force
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -364,7 +364,7 @@
 apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
 apply (rule bexI [OF _ Rep_star_star_n], auto)
 apply (rule_tac x = "exp u" in exI)
-apply (ultra, arith)
+apply ultra
 done
 
 lemma starfun_exp_add_HFinite_Infinitesimal_approx:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -323,7 +323,6 @@
 apply (drule add_strict_mono, assumption)
 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
                 mult_less_cancel_right)
-apply arith
 done
 
 lemma Integral_zero [simp]: "Integral(a,a) f 0"
@@ -423,7 +422,7 @@
                      \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
        in order_trans)
 apply (rule abs_triangle_ineq [THEN [2] order_trans])
-apply (simp add: right_diff_distrib, arith)
+apply (simp add: right_diff_distrib)
 apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
 apply (rule add_mono)
 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
@@ -434,7 +433,7 @@
 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
 apply (rule order_trans)
 apply (auto simp add: abs_le_interval_iff)
-apply (simp add: right_diff_distrib, arith)
+apply (simp add: right_diff_distrib)
 done
 
 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
@@ -577,7 +576,7 @@
 apply (auto dest: partition_lt_cancel)
 apply (rule_tac x=N and y=n in linorder_cases)
 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
-apply (drule_tac n = n in partition_lt_gen, auto, arith)
+apply (drule_tac n = n in partition_lt_gen, auto)
 apply (drule_tac x = n in spec)
 apply (simp split: split_if_asm)
 done
@@ -741,7 +740,6 @@
       ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
 apply (simp add: tpart_def partition_def, safe)
 apply (rule_tac x = "N - n" in exI, auto)
-apply (drule_tac x = "na + n" in spec, arith)+
 done
 
 lemma fine_right1:
@@ -752,7 +750,7 @@
       ==> fine ga (%x. D(x + n),%x. p(x + n))"
 apply (auto simp add: fine_def gauge_def)
 apply (drule_tac x = "na + n" in spec)
-apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
+apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
 apply (simp add: tpart_def, safe)
 apply (subgoal_tac "D n \<le> p (na + n)")
 apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
@@ -783,7 +781,7 @@
 apply ((drule spec)+, auto)
 apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
 apply (auto simp only: rsum_add left_distrib [symmetric]
-                mult_2_right [symmetric] real_mult_less_iff1, arith)
+                mult_2_right [symmetric] real_mult_less_iff1)
 done
 
 lemma partition_lt_gen2:
@@ -834,7 +832,7 @@
 apply arith
 apply (drule add_strict_mono, assumption)
 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
-                       real_mult_less_iff1, arith)
+                       real_mult_less_iff1)
 done
 
 lemma Integral_imp_Cauchy:
@@ -853,7 +851,7 @@
 apply (erule_tac V = "0 < e" in thin_rl)
 apply (drule add_strict_mono, assumption)
 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
-                       real_mult_less_iff1, arith)
+                       real_mult_less_iff1)
 done
 
 lemma Cauchy_iff2:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1484,7 +1484,7 @@
 apply (rule_tac x = s in exI, clarify)
 apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
 apply (drule_tac x = "xa-x" in spec)
-apply (auto simp add: abs_ge_self, arith+)
+apply (auto simp add: abs_ge_self)
 done
 
 text{*Refine the above to existence of least upper bound*}
@@ -2236,6 +2236,8 @@
   thus ?thesis by simp
 qed
 
+ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
+
 lemma LIMSEQ_SEQ_conv2:
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   shows "X -- a --> L"
@@ -2316,6 +2318,7 @@
   ultimately show False by simp
 qed
 
+ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
 
 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 f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -390,7 +390,7 @@
 
 lemma mod_exhaust_less_4:
      "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
-by (case_tac "m mod 4", auto, arith)
+by auto
 
 lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
      "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1349,7 +1349,8 @@
       ==> hypreal_of_real x + u < hypreal_of_real y"
 apply (simp add: Infinitesimal_def)
 apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
-apply (simp add: abs_less_iff)
+(* FIXME: arith simproc bug with   apply (simp add: abs_less_iff) *)
+apply simp
 done
 
 lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1023,7 +1023,7 @@
 apply (induct "p", auto)
 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
 apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult, arith)
+apply (auto intro!: mult_mono simp add: abs_mult)
 done
 
 end
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -745,7 +745,6 @@
 apply (simp add: Bseq_def, safe)
 apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
 apply auto
-apply arith
 apply (rule_tac x = N in exI, safe)
 apply (drule_tac x = n in spec, arith)
 apply (auto simp add: Bseq_iff2)
@@ -754,7 +753,7 @@
 lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
 apply (simp add: Bseq_def)
 apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
-apply (drule_tac [2] x = n in spec, arith+)
+apply (drule_tac x = n in spec, arith)
 done
 
 
@@ -824,9 +823,7 @@
 
 lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
           ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
-apply safe
-apply (drule spec, auto, arith)
-done
+by auto
 
 lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
 by auto
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -274,10 +274,6 @@
 apply (induct "no", auto)
 apply (drule_tac x = "Suc no" in spec)
 apply (simp add: add_ac)
-(* FIXME why does simp require a separate step to prove the (pure arithmetic)
-   left-over? With del cong: strong_setsum_cong it works!
-*)
-apply simp
 done
 
 lemma sumr_pos_lt_pair:
@@ -299,15 +295,7 @@
 apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
 prefer 3 apply assumption
 apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
-apply simp_all 
-apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
-apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
-prefer 3 apply simp
-apply (drule_tac [2] x = 0 in spec)
- prefer 2 apply simp 
-apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
-apply (simp add: abs_if)
-apply (auto simp add: linorder_not_less [symmetric])
+apply simp_all
 done
 
 text{*A summable series of positive terms has limit that is at least as
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -526,7 +526,7 @@
 apply (rule setsum_abs [THEN real_le_trans])
 apply (rule real_setsum_nat_ivl_bounded)
 apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
-apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
+apply (auto intro!: power_mono zero_le_power simp add: power_abs)
 done
 
 lemma lemma_termdiff4: 
@@ -576,9 +576,10 @@
 done
 
 
-
 text{* FIXME: Long proofs*}
 
+ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; 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 *
@@ -641,6 +642,8 @@
 apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
 done
 
+ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
+
 lemma termdiffs: 
     "[| summable(%n. c(n) * (K ^ n));  
         summable(%n. (diffs c)(n) * (K ^ n));  
@@ -748,7 +751,7 @@
 apply (subst lemma_exp_ext)
 apply (subgoal_tac "DERIV (%u. \<Sum>n. inverse (real (fact n)) * u ^ n) x :> (\<Sum>n. diffs (%n. inverse (real (fact n))) n * x ^ n)")
 apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
+apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs)
 done
 
 lemma lemma_sin_ext:
@@ -769,14 +772,14 @@
 apply (subst lemma_sin_ext)
 apply (auto simp add: sin_fdiffs2 [symmetric])
 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
+apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
 done
 
 lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
 apply (subst lemma_cos_ext)
 apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
 apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
-apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
+apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
 done
 
 
@@ -2533,7 +2536,7 @@
 apply (rule_tac x = ea in exI, auto)
 apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)
 apply auto
-apply (drule sym, auto, arith)
+apply (drule sym, auto)
 done
 
 lemma isCont_inv_fun_inv:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -101,7 +101,6 @@
 apply(rule ccontr)
 apply(drule_tac f = length in arg_cong)
 apply simp
-apply arith
 done
 
 lemma reduce_exec1:
@@ -293,6 +292,6 @@
   with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
 qed
 
-(* To Do: connect with Machine 0 using M_equiv *)
+(* TODO: connect with Machine 0 using M_equiv *)
 
-end
\ No newline at end of file
+end
diff -r f30b73385060 -r 25b068a99d2b src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMP/Machines.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -168,11 +168,10 @@
     apply fastsimp
    apply simp
   apply simp
-  apply arith
  apply simp
- apply arith
 apply(fastsimp simp add:exec01.JMPB)
 done
+
 (*
 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
 apply(induct xs)
@@ -188,6 +187,7 @@
 apply simp_all
 done
 *)
+
 lemma direction2:
  "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
   rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
diff -r f30b73385060 -r 25b068a99d2b src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMPP/Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -381,7 +381,6 @@
 apply (drule finite_subset)
 apply (erule finite_imageI)
 apply (simp (no_asm_simp))
-apply arith
 done
 
 lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>  
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -324,9 +324,6 @@
 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
        in int_val_lemma)
 apply simp
-apply (erule impE)
- apply (intro strip)
- apply (erule_tac x = "i+m" in allE, arith)
 apply (erule exE)
 apply (rule_tac x = "i+m" in exI, arith)
 done
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Jul 26 19:23:04 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, arith) 
+    by (simp add: congruent_def, arith)
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -88,12 +88,11 @@
 
 text{*Suggested by Matthias Daum*}
 lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x") 
- apply (simp add: nat_div_distrib [symmetric])
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
 apply (rule Divides.div_less_dividend, simp_all) 
 done
 
-
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
 (*"neg" is used in rewrite rules for binary comparisons*)
@@ -148,7 +147,6 @@
          else let d = z-z' in     
               if neg d then 0 else nat d)"
 apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
-apply (simp add: diff_is_0_eq nat_le_eq_zle)
 done
 
 lemma diff_nat_number_of [simp]: 
@@ -628,7 +626,6 @@
 
 lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
-  apply (simp add: neg_nat)
   done
 
 lemma nat_number_of_BIT_1:
@@ -676,7 +673,7 @@
 by (simp only: mult_2 nat_add_distrib of_nat_add) 
 
 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
-by (simp only:  nat_number_of_def, simp)
+by (simp only: nat_number_of_def)
 
 lemma of_nat_number_of_lemma:
      "of_nat (number_of v :: nat) =  
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Integ/Presburger.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -558,17 +558,13 @@
 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
 apply(induct rule: int_gr_induct)
  apply simp
- apply arith
 apply (simp add:int_distrib)
-apply arith
 done
 
 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
 apply(induct rule: int_gr_induct)
  apply simp
- apply arith
 apply (simp add:int_distrib)
-apply arith
 done
 
 lemma  minusinfinity:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -50,8 +50,7 @@
 lemma free_lift [simp]:
     "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
   apply (induct t fixing: i k)
-    apply (auto cong: conj_cong)
-  apply arith
+  apply (auto cong: conj_cong)
   done
 
 lemma free_subst [simp]:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Library/Word.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1383,7 +1383,7 @@
 proof (rule ccontr)
   from w0 wk
   have k1: "1 < k"
-    by (cases "k - 1",simp_all,arith)
+    by (cases "k - 1",simp_all)
   assume "~ length (int_to_bv i) \<le> k"
   hence "k < length (int_to_bv i)"
     by simp
@@ -1512,7 +1512,7 @@
 proof (rule ccontr)
   from w1 wk
   have k1: "1 < k"
-    by (cases "k - 1",simp_all,arith)
+    by (cases "k - 1",simp_all)
   assume "~ length (int_to_bv i) \<le> k"
   hence "k < length (int_to_bv i)"
     by simp
@@ -1731,8 +1731,6 @@
   have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le> 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
     apply (cases "length w1 \<le> length w2")
     apply (auto simp add: max_def)
-    apply arith
-    apply arith
     done
   also have "... = 2 ^ max (length w1) (length w2)"
   proof -
@@ -1982,7 +1980,6 @@
           apply simp
           apply (subst zpower_zadd_distrib [symmetric])
           apply simp
-          apply arith
           done
         finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
           .
@@ -2030,10 +2027,6 @@
         apply simp
         apply (subst zpower_zadd_distrib [symmetric])
         apply simp
-        apply (cut_tac lmw)
-        apply arith
-        apply (cut_tac p)
-        apply arith
         done
       hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
         by simp
@@ -2278,13 +2271,13 @@
   by (simp add: bv_chop_def Let_def)
 
 lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
-  by (simp add: bv_chop_def Let_def,arith)
+  by (simp add: bv_chop_def Let_def)
 
 lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
-  by (simp add: bv_chop_def Let_def,arith)
+  by (simp add: bv_chop_def Let_def)
 
 lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
-  by (auto simp add: bv_slice_def,arith)
+  by (auto simp add: bv_slice_def)
 
 definition
   length_nat :: "nat => nat"
@@ -2337,7 +2330,6 @@
     apply (drule norm_empty_bv_to_nat_zero)
     using prems
     apply simp
-    apply arith
     apply (cases "norm_unsigned (nat_to_bv (nat i))")
     apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
     using prems
@@ -2439,7 +2431,6 @@
     apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
     apply simp_all
     apply (simp_all add: w_defs min_def)
-    apply arith+
     done
 qed
 
@@ -2514,11 +2505,7 @@
 lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
   by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
 
-lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
-  apply (cases "y = 0",simp_all add: length_int_lt0)
-  apply (subgoal_tac "nat (- y) - Suc 0 \<le> nat (- x) - Suc 0")
-  apply (simp add: length_nat_mono)
-  apply arith
+lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"  apply (cases "y = 0",simp_all add: length_int_lt0)
   done
 
 lemmas [simp] = length_nat_non0
diff -r f30b73385060 -r 25b068a99d2b src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/List.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1691,7 +1691,6 @@
 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
 apply(induct j)
 apply auto
-apply arith
 done
 
 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -994,8 +994,6 @@
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: prems)+
   apply (auto)
-  apply (insert ncols_le[of A j])
-  apply (arith)
   proof -
     fix k
     fix l
diff -r f30b73385060 -r 25b068a99d2b src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -454,8 +454,10 @@
 apply (simp add: max_of_list_def)
 apply (induct xs)
 apply simp
+ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
 apply simp
 apply arith
+ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
 done
 
 
@@ -520,16 +522,7 @@
 lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
  \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
 apply (induct i)
-apply simp+
-  (* case Goto *)
-apply arith
-  (* case Ifcmpeq *)
-apply simp
-apply (erule disjE)
-apply arith
-apply arith
-  (* case Throw *)
-apply simp
+apply (arith|simp)+
 done
 
 
@@ -537,16 +530,7 @@
   \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> 
   \<Longrightarrow> n \<le> pc'"
 apply (induct i)
-apply simp+
-  (* case Goto *)
-apply arith
-  (* case Ifcmpeq *)
-apply simp
-apply (erule disjE)
-apply simp
-apply arith
-  (* case Throw *)
-apply simp
+apply (arith|simp)+
 done
 
 
@@ -975,7 +959,6 @@
 apply (simp (no_asm_simp))+
 apply simp
 apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
-apply (simp (no_asm_simp))+
 
   (* show check_type \<dots> *)
 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -2100,7 +2083,6 @@
   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
   apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
     (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
-  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
   apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
   apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
   apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -179,10 +179,6 @@
 lemma int_card_bdd_int_set_l_l: "0 < n ==>
     int(card {x. 0 < x & x < n}) = n - 1"
   apply (auto simp add: card_bdd_int_set_l_l)
-  apply (subgoal_tac "Suc 0 \<le> nat n")
-   apply (auto simp add: zdiff_int [symmetric])
-  apply (subgoal_tac "0 < nat n", arith)
-  apply (simp add: zero_less_nat_eq)
   done
 
 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Gauss.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -104,8 +104,6 @@
   apply (auto simp add: A_def ResSet_def)
   apply (rule_tac m = p in zcong_less_eq)
   apply (insert p_g_2, auto)
-  apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
-  apply (auto, auto simp add: p_minus_one_l)
   done
 
 lemma (in GAUSS) B_res: "ResSet p B"
@@ -255,6 +253,8 @@
 lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   by (auto simp add: D_eq)
 
+ML {* fast_arith_split_limit := 0; *} (*FIXME*)
+
 lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   apply (auto simp add: F_eq A_def)
 proof -
@@ -270,6 +270,8 @@
     using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
 qed
 
+ML {* fast_arith_split_limit := 9; *} (*FIXME*)
+
 lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Int2.thy
--- a/src/HOL/NumberTheory/Int2.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Int2.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -191,7 +191,7 @@
   have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
     by auto
   also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
-    by (simp only: nat_add_distrib, auto)
+    by (simp only: nat_add_distrib)
   also have "p - 2 + 1 = p - 1" by arith
   finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
     by (rule ssubst, auto)
diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Quadratic_Reciprocity.thy
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -193,6 +193,8 @@
   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
@@ -234,6 +236,8 @@
   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)
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Presburger.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -558,17 +558,13 @@
 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
 apply(induct rule: int_gr_induct)
  apply simp
- apply arith
 apply (simp add:int_distrib)
-apply arith
 done
 
 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
 apply(induct rule: int_gr_induct)
  apply simp
- apply arith
 apply (simp add:int_distrib)
-apply arith
 done
 
 lemma  minusinfinity:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/Float.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -28,9 +28,7 @@
     apply (auto, induct_tac n)
     apply (simp_all add: pow2_def)
     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
-    apply (auto simp add: h)
-    apply arith
-    done
+    by (auto simp add: h)
   show ?thesis
   proof (induct a)
     case (1 n)
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1066,10 +1066,7 @@
   apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply simp
-  apply (subst nat_diff_distrib)
   apply simp
-  apply (rule le_floor)
-  apply simp_all
 done
 
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
@@ -1206,13 +1203,7 @@
   apply (subgoal_tac "real a = real (int a)")
   apply (erule ssubst)
   apply simp
-  apply (subst nat_diff_distrib)
   apply simp
-  apply (rule order_trans)
-  prefer 2
-  apply (rule ceiling_mono2)
-  apply assumption
-  apply simp_all
 done
 
 lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Real/RealDef.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -1024,15 +1024,9 @@
 by (simp add: real_of_nat_ge_zero)
 
 lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
-apply (simp add: linorder_not_less)
-apply (auto intro: abs_ge_self [THEN order_trans])
-done
+by simp
  
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
-apply (simp add: real_add_assoc)
-apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
-apply (rule real_add_assoc [THEN subst])
-apply (rule abs_triangle_ineq)
-done
+by simp
 
 end
diff -r f30b73385060 -r 25b068a99d2b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Set.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -33,6 +33,7 @@
   Pow           :: "'a set => 'a set set"                -- "powerset"
   Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
   Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
+  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
   image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
   "op :"        :: "'a => 'a set => bool"                -- "membership"
 
@@ -117,11 +118,13 @@
   "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
   "_Bleast"       :: "id => 'a set => bool => 'a"      ("(3LEAST _:_./ _)" [0, 0, 10] 10)
 
 syntax (HOL)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
 
 translations
   "{x, xs}"     == "insert x {xs}"
@@ -138,16 +141,19 @@
   "INT x:A. B"  == "INTER A (%x. B)"
   "ALL x:A. P"  == "Ball A (%x. P)"
   "EX x:A. P"   == "Bex A (%x. P)"
+  "EX! x:A. P"  == "Bex1 A (%x. P)"
   "LEAST x:A. P" => "LEAST x. x:A & P"
 
 syntax (xsymbols)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
 
 syntax (HTML output)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
+  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
 
 syntax (xsymbols)
   "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
@@ -178,30 +184,35 @@
   "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
 
 syntax (xsymbols)
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
 
 syntax (HOL output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
 
 syntax (HTML output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
 
 translations
  "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
- "\<exists>A\<subset>B. P"    =>  "EX A. A \<subset> B & P"
- "\<forall>A\<subseteq>B. P"  =>  "ALL A. A \<subseteq> B --> P"
+ "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
+ "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
  "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
+ "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
 
 print_translation {*
 let
@@ -316,6 +327,7 @@
 defs
   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   Bex_def:      "Bex A P        == EX x. x:A & P(x)"
+  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
 
 defs (overloaded)
   subset_def:   "A <= B         == ALL x:A. x:B"
diff -r f30b73385060 -r 25b068a99d2b src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/SetInterval.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -301,7 +301,7 @@
   show "?B \<subseteq> ?A"
   proof
     fix n assume a: "n : ?B"
-    hence "n - k : {i..j}" by auto arith+
+    hence "n - k : {i..j}" by auto
     moreover have "n = (n - k) + k" using a by auto
     ultimately show "n : ?A" by blast
   qed
@@ -315,7 +315,7 @@
   show "?B \<subseteq> ?A"
   proof
     fix n assume a: "n : ?B"
-    hence "n - k : {i..<j}" by auto arith+
+    hence "n - k : {i..<j}" by auto
     moreover have "n = (n - k) + k" using a by auto
     ultimately show "n : ?A" by blast
   qed
@@ -384,7 +384,6 @@
   apply (rule card_image)
   apply (simp add: inj_on_def)
   apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
-  apply arith
   apply (rule_tac x = "x - l" in exI)
   apply arith
   done
diff -r f30b73385060 -r 25b068a99d2b src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -35,7 +35,6 @@
       setsum f (lessThan n) <= setsum g (lessThan n)"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
-apply (drule_tac x = n in spec, arith)
 done
 
 lemma tokens_mono_prefix [rule_format]:
diff -r f30b73385060 -r 25b068a99d2b src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -578,7 +578,6 @@
 	apply (insert n_less_u)
 	apply (insert u)
 	apply auto
-	apply arith
 	done
       ultimately show False by auto
     qed
diff -r f30b73385060 -r 25b068a99d2b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/arith_data.ML	Wed Jul 26 19:23:04 2006 +0200
@@ -29,7 +29,6 @@
     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   end;
 
-
 (* dest_sum *)
 
 val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
@@ -44,7 +43,6 @@
           SOME (t, u) => dest_sum t @ dest_sum u
         | NONE => [tm]));
 
-
 (** generic proof tools **)
 
 (* prove conversions *)
@@ -57,7 +55,6 @@
 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
 
-
 (* rewriting *)
 
 fun simp_all_tac rules =
@@ -70,7 +67,8 @@
 fun prep_simproc (name, pats, proc) =
   Simplifier.simproc (the_context ()) name pats proc;
 
-end;
+end;  (* NatArithUtils *)
+
 
 signature ARITH_DATA =
 sig
@@ -78,12 +76,12 @@
   val nat_cancel_sums: simproc list
 end;
 
+
 structure ArithData: ARITH_DATA =
 struct
 
 open NatArithUtils;
 
-
 (** cancel common summands **)
 
 structure Sum =
@@ -99,7 +97,6 @@
 fun gen_uncancel_tac rule ct =
   rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
 
-
 (* nat eq *)
 
 structure EqCancelSums = CancelSumsFun
@@ -110,7 +107,6 @@
   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
 end);
 
-
 (* nat less *)
 
 structure LessCancelSums = CancelSumsFun
@@ -121,7 +117,6 @@
   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
 end);
 
-
 (* nat le *)
 
 structure LeCancelSums = CancelSumsFun
@@ -132,7 +127,6 @@
   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
 end);
 
-
 (* nat diff *)
 
 structure DiffCancelSums = CancelSumsFun
@@ -143,8 +137,6 @@
   val uncancel_tac = gen_uncancel_tac diff_cancel;
 end);
 
-
-
 (** prepare nat_cancel simprocs **)
 
 val nat_cancel_sums_add = map prep_simproc
@@ -159,7 +151,7 @@
   [prep_simproc ("natdiff_cancel_sums",
     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
 
-end;
+end;  (* ArithData *)
 
 open ArithData;
 
@@ -172,6 +164,7 @@
 
 structure LA_Logic: LIN_ARITH_LOGIC =
 struct
+
 val ccontr = ccontr;
 val conjI = conjI;
 val notI = notI;
@@ -179,7 +172,6 @@
 val not_lessD = linorder_not_less RS iffD1;
 val not_leD = linorder_not_le RS iffD1;
 
-
 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
 
 val mk_Trueprop = HOLogic.mk_Trueprop;
@@ -202,7 +194,7 @@
   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   in instantiate ([],[(cn,ct)]) le0 end;
 
-end;
+end;  (* LA_Logic *)
 
 
 (* arith theory data *)
@@ -235,9 +227,18 @@
   {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
 
 
-structure LA_Data_Ref: LIN_ARITH_DATA =
+signature HOL_LIN_ARITH_DATA =
+sig
+  include LIN_ARITH_DATA
+  val fast_arith_split_limit : int ref
+end;
+
+structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
 struct
 
+(* internal representation of linear (in-)equations *)
+type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
+
 (* Decomposition of terms *)
 
 fun nT (Type("fun",[N,_])) = N = HOLogic.natT
@@ -370,16 +371,425 @@
 
 fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
 
+(*---------------------------------------------------------------------------*)
+(* code that performs certain goal transformations for linear arithmetic     *)
+(*---------------------------------------------------------------------------*)
+
+(* A "do nothing" variant of pre_decomp and pre_tac:
+
+fun pre_decomp sg Ts termitems = [termitems];
+fun pre_tac i = all_tac;
+*)
+
+(*---------------------------------------------------------------------------*)
+(* the following code performs splitting of certain constants (e.g. min,     *)
+(* max) in a linear arithmetic problem; similar to what split_tac later does *)
+(* to the proof state                                                        *)
+(*---------------------------------------------------------------------------*)
+
+val fast_arith_split_limit = ref 9;
+
+(* checks whether splitting with 'thm' is implemented                        *)
+
+(* Thm.thm -> bool *)
+
+fun is_split_thm thm =
+  case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>  (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
+    (case head_of lhs of
+      Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
+    | _            => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
+  | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
+
+(* substitute new for occurrences of old in a term, incrementing bound       *)
+(* variables as needed when substituting inside an abstraction               *)
+
+(* (term * term) list -> term -> term *)
+
+fun subst_term []    t = t
+  | subst_term pairs t =
+      (case AList.lookup (op aconv) pairs t of
+        SOME new =>
+          new
+      | NONE     =>
+          (case t of Abs (a, T, body) =>
+            let val pairs' = map (pairself (incr_boundvars 1)) pairs
+            in  Abs (a, T, subst_term pairs' body)  end
+          | t1 $ t2                   =>
+            subst_term pairs t1 $ subst_term pairs t2
+          | _ => t));
+
+(* approximates the effect of one application of split_tac (followed by NNF  *)
+(* normalization) on the subgoal represented by '(Ts, terms)'; returns a     *)
+(* list of new subgoals (each again represented by a typ list for bound      *)
+(* variables and a term list for premises), or NONE if split_tac would fail  *)
+(* on the subgoal                                                            *)
+
+(* theory -> typ list * term list -> (typ list * term list) list option *)
+
+(* FIXME: currently only the effect of certain split theorems is reproduced  *)
+(*        (which is why we need 'is_split_thm').  A more canonical           *)
+(*        implementation should analyze the right-hand side of the split     *)
+(*        theorem that can be applied, and modify the subgoal accordingly.   *)
+
+fun split_once_items sg (Ts, terms) =
+let
+  (* takes a list  [t1, ..., tn]  to the term                                *)
+  (*   tn' --> ... --> t1' --> False  ,                                      *)
+  (* where ti' = HOLogic.dest_Trueprop ti                                    *)
+  (* term list -> term *)
+  fun REPEAT_DETERM_etac_rev_mp terms' =
+    fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
+  val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
+  val cmap       = Splitter.cmap_of_split_thms split_thms
+  val splits     = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
+in
+  if length splits > !fast_arith_split_limit then (
+    tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
+    NONE
+  ) else (
+  case splits of [] =>
+    NONE  (* split_tac would fail: no possible split *)
+  | ((_, _, _, split_type, split_term) :: _) => (  (* ignore all but the first possible split *)
+    case strip_comb split_term of
+    (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
+      (Const ("Orderings.max", _), [t1, t2]) =>
+      let
+        val rev_terms     = rev terms
+        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2        = map (subst_term [(split_term, t2)]) rev_terms
+        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
+        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
+        val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (Ts, subgoal2)]
+      end
+    (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
+    | (Const ("Orderings.min", _), [t1, t2]) =>
+      let
+        val rev_terms     = rev terms
+        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2        = map (subst_term [(split_term, t2)]) rev_terms
+        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
+        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
+        val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (Ts, subgoal2)]
+      end
+    (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
+    | (Const ("HOL.abs", _), [t1]) =>
+      let
+        val rev_terms     = rev terms
+        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2        = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
+        val zero          = Const ("0", split_type)
+        val zero_leq_t1   = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
+        val t1_lt_zero    = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
+        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1      = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
+        val subgoal2      = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (Ts, subgoal2)]
+      end
+    (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
+    | (Const ("HOL.minus", _), [t1, t2]) =>
+      let
+        (* "d" in the above theorem becomes a new bound variable after NNF   *)
+        (* transformation, therefore some adjustment of indices is necessary *)
+        val rev_terms       = rev terms
+        val zero            = Const ("0", split_type)
+        val d               = Bound 0
+        val terms1          = map (subst_term [(split_term, zero)]) rev_terms
+        val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
+        val t1'             = incr_boundvars 1 t1
+        val t2'             = incr_boundvars 1 t2
+        val t1_lt_t2        = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
+        val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $ (Const ("HOL.plus", split_type --> split_type --> split_type) $ t2' $ d)
+        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
+        val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
+      end
+    (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
+    | (Const ("IntDef.nat", _), [t1]) =>
+      let
+        val rev_terms   = rev terms
+        val zero_int    = Const ("0", HOLogic.intT)
+        val zero_nat    = Const ("0", HOLogic.natT)
+        val n           = Bound 0
+        val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
+        val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
+        val t1'         = incr_boundvars 1 t1
+        val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+        val t1_lt_zero  = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
+        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
+        val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
+      in
+        SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
+      end
+    (* "?P ((?n::nat) mod (number_of ?k)) = ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
+    | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+      let
+        val rev_terms               = rev terms
+        val zero                    = Const ("0", split_type)
+        val i                       = Bound 1
+        val j                       = Bound 0
+        val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+        val t1'                     = incr_boundvars 2 t1
+        val t2'                     = incr_boundvars 2 t2
+        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
+                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
+      end
+    (* "?P ((?n::nat) div (number_of ?k)) = ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) --> (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
+    | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
+      let
+        val rev_terms               = rev terms
+        val zero                    = Const ("0", split_type)
+        val i                       = Bound 1
+        val j                       = Bound 0
+        val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
+        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+        val t1'                     = incr_boundvars 2 t1
+        val t2'                     = incr_boundvars 2 t2
+        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
+        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
+        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
+                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
+      in
+        SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
+      end
+    (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
+                                              (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
+                                              (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
+    | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+      let
+        val rev_terms               = rev terms
+        val zero                    = Const ("0", split_type)
+        val i                       = Bound 1
+        val j                       = Bound 0
+        val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
+        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
+        val t1'                     = incr_boundvars 2 t1
+        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
+        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
+        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
+        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
+                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
+        val subgoal2                = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
+                                        @ hd terms2_3
+                                        :: (if tl terms2_3 = [] then [not_false] else [])
+                                        @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
+                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+        val subgoal3                = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
+                                        @ hd terms2_3
+                                        :: (if tl terms2_3 = [] then [not_false] else [])
+                                        @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
+                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
+        val Ts'                     = split_type :: split_type :: Ts
+      in
+        SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
+      end
+    (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
+                                              (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
+                                              (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
+    | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
+      let
+        val rev_terms               = rev terms
+        val zero                    = Const ("0", split_type)
+        val i                       = Bound 1
+        val j                       = Bound 0
+        val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
+        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
+        val t1'                     = incr_boundvars 2 t1
+        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
+        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
+        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
+                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
+        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
+        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
+        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
+                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
+                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
+        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
+        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
+        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
+        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
+        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
+        val subgoal2                = (HOLogic.mk_Trueprop neg_minus_k)
+                                        :: terms2_3
+                                        @ not_false
+                                        :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
+        val subgoal3                = (HOLogic.mk_Trueprop neg_t2)
+                                        :: terms2_3
+                                        @ not_false
+                                        :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
+        val Ts'                     = split_type :: split_type :: Ts
+      in
+        SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
+      end
+    (* this will only happen if a split theorem can be applied for which no code exists above -- *)
+    (* in which case either the split theorem should be implemented above, or 'is_split_thm'     *)
+    (* should be modified to filter it out                                                       *)
+    | (t, ts) => (
+      warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
+               " argument(s)) not implemented; proof reconstruction is likely to fail");
+      NONE
+    ))
+  )
 end;
 
+(* remove terms that do not satisfy p; change the order of the remaining     *)
+(* terms in the same way as filter_prems_tac does                            *)
+
+(* (term -> bool) -> term list -> term list *)
+
+fun filter_prems_tac_items p terms =
+let
+  fun filter_prems (t, (left, right)) =
+    if  p t  then  (left, right @ [t])  else  (left @ right, [])
+  val (left, right) = foldl filter_prems ([], []) terms
+in
+  right @ left
+end;
+
+(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
+(* subgoal that has 'terms' as premises                                      *)
+
+(* term list -> bool *)
+
+fun negated_term_occurs_positively terms =
+  List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
+
+(* theory -> typ list * term list -> (typ list * term list) list *)
+
+fun pre_decomp sg (Ts, terms) =
+let
+  (* repeatedly split (including newly emerging subgoals) until no further   *)
+  (* splitting is possible                                                   *)
+  (* (typ list * term list) list -> (typ list * term list) list *)
+  fun split_loop [] = []
+    | split_loop (subgoal::subgoals) = (
+        case split_once_items sg subgoal of
+          SOME new_subgoals => split_loop (new_subgoals @ subgoals)
+        | NONE              => subgoal :: split_loop subgoals
+      )
+  fun is_relevant t  = isSome (decomp sg t)
+  val relevant_terms = filter_prems_tac_items is_relevant terms                                (* filter_prems_tac is_relevant *)
+  val split_goals    = split_loop [(Ts, relevant_terms)]                                       (* split_tac, NNF normalization *)
+  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals    (* necessary because split_once_tac may normalize terms *)
+  val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm  (* TRY (etac notE) THEN eq_assume_tac *)
+in
+  result
+end;
+
+(* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
+(* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
+(* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
+(* performs NNF-normalization of ~P, and eliminates conjunctions,            *)
+(* disjunctions and existential quantifiers from the premises, possibly (in  *)
+(* the case of disjunctions) resulting in several new subgoals, each of the  *)
+(* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
+(* !fast_arith_split_limit splits are possible.                              *)
+
+(* Thm.thm list -> int -> Tactical.tactic *)
+
+fun split_once_tac split_thms i =
+let
+  val nnf_simpset =
+    empty_ss setmkeqTrue mk_eq_True
+    setmksimps (mksimps mksimps_pairs)
+    addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, 
+      not_all, not_ex, not_not]
+  fun prem_nnf_tac i st =
+    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
+  fun cond_split_tac i st =
+    let
+      val subgoal = Logic.nth_prem (i, Thm.prop_of st)
+      val Ts      = rev (map snd (Logic.strip_params subgoal))
+      val concl   = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
+      val cmap    = Splitter.cmap_of_split_thms split_thms
+      val splits  = Splitter.split_posns cmap (theory_of_thm st) Ts concl
+    in
+      if length splits > !fast_arith_split_limit then
+        no_tac st
+      else
+        split_tac split_thms i st
+    end
+in
+  EVERY' [
+    REPEAT_DETERM o etac rev_mp,
+    cond_split_tac,
+    rtac ccontr,
+    prem_nnf_tac,
+    TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
+  ] i
+end;
+
+(* remove irrelevant premises, then split the i-th subgoal (and all new      *)
+(* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
+(* subgoals and finally attempt to solve them by finding an immediate        *)
+(* contradiction (i.e. a term and its negation) in their premises.           *)
+
+(* int -> Tactical.tactic *)
+
+fun pre_tac i st =
+let
+  val sg            = theory_of_thm st
+  val split_thms    = filter is_split_thm (#splits (ArithTheoryData.get sg))
+  fun is_relevant t = isSome (decomp sg t)
+in
+  DETERM (
+    TRY (filter_prems_tac is_relevant i)
+      THEN (
+        (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
+          THEN_ALL_NEW
+            ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
+              THEN'
+            (TRY o (etac notE THEN' eq_assume_tac)))
+      ) i
+  ) st
+end;
+
+end;  (* LA_Data_Ref *)
+
 
 structure Fast_Arith =
   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
 
-val fast_arith_tac    = Fast_Arith.lin_arith_tac false
-and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
-and trace_arith    = Fast_Arith.trace
-and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
+val fast_arith_tac         = Fast_Arith.lin_arith_tac false;
+val fast_ex_arith_tac      = Fast_Arith.lin_arith_tac;
+val trace_arith            = Fast_Arith.trace;
+val fast_arith_neq_limit   = Fast_Arith.fast_arith_neq_limit;
+val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
 
 local
 
@@ -439,7 +849,6 @@
   Simplifier.simproc (the_context ()) "fast_nat_arith"
     ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
 
-
 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
 useful to detect inconsistencies among the premises for subgoals which are
 *not* themselves (in)equalities, because the latter activate
@@ -449,58 +858,24 @@
 
 (* arith proof method *)
 
-(* FIXME: K true should be replaced by a sensible test to speed things up
-   in case there are lots of irrelevant terms involved;
-   elimination of min/max can be optimized:
-   (max m n + k <= r) = (m+k <= r & n+k <= r)
-   (l <= min m n + k) = (l <= m+k & l <= n+k)
-*)
 local
-(* a simpset for computations subject to optimization !!! *)
-(*
-val binarith = map thm
-  ["Pls_0_eq", "Min_1_eq",
- "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
-  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
-  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
-  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
-  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
-  "bin_add_Pls_right", "bin_add_Min_right"];
- val intarithrel = 
-     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
-		"int_le_number_of_eq","int_iszero_number_of_0",
-		"int_less_number_of_eq_neg"]) @
-     (map (fn s => thm s RS thm "lift_bool") 
-	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
-	   "int_neg_number_of_Min"])@
-     (map (fn s => thm s RS thm "nlift_bool") 
-	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
-     
-val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
-			"int_number_of_diff_sym", "int_number_of_mult_sym"];
-val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
-			"mult_nat_number_of", "eq_nat_number_of",
-			"less_nat_number_of"]
-val powerarith = 
-    (map thm ["nat_number_of", "zpower_number_of_even", 
-	      "zpower_Pls", "zpower_Min"]) @ 
-    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
-			   thm "one_eq_Numeral1_nring"] 
-  (thm "zpower_number_of_odd"))]
 
-val comp_arith = binarith @ intarith @ intarithrel @ natarith 
-	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
-
-val comp_ss = HOL_basic_ss addsimps comp_arith addsimps simp_thms;
-*)
 fun raw_arith_tac ex i st =
+  (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
+     decomp sg"?) to speed things up in case there are lots of irrelevant
+     terms involved; elimination of min/max can be optimized:
+     (max m n + k <= r) = (m+k <= r & n+k <= r)
+     (l <= min m n + k) = (l <= m+k & l <= n+k)
+  *)
   refute_tac (K true)
-   (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
-(*   (REPEAT o 
-    (fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i)
-		THEN (simp_tac comp_ss i))) *)
-   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
-   i st;
+    (* Splitting is also done inside fast_arith_tac, but not completely --   *)
+    (* split_tac may use split theorems that have not been implemented in    *)
+    (* fast_arith_tac (cf. pre_decomp and split_once_items above).           *)
+    (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
+    (* some goals that fast_arith_tac alone would fail on.                   *)
+    (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
+    (fast_ex_arith_tac ex)
+    i st;
 
 fun presburger_tac i st =
   (case ArithTheoryData.get (Thm.theory_of_thm st) of
@@ -510,19 +885,19 @@
 
 in
 
-val simple_arith_tac = FIRST' [fast_arith_tac,
-  ObjectLogic.atomize_tac THEN' raw_arith_tac true];
+  val simple_arith_tac = FIRST' [fast_arith_tac,
+    ObjectLogic.atomize_tac THEN' raw_arith_tac true];
 
-val arith_tac = FIRST' [fast_arith_tac,
-  ObjectLogic.atomize_tac THEN' raw_arith_tac true,
-  presburger_tac];
+  val arith_tac = FIRST' [fast_arith_tac,
+    ObjectLogic.atomize_tac THEN' raw_arith_tac true,
+    presburger_tac];
 
-val silent_arith_tac = FIRST' [fast_arith_tac,
-  ObjectLogic.atomize_tac THEN' raw_arith_tac false,
-  presburger_tac];
+  val silent_arith_tac = FIRST' [fast_arith_tac,
+    ObjectLogic.atomize_tac THEN' raw_arith_tac false,
+    presburger_tac];
 
-fun arith_method prems =
-  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
+  fun arith_method prems =
+    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
 
 end;
 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/ex/Adder.thy
--- a/src/HOL/ex/Adder.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/ex/Adder.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -80,22 +80,7 @@
 lemma cca_length [rule_format]:
      "\<forall>bs. length as = length bs --> 
            length (carry_chain_adder as bs c) = Suc (length bs)"
-      (is "?P as")
-proof (induct as,auto simp add: Let_def)
-  fix as :: "bit list"
-  fix xs :: "bit list"
-  assume ind: "?P as"
-  assume len: "Suc (length as) = length xs"
-  thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs"
-  proof (cases xs,simp_all)
-    fix b bs
-    assume [simp]: "xs = b # bs"
-    assume "length as = length bs"
-    with ind
-    show "length (carry_chain_adder as bs c) - Suc 0 = length bs"
-      by auto
-  qed
-qed
+  by (induct as,auto simp add: Let_def)
 
 lemma cca_correct [rule_format]:
      "\<forall>bs. length as = length bs --> 
diff -r f30b73385060 -r 25b068a99d2b src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/simpdata.ML	Wed Jul 26 19:23:04 2006 +0200
@@ -166,8 +166,6 @@
 end;
 
 
-
-
 (*** Simproc for Let ***)
 
 val use_let_simproc = ref true;
diff -r f30b73385060 -r 25b068a99d2b src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 26 19:23:04 2006 +0200
@@ -23,12 +23,12 @@
 
 signature LIN_ARITH_LOGIC =
 sig
-  val conjI:		thm (* P ==> Q ==> P & Q *)
+  val conjI:            thm (* P ==> Q ==> P & Q *)
   val ccontr:           thm (* (~ P ==> False) ==> P *)
   val notI:             thm (* (P ==> False) ==> ~ P *)
   val not_lessD:        thm (* ~(m < n) ==> n <= m *)
   val not_leD:          thm (* ~(m <= n) ==> n < m *)
-  val sym:		thm (* x = y ==> y = x *)
+  val sym:              thm (* x = y ==> y = x *)
   val mk_Eq: thm -> thm
   val atomize: thm -> thm list
   val mk_Trueprop: term -> term
@@ -52,16 +52,26 @@
 
 signature LIN_ARITH_DATA =
 sig
-  val decomp:
-    theory -> term -> ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool) option
+  type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool  (* internal representation of linear (in-)equations *)
+  val decomp: theory -> term -> decompT option
+  val pre_decomp: theory -> typ list * term list -> (typ list * term list) list  (* preprocessing, performed on a representation of subgoals as list of premises *)
+  val pre_tac   : int -> Tactical.tactic                                         (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
   val number_of: IntInf.int * typ -> term
 end;
 (*
 decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
    where Rel is one of "<", "~<", "<=", "~<=" and "=" and
-         p/q is the decomposition of the sum terms x/y into a list
-         of summand * multiplicity pairs and a constant summand and
-         d indicates if the domain is discrete.
+         p (q, respectively) is the decomposition of the sum term x
+         (y, respectively) into a list of summand * multiplicity
+         pairs and a constant summand and d indicates if the domain
+         is discrete.
+
+The relationship between pre_decomp and pre_tac is somewhat tricky.  The
+internal representation of a subgoal and the corresponding theorem must
+be modified by pre_decomp (pre_tac, resp.) in a corresponding way.  See
+the comment for split_items below.  (This is even necessary for eta- and
+beta-equivalent modifications, as some of the lin. arith. code is not
+insensitive to them.)
 
 ss must reduce contradictory <= to False.
    It should also cancel common summands to keep <= reduced;
@@ -192,32 +202,32 @@
 
 fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
 
-fun choose2 d ((lb,exactl),(ub,exactu)) =
-  if Rat.le(lb,Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
-     Rat.le(Rat.zero,ub) andalso (ub <> Rat.zero orelse exactu)
+fun choose2 d ((lb, exactl), (ub, exactu)) =
+  if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
+     Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
   then Rat.zero else
   if not d
   then (if Rat.ge0 lb
-        then if exactl then lb else ratmiddle(lb,ub)
-        else if exactu then ub else ratmiddle(lb,ub))
+        then if exactl then lb else ratmiddle (lb, ub)
+        else if exactu then ub else ratmiddle (lb, ub))
   else (* discrete domain, both bounds must be exact *)
   if Rat.ge0 lb then let val lb' = Rat.roundup lb
-                    in if Rat.le(lb',ub) then lb' else raise NoEx end
+                    in if Rat.le (lb', ub) then lb' else raise NoEx end
                else let val ub' = Rat.rounddown ub
-                    in if Rat.le(lb,ub') then ub' else raise NoEx end;
+                    in if Rat.le (lb, ub') then ub' else raise NoEx end;
 
-fun findex1 discr (ex,(v,lineqs)) =
+fun findex1 discr (ex, (v, lineqs)) =
   let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs;
       val ineqs = Library.foldl elim_eqns ([],nz)
       val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
-      val lb = ratrelmax(map (eval ex v) ge)
-      val ub = ratrelmin(map (eval ex v) le)
+      val lb = ratrelmax (map (eval ex v) ge)
+      val ub = ratrelmin (map (eval ex v) le)
   in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
 
 fun findex discr = Library.foldl (findex1 discr);
 
 fun elim1 v x =
-  map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
+  map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
                         nth_update (v, Rat.zero) bs));
 
 fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
@@ -327,7 +337,7 @@
 (* ------------------------------------------------------------------------- *)
 
 fun allpairs f xs ys =
-  maps (fn x => map (fn y => f x y) ys) xs;
+  List.concat (map (fn x => map (fn y => f x y) ys) xs);
 
 fun extract_first p =
   let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
@@ -346,25 +356,25 @@
 type history = (int * lineq list) list;
 datatype result = Success of injust | Failure of history;
 
-fun elim(ineqs,hist) =
-  let val dummy = print_ineqs ineqs;
-      val (triv,nontriv) = List.partition is_trivial ineqs in
-  if not(null triv)
+fun elim (ineqs, hist) =
+  let val dummy = print_ineqs ineqs
+      val (triv, nontriv) = List.partition is_trivial ineqs in
+  if not (null triv)
   then case Library.find_first is_answer triv of
-         NONE => elim(nontriv,hist)
+         NONE => elim (nontriv, hist)
        | SOME(Lineq(_,_,_,j)) => Success j
   else
-  if null nontriv then Failure(hist)
+  if null nontriv then Failure hist
   else
-  let val (eqs,noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
-  if not(null eqs) then
+  let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
+  if not (null eqs) then
      let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
          val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
                            (List.filter (fn i => i<>0) clist)
          val c = hd sclist
          val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
                extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
-         val v = find_index (fn x => x = c) ceq
+         val v = find_index_eq c ceq
          val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
                                      (othereqs @ noneqs)
          val others = map (elim_var v eq) roth @ ioth
@@ -390,10 +400,12 @@
 (* Translate back a proof.                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-fun trace_thm msg th = 
-    if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
+(* string -> Thm.thm -> Thm.thm *)
+fun trace_thm msg th =
+    (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
 
-fun trace_msg msg = 
+(* string -> unit *)
+fun trace_msg msg =
     if !trace then tracing msg else ();
 
 (* FIXME OPTIMIZE!!!! (partly done already)
@@ -408,21 +420,21 @@
 local
  exception FalseE of thm
 in
+(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
 fun mkthm (sg, ss) asms just =
   let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
           Data.get sg;
       val simpset' = Simplifier.inherit_context ss simpset;
-      val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
+      val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
                             map fst lhs  union  (map fst rhs  union  ats))
-                        ([], map_filter (fn thm => if Thm.no_prems thm
-                                        then LA_Data.decomp sg (concl_of thm)
-                                        else NONE) asms)
+                        ([], List.mapPartial (fn thm => if Thm.no_prems thm
+                                              then LA_Data.decomp sg (concl_of thm)
+                                              else NONE) asms)
 
       fun add2 thm1 thm2 =
         let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
         in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
         end;
-
       fun try_add [] _ = NONE
         | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
              NONE => try_add thm1s thm2 | some => some;
@@ -430,23 +442,18 @@
       fun addthms thm1 thm2 =
         case add2 thm1 thm2 of
           NONE => (case try_add ([thm1] RL inj_thms) thm2 of
-                     NONE => (the (try_add ([thm2] RL inj_thms) thm1)
+                     NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
                                handle Option =>
                                (trace_thm "" thm1; trace_thm "" thm2;
-                                sys_error "Lin.arith. failed to add thms"))
+                                sys_error "Lin.arith. failed to add thms")
+                             )
                    | SOME thm => thm)
         | SOME thm => thm;
 
       fun multn(n,thm) =
         let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
         in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
-(*
-      fun multn2(n,thm) =
-        let val SOME(mth,cv) =
-              get_first (fn (th,cv) => SOME(thm RS th,cv) handle THM _ => NONE) mult_mono_thms
-            val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
-        in instantiate ([],[(cv,ct)]) mth end
-*)
+
       fun multn2(n,thm) =
         let val SOME(mth) =
               get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
@@ -459,15 +466,15 @@
         let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
         in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
 
-      fun mk(Asm i) = trace_thm "Asm" (nth asms i)
-        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
-        | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
-        | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
-        | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
-        | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
-        | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
-        | mk(Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
-        | mk(Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
+      fun mk (Asm i) = trace_thm "Asm" (nth asms i)
+        | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i))
+        | mk (LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
+        | mk (NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
+        | mk (NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
+        | mk (NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
+        | mk (Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
+        | mk (Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
+        | mk (Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
 
   in trace_msg "mkthm";
      let val thm = trace_thm "Final thm:" (mk just)
@@ -475,19 +482,20 @@
         in trace_thm "After simplification:" fls;
            if LA_Logic.is_False fls then fls
            else
-            (tracing "Assumptions:"; List.app print_thm asms;
-             tracing "Proved:"; print_thm fls;
+            (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
+             tracing "Proved:"; tracing (Display.string_of_thm fls);
              warning "Linear arithmetic should have refuted the assumptions.\n\
                      \Please inform Tobias Nipkow (nipkow@in.tum.de).";
              fls)
         end
-     end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
+     end handle FalseE thm => trace_thm "False reached early:" thm
   end
 end;
 
 fun coeff poly atom : IntInf.int =
   AList.lookup (op =) poly atom |> the_default 0;
 
+(* int list -> int *)
 fun lcms is = Library.foldl lcm (1, is);
 
 fun integ(rlhs,r,rel,rrhs,s,d) =
@@ -499,8 +507,8 @@
 in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
 
 fun mklineq n atoms =
-  fn (item,k) =>
-  let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
+  fn (item, k) =>
+  let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item
       val lhsa = map (coeff lhs) atoms
       and rhsa = map (coeff rhs) atoms
       val diff = map2 (curry (op -)) rhsa lhsa
@@ -535,28 +543,33 @@
   curry (op ~~) sds
   #> map print_atom
   #> commas
-  #> curry (op ^) "Counter example:\n";
+  #> curry (op ^) "Counter example (possibly spurious):\n";
 
-fun trace_ex(sg,params,atoms,discr,n,hist:history) =
-  if null hist then ()
-  else let val frees = map Free params;
-           fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t));
-           val (v,lineqs) :: hist' = hist
-           val start = if v = ~1 then (findex0 discr n lineqs,hist')
-                       else (replicate n Rat.zero,hist)
-           val ex = SOME (produce_ex ((map s_of_t atoms)~~discr) (findex discr start))
-             handle NoEx => NONE;
-       in
-         (case ex of
-           SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
-         | NONE => warning "arith failed")
-       end;
+fun trace_ex (sg, params, atoms, discr, n, hist : history) =
+  case hist of
+    [] => ()
+  | (v, lineqs) :: hist' =>
+    let val frees = map Free params
+        fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
+        val start = if v = ~1 then (findex0 discr n lineqs, hist')
+                    else (replicate n Rat.zero, hist)
+        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
+          handle NoEx => NONE
+    in
+      case ex of
+        SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
+      | NONE => warning "arith failed"
+    end;
 
-fun mknat pTs ixs (atom,i) =
-  if LA_Logic.is_nat(pTs,atom)
+(* ------------------------------------------------------------------------- *)
+
+(* Term.typ list -> int list -> Term.term * int -> lineq option *)
+
+fun mknat pTs ixs (atom, i) =
+  if LA_Logic.is_nat (pTs, atom)
   then let val l = map (fn j => if j=i then 1 else 0) ixs
-       in SOME(Lineq(0,Le,l,Nat(i))) end
-  else NONE
+       in SOME (Lineq (0, Le, l, Nat i)) end
+  else NONE;
 
 (* This code is tricky. It takes a list of premises in the order they occur
 in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical
@@ -570,95 +583,184 @@
 
 For variables n of type nat, a constraint 0 <= n is added.
 *)
-fun split_items(items) =
-  let fun elim_neq front _ [] = [rev front]
-        | elim_neq front n (NONE::ineqs) = elim_neq front (n+1) ineqs
-        | elim_neq front n (SOME(ineq as (l,i,rel,r,j,d))::ineqs) =
-          if rel = "~=" then elim_neq front n (ineqs @ [SOME(l,i,"<",r,j,d)]) @
-                             elim_neq front n (ineqs @ [SOME(r,j,"<",l,i,d)])
-          else elim_neq ((ineq,n) :: front) (n+1) ineqs
-  in elim_neq [] 0 items end;
+
+(* FIXME: To optimize, the splitting of cases and the search for refutations *)
+(*        should be intertwined: separate the first (fully split) case,      *)
+(*        refute it, continue with splitting and refuting.  Terminate with   *)
+(*        failure as soon as a case could not be refuted; i.e. delay further *)
+(*        splitting until after a refutation for other cases has been found. *)
+
+(* Theory.theory -> bool -> typ list * term list -> (typ list * (decompT * int) list) list *)
+
+fun split_items sg do_pre (Ts, terms) =
+  let
+(*
+      val _ = trace_msg ("split_items: do_pre is " ^ Bool.toString do_pre ^ "\n" ^
+                         "  Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+                         "  terms = " ^ string_of_list (Sign.string_of_term sg) terms)
+*)
+      (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
+      (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
+      (* level                                                          *)
+      (* decompT option list -> decompT option list list *)
+      fun elim_neq []              = [[]]
+        | elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
+        | elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
+          if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
+                             elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
+          else map (cons (SOME ineq)) (elim_neq ineqs)
+      (* int -> decompT option list -> (decompT * int) list *)
+      fun number_hyps _ []             = []
+        | number_hyps n (NONE::xs)     = number_hyps (n+1) xs
+        | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
 
-fun add_atoms(ats,((lhs,_,_,rhs,_,_),_)) =
-    (map fst lhs) union ((map fst rhs) union ats)
+      val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
+                                  (* (typ list * term list) list *)
+                                  (if do_pre then LA_Data.pre_decomp sg else Library.single)
+                               |> (* compute the internal encoding of (in-)equalities *)
+                                  (* (typ list * decompT option list) list *)
+                                  map (apsnd (map (LA_Data.decomp sg)))
+                               |> (* splitting of inequalities *)
+                                  (* (typ list * decompT option list) list list *)
+                                  map (fn (Ts, items) => map (pair Ts) (elim_neq items))
+                               |> (* combine the list of lists of subgoals into a single list *)
+                                  (* (typ list * decompT option list) list *)
+                                  List.concat
+                               |> (* numbering of hypotheses, ignoring irrelevant ones *)
+                                  (* (typ list * (decompT * int) list) list *)
+                                  map (apsnd (number_hyps 0))
+(*
+      val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
+                ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
+                        ("  " ^ Int.toString n ^ ". Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
+                         "    items = " ^ string_of_list
+                                            (string_of_pair
+                                              (fn (l, i, rel, r, j, d) =>
+                                                enclose "(" ")" (commas
+                                                  [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
+                                                   Rat.string_of_rat i,
+                                                   rel,
+                                                   string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
+                                                   Rat.string_of_rat j,
+                                                   Bool.toString d]))
+                                              Int.toString) items, n+1)) result 1))
+*)
+  in result end;
 
-fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) =
-    (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats)
+(* term list * (decompT * int) -> term list *)
+
+fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
+    (map fst lhs) union ((map fst rhs) union ats);
+
+(* (bool * term) list * (decompT * int) -> (bool * term) list *)
+
+fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
+    (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
+
+(* (decompT * int) list -> bool list *)
 
 fun discr initems = map fst (Library.foldl add_datoms ([],initems));
 
-fun refutes sg (pTs,params) ex =
+(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+
+fun refutes sg params show_ex =
 let
-  fun refute (initems::initemss) js =
-    let val atoms = Library.foldl add_atoms ([],initems)
+  (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
+  fun refute ((Ts, initems)::initemss) js =
+    let val atoms = Library.foldl add_atoms ([], initems)
         val n = length atoms
         val mkleq = mklineq n atoms
         val ixs = 0 upto (n-1)
         val iatoms = atoms ~~ ixs
-        val natlineqs = map_filter (mknat pTs ixs) iatoms
+        val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
         val ineqs = map mkleq initems @ natlineqs
-    in case elim(ineqs,[]) of
-         Success(j) =>
-           (trace_msg "Contradiction!"; refute initemss (js@[j]))
-       | Failure(hist) =>
-           (if not ex then ()
-            else trace_ex(sg,params,atoms,discr initems,n,hist);
-            NONE)
+    in case elim (ineqs, []) of
+         Success j =>
+           (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
+       | Failure hist =>
+           (if not show_ex then
+              ()
+            else let
+              (* invent names for bound variables that are new, i.e. in Ts, but not in params *)
+              (* we assume that Ts still contains (map snd params) as a suffix                *)
+              val new_count = length Ts - length params - 1
+              val new_names = map Name.bound (0 upto new_count)
+              val params'   = (new_names @ map fst params) ~~ Ts
+            in
+              trace_ex (sg, params', atoms, discr initems, n, hist)
+            end; NONE)
     end
     | refute [] js = SOME js
 in refute end;
 
-fun refute sg ps ex items = refutes sg ps ex (split_items items) [];
+(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
 
-fun refute_tac ss (i,justs) =
+fun refute sg params show_ex do_pre terms =
+  refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
+
+(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
+
+fun refute_tac ss (i, justs) =
   fn state =>
-    let val sg = #sign(rep_thm state)
-        val {neqE, ...} = Data.get sg;
-        fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
-          METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
-    in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
-       EVERY(map just1 justs)
-    end
-    state;
+    let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
+        val sg          = theory_of_thm state
+        val {neqE, ...} = Data.get sg
+        fun just1 j =
+          REPEAT_DETERM (eresolve_tac neqE i) THEN                  (* eliminate inequalities *)
+            METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i  (* use theorems generated from the actual justifications *)
+    in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN  (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
+       DETERM (LA_Data.pre_tac i) THEN                               (* user-defined preprocessing of the subgoal *)
+       PRIMITIVE (trace_thm "State after pre_tac:") THEN
+       EVERY (map just1 justs)                                       (* prove every resulting subgoal, using its justification *)
+    end  state;
 
-fun count P xs = length(List.filter P xs);
+(* ('a -> bool) -> 'a list -> int *)
+
+fun count P xs = length (List.filter P xs);
 
 (* The limit on the number of ~= allowed.
    Because each ~= is split into two cases, this can lead to an explosion.
 *)
 val fast_arith_neq_limit = ref 9;
 
-fun prove sg ps ex Hs concl =
-let val Hitems = map (LA_Data.decomp sg) Hs
-in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
-      > !fast_arith_neq_limit then NONE
-   else
-   case LA_Data.decomp sg concl of
-     NONE => refute sg ps ex (Hitems@[NONE])
-   | SOME(citem as (r,i,rel,l,j,d)) =>
-       let val neg::rel0 = explode rel
-           val nrel = if neg = "~" then implode rel0 else "~"^rel
-       in refute sg ps ex (Hitems @ [SOME(r,i,nrel,l,j,d)]) end
-end;
+(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
+
+fun prove sg params show_ex do_pre Hs concl =
+  let
+    (* append the negated conclusion to 'Hs' -- this corresponds to     *)
+    (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
+    (* theorem/tactic level                                             *)
+    val Hs' = Hs @ [LA_Logic.neg_prop concl]
+    (* decompT option -> bool *)
+    fun is_neq NONE                 = false
+      | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
+  in
+    trace_msg "prove";
+    if count is_neq (map (LA_Data.decomp sg) Hs')
+      > !fast_arith_neq_limit then (
+      trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
+      NONE
+    ) else
+      refute sg params show_ex do_pre Hs'
+  end;
 
 (*
 Fast but very incomplete decider. Only premises and conclusions
 that are already (negated) (in)equations are taken into account.
 *)
-fun simpset_lin_arith_tac ss ex i st = SUBGOAL (fn (A,_) =>
-  let val params = rev(Logic.strip_params A)
-      val pTs = map snd params
-      val Hs = Logic.strip_assums_hyp A
-      val concl = Logic.strip_assums_concl A
+fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
+  let val params = rev (Logic.strip_params A)
+      val Hs     = Logic.strip_assums_hyp A
+      val concl  = Logic.strip_assums_concl A
   in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
-     case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of
+     case prove (Thm.sign_of_thm st) params show_ex true Hs concl of
        NONE => (trace_msg "Refutation failed."; no_tac)
-     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
+     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
   end) i st;
 
-fun lin_arith_tac ex i st =
+fun lin_arith_tac show_ex i st =
   simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
-    ex i st;
+    show_ex i st;
 
 fun cut_lin_arith_tac ss i =
   cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
@@ -673,47 +775,77 @@
 datatype splittree = Tip of thm list
                    | Spl of thm * cterm * splittree * cterm * splittree
 
+(* the cterm "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *)
+
+(* Thm.cterm -> Thm.cterm * Thm.cterm *)
+
 fun extract imp =
-let val (Il,r) = Thm.dest_comb imp
-    val (_,imp1) = Thm.dest_comb Il
-    val (Ict1,_) = Thm.dest_comb imp1
-    val (_,ct1) = Thm.dest_comb Ict1
-    val (Ir,_) = Thm.dest_comb r
-    val (_,Ict2r) = Thm.dest_comb Ir
-    val (Ict2,_) = Thm.dest_comb Ict2r
-    val (_,ct2) = Thm.dest_comb Ict2
-in (ct1,ct2) end;
+let val (Il, r)    = Thm.dest_comb imp
+    val (_, imp1)  = Thm.dest_comb Il
+    val (Ict1, _)  = Thm.dest_comb imp1
+    val (_, ct1)   = Thm.dest_comb Ict1
+    val (Ir, _)    = Thm.dest_comb r
+    val (_, Ict2r) = Thm.dest_comb Ir
+    val (Ict2, _)  = Thm.dest_comb Ict2r
+    val (_, ct2)   = Thm.dest_comb Ict2
+in (ct1, ct2) end;
+
+(* Theory.theory -> Thm.thm list -> splittree *)
 
 fun splitasms sg asms =
-let val {neqE, ...}  = Data.get sg;
-    fun split(asms',[]) = Tip(rev asms')
-      | split(asms',asm::asms) =
-      (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
-       of SOME spl =>
-          let val (ct1,ct2) = extract(cprop_of spl)
-              val thm1 = assume ct1 and thm2 = assume ct2
-          in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2]))
+let val {neqE, ...} = Data.get sg
+    fun elim_neq (asms', []) = Tip (rev asms')
+      | elim_neq (asms', asm::asms) =
+      (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
+        SOME spl =>
+          let val (ct1, ct2) = extract (cprop_of spl)
+              val thm1 = assume ct1
+              val thm2 = assume ct2
+          in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
           end
-       | NONE => split(asm::asms', asms))
-in split([],asms) end;
+      | NONE => elim_neq (asm::asms', asms))
+in elim_neq ([], asms) end;
+
+(* Theory.theory * MetaSimplifier.simpset -> splittree -> injust list -> (Thm.thm, injust list) *)
 
 fun fwdproof ctxt (Tip asms) (j::js) = (mkthm ctxt asms j, js)
-  | fwdproof ctxt (Spl(thm,ct1,tree1,ct2,tree2)) js =
-    let val (thm1,js1) = fwdproof ctxt tree1 js
-        val (thm2,js2) = fwdproof ctxt tree2 js1
+  | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js =
+    let val (thm1, js1) = fwdproof ctxt tree1 js
+        val (thm2, js2) = fwdproof ctxt tree2 js1
         val thm1' = implies_intr ct1 thm1
         val thm2' = implies_intr ct2 thm2
     in (thm2' COMP (thm1' COMP thm), js2) end;
 (* needs handle THM _ => NONE ? *)
 
-fun prover (ctxt as (sg, _)) thms Tconcl js pos =
-let val nTconcl = LA_Logic.neg_prop Tconcl
-    val cnTconcl = cterm_of sg nTconcl
-    val nTconclthm = assume cnTconcl
-    val tree = splitasms sg (thms @ [nTconclthm])
-    val (thm,_) = fwdproof ctxt tree js
-    val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
-in SOME(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end
+(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
+
+fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
+let 
+(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *)
+(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *)
+    (* There is no "forward version" of 'pre_tac'.  Therefore we combine the     *)
+    (* available theorems into a single proof state and perform "backward proof" *)
+    (* using 'refute_tac'.                                                       *)
+(*
+    val Hs    = map prop_of thms
+    val Prop  = fold (curry Logic.mk_implies) (rev Hs) Tconcl
+    val cProp = cterm_of sg Prop
+    val concl = Goal.init cProp
+                  |> refute_tac ss (1, js)
+                  |> Seq.hd
+                  |> Goal.finish
+                  |> fold (fn thA => fn thAB => implies_elim thAB thA) thms
+*)
+(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
+    val nTconcl       = LA_Logic.neg_prop Tconcl
+    val cnTconcl      = cterm_of sg nTconcl
+    val nTconclthm    = assume cnTconcl
+    val tree          = splitasms sg (thms @ [nTconclthm])
+    val (Falsethm, _) = fwdproof ctxt tree js
+    val contr         = if pos then LA_Logic.ccontr else LA_Logic.notI
+    val concl         = implies_intr cnTconcl Falsethm COMP contr
+in SOME (trace_thm "Proved by lin. arith. prover:"
+          (LA_Logic.mk_Eq concl)) end
 (* in case concl contains ?-var, which makes assume fail: *)
 handle THM _ => NONE;
 
@@ -723,15 +855,22 @@
    2. lin_arith_prover is applied by the simplifier which
       dives into terms and will thus try the non-negated concl anyway.
 *)
+
+(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
+
 fun lin_arith_prover sg ss concl =
-let
-    val thms = maps LA_Logic.atomize (prems_of_ss ss);
-    val Hs = map (#prop o rep_thm) thms
+let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
+    val Hs = map prop_of thms
     val Tconcl = LA_Logic.mk_Trueprop concl
-in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
+(*
+    val _ = trace_msg "lin_arith_prover"
+    val _ = map (trace_thm "thms:") thms
+    val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl)
+*)
+in case prove sg [] false false Hs Tconcl of (* concl provable? *)
      SOME js => prover (sg, ss) thms Tconcl js true
    | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl
-          in case prove sg ([],[]) false Hs nTconcl of (* ~concl provable? *)
+          in case prove sg [] false false Hs nTconcl of (* ~concl provable? *)
                SOME js => prover (sg, ss) thms nTconcl js false
              | NONE => NONE
           end
diff -r f30b73385060 -r 25b068a99d2b src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/Provers/splitter.ML	Wed Jul 26 19:23:04 2006 +0200
@@ -13,18 +13,23 @@
 signature SPLITTER_DATA =
 sig
   val mk_eq         : thm -> thm
-  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
-  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
-  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
-  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
-  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
-  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
-  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
-  val notnotD       : thm (* "~ ~ P ==> P"                         *)
+  val meta_eq_to_iff: thm (* "x == y ==> x = y"                      *)
+  val iffD          : thm (* "[| P = Q; Q |] ==> P"                  *)
+  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R"   *)
+  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R"   *)
+  val exE           : thm (* "[| EX x. P x; !!x. P x ==> Q |] ==> Q" *)
+  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"            *)
+  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"            *)
+  val notnotD       : thm (* "~ ~ P ==> P"                           *)
 end
 
 signature SPLITTER =
 sig
+  (* somewhat more internal functions *)
+  val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list
+  val split_posns        : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term ->
+    (thm * (typ * typ * int list) list * int list * typ * term) list  (* first argument is a "cmap", returns a list of "split packs" *)
+  (* the "real" interface, providing a number of tactics *)
   val split_tac       : thm list -> int -> tactic
   val split_inside_tac: thm list -> int -> tactic
   val split_asm_tac   : thm list -> int -> tactic
@@ -52,18 +57,42 @@
 val const_Trueprop = ObjectLogic.judgment_name (the_context ());
 
 
-fun split_format_err() = error("Wrong format for split rule");
+fun split_format_err () = error "Wrong format for split rule";
 
+(* thm -> (string * typ) * bool *)
 fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
      Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
        (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
      | _ => split_format_err ())
    | _ => split_format_err ();
 
+(* thm list -> (string * (typ * term * thm * typ * int) list) list *)
+fun cmap_of_split_thms thms =
+let
+  val splits = map Data.mk_eq thms
+  fun add_thm (cmap, thm) =
+        (case concl_of thm of _$(t as _$lhs)$_ =>
+           (case strip_comb lhs of (Const(a,aT),args) =>
+              let val info = (aT,lhs,thm,fastype_of t,length args)
+              in case AList.lookup (op =) cmap a of
+                   SOME infos => AList.update (op =) (a, info::infos) cmap
+                 | NONE => (a,[info])::cmap
+              end
+            | _ => split_format_err())
+         | _ => split_format_err())
+in
+  Library.foldl add_thm ([], splits)
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* mk_case_split_tac                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+(* (int * int -> order) -> thm list -> int -> tactic * <split_posns> *)
+
 fun mk_case_split_tac order =
 let
 
-
 (************************************************************
    Create lift-theorem "trlift" :
 
@@ -71,7 +100,8 @@
 
 *************************************************************)
 
-val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
+val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
+
 val lift =
   let val ct = read_cterm Pure.thy
            ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
@@ -129,12 +159,12 @@
 
 
 (* add all loose bound variables in t to list is *)
-fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
+fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
 
 (* check if the innermost abstraction that needs to be removed
    has a body of type T; otherwise the expansion thm will fail later on
 *)
-fun type_test(T,lbnos,apsns) =
+fun type_test (T,lbnos,apsns) =
   let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
   in T=U end;
 
@@ -166,7 +196,7 @@
           lifting is required before applying the split-theorem.
 ******************************************************************************)
 
-fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
+fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
   if n > length ts then []
   else let val lev = length apsns
            val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
@@ -198,26 +228,34 @@
    see Pure/pattern.ML for the full version;
 *)
 local
-exception MATCH
+  exception MATCH
 in
-fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
-                          handle Type.TYPE_MATCH => raise MATCH;
-fun fomatch sg args =
-  let
-    fun mtch tyinsts = fn
-        (Ts,Var(_,T), t)  => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
-      | (_,Free (a,T), Free (b,U)) =>
-          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
-      | (_,Const (a,T), Const (b,U))  =>
-          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
-      | (_,Bound i, Bound j)  =>  if  i=j  then tyinsts else raise MATCH
-      | (Ts,Abs(_,T,t), Abs(_,U,u))  =>
-          mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
-      | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
-      | _ => raise MATCH
-  in (mtch Vartab.empty args; true) handle MATCH => false end;
-end
+  (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *)
+  fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
+                            handle Type.TYPE_MATCH => raise MATCH
+  (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *)
+  fun fomatch sg args =
+    let
+      (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *)
+      fun mtch tyinsts = fn
+          (Ts, Var(_,T), t) =>
+            typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
+        | (_, Free (a,T), Free (b,U)) =>
+            if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
+        | (_, Const (a,T), Const (b,U)) =>
+            if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
+        | (_, Bound i, Bound j) =>
+            if i=j then tyinsts else raise MATCH
+        | (Ts, Abs(_,T,t), Abs(_,U,u)) =>
+            mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
+        | (Ts, f$t, g$u) =>
+            mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
+        | _ => raise MATCH
+    in (mtch Vartab.empty args; true) handle MATCH => false end;
+end  (* local *)
 
+(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
+  (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
 fun split_posns cmap sg Ts t =
   let
     val T' = fastype_of1 (Ts, t);
@@ -243,15 +281,13 @@
           in snd(Library.foldl iter ((0, a), ts)) end
   in posns Ts [] [] t end;
 
+fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
 
-fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
-
-fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
+fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
   prod_ord (int_ord o pairself length) (order o pairself length)
     ((ps, pos), (qs, qos));
 
 
-
 (************************************************************
    call split_posns with appropriate parameters
 *************************************************************)
@@ -261,8 +297,10 @@
       val goali = nth_subgoal i state
       val Ts = rev(map #2 (Logic.strip_params goali))
       val _ $ t $ _ = Logic.strip_assums_concl goali;
-  in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
+  in (Ts, t, sort shorter (split_posns cmap sg Ts t)) end;
 
+fun exported_split_posns cmap sg Ts t =
+  sort shorter (split_posns cmap sg Ts t);
 
 (*************************************************************
    instantiate lift theorem
@@ -322,20 +360,11 @@
    i      : number of subgoal the tactic should be applied to
 *****************************************************************************)
 
+(* thm list -> int -> tactic *)
+
 fun split_tac [] i = no_tac
   | split_tac splits i =
-  let val splits = map Data.mk_eq splits;
-      fun add_thm(cmap,thm) =
-            (case concl_of thm of _$(t as _$lhs)$_ =>
-               (case strip_comb lhs of (Const(a,aT),args) =>
-                  let val info = (aT,lhs,thm,fastype_of t,length args)
-                  in case AList.lookup (op =) cmap a of
-                       SOME infos => AList.update (op =) (a, info::infos) cmap
-                     | NONE => (a,[info])::cmap
-                  end
-                | _ => split_format_err())
-             | _ => split_format_err())
-      val cmap = Library.foldl add_thm ([],splits);
+  let val cmap = cmap_of_split_thms splits
       fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
       fun lift_split_tac state =
             let val (Ts, t, splits) = select cmap state i
@@ -352,12 +381,12 @@
           (rtac meta_iffD i THEN lift_split_tac)
   end;
 
-in split_tac end;
+in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
 
 
-val split_tac        = mk_case_split_tac              int_ord;
+val (split_tac, split_posns)        = mk_case_split_tac              int_ord;
 
-val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
+val (split_inside_tac, _)           = mk_case_split_tac (rev_order o int_ord);
 
 
 (*****************************************************************************
@@ -378,7 +407,7 @@
               |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
                                         first_prem_is_disj t
               |   first_prem_is_disj _ = false;
-      (* does not work properly if the split variable is bound by a quantfier *)
+      (* does not work properly if the split variable is bound by a quantifier *)
               fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
                            (if first_prem_is_disj t
                             then EVERY[etac Data.disjE i,rotate_tac ~1 i,
@@ -387,11 +416,11 @@
                             else all_tac)
                            THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
                            THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
-          in if n<0 then no_tac else DETERM (EVERY'
+          in if n<0 then  no_tac  else (DETERM (EVERY'
                 [rotate_tac n, etac Data.contrapos2,
                  split_tac splits,
                  rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
-                 flat_prems_tac] i)
+                 flat_prems_tac] i))
           end;
   in SUBGOAL tac
   end;