linear arithmetic splits certain operators (e.g. min, max, abs)
authorwebertj
Wed Jul 26 19:23:04 2006 +0200 (2006-07-26)
changeset 2021725b068a99d2b
parent 20216 f30b73385060
child 20218 be3bfb0699ba
linear arithmetic splits certain operators (e.g. min, max, abs)
NEWS
doc-src/TutorialI/Advanced/WFrec.thy
doc-src/TutorialI/Advanced/document/WFrec.tex
src/HOL/Algebra/UnivPoly.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard_Public.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Binomial.thy
src/HOL/Complex/CLim.thy
src/HOL/Divides.thy
src/HOL/HoareParallel/Graph.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Machines.thy
src/HOL/IMPP/Hoare.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Presburger.thy
src/HOL/Lambda/Eta.thy
src/HOL/Library/Word.thy
src/HOL/List.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/NumberTheory/Finite2.thy
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Int2.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/HOL/Presburger.thy
src/HOL/Real/Float.thy
src/HOL/Real/RComplete.thy
src/HOL/Real/RealDef.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/HOL/ZF/HOLZF.thy
src/HOL/arith_data.ML
src/HOL/ex/Adder.thy
src/HOL/simpdata.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/splitter.ML
     1.1 --- a/NEWS	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/NEWS	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -510,6 +510,12 @@
     1.4    (i.e. a boolean expression) by compiling it to ML. The goal is
     1.5    "proved" (via the oracle "Evaluation") if it evaluates to True.
     1.6  
     1.7 +* Linear arithmetic now splits certain operators (e.g. min, max, abs) also
     1.8 +when invoked by the simplifier.  This results in the simplifier being more
     1.9 +powerful on arithmetic goals.
    1.10 +INCOMPATIBILTY: rewrite proofs.  Set fast_arith_split_limit to 0 to obtain
    1.11 +the old behavior.
    1.12 +
    1.13  * Support for hex (0x20) and binary (0b1001) numerals. 
    1.14  
    1.15  *** HOL-Algebra ***
     2.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 13:31:07 2006 +0200
     2.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Jul 26 19:23:04 2006 +0200
     2.3 @@ -90,19 +90,10 @@
     2.4  
     2.5  \noindent
     2.6  The inclusion remains to be proved. After unfolding some definitions, 
     2.7 -we are left with simple arithmetic:
     2.8 +we are left with simple arithmetic that is dispatched automatically.
     2.9  *}
    2.10  
    2.11 -apply (clarify, simp add: measure_def inv_image_def)
    2.12 -
    2.13 -txt{*
    2.14 -@{subgoals[display,indent=0,margin=65]}
    2.15 -
    2.16 -\noindent
    2.17 -And that is dispatched automatically:
    2.18 -*}
    2.19 -
    2.20 -by arith
    2.21 +by (clarify, simp add: measure_def inv_image_def)
    2.22  
    2.23  text{*\noindent
    2.24  
     3.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 13:31:07 2006 +0200
     3.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Jul 26 19:23:04 2006 +0200
     3.3 @@ -119,22 +119,11 @@
     3.4  
     3.5  \noindent
     3.6  The inclusion remains to be proved. After unfolding some definitions, 
     3.7 -we are left with simple arithmetic:%
     3.8 -\end{isamarkuptxt}%
     3.9 -\isamarkuptrue%
    3.10 -\isacommand{apply}\isamarkupfalse%
    3.11 -\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
    3.12 -\begin{isamarkuptxt}%
    3.13 -\begin{isabelle}%
    3.14 -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b%
    3.15 -\end{isabelle}
    3.16 -
    3.17 -\noindent
    3.18 -And that is dispatched automatically:%
    3.19 +we are left with simple arithmetic that is dispatched automatically.%
    3.20  \end{isamarkuptxt}%
    3.21  \isamarkuptrue%
    3.22  \isacommand{by}\isamarkupfalse%
    3.23 -\ arith%
    3.24 +\ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}%
    3.25  \endisatagproof
    3.26  {\isafoldproof}%
    3.27  %
     4.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Jul 26 13:31:07 2006 +0200
     4.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Jul 26 19:23:04 2006 +0200
     4.3 @@ -972,13 +972,13 @@
     4.4      next
     4.5        case (Suc j)
     4.6        have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
     4.7 -        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
     4.8 +        using Suc by (auto intro!: funcset_mem [OF Rg])
     4.9        have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
    4.10 -        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
    4.11 +        using Suc by (auto intro!: funcset_mem [OF Rg])
    4.12        have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
    4.13          using Suc by (auto intro!: funcset_mem [OF Rf])
    4.14        have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
    4.15 -        using Suc by (auto intro!: funcset_mem [OF Rg]) arith
    4.16 +        using Suc by (auto intro!: funcset_mem [OF Rg])
    4.17        have R11: "g 0 \<in> carrier R"
    4.18          using Suc by (auto intro!: funcset_mem [OF Rg])
    4.19        from Suc show ?case
     5.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 13:31:07 2006 +0200
     5.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 19:23:04 2006 +0200
     5.3 @@ -231,7 +231,7 @@
     5.4  "greatest_msg other = 0"
     5.5  
     5.6  lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
     5.7 -by (induct X, auto, arith+)
     5.8 +by (induct X, auto)
     5.9  
    5.10  subsubsection{*sets of keys*}
    5.11  
     6.1 --- a/src/HOL/Auth/Guard/Guard_Public.thy	Wed Jul 26 13:31:07 2006 +0200
     6.2 +++ b/src/HOL/Auth/Guard/Guard_Public.thy	Wed Jul 26 19:23:04 2006 +0200
     6.3 @@ -95,7 +95,7 @@
     6.4  apply (induct evs, auto simp: initState.simps)
     6.5  apply (drule used_sub_parts_used, safe)
     6.6  apply (drule greatest_msg_is_greatest, arith)
     6.7 -by (simp, arith)
     6.8 +by simp
     6.9  
    6.10  subsubsection{*function giving a new nonce*}
    6.11  
    6.12 @@ -171,4 +171,4 @@
    6.13  apply (frule_tac A=A in priK_analz_iff_bad)
    6.14  by (simp add: knows_decomp)+
    6.15  
    6.16 -end
    6.17 \ No newline at end of file
    6.18 +end
     7.1 --- a/src/HOL/Bali/AxCompl.thy	Wed Jul 26 13:31:07 2006 +0200
     7.2 +++ b/src/HOL/Bali/AxCompl.thy	Wed Jul 26 19:23:04 2006 +0200
     7.3 @@ -1421,7 +1421,6 @@
     7.4  apply (drule finite_subset)
     7.5  apply (erule finite_imageI)
     7.6  apply auto
     7.7 -apply arith
     7.8  done
     7.9  
    7.10  
     8.1 --- a/src/HOL/Binomial.thy	Wed Jul 26 13:31:07 2006 +0200
     8.2 +++ b/src/HOL/Binomial.thy	Wed Jul 26 19:23:04 2006 +0200
     8.3 @@ -33,9 +33,8 @@
     8.4  by simp
     8.5  
     8.6  lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
     8.7 -apply (induct "n", auto)
     8.8 -apply (erule allE)
     8.9 -apply (erule mp, arith)
    8.10 +apply (induct "n")
    8.11 +apply auto
    8.12  done
    8.13  
    8.14  declare binomial_0 [simp del] binomial_Suc [simp del]
     9.1 --- a/src/HOL/Complex/CLim.thy	Wed Jul 26 13:31:07 2006 +0200
     9.2 +++ b/src/HOL/Complex/CLim.thy	Wed Jul 26 19:23:04 2006 +0200
     9.3 @@ -178,7 +178,7 @@
     9.4  apply (simp add: CInfinitesimal_hcmod_iff star_of_def
     9.5              Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod,  blast)
     9.6  apply (drule_tac x = r in spec, clarify)
     9.7 -apply (drule FreeUltrafilterNat_all, ultra, arith)
     9.8 +apply (drule FreeUltrafilterNat_all, ultra)
     9.9  done
    9.10  
    9.11  
    10.1 --- a/src/HOL/Divides.thy	Wed Jul 26 13:31:07 2006 +0200
    10.2 +++ b/src/HOL/Divides.thy	Wed Jul 26 19:23:04 2006 +0200
    10.3 @@ -710,8 +710,7 @@
    10.4    apply (rule iffI)
    10.5    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
    10.6  prefer 3; apply assumption
    10.7 -  apply (simp_all add: quorem_def)
    10.8 -  apply arith
    10.9 +  apply (simp_all add: quorem_def) apply arith
   10.10    apply (rule conjI)
   10.11    apply (rule_tac P="%x. n * (m div n) \<le> x" in
   10.12      subst [OF mod_div_equality [of _ n]])
    11.1 --- a/src/HOL/HoareParallel/Graph.thy	Wed Jul 26 13:31:07 2006 +0200
    11.2 +++ b/src/HOL/HoareParallel/Graph.thy	Wed Jul 26 19:23:04 2006 +0200
    11.3 @@ -126,7 +126,6 @@
    11.4   apply(case_tac "j=R")
    11.5    apply(erule_tac x = "Suc i" in allE)
    11.6    apply simp
    11.7 -  apply arith
    11.8   apply (force simp add:nth_list_update)
    11.9  apply simp
   11.10  apply(erule exE)
   11.11 @@ -154,7 +153,6 @@
   11.12  apply simp
   11.13  apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
   11.14   prefer 2 apply arith
   11.15 -apply simp
   11.16  apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
   11.17   prefer 2 apply arith
   11.18  apply simp
   11.19 @@ -175,24 +173,16 @@
   11.20   prefer 2 apply arith
   11.21   apply(drule_tac n = "Suc nata" in Compl_lemma)
   11.22   apply clarify
   11.23 + ML {* fast_arith_split_limit := 0; *}  (*FIXME*)
   11.24   apply force
   11.25 + ML {* fast_arith_split_limit := 9; *}  (*FIXME*)
   11.26  apply(drule leI)
   11.27  apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
   11.28   apply(erule_tac x = "m - (Suc nata)" in allE)
   11.29   apply(case_tac "m")
   11.30    apply simp
   11.31   apply simp
   11.32 - apply(subgoal_tac "natb - nata < Suc natb")
   11.33 -  prefer 2 apply(erule thin_rl)+ apply arith
   11.34 - apply simp
   11.35 - apply(case_tac "length path")
   11.36 -  apply force
   11.37 -apply (erule_tac V = "Suc natb \<le> length path - Suc 0" in thin_rl)
   11.38  apply simp
   11.39 -apply(frule_tac i1 = "length path" and j1 = "length path - Suc 0" and k1 = "m" in diff_diff_right [THEN mp])
   11.40 -apply(erule_tac V = "length path - Suc m + nat = length path - Suc 0" in thin_rl)
   11.41 -apply simp
   11.42 -apply arith
   11.43  done
   11.44  
   11.45  
   11.46 @@ -253,8 +243,6 @@
   11.47    apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
   11.48      prefer 2 apply arith
   11.49     apply simp
   11.50 -  apply(erule mp)
   11.51 -  apply arith
   11.52  --{* T is a root *}
   11.53   apply(case_tac "m=0")
   11.54    apply force
    12.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Wed Jul 26 13:31:07 2006 +0200
    12.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Wed Jul 26 19:23:04 2006 +0200
    12.3 @@ -298,7 +298,6 @@
    12.4  --{* 98 verification conditions *}
    12.5  apply auto 
    12.6  --{* auto takes about 3 minutes !! *}
    12.7 -apply arith+
    12.8  done
    12.9  
   12.10  text {* Easier Version: without AWAIT.  Apt and Olderog. page 256: *}
   12.11 @@ -332,7 +331,6 @@
   12.12  --{* 20 vc *}
   12.13  apply auto
   12.14  --{* auto takes aprox. 2 minutes. *}
   12.15 -apply arith+
   12.16  done
   12.17  
   12.18  subsection {* Producer/Consumer *}
    13.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
    13.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
    13.3 @@ -361,11 +361,8 @@
    13.4  apply clarify
    13.5  apply(frule_tac j=0 and k="j" and p=pre in stability)
    13.6        apply simp_all
    13.7 -    apply arith
    13.8    apply(erule_tac x=i in allE,simp)
    13.9   apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all)
   13.10 -  apply arith
   13.11 - apply arith
   13.12  apply(case_tac "x!j")
   13.13  apply clarify
   13.14  apply simp
   13.15 @@ -492,11 +489,8 @@
   13.16  apply(simp add:assum_def)
   13.17  apply clarify
   13.18  apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all)
   13.19 -   apply arith
   13.20    apply(erule_tac x=i in allE,simp)
   13.21   apply(erule_tac i=j in unique_ctran_Await,force,simp_all)
   13.22 -  apply arith
   13.23 - apply arith
   13.24  apply(case_tac "x!j")
   13.25  apply clarify
   13.26  apply simp
   13.27 @@ -543,7 +537,6 @@
   13.28      apply(simp add:assum_def)
   13.29     apply(simp add:assum_def)
   13.30    apply(erule_tac m="length x" in etran_or_ctran,simp+)
   13.31 -  apply(case_tac x,simp+)
   13.32   apply(case_tac x, (simp add:last_length)+)
   13.33  apply(erule exE)
   13.34  apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence)
   13.35 @@ -555,18 +548,7 @@
   13.36   apply(erule_tac x="sa" in allE)
   13.37   apply(drule_tac c="drop (Suc m) x" in subsetD)
   13.38    apply simp
   13.39 -  apply(rule conjI)
   13.40 -   apply force
   13.41    apply clarify
   13.42 -  apply(subgoal_tac "(Suc m) + i \<le> length x")
   13.43 -   apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
   13.44 -    apply(rotate_tac -2)
   13.45 -    apply simp
   13.46 -    apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
   13.47 -    apply(subgoal_tac "Suc (Suc (m + i)) < length x",simp)
   13.48 -    apply arith
   13.49 -   apply arith
   13.50 -  apply arith
   13.51   apply simp
   13.52   apply clarify
   13.53   apply(case_tac "i\<le>m")
   13.54 @@ -575,49 +557,33 @@
   13.55     apply(erule_tac x=i in allE, erule impE, assumption)
   13.56     apply simp+
   13.57   apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   13.58 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   13.59 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   13.60 -    apply(rotate_tac -2)
   13.61 -    apply simp
   13.62 -    apply(erule mp)
   13.63 -    apply arith
   13.64 -   apply arith
   13.65 -  apply arith
   13.66 -  apply(case_tac "length (drop (Suc m) x)",simp)
   13.67 -  apply(erule_tac x="sa" in allE)
   13.68 -  back
   13.69 -  apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
   13.70 -   apply(rule conjI)
   13.71 -    apply force
   13.72 -   apply clarify
   13.73 -   apply(subgoal_tac "(Suc m) + i \<le> length x")
   13.74 -    apply(subgoal_tac "(Suc m) + (Suc i) \<le> length x")
   13.75 -     apply(rotate_tac -2)
   13.76 -     apply simp
   13.77 -     apply(erule_tac x="Suc (m + i)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE)
   13.78 -     apply(subgoal_tac "Suc (Suc (m + i)) < length x")
   13.79 -      apply simp
   13.80 -     apply arith
   13.81 -    apply arith
   13.82 -   apply arith
   13.83 -  apply simp
   13.84 -  apply clarify
   13.85 -  apply(case_tac "i\<le>m")
   13.86 -   apply(drule le_imp_less_or_eq)
   13.87 -   apply(erule disjE)
   13.88 -    apply(erule_tac x=i in allE, erule impE, assumption)
   13.89 -    apply simp
   13.90 + apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   13.91 +  apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   13.92 +   apply(rotate_tac -2)
   13.93     apply simp
   13.94 -  apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
   13.95 -  apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
   13.96 -   apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
   13.97 -    apply(rotate_tac -2)
   13.98 -    apply simp
   13.99 -    apply(erule mp)
  13.100 -   apply arith
  13.101    apply arith
  13.102   apply arith
  13.103 - done  
  13.104 +apply(case_tac "length (drop (Suc m) x)",simp)
  13.105 +apply(erule_tac x="sa" in allE)
  13.106 +back
  13.107 +apply(drule_tac c="drop (Suc m) x" in subsetD,simp)
  13.108 + apply clarify
  13.109 +apply simp
  13.110 +apply clarify
  13.111 +apply(case_tac "i\<le>m")
  13.112 + apply(drule le_imp_less_or_eq)
  13.113 + apply(erule disjE)
  13.114 +  apply(erule_tac x=i in allE, erule impE, assumption)
  13.115 +  apply simp
  13.116 + apply simp
  13.117 +apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE)
  13.118 +apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x")
  13.119 + apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x")
  13.120 +  apply(rotate_tac -2)
  13.121 +  apply simp
  13.122 + apply arith
  13.123 +apply arith
  13.124 +done
  13.125  
  13.126  subsubsection{* Soundness of the Sequential rule *}
  13.127  
  13.128 @@ -862,8 +828,6 @@
  13.129        apply simp
  13.130        apply(erule mp)
  13.131        apply(case_tac ys,simp+)
  13.132 -     apply arith
  13.133 -    apply arith
  13.134     apply force
  13.135    apply arith
  13.136   apply force
    14.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Jul 26 13:31:07 2006 +0200
    14.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Wed Jul 26 19:23:04 2006 +0200
    14.3 @@ -364,7 +364,7 @@
    14.4  apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
    14.5  apply (rule bexI [OF _ Rep_star_star_n], auto)
    14.6  apply (rule_tac x = "exp u" in exI)
    14.7 -apply (ultra, arith)
    14.8 +apply ultra
    14.9  done
   14.10  
   14.11  lemma starfun_exp_add_HFinite_Infinitesimal_approx:
    15.1 --- a/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 13:31:07 2006 +0200
    15.2 +++ b/src/HOL/Hyperreal/Integration.thy	Wed Jul 26 19:23:04 2006 +0200
    15.3 @@ -323,7 +323,6 @@
    15.4  apply (drule add_strict_mono, assumption)
    15.5  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
    15.6                  mult_less_cancel_right)
    15.7 -apply arith
    15.8  done
    15.9  
   15.10  lemma Integral_zero [simp]: "Integral(a,a) f 0"
   15.11 @@ -423,7 +422,7 @@
   15.12                       \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>"
   15.13         in order_trans)
   15.14  apply (rule abs_triangle_ineq [THEN [2] order_trans])
   15.15 -apply (simp add: right_diff_distrib, arith)
   15.16 +apply (simp add: right_diff_distrib)
   15.17  apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst])
   15.18  apply (rule add_mono)
   15.19  apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans)
   15.20 @@ -434,7 +433,7 @@
   15.21  apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
   15.22  apply (rule order_trans)
   15.23  apply (auto simp add: abs_le_interval_iff)
   15.24 -apply (simp add: right_diff_distrib, arith)
   15.25 +apply (simp add: right_diff_distrib)
   15.26  done
   15.27  
   15.28  lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   15.29 @@ -577,7 +576,7 @@
   15.30  apply (auto dest: partition_lt_cancel)
   15.31  apply (rule_tac x=N and y=n in linorder_cases)
   15.32  apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
   15.33 -apply (drule_tac n = n in partition_lt_gen, auto, arith)
   15.34 +apply (drule_tac n = n in partition_lt_gen, auto)
   15.35  apply (drule_tac x = n in spec)
   15.36  apply (simp split: split_if_asm)
   15.37  done
   15.38 @@ -741,7 +740,6 @@
   15.39        ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
   15.40  apply (simp add: tpart_def partition_def, safe)
   15.41  apply (rule_tac x = "N - n" in exI, auto)
   15.42 -apply (drule_tac x = "na + n" in spec, arith)+
   15.43  done
   15.44  
   15.45  lemma fine_right1:
   15.46 @@ -752,7 +750,7 @@
   15.47        ==> fine ga (%x. D(x + n),%x. p(x + n))"
   15.48  apply (auto simp add: fine_def gauge_def)
   15.49  apply (drule_tac x = "na + n" in spec)
   15.50 -apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   15.51 +apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto)
   15.52  apply (simp add: tpart_def, safe)
   15.53  apply (subgoal_tac "D n \<le> p (na + n)")
   15.54  apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq)
   15.55 @@ -783,7 +781,7 @@
   15.56  apply ((drule spec)+, auto)
   15.57  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)
   15.58  apply (auto simp only: rsum_add left_distrib [symmetric]
   15.59 -                mult_2_right [symmetric] real_mult_less_iff1, arith)
   15.60 +                mult_2_right [symmetric] real_mult_less_iff1)
   15.61  done
   15.62  
   15.63  lemma partition_lt_gen2:
   15.64 @@ -834,7 +832,7 @@
   15.65  apply arith
   15.66  apply (drule add_strict_mono, assumption)
   15.67  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   15.68 -                       real_mult_less_iff1, arith)
   15.69 +                       real_mult_less_iff1)
   15.70  done
   15.71  
   15.72  lemma Integral_imp_Cauchy:
   15.73 @@ -853,7 +851,7 @@
   15.74  apply (erule_tac V = "0 < e" in thin_rl)
   15.75  apply (drule add_strict_mono, assumption)
   15.76  apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   15.77 -                       real_mult_less_iff1, arith)
   15.78 +                       real_mult_less_iff1)
   15.79  done
   15.80  
   15.81  lemma Cauchy_iff2:
    16.1 --- a/src/HOL/Hyperreal/Lim.thy	Wed Jul 26 13:31:07 2006 +0200
    16.2 +++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 26 19:23:04 2006 +0200
    16.3 @@ -1484,7 +1484,7 @@
    16.4  apply (rule_tac x = s in exI, clarify)
    16.5  apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
    16.6  apply (drule_tac x = "xa-x" in spec)
    16.7 -apply (auto simp add: abs_ge_self, arith+)
    16.8 +apply (auto simp add: abs_ge_self)
    16.9  done
   16.10  
   16.11  text{*Refine the above to existence of least upper bound*}
   16.12 @@ -2236,6 +2236,8 @@
   16.13    thus ?thesis by simp
   16.14  qed
   16.15  
   16.16 +ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}
   16.17 +
   16.18  lemma LIMSEQ_SEQ_conv2:
   16.19    assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
   16.20    shows "X -- a --> L"
   16.21 @@ -2316,6 +2318,7 @@
   16.22    ultimately show False by simp
   16.23  qed
   16.24  
   16.25 +ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
   16.26  
   16.27  lemma LIMSEQ_SEQ_conv:
   16.28    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L) = (X -- a --> L)"
    17.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 26 13:31:07 2006 +0200
    17.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jul 26 19:23:04 2006 +0200
    17.3 @@ -390,7 +390,7 @@
    17.4  
    17.5  lemma mod_exhaust_less_4:
    17.6       "m mod 4 = 0 | m mod 4 = 1 | m mod 4 = 2 | m mod 4 = (3::nat)"
    17.7 -by (case_tac "m mod 4", auto, arith)
    17.8 +by auto
    17.9  
   17.10  lemma Suc_Suc_mult_two_diff_two [rule_format, simp]:
   17.11       "0 < n --> Suc (Suc (2 * n - 2)) = 2*n"
    18.1 --- a/src/HOL/Hyperreal/NSA.thy	Wed Jul 26 13:31:07 2006 +0200
    18.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Jul 26 19:23:04 2006 +0200
    18.3 @@ -1349,7 +1349,8 @@
    18.4        ==> hypreal_of_real x + u < hypreal_of_real y"
    18.5  apply (simp add: Infinitesimal_def)
    18.6  apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)
    18.7 -apply (simp add: abs_less_iff)
    18.8 +(* FIXME: arith simproc bug with   apply (simp add: abs_less_iff) *)
    18.9 +apply simp
   18.10  done
   18.11  
   18.12  lemma Infinitesimal_add_hrabs_hypreal_of_real_less:
    19.1 --- a/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 13:31:07 2006 +0200
    19.2 +++ b/src/HOL/Hyperreal/Poly.thy	Wed Jul 26 19:23:04 2006 +0200
    19.3 @@ -1023,7 +1023,7 @@
    19.4  apply (induct "p", auto)
    19.5  apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
    19.6  apply (rule abs_triangle_ineq)
    19.7 -apply (auto intro!: mult_mono simp add: abs_mult, arith)
    19.8 +apply (auto intro!: mult_mono simp add: abs_mult)
    19.9  done
   19.10  
   19.11  end
    20.1 --- a/src/HOL/Hyperreal/SEQ.thy	Wed Jul 26 13:31:07 2006 +0200
    20.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 26 19:23:04 2006 +0200
    20.3 @@ -745,7 +745,6 @@
    20.4  apply (simp add: Bseq_def, safe)
    20.5  apply (rule_tac x = "K + \<bar>X N\<bar> " in exI)
    20.6  apply auto
    20.7 -apply arith
    20.8  apply (rule_tac x = N in exI, safe)
    20.9  apply (drule_tac x = n in spec, arith)
   20.10  apply (auto simp add: Bseq_iff2)
   20.11 @@ -754,7 +753,7 @@
   20.12  lemma BseqI2: "(\<forall>n. k \<le> f n & f n \<le> K) ==> Bseq f"
   20.13  apply (simp add: Bseq_def)
   20.14  apply (rule_tac x = " (\<bar>k\<bar> + \<bar>K\<bar>) + 1" in exI, auto)
   20.15 -apply (drule_tac [2] x = n in spec, arith+)
   20.16 +apply (drule_tac x = n in spec, arith)
   20.17  done
   20.18  
   20.19  
   20.20 @@ -824,9 +823,7 @@
   20.21  
   20.22  lemma lemmaCauchy: "\<forall>n \<ge> M. \<bar>X M + - X n\<bar> < (1::real)
   20.23            ==>  \<forall>n \<ge> M. \<bar>X n\<bar> < 1 + \<bar>X M\<bar>"
   20.24 -apply safe
   20.25 -apply (drule spec, auto, arith)
   20.26 -done
   20.27 +by auto
   20.28  
   20.29  lemma less_Suc_cancel_iff: "(n < Suc M) = (n \<le> M)"
   20.30  by auto
    21.1 --- a/src/HOL/Hyperreal/Series.thy	Wed Jul 26 13:31:07 2006 +0200
    21.2 +++ b/src/HOL/Hyperreal/Series.thy	Wed Jul 26 19:23:04 2006 +0200
    21.3 @@ -274,10 +274,6 @@
    21.4  apply (induct "no", auto)
    21.5  apply (drule_tac x = "Suc no" in spec)
    21.6  apply (simp add: add_ac)
    21.7 -(* FIXME why does simp require a separate step to prove the (pure arithmetic)
    21.8 -   left-over? With del cong: strong_setsum_cong it works!
    21.9 -*)
   21.10 -apply simp
   21.11  done
   21.12  
   21.13  lemma sumr_pos_lt_pair:
   21.14 @@ -299,15 +295,7 @@
   21.15  apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
   21.16  prefer 3 apply assumption
   21.17  apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
   21.18 -apply simp_all 
   21.19 -apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
   21.20 -apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
   21.21 -prefer 3 apply simp
   21.22 -apply (drule_tac [2] x = 0 in spec)
   21.23 - prefer 2 apply simp 
   21.24 -apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
   21.25 -apply (simp add: abs_if)
   21.26 -apply (auto simp add: linorder_not_less [symmetric])
   21.27 +apply simp_all
   21.28  done
   21.29  
   21.30  text{*A summable series of positive terms has limit that is at least as
    22.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 26 13:31:07 2006 +0200
    22.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jul 26 19:23:04 2006 +0200
    22.3 @@ -526,7 +526,7 @@
    22.4  apply (rule setsum_abs [THEN real_le_trans])
    22.5  apply (rule real_setsum_nat_ivl_bounded)
    22.6  apply (auto dest!: less_add_one intro!: mult_mono simp add: power_add abs_mult)
    22.7 -apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
    22.8 +apply (auto intro!: power_mono zero_le_power simp add: power_abs)
    22.9  done
   22.10  
   22.11  lemma lemma_termdiff4: 
   22.12 @@ -576,9 +576,10 @@
   22.13  done
   22.14  
   22.15  
   22.16 -
   22.17  text{* FIXME: Long proofs*}
   22.18  
   22.19 +ML {* val old_fast_arith_split_limit = !fast_arith_split_limit; fast_arith_split_limit := 0; *}  (* FIXME: rewrite proofs *)
   22.20 +
   22.21  lemma termdiffs_aux:
   22.22       "[|summable (\<lambda>n. diffs (diffs c) n * K ^ n); \<bar>x\<bar> < \<bar>K\<bar> |]
   22.23      ==> (\<lambda>h. \<Sum>n. c n *
   22.24 @@ -641,6 +642,8 @@
   22.25  apply (auto intro: abs_triangle_ineq [THEN order_trans], arith)
   22.26  done
   22.27  
   22.28 +ML {* fast_arith_split_limit := old_fast_arith_split_limit; *}
   22.29 +
   22.30  lemma termdiffs: 
   22.31      "[| summable(%n. c(n) * (K ^ n));  
   22.32          summable(%n. (diffs c)(n) * (K ^ n));  
   22.33 @@ -748,7 +751,7 @@
   22.34  apply (subst lemma_exp_ext)
   22.35  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)")
   22.36  apply (rule_tac [2] K = "1 + \<bar>x\<bar>" in termdiffs)
   22.37 -apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs, arith)
   22.38 +apply (auto intro: exp_converges [THEN sums_summable] simp add: exp_fdiffs)
   22.39  done
   22.40  
   22.41  lemma lemma_sin_ext:
   22.42 @@ -769,14 +772,14 @@
   22.43  apply (subst lemma_sin_ext)
   22.44  apply (auto simp add: sin_fdiffs2 [symmetric])
   22.45  apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
   22.46 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs, arith)
   22.47 +apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs)
   22.48  done
   22.49  
   22.50  lemma DERIV_cos [simp]: "DERIV cos x :> -sin(x)"
   22.51  apply (subst lemma_cos_ext)
   22.52  apply (auto simp add: lemma_sin_minus cos_fdiffs2 [symmetric] minus_mult_left)
   22.53  apply (rule_tac K = "1 + \<bar>x\<bar>" in termdiffs)
   22.54 -apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus, arith)
   22.55 +apply (auto intro: sin_converges cos_converges sums_summable intro!: sums_minus [THEN sums_summable] simp add: cos_fdiffs sin_fdiffs diffs_minus)
   22.56  done
   22.57  
   22.58  
   22.59 @@ -2533,7 +2536,7 @@
   22.60  apply (rule_tac x = ea in exI, auto)
   22.61  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)
   22.62  apply auto
   22.63 -apply (drule sym, auto, arith)
   22.64 +apply (drule sym, auto)
   22.65  done
   22.66  
   22.67  lemma isCont_inv_fun_inv:
    23.1 --- a/src/HOL/IMP/Compiler.thy	Wed Jul 26 13:31:07 2006 +0200
    23.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Jul 26 19:23:04 2006 +0200
    23.3 @@ -101,7 +101,6 @@
    23.4  apply(rule ccontr)
    23.5  apply(drule_tac f = length in arg_cong)
    23.6  apply simp
    23.7 -apply arith
    23.8  done
    23.9  
   23.10  lemma reduce_exec1:
   23.11 @@ -293,6 +292,6 @@
   23.12    with ob show "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c t" by fast
   23.13  qed
   23.14  
   23.15 -(* To Do: connect with Machine 0 using M_equiv *)
   23.16 +(* TODO: connect with Machine 0 using M_equiv *)
   23.17  
   23.18 -end
   23.19 \ No newline at end of file
   23.20 +end
    24.1 --- a/src/HOL/IMP/Machines.thy	Wed Jul 26 13:31:07 2006 +0200
    24.2 +++ b/src/HOL/IMP/Machines.thy	Wed Jul 26 19:23:04 2006 +0200
    24.3 @@ -168,11 +168,10 @@
    24.4      apply fastsimp
    24.5     apply simp
    24.6    apply simp
    24.7 -  apply arith
    24.8   apply simp
    24.9 - apply arith
   24.10  apply(fastsimp simp add:exec01.JMPB)
   24.11  done
   24.12 +
   24.13  (*
   24.14  lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)"
   24.15  apply(induct xs)
   24.16 @@ -188,6 +187,7 @@
   24.17  apply simp_all
   24.18  done
   24.19  *)
   24.20 +
   24.21  lemma direction2:
   24.22   "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow>
   24.23    rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow>
    25.1 --- a/src/HOL/IMPP/Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
    25.2 +++ b/src/HOL/IMPP/Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
    25.3 @@ -381,7 +381,6 @@
    25.4  apply (drule finite_subset)
    25.5  apply (erule finite_imageI)
    25.6  apply (simp (no_asm_simp))
    25.7 -apply arith
    25.8  done
    25.9  
   25.10  lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>  
    26.1 --- a/src/HOL/Integ/IntArith.thy	Wed Jul 26 13:31:07 2006 +0200
    26.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Jul 26 19:23:04 2006 +0200
    26.3 @@ -324,9 +324,6 @@
    26.4  apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
    26.5         in int_val_lemma)
    26.6  apply simp
    26.7 -apply (erule impE)
    26.8 - apply (intro strip)
    26.9 - apply (erule_tac x = "i+m" in allE, arith)
   26.10  apply (erule exE)
   26.11  apply (rule_tac x = "i+m" in exI, arith)
   26.12  done
    27.1 --- a/src/HOL/Integ/IntDef.thy	Wed Jul 26 13:31:07 2006 +0200
    27.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Jul 26 19:23:04 2006 +0200
    27.3 @@ -387,7 +387,7 @@
    27.4  lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
    27.5  proof -
    27.6    have "(\<lambda>(x,y). {x-y}) respects intrel"
    27.7 -    by (simp add: congruent_def, arith) 
    27.8 +    by (simp add: congruent_def, arith)
    27.9    thus ?thesis
   27.10      by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
   27.11  qed
    28.1 --- a/src/HOL/Integ/NatBin.thy	Wed Jul 26 13:31:07 2006 +0200
    28.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Jul 26 19:23:04 2006 +0200
    28.3 @@ -88,12 +88,11 @@
    28.4  
    28.5  text{*Suggested by Matthias Daum*}
    28.6  lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
    28.7 -apply (subgoal_tac "nat x div nat k < nat x") 
    28.8 - apply (simp add: nat_div_distrib [symmetric])
    28.9 +apply (subgoal_tac "nat x div nat k < nat x")
   28.10 + apply (simp (asm_lr) add: nat_div_distrib [symmetric])
   28.11  apply (rule Divides.div_less_dividend, simp_all) 
   28.12  done
   28.13  
   28.14 -
   28.15  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
   28.16  
   28.17  (*"neg" is used in rewrite rules for binary comparisons*)
   28.18 @@ -148,7 +147,6 @@
   28.19           else let d = z-z' in     
   28.20                if neg d then 0 else nat d)"
   28.21  apply (simp add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   28.22 -apply (simp add: diff_is_0_eq nat_le_eq_zle)
   28.23  done
   28.24  
   28.25  lemma diff_nat_number_of [simp]: 
   28.26 @@ -628,7 +626,6 @@
   28.27  
   28.28  lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   28.29    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   28.30 -  apply (simp add: neg_nat)
   28.31    done
   28.32  
   28.33  lemma nat_number_of_BIT_1:
   28.34 @@ -676,7 +673,7 @@
   28.35  by (simp only: mult_2 nat_add_distrib of_nat_add) 
   28.36  
   28.37  lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
   28.38 -by (simp only:  nat_number_of_def, simp)
   28.39 +by (simp only: nat_number_of_def)
   28.40  
   28.41  lemma of_nat_number_of_lemma:
   28.42       "of_nat (number_of v :: nat) =  
    29.1 --- a/src/HOL/Integ/Presburger.thy	Wed Jul 26 13:31:07 2006 +0200
    29.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Jul 26 19:23:04 2006 +0200
    29.3 @@ -558,17 +558,13 @@
    29.4  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
    29.5  apply(induct rule: int_gr_induct)
    29.6   apply simp
    29.7 - apply arith
    29.8  apply (simp add:int_distrib)
    29.9 -apply arith
   29.10  done
   29.11  
   29.12  lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   29.13  apply(induct rule: int_gr_induct)
   29.14   apply simp
   29.15 - apply arith
   29.16  apply (simp add:int_distrib)
   29.17 -apply arith
   29.18  done
   29.19  
   29.20  lemma  minusinfinity:
    30.1 --- a/src/HOL/Lambda/Eta.thy	Wed Jul 26 13:31:07 2006 +0200
    30.2 +++ b/src/HOL/Lambda/Eta.thy	Wed Jul 26 19:23:04 2006 +0200
    30.3 @@ -50,8 +50,7 @@
    30.4  lemma free_lift [simp]:
    30.5      "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    30.6    apply (induct t fixing: i k)
    30.7 -    apply (auto cong: conj_cong)
    30.8 -  apply arith
    30.9 +  apply (auto cong: conj_cong)
   30.10    done
   30.11  
   30.12  lemma free_subst [simp]:
    31.1 --- a/src/HOL/Library/Word.thy	Wed Jul 26 13:31:07 2006 +0200
    31.2 +++ b/src/HOL/Library/Word.thy	Wed Jul 26 19:23:04 2006 +0200
    31.3 @@ -1383,7 +1383,7 @@
    31.4  proof (rule ccontr)
    31.5    from w0 wk
    31.6    have k1: "1 < k"
    31.7 -    by (cases "k - 1",simp_all,arith)
    31.8 +    by (cases "k - 1",simp_all)
    31.9    assume "~ length (int_to_bv i) \<le> k"
   31.10    hence "k < length (int_to_bv i)"
   31.11      by simp
   31.12 @@ -1512,7 +1512,7 @@
   31.13  proof (rule ccontr)
   31.14    from w1 wk
   31.15    have k1: "1 < k"
   31.16 -    by (cases "k - 1",simp_all,arith)
   31.17 +    by (cases "k - 1",simp_all)
   31.18    assume "~ length (int_to_bv i) \<le> k"
   31.19    hence "k < length (int_to_bv i)"
   31.20      by simp
   31.21 @@ -1731,8 +1731,6 @@
   31.22    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)"
   31.23      apply (cases "length w1 \<le> length w2")
   31.24      apply (auto simp add: max_def)
   31.25 -    apply arith
   31.26 -    apply arith
   31.27      done
   31.28    also have "... = 2 ^ max (length w1) (length w2)"
   31.29    proof -
   31.30 @@ -1982,7 +1980,6 @@
   31.31            apply simp
   31.32            apply (subst zpower_zadd_distrib [symmetric])
   31.33            apply simp
   31.34 -          apply arith
   31.35            done
   31.36          finally show "?Q < 2 ^ (length w1 + length w2 - Suc 0)"
   31.37            .
   31.38 @@ -2030,10 +2027,6 @@
   31.39          apply simp
   31.40          apply (subst zpower_zadd_distrib [symmetric])
   31.41          apply simp
   31.42 -        apply (cut_tac lmw)
   31.43 -        apply arith
   31.44 -        apply (cut_tac p)
   31.45 -        apply arith
   31.46          done
   31.47        hence "-((2::int) ^ (length w1 + length w2 - Suc 0)) \<le> -(2^(length w1 - 1) * 2 ^ (length w2 - 1))"
   31.48          by simp
   31.49 @@ -2278,13 +2271,13 @@
   31.50    by (simp add: bv_chop_def Let_def)
   31.51  
   31.52  lemma bv_chop_length_fst [simp]: "length (fst (bv_chop w i)) = length w - i"
   31.53 -  by (simp add: bv_chop_def Let_def,arith)
   31.54 +  by (simp add: bv_chop_def Let_def)
   31.55  
   31.56  lemma bv_chop_length_snd [simp]: "length (snd (bv_chop w i)) = min i (length w)"
   31.57 -  by (simp add: bv_chop_def Let_def,arith)
   31.58 +  by (simp add: bv_chop_def Let_def)
   31.59  
   31.60  lemma bv_slice_length [simp]: "[| j \<le> i; i < length w |] ==> length (bv_slice w (i,j)) = i - j + 1"
   31.61 -  by (auto simp add: bv_slice_def,arith)
   31.62 +  by (auto simp add: bv_slice_def)
   31.63  
   31.64  definition
   31.65    length_nat :: "nat => nat"
   31.66 @@ -2337,7 +2330,6 @@
   31.67      apply (drule norm_empty_bv_to_nat_zero)
   31.68      using prems
   31.69      apply simp
   31.70 -    apply arith
   31.71      apply (cases "norm_unsigned (nat_to_bv (nat i))")
   31.72      apply (drule norm_empty_bv_to_nat_zero [of "nat_to_bv (nat i)"])
   31.73      using prems
   31.74 @@ -2439,7 +2431,6 @@
   31.75      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])
   31.76      apply simp_all
   31.77      apply (simp_all add: w_defs min_def)
   31.78 -    apply arith+
   31.79      done
   31.80  qed
   31.81  
   31.82 @@ -2514,11 +2505,7 @@
   31.83  lemma length_int_mono_gt0: "[| 0 \<le> x ; x \<le> y |] ==> length_int x \<le> length_int y"
   31.84    by (cases "x = 0",simp_all add: length_int_gt0 nat_le_eq_zle)
   31.85  
   31.86 -lemma length_int_mono_lt0: "[| x \<le> y ; y \<le> 0 |] ==> length_int y \<le> length_int x"
   31.87 -  apply (cases "y = 0",simp_all add: length_int_lt0)
   31.88 -  apply (subgoal_tac "nat (- y) - Suc 0 \<le> nat (- x) - Suc 0")
   31.89 -  apply (simp add: length_nat_mono)
   31.90 -  apply arith
   31.91 +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)
   31.92    done
   31.93  
   31.94  lemmas [simp] = length_nat_non0
    32.1 --- a/src/HOL/List.thy	Wed Jul 26 13:31:07 2006 +0200
    32.2 +++ b/src/HOL/List.thy	Wed Jul 26 19:23:04 2006 +0200
    32.3 @@ -1691,7 +1691,6 @@
    32.4  lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
    32.5  apply(induct j)
    32.6  apply auto
    32.7 -apply arith
    32.8  done
    32.9  
   32.10  lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
    33.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Jul 26 13:31:07 2006 +0200
    33.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Jul 26 19:23:04 2006 +0200
    33.3 @@ -994,8 +994,6 @@
    33.4    apply (subst foldseq_almostzero[of _ j])
    33.5    apply (simp add: prems)+
    33.6    apply (auto)
    33.7 -  apply (insert ncols_le[of A j])
    33.8 -  apply (arith)
    33.9    proof -
   33.10      fix k
   33.11      fix l
    34.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Jul 26 13:31:07 2006 +0200
    34.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Jul 26 19:23:04 2006 +0200
    34.3 @@ -454,8 +454,10 @@
    34.4  apply (simp add: max_of_list_def)
    34.5  apply (induct xs)
    34.6  apply simp
    34.7 +ML {* fast_arith_split_limit := 0; *}  (* FIXME *)
    34.8  apply simp
    34.9  apply arith
   34.10 +ML {* fast_arith_split_limit := 9; *}  (* FIXME *)
   34.11  done
   34.12  
   34.13  
   34.14 @@ -520,16 +522,7 @@
   34.15  lemma pc_succs_shift: "pc'\<in>set (succs i (pc'' + n))
   34.16   \<Longrightarrow> ((pc' - n) \<in>set (succs i pc''))"
   34.17  apply (induct i)
   34.18 -apply simp+
   34.19 -  (* case Goto *)
   34.20 -apply arith
   34.21 -  (* case Ifcmpeq *)
   34.22 -apply simp
   34.23 -apply (erule disjE)
   34.24 -apply arith
   34.25 -apply arith
   34.26 -  (* case Throw *)
   34.27 -apply simp
   34.28 +apply (arith|simp)+
   34.29  done
   34.30  
   34.31  
   34.32 @@ -537,16 +530,7 @@
   34.33    \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk> 
   34.34    \<Longrightarrow> n \<le> pc'"
   34.35  apply (induct i)
   34.36 -apply simp+
   34.37 -  (* case Goto *)
   34.38 -apply arith
   34.39 -  (* case Ifcmpeq *)
   34.40 -apply simp
   34.41 -apply (erule disjE)
   34.42 -apply simp
   34.43 -apply arith
   34.44 -  (* case Throw *)
   34.45 -apply simp
   34.46 +apply (arith|simp)+
   34.47  done
   34.48  
   34.49  
   34.50 @@ -975,7 +959,6 @@
   34.51  apply (simp (no_asm_simp))+
   34.52  apply simp
   34.53  apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
   34.54 -apply (simp (no_asm_simp))+
   34.55  
   34.56    (* show check_type \<dots> *)
   34.57  apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
   34.58 @@ -2100,7 +2083,6 @@
   34.59    apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
   34.60    apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
   34.61      (* \<dots> ! nat (int pc + i) = \<dots> ! pc *)
   34.62 -  apply (simp (no_asm_simp) only: int_outside_right nat_int, simp (no_asm_simp))
   34.63    apply (simp (no_asm_simp) add: length_compTpExpr length_compTpStmt)
   34.64    apply (simp (no_asm_simp) add: pushST_def popST_def nochangeST_def)
   34.65    apply (simp only: compTpExpr_LT_ST compTpStmt_LT_ST)
    35.1 --- a/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 13:31:07 2006 +0200
    35.2 +++ b/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 19:23:04 2006 +0200
    35.3 @@ -179,10 +179,6 @@
    35.4  lemma int_card_bdd_int_set_l_l: "0 < n ==>
    35.5      int(card {x. 0 < x & x < n}) = n - 1"
    35.6    apply (auto simp add: card_bdd_int_set_l_l)
    35.7 -  apply (subgoal_tac "Suc 0 \<le> nat n")
    35.8 -   apply (auto simp add: zdiff_int [symmetric])
    35.9 -  apply (subgoal_tac "0 < nat n", arith)
   35.10 -  apply (simp add: zero_less_nat_eq)
   35.11    done
   35.12  
   35.13  lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>
    36.1 --- a/src/HOL/NumberTheory/Gauss.thy	Wed Jul 26 13:31:07 2006 +0200
    36.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Wed Jul 26 19:23:04 2006 +0200
    36.3 @@ -104,8 +104,6 @@
    36.4    apply (auto simp add: A_def ResSet_def)
    36.5    apply (rule_tac m = p in zcong_less_eq)
    36.6    apply (insert p_g_2, auto)
    36.7 -  apply (subgoal_tac [1-2] "(p - 1) div 2 < p")
    36.8 -  apply (auto, auto simp add: p_minus_one_l)
    36.9    done
   36.10  
   36.11  lemma (in GAUSS) B_res: "ResSet p B"
   36.12 @@ -255,6 +253,8 @@
   36.13  lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   36.14    by (auto simp add: D_eq)
   36.15  
   36.16 +ML {* fast_arith_split_limit := 0; *} (*FIXME*)
   36.17 +
   36.18  lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   36.19    apply (auto simp add: F_eq A_def)
   36.20  proof -
   36.21 @@ -270,6 +270,8 @@
   36.22      using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   36.23  qed
   36.24  
   36.25 +ML {* fast_arith_split_limit := 9; *} (*FIXME*)
   36.26 +
   36.27  lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   36.28    using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   36.29  
    37.1 --- a/src/HOL/NumberTheory/Int2.thy	Wed Jul 26 13:31:07 2006 +0200
    37.2 +++ b/src/HOL/NumberTheory/Int2.thy	Wed Jul 26 19:23:04 2006 +0200
    37.3 @@ -191,7 +191,7 @@
    37.4    have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
    37.5      by auto
    37.6    also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
    37.7 -    by (simp only: nat_add_distrib, auto)
    37.8 +    by (simp only: nat_add_distrib)
    37.9    also have "p - 2 + 1 = p - 1" by arith
   37.10    finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
   37.11      by (rule ssubst, auto)
    38.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 13:31:07 2006 +0200
    38.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Wed Jul 26 19:23:04 2006 +0200
    38.3 @@ -193,6 +193,8 @@
    38.4    then show ?thesis by auto
    38.5  qed
    38.6  
    38.7 +ML {* fast_arith_split_limit := 0; *} (*FIXME*)
    38.8 +
    38.9  lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
   38.10      (p * b \<noteq> q * a)"
   38.11  proof
   38.12 @@ -234,6 +236,8 @@
   38.13    with q_g_2 show False by auto
   38.14  qed
   38.15  
   38.16 +ML {* fast_arith_split_limit := 9; *} (*FIXME*)
   38.17 +
   38.18  lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   38.19    using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
   38.20  
    39.1 --- a/src/HOL/Presburger.thy	Wed Jul 26 13:31:07 2006 +0200
    39.2 +++ b/src/HOL/Presburger.thy	Wed Jul 26 19:23:04 2006 +0200
    39.3 @@ -558,17 +558,13 @@
    39.4  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
    39.5  apply(induct rule: int_gr_induct)
    39.6   apply simp
    39.7 - apply arith
    39.8  apply (simp add:int_distrib)
    39.9 -apply arith
   39.10  done
   39.11  
   39.12  lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   39.13  apply(induct rule: int_gr_induct)
   39.14   apply simp
   39.15 - apply arith
   39.16  apply (simp add:int_distrib)
   39.17 -apply arith
   39.18  done
   39.19  
   39.20  lemma  minusinfinity:
    40.1 --- a/src/HOL/Real/Float.thy	Wed Jul 26 13:31:07 2006 +0200
    40.2 +++ b/src/HOL/Real/Float.thy	Wed Jul 26 19:23:04 2006 +0200
    40.3 @@ -28,9 +28,7 @@
    40.4      apply (auto, induct_tac n)
    40.5      apply (simp_all add: pow2_def)
    40.6      apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    40.7 -    apply (auto simp add: h)
    40.8 -    apply arith
    40.9 -    done
   40.10 +    by (auto simp add: h)
   40.11    show ?thesis
   40.12    proof (induct a)
   40.13      case (1 n)
    41.1 --- a/src/HOL/Real/RComplete.thy	Wed Jul 26 13:31:07 2006 +0200
    41.2 +++ b/src/HOL/Real/RComplete.thy	Wed Jul 26 19:23:04 2006 +0200
    41.3 @@ -1066,10 +1066,7 @@
    41.4    apply (subgoal_tac "real a = real (int a)")
    41.5    apply (erule ssubst)
    41.6    apply simp
    41.7 -  apply (subst nat_diff_distrib)
    41.8    apply simp
    41.9 -  apply (rule le_floor)
   41.10 -  apply simp_all
   41.11  done
   41.12  
   41.13  lemma natceiling_zero [simp]: "natceiling 0 = 0"
   41.14 @@ -1206,13 +1203,7 @@
   41.15    apply (subgoal_tac "real a = real (int a)")
   41.16    apply (erule ssubst)
   41.17    apply simp
   41.18 -  apply (subst nat_diff_distrib)
   41.19    apply simp
   41.20 -  apply (rule order_trans)
   41.21 -  prefer 2
   41.22 -  apply (rule ceiling_mono2)
   41.23 -  apply assumption
   41.24 -  apply simp_all
   41.25  done
   41.26  
   41.27  lemma natfloor_div_nat: "1 <= x ==> 0 < y ==>
    42.1 --- a/src/HOL/Real/RealDef.thy	Wed Jul 26 13:31:07 2006 +0200
    42.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jul 26 19:23:04 2006 +0200
    42.3 @@ -1024,15 +1024,9 @@
    42.4  by (simp add: real_of_nat_ge_zero)
    42.5  
    42.6  lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x"
    42.7 -apply (simp add: linorder_not_less)
    42.8 -apply (auto intro: abs_ge_self [THEN order_trans])
    42.9 -done
   42.10 +by simp
   42.11   
   42.12  lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
   42.13 -apply (simp add: real_add_assoc)
   42.14 -apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
   42.15 -apply (rule real_add_assoc [THEN subst])
   42.16 -apply (rule abs_triangle_ineq)
   42.17 -done
   42.18 +by simp
   42.19  
   42.20  end
    43.1 --- a/src/HOL/Set.thy	Wed Jul 26 13:31:07 2006 +0200
    43.2 +++ b/src/HOL/Set.thy	Wed Jul 26 19:23:04 2006 +0200
    43.3 @@ -33,6 +33,7 @@
    43.4    Pow           :: "'a set => 'a set set"                -- "powerset"
    43.5    Ball          :: "'a set => ('a => bool) => bool"      -- "bounded universal quantifiers"
    43.6    Bex           :: "'a set => ('a => bool) => bool"      -- "bounded existential quantifiers"
    43.7 +  Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
    43.8    image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
    43.9    "op :"        :: "'a => 'a set => bool"                -- "membership"
   43.10  
   43.11 @@ -117,11 +118,13 @@
   43.12    "@UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" 10)
   43.13    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   43.14    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   43.15 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
   43.16    "_Bleast"       :: "id => 'a set => bool => 'a"      ("(3LEAST _:_./ _)" [0, 0, 10] 10)
   43.17  
   43.18  syntax (HOL)
   43.19    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3! _:_./ _)" [0, 0, 10] 10)
   43.20    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   43.21 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
   43.22  
   43.23  translations
   43.24    "{x, xs}"     == "insert x {xs}"
   43.25 @@ -138,16 +141,19 @@
   43.26    "INT x:A. B"  == "INTER A (%x. B)"
   43.27    "ALL x:A. P"  == "Ball A (%x. P)"
   43.28    "EX x:A. P"   == "Bex A (%x. P)"
   43.29 +  "EX! x:A. P"  == "Bex1 A (%x. P)"
   43.30    "LEAST x:A. P" => "LEAST x. x:A & P"
   43.31  
   43.32  syntax (xsymbols)
   43.33    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   43.34    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   43.35 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   43.36    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
   43.37  
   43.38  syntax (HTML output)
   43.39    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   43.40    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   43.41 +  "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   43.42  
   43.43  syntax (xsymbols)
   43.44    "@Collect"    :: "idt => 'a set => bool => 'a set"      ("(1{_ \<in>/ _./ _})")
   43.45 @@ -178,30 +184,35 @@
   43.46    "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   43.47    "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   43.48    "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
   43.49 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
   43.50  
   43.51  syntax (xsymbols)
   43.52    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   43.53    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   43.54    "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.55    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.56 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.57  
   43.58  syntax (HOL output)
   43.59    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   43.60    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
   43.61    "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3! _<=_./ _)" [0, 0, 10] 10)
   43.62    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   43.63 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
   43.64  
   43.65  syntax (HTML output)
   43.66    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
   43.67    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
   43.68    "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.69    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.70 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
   43.71  
   43.72  translations
   43.73   "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
   43.74 - "\<exists>A\<subset>B. P"    =>  "EX A. A \<subset> B & P"
   43.75 - "\<forall>A\<subseteq>B. P"  =>  "ALL A. A \<subseteq> B --> P"
   43.76 + "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
   43.77 + "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
   43.78   "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
   43.79 + "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
   43.80  
   43.81  print_translation {*
   43.82  let
   43.83 @@ -316,6 +327,7 @@
   43.84  defs
   43.85    Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
   43.86    Bex_def:      "Bex A P        == EX x. x:A & P(x)"
   43.87 +  Bex1_def:     "Bex1 A P       == EX! x. x:A & P(x)"
   43.88  
   43.89  defs (overloaded)
   43.90    subset_def:   "A <= B         == ALL x:A. x:B"
    44.1 --- a/src/HOL/SetInterval.thy	Wed Jul 26 13:31:07 2006 +0200
    44.2 +++ b/src/HOL/SetInterval.thy	Wed Jul 26 19:23:04 2006 +0200
    44.3 @@ -301,7 +301,7 @@
    44.4    show "?B \<subseteq> ?A"
    44.5    proof
    44.6      fix n assume a: "n : ?B"
    44.7 -    hence "n - k : {i..j}" by auto arith+
    44.8 +    hence "n - k : {i..j}" by auto
    44.9      moreover have "n = (n - k) + k" using a by auto
   44.10      ultimately show "n : ?A" by blast
   44.11    qed
   44.12 @@ -315,7 +315,7 @@
   44.13    show "?B \<subseteq> ?A"
   44.14    proof
   44.15      fix n assume a: "n : ?B"
   44.16 -    hence "n - k : {i..<j}" by auto arith+
   44.17 +    hence "n - k : {i..<j}" by auto
   44.18      moreover have "n = (n - k) + k" using a by auto
   44.19      ultimately show "n : ?A" by blast
   44.20    qed
   44.21 @@ -384,7 +384,6 @@
   44.22    apply (rule card_image)
   44.23    apply (simp add: inj_on_def)
   44.24    apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
   44.25 -  apply arith
   44.26    apply (rule_tac x = "x - l" in exI)
   44.27    apply arith
   44.28    done
    45.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 13:31:07 2006 +0200
    45.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 19:23:04 2006 +0200
    45.3 @@ -35,7 +35,6 @@
    45.4        setsum f (lessThan n) <= setsum g (lessThan n)"
    45.5  apply (induct_tac "n")
    45.6  apply (auto simp add: lessThan_Suc)
    45.7 -apply (drule_tac x = n in spec, arith)
    45.8  done
    45.9  
   45.10  lemma tokens_mono_prefix [rule_format]:
    46.1 --- a/src/HOL/ZF/HOLZF.thy	Wed Jul 26 13:31:07 2006 +0200
    46.2 +++ b/src/HOL/ZF/HOLZF.thy	Wed Jul 26 19:23:04 2006 +0200
    46.3 @@ -578,7 +578,6 @@
    46.4  	apply (insert n_less_u)
    46.5  	apply (insert u)
    46.6  	apply auto
    46.7 -	apply arith
    46.8  	done
    46.9        ultimately show False by auto
   46.10      qed
    47.1 --- a/src/HOL/arith_data.ML	Wed Jul 26 13:31:07 2006 +0200
    47.2 +++ b/src/HOL/arith_data.ML	Wed Jul 26 19:23:04 2006 +0200
    47.3 @@ -29,7 +29,6 @@
    47.4      funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    47.5    end;
    47.6  
    47.7 -
    47.8  (* dest_sum *)
    47.9  
   47.10  val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
   47.11 @@ -44,7 +43,6 @@
   47.12            SOME (t, u) => dest_sum t @ dest_sum u
   47.13          | NONE => [tm]));
   47.14  
   47.15 -
   47.16  (** generic proof tools **)
   47.17  
   47.18  (* prove conversions *)
   47.19 @@ -57,7 +55,6 @@
   47.20  val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   47.21    (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
   47.22  
   47.23 -
   47.24  (* rewriting *)
   47.25  
   47.26  fun simp_all_tac rules =
   47.27 @@ -70,7 +67,8 @@
   47.28  fun prep_simproc (name, pats, proc) =
   47.29    Simplifier.simproc (the_context ()) name pats proc;
   47.30  
   47.31 -end;
   47.32 +end;  (* NatArithUtils *)
   47.33 +
   47.34  
   47.35  signature ARITH_DATA =
   47.36  sig
   47.37 @@ -78,12 +76,12 @@
   47.38    val nat_cancel_sums: simproc list
   47.39  end;
   47.40  
   47.41 +
   47.42  structure ArithData: ARITH_DATA =
   47.43  struct
   47.44  
   47.45  open NatArithUtils;
   47.46  
   47.47 -
   47.48  (** cancel common summands **)
   47.49  
   47.50  structure Sum =
   47.51 @@ -99,7 +97,6 @@
   47.52  fun gen_uncancel_tac rule ct =
   47.53    rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
   47.54  
   47.55 -
   47.56  (* nat eq *)
   47.57  
   47.58  structure EqCancelSums = CancelSumsFun
   47.59 @@ -110,7 +107,6 @@
   47.60    val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
   47.61  end);
   47.62  
   47.63 -
   47.64  (* nat less *)
   47.65  
   47.66  structure LessCancelSums = CancelSumsFun
   47.67 @@ -121,7 +117,6 @@
   47.68    val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
   47.69  end);
   47.70  
   47.71 -
   47.72  (* nat le *)
   47.73  
   47.74  structure LeCancelSums = CancelSumsFun
   47.75 @@ -132,7 +127,6 @@
   47.76    val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
   47.77  end);
   47.78  
   47.79 -
   47.80  (* nat diff *)
   47.81  
   47.82  structure DiffCancelSums = CancelSumsFun
   47.83 @@ -143,8 +137,6 @@
   47.84    val uncancel_tac = gen_uncancel_tac diff_cancel;
   47.85  end);
   47.86  
   47.87 -
   47.88 -
   47.89  (** prepare nat_cancel simprocs **)
   47.90  
   47.91  val nat_cancel_sums_add = map prep_simproc
   47.92 @@ -159,7 +151,7 @@
   47.93    [prep_simproc ("natdiff_cancel_sums",
   47.94      ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
   47.95  
   47.96 -end;
   47.97 +end;  (* ArithData *)
   47.98  
   47.99  open ArithData;
  47.100  
  47.101 @@ -172,6 +164,7 @@
  47.102  
  47.103  structure LA_Logic: LIN_ARITH_LOGIC =
  47.104  struct
  47.105 +
  47.106  val ccontr = ccontr;
  47.107  val conjI = conjI;
  47.108  val notI = notI;
  47.109 @@ -179,7 +172,6 @@
  47.110  val not_lessD = linorder_not_less RS iffD1;
  47.111  val not_leD = linorder_not_le RS iffD1;
  47.112  
  47.113 -
  47.114  fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
  47.115  
  47.116  val mk_Trueprop = HOLogic.mk_Trueprop;
  47.117 @@ -202,7 +194,7 @@
  47.118    let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
  47.119    in instantiate ([],[(cn,ct)]) le0 end;
  47.120  
  47.121 -end;
  47.122 +end;  (* LA_Logic *)
  47.123  
  47.124  
  47.125  (* arith theory data *)
  47.126 @@ -235,9 +227,18 @@
  47.127    {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
  47.128  
  47.129  
  47.130 -structure LA_Data_Ref: LIN_ARITH_DATA =
  47.131 +signature HOL_LIN_ARITH_DATA =
  47.132 +sig
  47.133 +  include LIN_ARITH_DATA
  47.134 +  val fast_arith_split_limit : int ref
  47.135 +end;
  47.136 +
  47.137 +structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
  47.138  struct
  47.139  
  47.140 +(* internal representation of linear (in-)equations *)
  47.141 +type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
  47.142 +
  47.143  (* Decomposition of terms *)
  47.144  
  47.145  fun nT (Type("fun",[N,_])) = N = HOLogic.natT
  47.146 @@ -370,16 +371,425 @@
  47.147  
  47.148  fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n)
  47.149  
  47.150 +(*---------------------------------------------------------------------------*)
  47.151 +(* code that performs certain goal transformations for linear arithmetic     *)
  47.152 +(*---------------------------------------------------------------------------*)
  47.153 +
  47.154 +(* A "do nothing" variant of pre_decomp and pre_tac:
  47.155 +
  47.156 +fun pre_decomp sg Ts termitems = [termitems];
  47.157 +fun pre_tac i = all_tac;
  47.158 +*)
  47.159 +
  47.160 +(*---------------------------------------------------------------------------*)
  47.161 +(* the following code performs splitting of certain constants (e.g. min,     *)
  47.162 +(* max) in a linear arithmetic problem; similar to what split_tac later does *)
  47.163 +(* to the proof state                                                        *)
  47.164 +(*---------------------------------------------------------------------------*)
  47.165 +
  47.166 +val fast_arith_split_limit = ref 9;
  47.167 +
  47.168 +(* checks whether splitting with 'thm' is implemented                        *)
  47.169 +
  47.170 +(* Thm.thm -> bool *)
  47.171 +
  47.172 +fun is_split_thm thm =
  47.173 +  case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>  (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
  47.174 +    (case head_of lhs of
  47.175 +      Const (a, _) => a mem_string ["Orderings.max", "Orderings.min", "HOL.abs", "HOL.minus", "IntDef.nat", "Divides.op mod", "Divides.op div"]
  47.176 +    | _            => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false))
  47.177 +  | _ => (warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm thm); false);
  47.178 +
  47.179 +(* substitute new for occurrences of old in a term, incrementing bound       *)
  47.180 +(* variables as needed when substituting inside an abstraction               *)
  47.181 +
  47.182 +(* (term * term) list -> term -> term *)
  47.183 +
  47.184 +fun subst_term []    t = t
  47.185 +  | subst_term pairs t =
  47.186 +      (case AList.lookup (op aconv) pairs t of
  47.187 +        SOME new =>
  47.188 +          new
  47.189 +      | NONE     =>
  47.190 +          (case t of Abs (a, T, body) =>
  47.191 +            let val pairs' = map (pairself (incr_boundvars 1)) pairs
  47.192 +            in  Abs (a, T, subst_term pairs' body)  end
  47.193 +          | t1 $ t2                   =>
  47.194 +            subst_term pairs t1 $ subst_term pairs t2
  47.195 +          | _ => t));
  47.196 +
  47.197 +(* approximates the effect of one application of split_tac (followed by NNF  *)
  47.198 +(* normalization) on the subgoal represented by '(Ts, terms)'; returns a     *)
  47.199 +(* list of new subgoals (each again represented by a typ list for bound      *)
  47.200 +(* variables and a term list for premises), or NONE if split_tac would fail  *)
  47.201 +(* on the subgoal                                                            *)
  47.202 +
  47.203 +(* theory -> typ list * term list -> (typ list * term list) list option *)
  47.204 +
  47.205 +(* FIXME: currently only the effect of certain split theorems is reproduced  *)
  47.206 +(*        (which is why we need 'is_split_thm').  A more canonical           *)
  47.207 +(*        implementation should analyze the right-hand side of the split     *)
  47.208 +(*        theorem that can be applied, and modify the subgoal accordingly.   *)
  47.209 +
  47.210 +fun split_once_items sg (Ts, terms) =
  47.211 +let
  47.212 +  (* takes a list  [t1, ..., tn]  to the term                                *)
  47.213 +  (*   tn' --> ... --> t1' --> False  ,                                      *)
  47.214 +  (* where ti' = HOLogic.dest_Trueprop ti                                    *)
  47.215 +  (* term list -> term *)
  47.216 +  fun REPEAT_DETERM_etac_rev_mp terms' =
  47.217 +    fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
  47.218 +  val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
  47.219 +  val cmap       = Splitter.cmap_of_split_thms split_thms
  47.220 +  val splits     = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
  47.221 +in
  47.222 +  if length splits > !fast_arith_split_limit then (
  47.223 +    tracing ("fast_arith_split_limit exceeded (current value is " ^ string_of_int (!fast_arith_split_limit) ^ ")");
  47.224 +    NONE
  47.225 +  ) else (
  47.226 +  case splits of [] =>
  47.227 +    NONE  (* split_tac would fail: no possible split *)
  47.228 +  | ((_, _, _, split_type, split_term) :: _) => (  (* ignore all but the first possible split *)
  47.229 +    case strip_comb split_term of
  47.230 +    (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
  47.231 +      (Const ("Orderings.max", _), [t1, t2]) =>
  47.232 +      let
  47.233 +        val rev_terms     = rev terms
  47.234 +        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
  47.235 +        val terms2        = map (subst_term [(split_term, t2)]) rev_terms
  47.236 +        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  47.237 +        val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
  47.238 +        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.239 +        val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
  47.240 +        val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
  47.241 +      in
  47.242 +        SOME [(Ts, subgoal1), (Ts, subgoal2)]
  47.243 +      end
  47.244 +    (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
  47.245 +    | (Const ("Orderings.min", _), [t1, t2]) =>
  47.246 +      let
  47.247 +        val rev_terms     = rev terms
  47.248 +        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
  47.249 +        val terms2        = map (subst_term [(split_term, t2)]) rev_terms
  47.250 +        val t1_leq_t2     = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  47.251 +        val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
  47.252 +        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.253 +        val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
  47.254 +        val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
  47.255 +      in
  47.256 +        SOME [(Ts, subgoal1), (Ts, subgoal2)]
  47.257 +      end
  47.258 +    (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
  47.259 +    | (Const ("HOL.abs", _), [t1]) =>
  47.260 +      let
  47.261 +        val rev_terms     = rev terms
  47.262 +        val terms1        = map (subst_term [(split_term, t1)]) rev_terms
  47.263 +        val terms2        = map (subst_term [(split_term, Const ("HOL.uminus", split_type --> split_type) $ t1)]) rev_terms
  47.264 +        val zero          = Const ("0", split_type)
  47.265 +        val zero_leq_t1   = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ t1
  47.266 +        val t1_lt_zero    = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
  47.267 +        val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.268 +        val subgoal1      = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
  47.269 +        val subgoal2      = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
  47.270 +      in
  47.271 +        SOME [(Ts, subgoal1), (Ts, subgoal2)]
  47.272 +      end
  47.273 +    (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
  47.274 +    | (Const ("HOL.minus", _), [t1, t2]) =>
  47.275 +      let
  47.276 +        (* "d" in the above theorem becomes a new bound variable after NNF   *)
  47.277 +        (* transformation, therefore some adjustment of indices is necessary *)
  47.278 +        val rev_terms       = rev terms
  47.279 +        val zero            = Const ("0", split_type)
  47.280 +        val d               = Bound 0
  47.281 +        val terms1          = map (subst_term [(split_term, zero)]) rev_terms
  47.282 +        val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)]) (map (incr_boundvars 1) rev_terms)
  47.283 +        val t1'             = incr_boundvars 1 t1
  47.284 +        val t2'             = incr_boundvars 1 t2
  47.285 +        val t1_lt_t2        = Const ("Orderings.less", split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  47.286 +        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)
  47.287 +        val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.288 +        val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
  47.289 +        val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
  47.290 +      in
  47.291 +        SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
  47.292 +      end
  47.293 +    (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
  47.294 +    | (Const ("IntDef.nat", _), [t1]) =>
  47.295 +      let
  47.296 +        val rev_terms   = rev terms
  47.297 +        val zero_int    = Const ("0", HOLogic.intT)
  47.298 +        val zero_nat    = Const ("0", HOLogic.natT)
  47.299 +        val n           = Bound 0
  47.300 +        val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)]) (map (incr_boundvars 1) rev_terms)
  47.301 +        val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
  47.302 +        val t1'         = incr_boundvars 1 t1
  47.303 +        val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $ (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
  47.304 +        val t1_lt_zero  = Const ("Orderings.less", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
  47.305 +        val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.306 +        val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
  47.307 +        val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
  47.308 +      in
  47.309 +        SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
  47.310 +      end
  47.311 +    (* "?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))) *)
  47.312 +    | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  47.313 +      let
  47.314 +        val rev_terms               = rev terms
  47.315 +        val zero                    = Const ("0", split_type)
  47.316 +        val i                       = Bound 1
  47.317 +        val j                       = Bound 0
  47.318 +        val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  47.319 +        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
  47.320 +        val t1'                     = incr_boundvars 2 t1
  47.321 +        val t2'                     = incr_boundvars 2 t2
  47.322 +        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  47.323 +        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
  47.324 +        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  47.325 +        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  47.326 +                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
  47.327 +                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
  47.328 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.329 +        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  47.330 +        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
  47.331 +      in
  47.332 +        SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
  47.333 +      end
  47.334 +    (* "?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))) *)
  47.335 +    | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  47.336 +      let
  47.337 +        val rev_terms               = rev terms
  47.338 +        val zero                    = Const ("0", split_type)
  47.339 +        val i                       = Bound 1
  47.340 +        val j                       = Bound 0
  47.341 +        val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  47.342 +        val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
  47.343 +        val t1'                     = incr_boundvars 2 t1
  47.344 +        val t2'                     = incr_boundvars 2 t2
  47.345 +        val t2_eq_zero              = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  47.346 +        val t2_neq_zero             = HOLogic.mk_not (Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
  47.347 +        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  47.348 +        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  47.349 +                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
  47.350 +                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
  47.351 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.352 +        val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  47.353 +        val subgoal2                = (map HOLogic.mk_Trueprop [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j]) @ terms2 @ [not_false]
  47.354 +      in
  47.355 +        SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
  47.356 +      end
  47.357 +    (* "?P ((?n::int) mod (number_of ?k)) = ((iszero (number_of ?k) --> ?P ?n) &
  47.358 +                                              (neg (number_of (bin_minus ?k)) --> (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
  47.359 +                                              (neg (number_of ?k) --> (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
  47.360 +    | (Const ("Divides.op mod", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
  47.361 +      let
  47.362 +        val rev_terms               = rev terms
  47.363 +        val zero                    = Const ("0", split_type)
  47.364 +        val i                       = Bound 1
  47.365 +        val j                       = Bound 0
  47.366 +        val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  47.367 +        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)]) (map (incr_boundvars 2) rev_terms)
  47.368 +        val t1'                     = incr_boundvars 2 t1
  47.369 +        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
  47.370 +        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
  47.371 +        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
  47.372 +                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
  47.373 +        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
  47.374 +        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  47.375 +        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  47.376 +                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
  47.377 +                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
  47.378 +        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
  47.379 +        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  47.380 +        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
  47.381 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.382 +        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
  47.383 +        val subgoal2                = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
  47.384 +                                        @ hd terms2_3
  47.385 +                                        :: (if tl terms2_3 = [] then [not_false] else [])
  47.386 +                                        @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
  47.387 +                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
  47.388 +        val subgoal3                = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
  47.389 +                                        @ hd terms2_3
  47.390 +                                        :: (if tl terms2_3 = [] then [not_false] else [])
  47.391 +                                        @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
  47.392 +                                        @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
  47.393 +        val Ts'                     = split_type :: split_type :: Ts
  47.394 +      in
  47.395 +        SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
  47.396 +      end
  47.397 +    (* "?P ((?n::int) div (number_of ?k)) = ((iszero (number_of ?k) --> ?P 0) &
  47.398 +                                              (neg (number_of (bin_minus ?k)) --> (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
  47.399 +                                              (neg (number_of ?k) --> (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
  47.400 +    | (Const ("Divides.op div", Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
  47.401 +      let
  47.402 +        val rev_terms               = rev terms
  47.403 +        val zero                    = Const ("0", split_type)
  47.404 +        val i                       = Bound 1
  47.405 +        val j                       = Bound 0
  47.406 +        val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  47.407 +        val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)]) (map (incr_boundvars 2) rev_terms)
  47.408 +        val t1'                     = incr_boundvars 2 t1
  47.409 +        val (t2' as (_ $ k'))       = incr_boundvars 2 t2
  47.410 +        val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
  47.411 +        val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
  47.412 +                                        (number_of $ (Const ("Numeral.bin_minus", HOLogic.binT --> HOLogic.binT) $ k'))
  47.413 +        val zero_leq_j              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ zero $ j
  47.414 +        val j_lt_t2                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  47.415 +        val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  47.416 +                                       (Const ("HOL.plus", split_type --> split_type --> split_type) $
  47.417 +                                         (Const ("HOL.times", split_type --> split_type --> split_type) $ t2' $ i) $ j)
  47.418 +        val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
  47.419 +        val t2_lt_j                 = Const ("Orderings.less", split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  47.420 +        val j_leq_zero              = Const ("Orderings.less_eq", split_type --> split_type --> HOLogic.boolT) $ j $ zero
  47.421 +        val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  47.422 +        val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
  47.423 +        val subgoal2                = (HOLogic.mk_Trueprop neg_minus_k)
  47.424 +                                        :: terms2_3
  47.425 +                                        @ not_false
  47.426 +                                        :: (map HOLogic.mk_Trueprop [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
  47.427 +        val subgoal3                = (HOLogic.mk_Trueprop neg_t2)
  47.428 +                                        :: terms2_3
  47.429 +                                        @ not_false
  47.430 +                                        :: (map HOLogic.mk_Trueprop [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
  47.431 +        val Ts'                     = split_type :: split_type :: Ts
  47.432 +      in
  47.433 +        SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
  47.434 +      end
  47.435 +    (* this will only happen if a split theorem can be applied for which no code exists above -- *)
  47.436 +    (* in which case either the split theorem should be implemented above, or 'is_split_thm'     *)
  47.437 +    (* should be modified to filter it out                                                       *)
  47.438 +    | (t, ts) => (
  47.439 +      warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ " (with " ^ Int.toString (length ts) ^
  47.440 +               " argument(s)) not implemented; proof reconstruction is likely to fail");
  47.441 +      NONE
  47.442 +    ))
  47.443 +  )
  47.444  end;
  47.445  
  47.446 +(* remove terms that do not satisfy p; change the order of the remaining     *)
  47.447 +(* terms in the same way as filter_prems_tac does                            *)
  47.448 +
  47.449 +(* (term -> bool) -> term list -> term list *)
  47.450 +
  47.451 +fun filter_prems_tac_items p terms =
  47.452 +let
  47.453 +  fun filter_prems (t, (left, right)) =
  47.454 +    if  p t  then  (left, right @ [t])  else  (left @ right, [])
  47.455 +  val (left, right) = foldl filter_prems ([], []) terms
  47.456 +in
  47.457 +  right @ left
  47.458 +end;
  47.459 +
  47.460 +(* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
  47.461 +(* subgoal that has 'terms' as premises                                      *)
  47.462 +
  47.463 +(* term list -> bool *)
  47.464 +
  47.465 +fun negated_term_occurs_positively terms =
  47.466 +  List.exists (fn (TP $ (Const ("Not", _) $ t)) => member (op aconv) terms (TP $ t) | _ => false) terms;
  47.467 +
  47.468 +(* theory -> typ list * term list -> (typ list * term list) list *)
  47.469 +
  47.470 +fun pre_decomp sg (Ts, terms) =
  47.471 +let
  47.472 +  (* repeatedly split (including newly emerging subgoals) until no further   *)
  47.473 +  (* splitting is possible                                                   *)
  47.474 +  (* (typ list * term list) list -> (typ list * term list) list *)
  47.475 +  fun split_loop [] = []
  47.476 +    | split_loop (subgoal::subgoals) = (
  47.477 +        case split_once_items sg subgoal of
  47.478 +          SOME new_subgoals => split_loop (new_subgoals @ subgoals)
  47.479 +        | NONE              => subgoal :: split_loop subgoals
  47.480 +      )
  47.481 +  fun is_relevant t  = isSome (decomp sg t)
  47.482 +  val relevant_terms = filter_prems_tac_items is_relevant terms                                (* filter_prems_tac is_relevant *)
  47.483 +  val split_goals    = split_loop [(Ts, relevant_terms)]                                       (* split_tac, NNF normalization *)
  47.484 +  val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals    (* necessary because split_once_tac may normalize terms *)
  47.485 +  val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm  (* TRY (etac notE) THEN eq_assume_tac *)
  47.486 +in
  47.487 +  result
  47.488 +end;
  47.489 +
  47.490 +(* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
  47.491 +(* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
  47.492 +(* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
  47.493 +(* performs NNF-normalization of ~P, and eliminates conjunctions,            *)
  47.494 +(* disjunctions and existential quantifiers from the premises, possibly (in  *)
  47.495 +(* the case of disjunctions) resulting in several new subgoals, each of the  *)
  47.496 +(* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
  47.497 +(* !fast_arith_split_limit splits are possible.                              *)
  47.498 +
  47.499 +(* Thm.thm list -> int -> Tactical.tactic *)
  47.500 +
  47.501 +fun split_once_tac split_thms i =
  47.502 +let
  47.503 +  val nnf_simpset =
  47.504 +    empty_ss setmkeqTrue mk_eq_True
  47.505 +    setmksimps (mksimps mksimps_pairs)
  47.506 +    addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, 
  47.507 +      not_all, not_ex, not_not]
  47.508 +  fun prem_nnf_tac i st =
  47.509 +    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
  47.510 +  fun cond_split_tac i st =
  47.511 +    let
  47.512 +      val subgoal = Logic.nth_prem (i, Thm.prop_of st)
  47.513 +      val Ts      = rev (map snd (Logic.strip_params subgoal))
  47.514 +      val concl   = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
  47.515 +      val cmap    = Splitter.cmap_of_split_thms split_thms
  47.516 +      val splits  = Splitter.split_posns cmap (theory_of_thm st) Ts concl
  47.517 +    in
  47.518 +      if length splits > !fast_arith_split_limit then
  47.519 +        no_tac st
  47.520 +      else
  47.521 +        split_tac split_thms i st
  47.522 +    end
  47.523 +in
  47.524 +  EVERY' [
  47.525 +    REPEAT_DETERM o etac rev_mp,
  47.526 +    cond_split_tac,
  47.527 +    rtac ccontr,
  47.528 +    prem_nnf_tac,
  47.529 +    TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
  47.530 +  ] i
  47.531 +end;
  47.532 +
  47.533 +(* remove irrelevant premises, then split the i-th subgoal (and all new      *)
  47.534 +(* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
  47.535 +(* subgoals and finally attempt to solve them by finding an immediate        *)
  47.536 +(* contradiction (i.e. a term and its negation) in their premises.           *)
  47.537 +
  47.538 +(* int -> Tactical.tactic *)
  47.539 +
  47.540 +fun pre_tac i st =
  47.541 +let
  47.542 +  val sg            = theory_of_thm st
  47.543 +  val split_thms    = filter is_split_thm (#splits (ArithTheoryData.get sg))
  47.544 +  fun is_relevant t = isSome (decomp sg t)
  47.545 +in
  47.546 +  DETERM (
  47.547 +    TRY (filter_prems_tac is_relevant i)
  47.548 +      THEN (
  47.549 +        (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
  47.550 +          THEN_ALL_NEW
  47.551 +            ((fn j => PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
  47.552 +              THEN'
  47.553 +            (TRY o (etac notE THEN' eq_assume_tac)))
  47.554 +      ) i
  47.555 +  ) st
  47.556 +end;
  47.557 +
  47.558 +end;  (* LA_Data_Ref *)
  47.559 +
  47.560  
  47.561  structure Fast_Arith =
  47.562    Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
  47.563  
  47.564 -val fast_arith_tac    = Fast_Arith.lin_arith_tac false
  47.565 -and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
  47.566 -and trace_arith    = Fast_Arith.trace
  47.567 -and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
  47.568 +val fast_arith_tac         = Fast_Arith.lin_arith_tac false;
  47.569 +val fast_ex_arith_tac      = Fast_Arith.lin_arith_tac;
  47.570 +val trace_arith            = Fast_Arith.trace;
  47.571 +val fast_arith_neq_limit   = Fast_Arith.fast_arith_neq_limit;
  47.572 +val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
  47.573  
  47.574  local
  47.575  
  47.576 @@ -439,7 +849,6 @@
  47.577    Simplifier.simproc (the_context ()) "fast_nat_arith"
  47.578      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
  47.579  
  47.580 -
  47.581  (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
  47.582  useful to detect inconsistencies among the premises for subgoals which are
  47.583  *not* themselves (in)equalities, because the latter activate
  47.584 @@ -449,58 +858,24 @@
  47.585  
  47.586  (* arith proof method *)
  47.587  
  47.588 -(* FIXME: K true should be replaced by a sensible test to speed things up
  47.589 -   in case there are lots of irrelevant terms involved;
  47.590 -   elimination of min/max can be optimized:
  47.591 -   (max m n + k <= r) = (m+k <= r & n+k <= r)
  47.592 -   (l <= min m n + k) = (l <= m+k & l <= n+k)
  47.593 -*)
  47.594  local
  47.595 -(* a simpset for computations subject to optimization !!! *)
  47.596 -(*
  47.597 -val binarith = map thm
  47.598 -  ["Pls_0_eq", "Min_1_eq",
  47.599 - "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
  47.600 -  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
  47.601 -  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
  47.602 -  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
  47.603 -  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
  47.604 -  "bin_add_Pls_right", "bin_add_Min_right"];
  47.605 - val intarithrel = 
  47.606 -     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
  47.607 -		"int_le_number_of_eq","int_iszero_number_of_0",
  47.608 -		"int_less_number_of_eq_neg"]) @
  47.609 -     (map (fn s => thm s RS thm "lift_bool") 
  47.610 -	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
  47.611 -	   "int_neg_number_of_Min"])@
  47.612 -     (map (fn s => thm s RS thm "nlift_bool") 
  47.613 -	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
  47.614 -     
  47.615 -val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
  47.616 -			"int_number_of_diff_sym", "int_number_of_mult_sym"];
  47.617 -val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
  47.618 -			"mult_nat_number_of", "eq_nat_number_of",
  47.619 -			"less_nat_number_of"]
  47.620 -val powerarith = 
  47.621 -    (map thm ["nat_number_of", "zpower_number_of_even", 
  47.622 -	      "zpower_Pls", "zpower_Min"]) @ 
  47.623 -    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
  47.624 -			   thm "one_eq_Numeral1_nring"] 
  47.625 -  (thm "zpower_number_of_odd"))]
  47.626  
  47.627 -val comp_arith = binarith @ intarith @ intarithrel @ natarith 
  47.628 -	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
  47.629 -
  47.630 -val comp_ss = HOL_basic_ss addsimps comp_arith addsimps simp_thms;
  47.631 -*)
  47.632  fun raw_arith_tac ex i st =
  47.633 +  (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
  47.634 +     decomp sg"?) to speed things up in case there are lots of irrelevant
  47.635 +     terms involved; elimination of min/max can be optimized:
  47.636 +     (max m n + k <= r) = (m+k <= r & n+k <= r)
  47.637 +     (l <= min m n + k) = (l <= m+k & l <= n+k)
  47.638 +  *)
  47.639    refute_tac (K true)
  47.640 -   (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
  47.641 -(*   (REPEAT o 
  47.642 -    (fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i)
  47.643 -		THEN (simp_tac comp_ss i))) *)
  47.644 -   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
  47.645 -   i st;
  47.646 +    (* Splitting is also done inside fast_arith_tac, but not completely --   *)
  47.647 +    (* split_tac may use split theorems that have not been implemented in    *)
  47.648 +    (* fast_arith_tac (cf. pre_decomp and split_once_items above).           *)
  47.649 +    (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
  47.650 +    (* some goals that fast_arith_tac alone would fail on.                   *)
  47.651 +    (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
  47.652 +    (fast_ex_arith_tac ex)
  47.653 +    i st;
  47.654  
  47.655  fun presburger_tac i st =
  47.656    (case ArithTheoryData.get (Thm.theory_of_thm st) of
  47.657 @@ -510,19 +885,19 @@
  47.658  
  47.659  in
  47.660  
  47.661 -val simple_arith_tac = FIRST' [fast_arith_tac,
  47.662 -  ObjectLogic.atomize_tac THEN' raw_arith_tac true];
  47.663 +  val simple_arith_tac = FIRST' [fast_arith_tac,
  47.664 +    ObjectLogic.atomize_tac THEN' raw_arith_tac true];
  47.665  
  47.666 -val arith_tac = FIRST' [fast_arith_tac,
  47.667 -  ObjectLogic.atomize_tac THEN' raw_arith_tac true,
  47.668 -  presburger_tac];
  47.669 +  val arith_tac = FIRST' [fast_arith_tac,
  47.670 +    ObjectLogic.atomize_tac THEN' raw_arith_tac true,
  47.671 +    presburger_tac];
  47.672  
  47.673 -val silent_arith_tac = FIRST' [fast_arith_tac,
  47.674 -  ObjectLogic.atomize_tac THEN' raw_arith_tac false,
  47.675 -  presburger_tac];
  47.676 +  val silent_arith_tac = FIRST' [fast_arith_tac,
  47.677 +    ObjectLogic.atomize_tac THEN' raw_arith_tac false,
  47.678 +    presburger_tac];
  47.679  
  47.680 -fun arith_method prems =
  47.681 -  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
  47.682 +  fun arith_method prems =
  47.683 +    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
  47.684  
  47.685  end;
  47.686  
    48.1 --- a/src/HOL/ex/Adder.thy	Wed Jul 26 13:31:07 2006 +0200
    48.2 +++ b/src/HOL/ex/Adder.thy	Wed Jul 26 19:23:04 2006 +0200
    48.3 @@ -80,22 +80,7 @@
    48.4  lemma cca_length [rule_format]:
    48.5       "\<forall>bs. length as = length bs --> 
    48.6             length (carry_chain_adder as bs c) = Suc (length bs)"
    48.7 -      (is "?P as")
    48.8 -proof (induct as,auto simp add: Let_def)
    48.9 -  fix as :: "bit list"
   48.10 -  fix xs :: "bit list"
   48.11 -  assume ind: "?P as"
   48.12 -  assume len: "Suc (length as) = length xs"
   48.13 -  thus "Suc (length (carry_chain_adder as (tl xs) c) - Suc 0) = length xs"
   48.14 -  proof (cases xs,simp_all)
   48.15 -    fix b bs
   48.16 -    assume [simp]: "xs = b # bs"
   48.17 -    assume "length as = length bs"
   48.18 -    with ind
   48.19 -    show "length (carry_chain_adder as bs c) - Suc 0 = length bs"
   48.20 -      by auto
   48.21 -  qed
   48.22 -qed
   48.23 +  by (induct as,auto simp add: Let_def)
   48.24  
   48.25  lemma cca_correct [rule_format]:
   48.26       "\<forall>bs. length as = length bs --> 
    49.1 --- a/src/HOL/simpdata.ML	Wed Jul 26 13:31:07 2006 +0200
    49.2 +++ b/src/HOL/simpdata.ML	Wed Jul 26 19:23:04 2006 +0200
    49.3 @@ -166,8 +166,6 @@
    49.4  end;
    49.5  
    49.6  
    49.7 -
    49.8 -
    49.9  (*** Simproc for Let ***)
   49.10  
   49.11  val use_let_simproc = ref true;
    50.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 26 13:31:07 2006 +0200
    50.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Jul 26 19:23:04 2006 +0200
    50.3 @@ -23,12 +23,12 @@
    50.4  
    50.5  signature LIN_ARITH_LOGIC =
    50.6  sig
    50.7 -  val conjI:		thm (* P ==> Q ==> P & Q *)
    50.8 +  val conjI:            thm (* P ==> Q ==> P & Q *)
    50.9    val ccontr:           thm (* (~ P ==> False) ==> P *)
   50.10    val notI:             thm (* (P ==> False) ==> ~ P *)
   50.11    val not_lessD:        thm (* ~(m < n) ==> n <= m *)
   50.12    val not_leD:          thm (* ~(m <= n) ==> n < m *)
   50.13 -  val sym:		thm (* x = y ==> y = x *)
   50.14 +  val sym:              thm (* x = y ==> y = x *)
   50.15    val mk_Eq: thm -> thm
   50.16    val atomize: thm -> thm list
   50.17    val mk_Trueprop: term -> term
   50.18 @@ -52,16 +52,26 @@
   50.19  
   50.20  signature LIN_ARITH_DATA =
   50.21  sig
   50.22 -  val decomp:
   50.23 -    theory -> term -> ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool) option
   50.24 +  type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool  (* internal representation of linear (in-)equations *)
   50.25 +  val decomp: theory -> term -> decompT option
   50.26 +  val pre_decomp: theory -> typ list * term list -> (typ list * term list) list  (* preprocessing, performed on a representation of subgoals as list of premises *)
   50.27 +  val pre_tac   : int -> Tactical.tactic                                         (* preprocessing, performed on the goal -- must do the same as 'pre_decomp' *)
   50.28    val number_of: IntInf.int * typ -> term
   50.29  end;
   50.30  (*
   50.31  decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
   50.32     where Rel is one of "<", "~<", "<=", "~<=" and "=" and
   50.33 -         p/q is the decomposition of the sum terms x/y into a list
   50.34 -         of summand * multiplicity pairs and a constant summand and
   50.35 -         d indicates if the domain is discrete.
   50.36 +         p (q, respectively) is the decomposition of the sum term x
   50.37 +         (y, respectively) into a list of summand * multiplicity
   50.38 +         pairs and a constant summand and d indicates if the domain
   50.39 +         is discrete.
   50.40 +
   50.41 +The relationship between pre_decomp and pre_tac is somewhat tricky.  The
   50.42 +internal representation of a subgoal and the corresponding theorem must
   50.43 +be modified by pre_decomp (pre_tac, resp.) in a corresponding way.  See
   50.44 +the comment for split_items below.  (This is even necessary for eta- and
   50.45 +beta-equivalent modifications, as some of the lin. arith. code is not
   50.46 +insensitive to them.)
   50.47  
   50.48  ss must reduce contradictory <= to False.
   50.49     It should also cancel common summands to keep <= reduced;
   50.50 @@ -192,32 +202,32 @@
   50.51  
   50.52  fun ratmiddle(r,s) = Rat.mult(Rat.add(r,s),Rat.inv(Rat.rat_of_int 2));
   50.53  
   50.54 -fun choose2 d ((lb,exactl),(ub,exactu)) =
   50.55 -  if Rat.le(lb,Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
   50.56 -     Rat.le(Rat.zero,ub) andalso (ub <> Rat.zero orelse exactu)
   50.57 +fun choose2 d ((lb, exactl), (ub, exactu)) =
   50.58 +  if Rat.le (lb, Rat.zero) andalso (lb <> Rat.zero orelse exactl) andalso
   50.59 +     Rat.le (Rat.zero, ub) andalso (ub <> Rat.zero orelse exactu)
   50.60    then Rat.zero else
   50.61    if not d
   50.62    then (if Rat.ge0 lb
   50.63 -        then if exactl then lb else ratmiddle(lb,ub)
   50.64 -        else if exactu then ub else ratmiddle(lb,ub))
   50.65 +        then if exactl then lb else ratmiddle (lb, ub)
   50.66 +        else if exactu then ub else ratmiddle (lb, ub))
   50.67    else (* discrete domain, both bounds must be exact *)
   50.68    if Rat.ge0 lb then let val lb' = Rat.roundup lb
   50.69 -                    in if Rat.le(lb',ub) then lb' else raise NoEx end
   50.70 +                    in if Rat.le (lb', ub) then lb' else raise NoEx end
   50.71                 else let val ub' = Rat.rounddown ub
   50.72 -                    in if Rat.le(lb,ub') then ub' else raise NoEx end;
   50.73 +                    in if Rat.le (lb, ub') then ub' else raise NoEx end;
   50.74  
   50.75 -fun findex1 discr (ex,(v,lineqs)) =
   50.76 +fun findex1 discr (ex, (v, lineqs)) =
   50.77    let val nz = List.filter (fn (Lineq(_,_,cs,_)) => el v cs <> 0) lineqs;
   50.78        val ineqs = Library.foldl elim_eqns ([],nz)
   50.79        val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
   50.80 -      val lb = ratrelmax(map (eval ex v) ge)
   50.81 -      val ub = ratrelmin(map (eval ex v) le)
   50.82 +      val lb = ratrelmax (map (eval ex v) ge)
   50.83 +      val ub = ratrelmin (map (eval ex v) le)
   50.84    in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
   50.85  
   50.86  fun findex discr = Library.foldl (findex1 discr);
   50.87  
   50.88  fun elim1 v x =
   50.89 -  map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
   50.90 +  map (fn (a,le,bs) => (Rat.add (a, Rat.neg (Rat.mult (el v bs, x))), le,
   50.91                          nth_update (v, Rat.zero) bs));
   50.92  
   50.93  fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
   50.94 @@ -327,7 +337,7 @@
   50.95  (* ------------------------------------------------------------------------- *)
   50.96  
   50.97  fun allpairs f xs ys =
   50.98 -  maps (fn x => map (fn y => f x y) ys) xs;
   50.99 +  List.concat (map (fn x => map (fn y => f x y) ys) xs);
  50.100  
  50.101  fun extract_first p =
  50.102    let fun extract xs (y::ys) = if p y then (SOME y,xs@ys)
  50.103 @@ -346,25 +356,25 @@
  50.104  type history = (int * lineq list) list;
  50.105  datatype result = Success of injust | Failure of history;
  50.106  
  50.107 -fun elim(ineqs,hist) =
  50.108 -  let val dummy = print_ineqs ineqs;
  50.109 -      val (triv,nontriv) = List.partition is_trivial ineqs in
  50.110 -  if not(null triv)
  50.111 +fun elim (ineqs, hist) =
  50.112 +  let val dummy = print_ineqs ineqs
  50.113 +      val (triv, nontriv) = List.partition is_trivial ineqs in
  50.114 +  if not (null triv)
  50.115    then case Library.find_first is_answer triv of
  50.116 -         NONE => elim(nontriv,hist)
  50.117 +         NONE => elim (nontriv, hist)
  50.118         | SOME(Lineq(_,_,_,j)) => Success j
  50.119    else
  50.120 -  if null nontriv then Failure(hist)
  50.121 +  if null nontriv then Failure hist
  50.122    else
  50.123 -  let val (eqs,noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
  50.124 -  if not(null eqs) then
  50.125 +  let val (eqs, noneqs) = List.partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in
  50.126 +  if not (null eqs) then
  50.127       let val clist = Library.foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs)
  50.128           val sclist = sort (fn (x,y) => IntInf.compare(abs(x),abs(y)))
  50.129                             (List.filter (fn i => i<>0) clist)
  50.130           val c = hd sclist
  50.131           val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
  50.132                 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
  50.133 -         val v = find_index (fn x => x = c) ceq
  50.134 +         val v = find_index_eq c ceq
  50.135           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
  50.136                                       (othereqs @ noneqs)
  50.137           val others = map (elim_var v eq) roth @ ioth
  50.138 @@ -390,10 +400,12 @@
  50.139  (* Translate back a proof.                                                   *)
  50.140  (* ------------------------------------------------------------------------- *)
  50.141  
  50.142 -fun trace_thm msg th = 
  50.143 -    if !trace then (tracing msg; tracing (Display.string_of_thm th); th) else th;
  50.144 +(* string -> Thm.thm -> Thm.thm *)
  50.145 +fun trace_thm msg th =
  50.146 +    (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
  50.147  
  50.148 -fun trace_msg msg = 
  50.149 +(* string -> unit *)
  50.150 +fun trace_msg msg =
  50.151      if !trace then tracing msg else ();
  50.152  
  50.153  (* FIXME OPTIMIZE!!!! (partly done already)
  50.154 @@ -408,21 +420,21 @@
  50.155  local
  50.156   exception FalseE of thm
  50.157  in
  50.158 +(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> injust -> Thm.thm *)
  50.159  fun mkthm (sg, ss) asms just =
  50.160    let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
  50.161            Data.get sg;
  50.162        val simpset' = Simplifier.inherit_context ss simpset;
  50.163 -      val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
  50.164 +      val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) =>
  50.165                              map fst lhs  union  (map fst rhs  union  ats))
  50.166 -                        ([], map_filter (fn thm => if Thm.no_prems thm
  50.167 -                                        then LA_Data.decomp sg (concl_of thm)
  50.168 -                                        else NONE) asms)
  50.169 +                        ([], List.mapPartial (fn thm => if Thm.no_prems thm
  50.170 +                                              then LA_Data.decomp sg (concl_of thm)
  50.171 +                                              else NONE) asms)
  50.172  
  50.173        fun add2 thm1 thm2 =
  50.174          let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
  50.175          in get_first (fn th => SOME(conj RS th) handle THM _ => NONE) add_mono_thms
  50.176          end;
  50.177 -
  50.178        fun try_add [] _ = NONE
  50.179          | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
  50.180               NONE => try_add thm1s thm2 | some => some;
  50.181 @@ -430,23 +442,18 @@
  50.182        fun addthms thm1 thm2 =
  50.183          case add2 thm1 thm2 of
  50.184            NONE => (case try_add ([thm1] RL inj_thms) thm2 of
  50.185 -                     NONE => (the (try_add ([thm2] RL inj_thms) thm1)
  50.186 +                     NONE => ( the (try_add ([thm2] RL inj_thms) thm1)
  50.187                                 handle Option =>
  50.188                                 (trace_thm "" thm1; trace_thm "" thm2;
  50.189 -                                sys_error "Lin.arith. failed to add thms"))
  50.190 +                                sys_error "Lin.arith. failed to add thms")
  50.191 +                             )
  50.192                     | SOME thm => thm)
  50.193          | SOME thm => thm;
  50.194  
  50.195        fun multn(n,thm) =
  50.196          let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
  50.197          in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
  50.198 -(*
  50.199 -      fun multn2(n,thm) =
  50.200 -        let val SOME(mth,cv) =
  50.201 -              get_first (fn (th,cv) => SOME(thm RS th,cv) handle THM _ => NONE) mult_mono_thms
  50.202 -            val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
  50.203 -        in instantiate ([],[(cv,ct)]) mth end
  50.204 -*)
  50.205 +
  50.206        fun multn2(n,thm) =
  50.207          let val SOME(mth) =
  50.208                get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
  50.209 @@ -459,15 +466,15 @@
  50.210          let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
  50.211          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
  50.212  
  50.213 -      fun mk(Asm i) = trace_thm "Asm" (nth asms i)
  50.214 -        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
  50.215 -        | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
  50.216 -        | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
  50.217 -        | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
  50.218 -        | mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
  50.219 -        | mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
  50.220 -        | mk(Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
  50.221 -        | mk(Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
  50.222 +      fun mk (Asm i) = trace_thm "Asm" (nth asms i)
  50.223 +        | mk (Nat i) = trace_thm "Nat" (LA_Logic.mk_nat_thm sg (nth atoms i))
  50.224 +        | mk (LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
  50.225 +        | mk (NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
  50.226 +        | mk (NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
  50.227 +        | mk (NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
  50.228 +        | mk (Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2)))
  50.229 +        | mk (Multiplied(n,j)) = (trace_msg("*"^IntInf.toString n); trace_thm "*" (multn(n,mk j)))
  50.230 +        | mk (Multiplied2(n,j)) = simp (trace_msg("**"^IntInf.toString n); trace_thm "**" (multn2(n,mk j)))
  50.231  
  50.232    in trace_msg "mkthm";
  50.233       let val thm = trace_thm "Final thm:" (mk just)
  50.234 @@ -475,19 +482,20 @@
  50.235          in trace_thm "After simplification:" fls;
  50.236             if LA_Logic.is_False fls then fls
  50.237             else
  50.238 -            (tracing "Assumptions:"; List.app print_thm asms;
  50.239 -             tracing "Proved:"; print_thm fls;
  50.240 +            (tracing "Assumptions:"; List.app (tracing o Display.string_of_thm) asms;
  50.241 +             tracing "Proved:"; tracing (Display.string_of_thm fls);
  50.242               warning "Linear arithmetic should have refuted the assumptions.\n\
  50.243                       \Please inform Tobias Nipkow (nipkow@in.tum.de).";
  50.244               fls)
  50.245          end
  50.246 -     end handle FalseE thm => (trace_thm "False reached early:" thm; thm)
  50.247 +     end handle FalseE thm => trace_thm "False reached early:" thm
  50.248    end
  50.249  end;
  50.250  
  50.251  fun coeff poly atom : IntInf.int =
  50.252    AList.lookup (op =) poly atom |> the_default 0;
  50.253  
  50.254 +(* int list -> int *)
  50.255  fun lcms is = Library.foldl lcm (1, is);
  50.256  
  50.257  fun integ(rlhs,r,rel,rrhs,s,d) =
  50.258 @@ -499,8 +507,8 @@
  50.259  in (m,(map mult rlhs, rn*(m div rd), rel, map mult rrhs, sn*(m div sd), d)) end
  50.260  
  50.261  fun mklineq n atoms =
  50.262 -  fn (item,k) =>
  50.263 -  let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
  50.264 +  fn (item, k) =>
  50.265 +  let val (m, (lhs,i,rel,rhs,j,discrete)) = integ item
  50.266        val lhsa = map (coeff lhs) atoms
  50.267        and rhsa = map (coeff rhs) atoms
  50.268        val diff = map2 (curry (op -)) rhsa lhsa
  50.269 @@ -535,28 +543,33 @@
  50.270    curry (op ~~) sds
  50.271    #> map print_atom
  50.272    #> commas
  50.273 -  #> curry (op ^) "Counter example:\n";
  50.274 +  #> curry (op ^) "Counter example (possibly spurious):\n";
  50.275  
  50.276 -fun trace_ex(sg,params,atoms,discr,n,hist:history) =
  50.277 -  if null hist then ()
  50.278 -  else let val frees = map Free params;
  50.279 -           fun s_of_t t = Sign.string_of_term sg (subst_bounds(frees,t));
  50.280 -           val (v,lineqs) :: hist' = hist
  50.281 -           val start = if v = ~1 then (findex0 discr n lineqs,hist')
  50.282 -                       else (replicate n Rat.zero,hist)
  50.283 -           val ex = SOME (produce_ex ((map s_of_t atoms)~~discr) (findex discr start))
  50.284 -             handle NoEx => NONE;
  50.285 -       in
  50.286 -         (case ex of
  50.287 -           SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
  50.288 -         | NONE => warning "arith failed")
  50.289 -       end;
  50.290 +fun trace_ex (sg, params, atoms, discr, n, hist : history) =
  50.291 +  case hist of
  50.292 +    [] => ()
  50.293 +  | (v, lineqs) :: hist' =>
  50.294 +    let val frees = map Free params
  50.295 +        fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t))
  50.296 +        val start = if v = ~1 then (findex0 discr n lineqs, hist')
  50.297 +                    else (replicate n Rat.zero, hist)
  50.298 +        val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) (findex discr start))
  50.299 +          handle NoEx => NONE
  50.300 +    in
  50.301 +      case ex of
  50.302 +        SOME s => (warning "arith failed - see trace for a counter example"; tracing s)
  50.303 +      | NONE => warning "arith failed"
  50.304 +    end;
  50.305  
  50.306 -fun mknat pTs ixs (atom,i) =
  50.307 -  if LA_Logic.is_nat(pTs,atom)
  50.308 +(* ------------------------------------------------------------------------- *)
  50.309 +
  50.310 +(* Term.typ list -> int list -> Term.term * int -> lineq option *)
  50.311 +
  50.312 +fun mknat pTs ixs (atom, i) =
  50.313 +  if LA_Logic.is_nat (pTs, atom)
  50.314    then let val l = map (fn j => if j=i then 1 else 0) ixs
  50.315 -       in SOME(Lineq(0,Le,l,Nat(i))) end
  50.316 -  else NONE
  50.317 +       in SOME (Lineq (0, Le, l, Nat i)) end
  50.318 +  else NONE;
  50.319  
  50.320  (* This code is tricky. It takes a list of premises in the order they occur
  50.321  in the subgoal. Numerical premises are coded as SOME(tuple), non-numerical
  50.322 @@ -570,95 +583,184 @@
  50.323  
  50.324  For variables n of type nat, a constraint 0 <= n is added.
  50.325  *)
  50.326 -fun split_items(items) =
  50.327 -  let fun elim_neq front _ [] = [rev front]
  50.328 -        | elim_neq front n (NONE::ineqs) = elim_neq front (n+1) ineqs
  50.329 -        | elim_neq front n (SOME(ineq as (l,i,rel,r,j,d))::ineqs) =
  50.330 -          if rel = "~=" then elim_neq front n (ineqs @ [SOME(l,i,"<",r,j,d)]) @
  50.331 -                             elim_neq front n (ineqs @ [SOME(r,j,"<",l,i,d)])
  50.332 -          else elim_neq ((ineq,n) :: front) (n+1) ineqs
  50.333 -  in elim_neq [] 0 items end;
  50.334 +
  50.335 +(* FIXME: To optimize, the splitting of cases and the search for refutations *)
  50.336 +(*        should be intertwined: separate the first (fully split) case,      *)
  50.337 +(*        refute it, continue with splitting and refuting.  Terminate with   *)
  50.338 +(*        failure as soon as a case could not be refuted; i.e. delay further *)
  50.339 +(*        splitting until after a refutation for other cases has been found. *)
  50.340 +
  50.341 +(* Theory.theory -> bool -> typ list * term list -> (typ list * (decompT * int) list) list *)
  50.342 +
  50.343 +fun split_items sg do_pre (Ts, terms) =
  50.344 +  let
  50.345 +(*
  50.346 +      val _ = trace_msg ("split_items: do_pre is " ^ Bool.toString do_pre ^ "\n" ^
  50.347 +                         "  Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
  50.348 +                         "  terms = " ^ string_of_list (Sign.string_of_term sg) terms)
  50.349 +*)
  50.350 +      (* splits inequalities '~=' into '<' and '>'; this corresponds to *)
  50.351 +      (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic    *)
  50.352 +      (* level                                                          *)
  50.353 +      (* decompT option list -> decompT option list list *)
  50.354 +      fun elim_neq []              = [[]]
  50.355 +        | elim_neq (NONE :: ineqs) = map (cons NONE) (elim_neq ineqs)
  50.356 +        | elim_neq (SOME(ineq as (l,i,rel,r,j,d)) :: ineqs) =
  50.357 +          if rel = "~=" then elim_neq (ineqs @ [SOME (l, i, "<", r, j, d)]) @
  50.358 +                             elim_neq (ineqs @ [SOME (r, j, "<", l, i, d)])
  50.359 +          else map (cons (SOME ineq)) (elim_neq ineqs)
  50.360 +      (* int -> decompT option list -> (decompT * int) list *)
  50.361 +      fun number_hyps _ []             = []
  50.362 +        | number_hyps n (NONE::xs)     = number_hyps (n+1) xs
  50.363 +        | number_hyps n ((SOME x)::xs) = (x, n) :: number_hyps (n+1) xs
  50.364  
  50.365 -fun add_atoms(ats,((lhs,_,_,rhs,_,_),_)) =
  50.366 -    (map fst lhs) union ((map fst rhs) union ats)
  50.367 +      val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *)
  50.368 +                                  (* (typ list * term list) list *)
  50.369 +                                  (if do_pre then LA_Data.pre_decomp sg else Library.single)
  50.370 +                               |> (* compute the internal encoding of (in-)equalities *)
  50.371 +                                  (* (typ list * decompT option list) list *)
  50.372 +                                  map (apsnd (map (LA_Data.decomp sg)))
  50.373 +                               |> (* splitting of inequalities *)
  50.374 +                                  (* (typ list * decompT option list) list list *)
  50.375 +                                  map (fn (Ts, items) => map (pair Ts) (elim_neq items))
  50.376 +                               |> (* combine the list of lists of subgoals into a single list *)
  50.377 +                                  (* (typ list * decompT option list) list *)
  50.378 +                                  List.concat
  50.379 +                               |> (* numbering of hypotheses, ignoring irrelevant ones *)
  50.380 +                                  (* (typ list * (decompT * int) list) list *)
  50.381 +                                  map (apsnd (number_hyps 0))
  50.382 +(*
  50.383 +      val _ = trace_msg ("split_items: result has " ^ Int.toString (length result) ^ " subgoal(s)"
  50.384 +                ^ "\n" ^ (cat_lines o fst) (fold_map (fn (Ts, items) => fn n =>
  50.385 +                        ("  " ^ Int.toString n ^ ". Ts    = " ^ string_of_list (Sign.string_of_typ sg) Ts ^ "\n" ^
  50.386 +                         "    items = " ^ string_of_list
  50.387 +                                            (string_of_pair
  50.388 +                                              (fn (l, i, rel, r, j, d) =>
  50.389 +                                                enclose "(" ")" (commas
  50.390 +                                                  [string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) l,
  50.391 +                                                   Rat.string_of_rat i,
  50.392 +                                                   rel,
  50.393 +                                                   string_of_list (string_of_pair (Sign.string_of_term sg) Rat.string_of_rat) r,
  50.394 +                                                   Rat.string_of_rat j,
  50.395 +                                                   Bool.toString d]))
  50.396 +                                              Int.toString) items, n+1)) result 1))
  50.397 +*)
  50.398 +  in result end;
  50.399  
  50.400 -fun add_datoms(dats,((lhs,_,_,rhs,_,d),_)) =
  50.401 -    (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats)
  50.402 +(* term list * (decompT * int) -> term list *)
  50.403 +
  50.404 +fun add_atoms (ats, ((lhs,_,_,rhs,_,_),_)) =
  50.405 +    (map fst lhs) union ((map fst rhs) union ats);
  50.406 +
  50.407 +(* (bool * term) list * (decompT * int) -> (bool * term) list *)
  50.408 +
  50.409 +fun add_datoms (dats, ((lhs,_,_,rhs,_,d),_)) =
  50.410 +    (map (pair d o fst) lhs) union ((map (pair d o fst) rhs) union dats);
  50.411 +
  50.412 +(* (decompT * int) list -> bool list *)
  50.413  
  50.414  fun discr initems = map fst (Library.foldl add_datoms ([],initems));
  50.415  
  50.416 -fun refutes sg (pTs,params) ex =
  50.417 +(* Theory.theory -> (string * typ) list -> bool -> (typ list * (decompT * int) list) list -> injust list -> injust list option *)
  50.418 +
  50.419 +fun refutes sg params show_ex =
  50.420  let
  50.421 -  fun refute (initems::initemss) js =
  50.422 -    let val atoms = Library.foldl add_atoms ([],initems)
  50.423 +  (* (typ list * (decompT * int) list) list -> injust list -> injust list option *)
  50.424 +  fun refute ((Ts, initems)::initemss) js =
  50.425 +    let val atoms = Library.foldl add_atoms ([], initems)
  50.426          val n = length atoms
  50.427          val mkleq = mklineq n atoms
  50.428          val ixs = 0 upto (n-1)
  50.429          val iatoms = atoms ~~ ixs
  50.430 -        val natlineqs = map_filter (mknat pTs ixs) iatoms
  50.431 +        val natlineqs = List.mapPartial (mknat Ts ixs) iatoms
  50.432          val ineqs = map mkleq initems @ natlineqs
  50.433 -    in case elim(ineqs,[]) of
  50.434 -         Success(j) =>
  50.435 -           (trace_msg "Contradiction!"; refute initemss (js@[j]))
  50.436 -       | Failure(hist) =>
  50.437 -           (if not ex then ()
  50.438 -            else trace_ex(sg,params,atoms,discr initems,n,hist);
  50.439 -            NONE)
  50.440 +    in case elim (ineqs, []) of
  50.441 +         Success j =>
  50.442 +           (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); refute initemss (js@[j]))
  50.443 +       | Failure hist =>
  50.444 +           (if not show_ex then
  50.445 +              ()
  50.446 +            else let
  50.447 +              (* invent names for bound variables that are new, i.e. in Ts, but not in params *)
  50.448 +              (* we assume that Ts still contains (map snd params) as a suffix                *)
  50.449 +              val new_count = length Ts - length params - 1
  50.450 +              val new_names = map Name.bound (0 upto new_count)
  50.451 +              val params'   = (new_names @ map fst params) ~~ Ts
  50.452 +            in
  50.453 +              trace_ex (sg, params', atoms, discr initems, n, hist)
  50.454 +            end; NONE)
  50.455      end
  50.456      | refute [] js = SOME js
  50.457  in refute end;
  50.458  
  50.459 -fun refute sg ps ex items = refutes sg ps ex (split_items items) [];
  50.460 +(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> term list -> injust list option *)
  50.461  
  50.462 -fun refute_tac ss (i,justs) =
  50.463 +fun refute sg params show_ex do_pre terms =
  50.464 +  refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) [];
  50.465 +
  50.466 +(* MetaSimplifier.simpset -> int * injust list -> Tactical.tactic *)
  50.467 +
  50.468 +fun refute_tac ss (i, justs) =
  50.469    fn state =>
  50.470 -    let val sg = #sign(rep_thm state)
  50.471 -        val {neqE, ...} = Data.get sg;
  50.472 -        fun just1 j = REPEAT_DETERM(eresolve_tac neqE i) THEN
  50.473 -          METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i
  50.474 -    in DETERM(resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i) THEN
  50.475 -       EVERY(map just1 justs)
  50.476 -    end
  50.477 -    state;
  50.478 +    let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ Int.toString (length justs) ^ " justification(s)):") state
  50.479 +        val sg          = theory_of_thm state
  50.480 +        val {neqE, ...} = Data.get sg
  50.481 +        fun just1 j =
  50.482 +          REPEAT_DETERM (eresolve_tac neqE i) THEN                  (* eliminate inequalities *)
  50.483 +            METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i  (* use theorems generated from the actual justifications *)
  50.484 +    in DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN  (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
  50.485 +       DETERM (LA_Data.pre_tac i) THEN                               (* user-defined preprocessing of the subgoal *)
  50.486 +       PRIMITIVE (trace_thm "State after pre_tac:") THEN
  50.487 +       EVERY (map just1 justs)                                       (* prove every resulting subgoal, using its justification *)
  50.488 +    end  state;
  50.489  
  50.490 -fun count P xs = length(List.filter P xs);
  50.491 +(* ('a -> bool) -> 'a list -> int *)
  50.492 +
  50.493 +fun count P xs = length (List.filter P xs);
  50.494  
  50.495  (* The limit on the number of ~= allowed.
  50.496     Because each ~= is split into two cases, this can lead to an explosion.
  50.497  *)
  50.498  val fast_arith_neq_limit = ref 9;
  50.499  
  50.500 -fun prove sg ps ex Hs concl =
  50.501 -let val Hitems = map (LA_Data.decomp sg) Hs
  50.502 -in if count (fn NONE => false | SOME(_,_,r,_,_,_) => r = "~=") Hitems
  50.503 -      > !fast_arith_neq_limit then NONE
  50.504 -   else
  50.505 -   case LA_Data.decomp sg concl of
  50.506 -     NONE => refute sg ps ex (Hitems@[NONE])
  50.507 -   | SOME(citem as (r,i,rel,l,j,d)) =>
  50.508 -       let val neg::rel0 = explode rel
  50.509 -           val nrel = if neg = "~" then implode rel0 else "~"^rel
  50.510 -       in refute sg ps ex (Hitems @ [SOME(r,i,nrel,l,j,d)]) end
  50.511 -end;
  50.512 +(* Theory.theory -> (string * Term.typ) list -> bool -> bool -> Term.term list -> Term.term -> injust list option *)
  50.513 +
  50.514 +fun prove sg params show_ex do_pre Hs concl =
  50.515 +  let
  50.516 +    (* append the negated conclusion to 'Hs' -- this corresponds to     *)
  50.517 +    (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *)
  50.518 +    (* theorem/tactic level                                             *)
  50.519 +    val Hs' = Hs @ [LA_Logic.neg_prop concl]
  50.520 +    (* decompT option -> bool *)
  50.521 +    fun is_neq NONE                 = false
  50.522 +      | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=")
  50.523 +  in
  50.524 +    trace_msg "prove";
  50.525 +    if count is_neq (map (LA_Data.decomp sg) Hs')
  50.526 +      > !fast_arith_neq_limit then (
  50.527 +      trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ string_of_int (!fast_arith_neq_limit) ^ ")");
  50.528 +      NONE
  50.529 +    ) else
  50.530 +      refute sg params show_ex do_pre Hs'
  50.531 +  end;
  50.532  
  50.533  (*
  50.534  Fast but very incomplete decider. Only premises and conclusions
  50.535  that are already (negated) (in)equations are taken into account.
  50.536  *)
  50.537 -fun simpset_lin_arith_tac ss ex i st = SUBGOAL (fn (A,_) =>
  50.538 -  let val params = rev(Logic.strip_params A)
  50.539 -      val pTs = map snd params
  50.540 -      val Hs = Logic.strip_assums_hyp A
  50.541 -      val concl = Logic.strip_assums_concl A
  50.542 +fun simpset_lin_arith_tac ss show_ex i st = SUBGOAL (fn (A,_) =>
  50.543 +  let val params = rev (Logic.strip_params A)
  50.544 +      val Hs     = Logic.strip_assums_hyp A
  50.545 +      val concl  = Logic.strip_assums_concl A
  50.546    in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st;
  50.547 -     case prove (Thm.sign_of_thm st) (pTs,params) ex Hs concl of
  50.548 +     case prove (Thm.sign_of_thm st) params show_ex true Hs concl of
  50.549         NONE => (trace_msg "Refutation failed."; no_tac)
  50.550 -     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
  50.551 +     | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js))
  50.552    end) i st;
  50.553  
  50.554 -fun lin_arith_tac ex i st =
  50.555 +fun lin_arith_tac show_ex i st =
  50.556    simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
  50.557 -    ex i st;
  50.558 +    show_ex i st;
  50.559  
  50.560  fun cut_lin_arith_tac ss i =
  50.561    cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
  50.562 @@ -673,47 +775,77 @@
  50.563  datatype splittree = Tip of thm list
  50.564                     | Spl of thm * cterm * splittree * cterm * splittree
  50.565  
  50.566 +(* the cterm "(ct1 ==> ?R) ==> (ct2 ==> ?R) ==> ?R" is taken to (ct1, ct2) *)
  50.567 +
  50.568 +(* Thm.cterm -> Thm.cterm * Thm.cterm *)
  50.569 +
  50.570  fun extract imp =
  50.571 -let val (Il,r) = Thm.dest_comb imp
  50.572 -    val (_,imp1) = Thm.dest_comb Il
  50.573 -    val (Ict1,_) = Thm.dest_comb imp1
  50.574 -    val (_,ct1) = Thm.dest_comb Ict1
  50.575 -    val (Ir,_) = Thm.dest_comb r
  50.576 -    val (_,Ict2r) = Thm.dest_comb Ir
  50.577 -    val (Ict2,_) = Thm.dest_comb Ict2r
  50.578 -    val (_,ct2) = Thm.dest_comb Ict2
  50.579 -in (ct1,ct2) end;
  50.580 +let val (Il, r)    = Thm.dest_comb imp
  50.581 +    val (_, imp1)  = Thm.dest_comb Il
  50.582 +    val (Ict1, _)  = Thm.dest_comb imp1
  50.583 +    val (_, ct1)   = Thm.dest_comb Ict1
  50.584 +    val (Ir, _)    = Thm.dest_comb r
  50.585 +    val (_, Ict2r) = Thm.dest_comb Ir
  50.586 +    val (Ict2, _)  = Thm.dest_comb Ict2r
  50.587 +    val (_, ct2)   = Thm.dest_comb Ict2
  50.588 +in (ct1, ct2) end;
  50.589 +
  50.590 +(* Theory.theory -> Thm.thm list -> splittree *)
  50.591  
  50.592  fun splitasms sg asms =
  50.593 -let val {neqE, ...}  = Data.get sg;
  50.594 -    fun split(asms',[]) = Tip(rev asms')
  50.595 -      | split(asms',asm::asms) =
  50.596 -      (case get_first (fn th => SOME(asm COMP th) handle THM _ => NONE) neqE
  50.597 -       of SOME spl =>
  50.598 -          let val (ct1,ct2) = extract(cprop_of spl)
  50.599 -              val thm1 = assume ct1 and thm2 = assume ct2
  50.600 -          in Spl(spl,ct1,split(asms',asms@[thm1]),ct2,split(asms',asms@[thm2]))
  50.601 +let val {neqE, ...} = Data.get sg
  50.602 +    fun elim_neq (asms', []) = Tip (rev asms')
  50.603 +      | elim_neq (asms', asm::asms) =
  50.604 +      (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of
  50.605 +        SOME spl =>
  50.606 +          let val (ct1, ct2) = extract (cprop_of spl)
  50.607 +              val thm1 = assume ct1
  50.608 +              val thm2 = assume ct2
  50.609 +          in Spl (spl, ct1, elim_neq (asms', asms@[thm1]), ct2, elim_neq (asms', asms@[thm2]))
  50.610            end
  50.611 -       | NONE => split(asm::asms', asms))
  50.612 -in split([],asms) end;
  50.613 +      | NONE => elim_neq (asm::asms', asms))
  50.614 +in elim_neq ([], asms) end;
  50.615 +
  50.616 +(* Theory.theory * MetaSimplifier.simpset -> splittree -> injust list -> (Thm.thm, injust list) *)
  50.617  
  50.618  fun fwdproof ctxt (Tip asms) (j::js) = (mkthm ctxt asms j, js)
  50.619 -  | fwdproof ctxt (Spl(thm,ct1,tree1,ct2,tree2)) js =
  50.620 -    let val (thm1,js1) = fwdproof ctxt tree1 js
  50.621 -        val (thm2,js2) = fwdproof ctxt tree2 js1
  50.622 +  | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js =
  50.623 +    let val (thm1, js1) = fwdproof ctxt tree1 js
  50.624 +        val (thm2, js2) = fwdproof ctxt tree2 js1
  50.625          val thm1' = implies_intr ct1 thm1
  50.626          val thm2' = implies_intr ct2 thm2
  50.627      in (thm2' COMP (thm1' COMP thm), js2) end;
  50.628  (* needs handle THM _ => NONE ? *)
  50.629  
  50.630 -fun prover (ctxt as (sg, _)) thms Tconcl js pos =
  50.631 -let val nTconcl = LA_Logic.neg_prop Tconcl
  50.632 -    val cnTconcl = cterm_of sg nTconcl
  50.633 -    val nTconclthm = assume cnTconcl
  50.634 -    val tree = splitasms sg (thms @ [nTconclthm])
  50.635 -    val (thm,_) = fwdproof ctxt tree js
  50.636 -    val contr = if pos then LA_Logic.ccontr else LA_Logic.notI
  50.637 -in SOME(LA_Logic.mk_Eq((implies_intr cnTconcl thm) COMP contr)) end
  50.638 +(* Theory.theory * MetaSimplifier.simpset -> Thm.thm list -> Term.term -> injust list -> bool -> Thm.thm option *)
  50.639 +
  50.640 +fun prover (ctxt as (sg, ss)) thms Tconcl js pos =
  50.641 +let 
  50.642 +(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *)
  50.643 +(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *)
  50.644 +    (* There is no "forward version" of 'pre_tac'.  Therefore we combine the     *)
  50.645 +    (* available theorems into a single proof state and perform "backward proof" *)
  50.646 +    (* using 'refute_tac'.                                                       *)
  50.647 +(*
  50.648 +    val Hs    = map prop_of thms
  50.649 +    val Prop  = fold (curry Logic.mk_implies) (rev Hs) Tconcl
  50.650 +    val cProp = cterm_of sg Prop
  50.651 +    val concl = Goal.init cProp
  50.652 +                  |> refute_tac ss (1, js)
  50.653 +                  |> Seq.hd
  50.654 +                  |> Goal.finish
  50.655 +                  |> fold (fn thA => fn thAB => implies_elim thAB thA) thms
  50.656 +*)
  50.657 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
  50.658 +    val nTconcl       = LA_Logic.neg_prop Tconcl
  50.659 +    val cnTconcl      = cterm_of sg nTconcl
  50.660 +    val nTconclthm    = assume cnTconcl
  50.661 +    val tree          = splitasms sg (thms @ [nTconclthm])
  50.662 +    val (Falsethm, _) = fwdproof ctxt tree js
  50.663 +    val contr         = if pos then LA_Logic.ccontr else LA_Logic.notI
  50.664 +    val concl         = implies_intr cnTconcl Falsethm COMP contr
  50.665 +in SOME (trace_thm "Proved by lin. arith. prover:"
  50.666 +          (LA_Logic.mk_Eq concl)) end
  50.667  (* in case concl contains ?-var, which makes assume fail: *)
  50.668  handle THM _ => NONE;
  50.669  
  50.670 @@ -723,15 +855,22 @@
  50.671     2. lin_arith_prover is applied by the simplifier which
  50.672        dives into terms and will thus try the non-negated concl anyway.
  50.673  *)
  50.674 +
  50.675 +(* Theory.theory -> MetaSimplifier.simpset -> Term.term -> Thm.thm option *)
  50.676 +
  50.677  fun lin_arith_prover sg ss concl =
  50.678 -let
  50.679 -    val thms = maps LA_Logic.atomize (prems_of_ss ss);
  50.680 -    val Hs = map (#prop o rep_thm) thms
  50.681 +let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss));
  50.682 +    val Hs = map prop_of thms
  50.683      val Tconcl = LA_Logic.mk_Trueprop concl
  50.684 -in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
  50.685 +(*
  50.686 +    val _ = trace_msg "lin_arith_prover"
  50.687 +    val _ = map (trace_thm "thms:") thms
  50.688 +    val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl)
  50.689 +*)
  50.690 +in case prove sg [] false false Hs Tconcl of (* concl provable? *)
  50.691       SOME js => prover (sg, ss) thms Tconcl js true
  50.692     | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl
  50.693 -          in case prove sg ([],[]) false Hs nTconcl of (* ~concl provable? *)
  50.694 +          in case prove sg [] false false Hs nTconcl of (* ~concl provable? *)
  50.695                 SOME js => prover (sg, ss) thms nTconcl js false
  50.696               | NONE => NONE
  50.697            end
    51.1 --- a/src/Provers/splitter.ML	Wed Jul 26 13:31:07 2006 +0200
    51.2 +++ b/src/Provers/splitter.ML	Wed Jul 26 19:23:04 2006 +0200
    51.3 @@ -13,18 +13,23 @@
    51.4  signature SPLITTER_DATA =
    51.5  sig
    51.6    val mk_eq         : thm -> thm
    51.7 -  val meta_eq_to_iff: thm (* "x == y ==> x = y"                    *)
    51.8 -  val iffD          : thm (* "[| P = Q; Q |] ==> P"                *)
    51.9 -  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R" *)
   51.10 -  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R" *)
   51.11 -  val exE           : thm (* "[|  x. P x; !!x. P x ==> Q |] ==> Q" *)
   51.12 -  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"          *)
   51.13 -  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"          *)
   51.14 -  val notnotD       : thm (* "~ ~ P ==> P"                         *)
   51.15 +  val meta_eq_to_iff: thm (* "x == y ==> x = y"                      *)
   51.16 +  val iffD          : thm (* "[| P = Q; Q |] ==> P"                  *)
   51.17 +  val disjE         : thm (* "[| P | Q; P ==> R; Q ==> R |] ==> R"   *)
   51.18 +  val conjE         : thm (* "[| P & Q; [| P; Q |] ==> R |] ==> R"   *)
   51.19 +  val exE           : thm (* "[| EX x. P x; !!x. P x ==> Q |] ==> Q" *)
   51.20 +  val contrapos     : thm (* "[| ~ Q; P ==> Q |] ==> ~ P"            *)
   51.21 +  val contrapos2    : thm (* "[| Q; ~ P ==> ~ Q |] ==> P"            *)
   51.22 +  val notnotD       : thm (* "~ ~ P ==> P"                           *)
   51.23  end
   51.24  
   51.25  signature SPLITTER =
   51.26  sig
   51.27 +  (* somewhat more internal functions *)
   51.28 +  val cmap_of_split_thms : thm list -> (string * (typ * term * thm * typ * int) list) list
   51.29 +  val split_posns        : (string * (typ * term * thm * typ * int) list) list -> theory -> typ list -> term ->
   51.30 +    (thm * (typ * typ * int list) list * int list * typ * term) list  (* first argument is a "cmap", returns a list of "split packs" *)
   51.31 +  (* the "real" interface, providing a number of tactics *)
   51.32    val split_tac       : thm list -> int -> tactic
   51.33    val split_inside_tac: thm list -> int -> tactic
   51.34    val split_asm_tac   : thm list -> int -> tactic
   51.35 @@ -52,18 +57,42 @@
   51.36  val const_Trueprop = ObjectLogic.judgment_name (the_context ());
   51.37  
   51.38  
   51.39 -fun split_format_err() = error("Wrong format for split rule");
   51.40 +fun split_format_err () = error "Wrong format for split rule";
   51.41  
   51.42 +(* thm -> (string * typ) * bool *)
   51.43  fun split_thm_info thm = case concl_of (Data.mk_eq thm) of
   51.44       Const("==", _) $ (Var _ $ t) $ c => (case strip_comb t of
   51.45         (Const p, _) => (p, case c of (Const (s, _) $ _) => s = const_not | _ => false)
   51.46       | _ => split_format_err ())
   51.47     | _ => split_format_err ();
   51.48  
   51.49 +(* thm list -> (string * (typ * term * thm * typ * int) list) list *)
   51.50 +fun cmap_of_split_thms thms =
   51.51 +let
   51.52 +  val splits = map Data.mk_eq thms
   51.53 +  fun add_thm (cmap, thm) =
   51.54 +        (case concl_of thm of _$(t as _$lhs)$_ =>
   51.55 +           (case strip_comb lhs of (Const(a,aT),args) =>
   51.56 +              let val info = (aT,lhs,thm,fastype_of t,length args)
   51.57 +              in case AList.lookup (op =) cmap a of
   51.58 +                   SOME infos => AList.update (op =) (a, info::infos) cmap
   51.59 +                 | NONE => (a,[info])::cmap
   51.60 +              end
   51.61 +            | _ => split_format_err())
   51.62 +         | _ => split_format_err())
   51.63 +in
   51.64 +  Library.foldl add_thm ([], splits)
   51.65 +end;
   51.66 +
   51.67 +(* ------------------------------------------------------------------------- *)
   51.68 +(* mk_case_split_tac                                                         *)
   51.69 +(* ------------------------------------------------------------------------- *)
   51.70 +
   51.71 +(* (int * int -> order) -> thm list -> int -> tactic * <split_posns> *)
   51.72 +
   51.73  fun mk_case_split_tac order =
   51.74  let
   51.75  
   51.76 -
   51.77  (************************************************************
   51.78     Create lift-theorem "trlift" :
   51.79  
   51.80 @@ -71,7 +100,8 @@
   51.81  
   51.82  *************************************************************)
   51.83  
   51.84 -val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;
   51.85 +val meta_iffD = Data.meta_eq_to_iff RS Data.iffD;  (* (P == Q) ==> Q ==> P *)
   51.86 +
   51.87  val lift =
   51.88    let val ct = read_cterm Pure.thy
   51.89             ("(!!x. (Q::('b::{})=>('c::{}))(x) == R(x)) ==> \
   51.90 @@ -129,12 +159,12 @@
   51.91  
   51.92  
   51.93  (* add all loose bound variables in t to list is *)
   51.94 -fun add_lbnos(is,t) = add_loose_bnos(t,0,is);
   51.95 +fun add_lbnos (is,t) = add_loose_bnos (t,0,is);
   51.96  
   51.97  (* check if the innermost abstraction that needs to be removed
   51.98     has a body of type T; otherwise the expansion thm will fail later on
   51.99  *)
  51.100 -fun type_test(T,lbnos,apsns) =
  51.101 +fun type_test (T,lbnos,apsns) =
  51.102    let val (_,U,_) = List.nth(apsns, Library.foldl Int.min (hd lbnos, tl lbnos))
  51.103    in T=U end;
  51.104  
  51.105 @@ -166,7 +196,7 @@
  51.106            lifting is required before applying the split-theorem.
  51.107  ******************************************************************************)
  51.108  
  51.109 -fun mk_split_pack(thm, T, T', n, ts, apsns, pos, TB, t) =
  51.110 +fun mk_split_pack (thm, T, T', n, ts, apsns, pos, TB, t) =
  51.111    if n > length ts then []
  51.112    else let val lev = length apsns
  51.113             val lbnos = Library.foldl add_lbnos ([],Library.take(n,ts))
  51.114 @@ -198,26 +228,34 @@
  51.115     see Pure/pattern.ML for the full version;
  51.116  *)
  51.117  local
  51.118 -exception MATCH
  51.119 +  exception MATCH
  51.120  in
  51.121 -fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
  51.122 -                          handle Type.TYPE_MATCH => raise MATCH;
  51.123 -fun fomatch sg args =
  51.124 -  let
  51.125 -    fun mtch tyinsts = fn
  51.126 -        (Ts,Var(_,T), t)  => typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
  51.127 -      | (_,Free (a,T), Free (b,U)) =>
  51.128 -          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
  51.129 -      | (_,Const (a,T), Const (b,U))  =>
  51.130 -          if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
  51.131 -      | (_,Bound i, Bound j)  =>  if  i=j  then tyinsts else raise MATCH
  51.132 -      | (Ts,Abs(_,T,t), Abs(_,U,u))  =>
  51.133 -          mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
  51.134 -      | (Ts, f$t, g$u) => mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
  51.135 -      | _ => raise MATCH
  51.136 -  in (mtch Vartab.empty args; true) handle MATCH => false end;
  51.137 -end
  51.138 +  (* Context.theory -> Type.tyenv * (Term.typ * Term.typ) -> Type.tyenv *)
  51.139 +  fun typ_match sg (tyenv, TU) = (Sign.typ_match sg TU tyenv)
  51.140 +                            handle Type.TYPE_MATCH => raise MATCH
  51.141 +  (* Context.theory -> Term.typ list * Term.term * Term.term -> bool *)
  51.142 +  fun fomatch sg args =
  51.143 +    let
  51.144 +      (* Type.tyenv -> Term.typ list * Term.term * Term.term -> Type.tyenv *)
  51.145 +      fun mtch tyinsts = fn
  51.146 +          (Ts, Var(_,T), t) =>
  51.147 +            typ_match sg (tyinsts, (T, fastype_of1(Ts,t)))
  51.148 +        | (_, Free (a,T), Free (b,U)) =>
  51.149 +            if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
  51.150 +        | (_, Const (a,T), Const (b,U)) =>
  51.151 +            if a=b then typ_match sg (tyinsts,(T,U)) else raise MATCH
  51.152 +        | (_, Bound i, Bound j) =>
  51.153 +            if i=j then tyinsts else raise MATCH
  51.154 +        | (Ts, Abs(_,T,t), Abs(_,U,u)) =>
  51.155 +            mtch (typ_match sg (tyinsts,(T,U))) (U::Ts,t,u)
  51.156 +        | (Ts, f$t, g$u) =>
  51.157 +            mtch (mtch tyinsts (Ts,f,g)) (Ts, t, u)
  51.158 +        | _ => raise MATCH
  51.159 +    in (mtch Vartab.empty args; true) handle MATCH => false end;
  51.160 +end  (* local *)
  51.161  
  51.162 +(* (string * (Term.typ * Term.term * Thm.thm * Term.typ * int) list) list -> Context.theory -> Term.typ list -> Term.term ->
  51.163 +  (Thm.thm * (Term.typ * Term.typ * int list) list * int list * Term.typ * Term.term) list *)
  51.164  fun split_posns cmap sg Ts t =
  51.165    let
  51.166      val T' = fastype_of1 (Ts, t);
  51.167 @@ -243,15 +281,13 @@
  51.168            in snd(Library.foldl iter ((0, a), ts)) end
  51.169    in posns Ts [] [] t end;
  51.170  
  51.171 +fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
  51.172  
  51.173 -fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
  51.174 -
  51.175 -fun shorter((_,ps,pos,_,_),(_,qs,qos,_,_)) =
  51.176 +fun shorter ((_,ps,pos,_,_), (_,qs,qos,_,_)) =
  51.177    prod_ord (int_ord o pairself length) (order o pairself length)
  51.178      ((ps, pos), (qs, qos));
  51.179  
  51.180  
  51.181 -
  51.182  (************************************************************
  51.183     call split_posns with appropriate parameters
  51.184  *************************************************************)
  51.185 @@ -261,8 +297,10 @@
  51.186        val goali = nth_subgoal i state
  51.187        val Ts = rev(map #2 (Logic.strip_params goali))
  51.188        val _ $ t $ _ = Logic.strip_assums_concl goali;
  51.189 -  in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
  51.190 +  in (Ts, t, sort shorter (split_posns cmap sg Ts t)) end;
  51.191  
  51.192 +fun exported_split_posns cmap sg Ts t =
  51.193 +  sort shorter (split_posns cmap sg Ts t);
  51.194  
  51.195  (*************************************************************
  51.196     instantiate lift theorem
  51.197 @@ -322,20 +360,11 @@
  51.198     i      : number of subgoal the tactic should be applied to
  51.199  *****************************************************************************)
  51.200  
  51.201 +(* thm list -> int -> tactic *)
  51.202 +
  51.203  fun split_tac [] i = no_tac
  51.204    | split_tac splits i =
  51.205 -  let val splits = map Data.mk_eq splits;
  51.206 -      fun add_thm(cmap,thm) =
  51.207 -            (case concl_of thm of _$(t as _$lhs)$_ =>
  51.208 -               (case strip_comb lhs of (Const(a,aT),args) =>
  51.209 -                  let val info = (aT,lhs,thm,fastype_of t,length args)
  51.210 -                  in case AList.lookup (op =) cmap a of
  51.211 -                       SOME infos => AList.update (op =) (a, info::infos) cmap
  51.212 -                     | NONE => (a,[info])::cmap
  51.213 -                  end
  51.214 -                | _ => split_format_err())
  51.215 -             | _ => split_format_err())
  51.216 -      val cmap = Library.foldl add_thm ([],splits);
  51.217 +  let val cmap = cmap_of_split_thms splits
  51.218        fun lift_tac Ts t p st = rtac (inst_lift Ts t p st i) i st
  51.219        fun lift_split_tac state =
  51.220              let val (Ts, t, splits) = select cmap state i
  51.221 @@ -352,12 +381,12 @@
  51.222            (rtac meta_iffD i THEN lift_split_tac)
  51.223    end;
  51.224  
  51.225 -in split_tac end;
  51.226 +in (split_tac, exported_split_posns) end;  (* mk_case_split_tac *)
  51.227  
  51.228  
  51.229 -val split_tac        = mk_case_split_tac              int_ord;
  51.230 +val (split_tac, split_posns)        = mk_case_split_tac              int_ord;
  51.231  
  51.232 -val split_inside_tac = mk_case_split_tac (rev_order o int_ord);
  51.233 +val (split_inside_tac, _)           = mk_case_split_tac (rev_order o int_ord);
  51.234  
  51.235  
  51.236  (*****************************************************************************
  51.237 @@ -378,7 +407,7 @@
  51.238                |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) =
  51.239                                          first_prem_is_disj t
  51.240                |   first_prem_is_disj _ = false;
  51.241 -      (* does not work properly if the split variable is bound by a quantfier *)
  51.242 +      (* does not work properly if the split variable is bound by a quantifier *)
  51.243                fun flat_prems_tac i = SUBGOAL (fn (t,i) =>
  51.244                             (if first_prem_is_disj t
  51.245                              then EVERY[etac Data.disjE i,rotate_tac ~1 i,
  51.246 @@ -387,11 +416,11 @@
  51.247                              else all_tac)
  51.248                             THEN REPEAT (eresolve_tac [Data.conjE,Data.exE] i)
  51.249                             THEN REPEAT (dresolve_tac [Data.notnotD]   i)) i;
  51.250 -          in if n<0 then no_tac else DETERM (EVERY'
  51.251 +          in if n<0 then  no_tac  else (DETERM (EVERY'
  51.252                  [rotate_tac n, etac Data.contrapos2,
  51.253                   split_tac splits,
  51.254                   rotate_tac ~1, etac Data.contrapos, rotate_tac ~1,
  51.255 -                 flat_prems_tac] i)
  51.256 +                 flat_prems_tac] i))
  51.257            end;
  51.258    in SUBGOAL tac
  51.259    end;