src/HOL/arith_data.ML
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15121 1198032bad25 child 15184 d2c19aea17bc permissions -rw-r--r--
import -> imports
```     1 (*  Title:      HOL/arith_data.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Markus Wenzel, Stefan Berghofer and Tobias Nipkow
```
```     4
```
```     5 Various arithmetic proof procedures.
```
```     6 *)
```
```     7
```
```     8 (*---------------------------------------------------------------------------*)
```
```     9 (* 1. Cancellation of common terms                                           *)
```
```    10 (*---------------------------------------------------------------------------*)
```
```    11
```
```    12 structure NatArithUtils =
```
```    13 struct
```
```    14
```
```    15 (** abstract syntax of structure nat: 0, Suc, + **)
```
```    16
```
```    17 (* mk_sum, mk_norm_sum *)
```
```    18
```
```    19 val one = HOLogic.mk_nat 1;
```
```    20 val mk_plus = HOLogic.mk_binop "op +";
```
```    21
```
```    22 fun mk_sum [] = HOLogic.zero
```
```    23   | mk_sum [t] = t
```
```    24   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
```
```    25
```
```    26 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
```
```    27 fun mk_norm_sum ts =
```
```    28   let val (ones, sums) = partition (equal one) ts in
```
```    29     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
```
```    30   end;
```
```    31
```
```    32
```
```    33 (* dest_sum *)
```
```    34
```
```    35 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
```
```    36
```
```    37 fun dest_sum tm =
```
```    38   if HOLogic.is_zero tm then []
```
```    39   else
```
```    40     (case try HOLogic.dest_Suc tm of
```
```    41       Some t => one :: dest_sum t
```
```    42     | None =>
```
```    43         (case try dest_plus tm of
```
```    44           Some (t, u) => dest_sum t @ dest_sum u
```
```    45         | None => [tm]));
```
```    46
```
```    47
```
```    48 (** generic proof tools **)
```
```    49
```
```    50 (* prove conversions *)
```
```    51
```
```    52 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
```
```    53
```
```    54 fun prove_conv expand_tac norm_tac sg tu =
```
```    55   mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
```
```    56     (K [expand_tac, norm_tac]))
```
```    57   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
```
```    58     (string_of_cterm (cterm_of sg (mk_eqv tu))));
```
```    59
```
```    60 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
```
```    61   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
```
```    62
```
```    63
```
```    64 (* rewriting *)
```
```    65
```
```    66 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
```
```    67
```
```    68 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
```
```    69 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
```
```    70
```
```    71 fun prep_simproc (name, pats, proc) =
```
```    72   Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
```
```    73
```
```    74 end;
```
```    75
```
```    76 signature ARITH_DATA =
```
```    77 sig
```
```    78   val nat_cancel_sums_add: simproc list
```
```    79   val nat_cancel_sums: simproc list
```
```    80 end;
```
```    81
```
```    82 structure ArithData: ARITH_DATA =
```
```    83 struct
```
```    84
```
```    85 open NatArithUtils;
```
```    86
```
```    87
```
```    88 (** cancel common summands **)
```
```    89
```
```    90 structure Sum =
```
```    91 struct
```
```    92   val mk_sum = mk_norm_sum;
```
```    93   val dest_sum = dest_sum;
```
```    94   val prove_conv = prove_conv;
```
```    95   val norm_tac = simp_all add_rules THEN simp_all add_ac;
```
```    96 end;
```
```    97
```
```    98 fun gen_uncancel_tac rule ct =
```
```    99   rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
```
```   100
```
```   101
```
```   102 (* nat eq *)
```
```   103
```
```   104 structure EqCancelSums = CancelSumsFun
```
```   105 (struct
```
```   106   open Sum;
```
```   107   val mk_bal = HOLogic.mk_eq;
```
```   108   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
```
```   109   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
```
```   110 end);
```
```   111
```
```   112
```
```   113 (* nat less *)
```
```   114
```
```   115 structure LessCancelSums = CancelSumsFun
```
```   116 (struct
```
```   117   open Sum;
```
```   118   val mk_bal = HOLogic.mk_binrel "op <";
```
```   119   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
```
```   120   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
```
```   121 end);
```
```   122
```
```   123
```
```   124 (* nat le *)
```
```   125
```
```   126 structure LeCancelSums = CancelSumsFun
```
```   127 (struct
```
```   128   open Sum;
```
```   129   val mk_bal = HOLogic.mk_binrel "op <=";
```
```   130   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
```
```   131   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
```
```   132 end);
```
```   133
```
```   134
```
```   135 (* nat diff *)
```
```   136
```
```   137 structure DiffCancelSums = CancelSumsFun
```
```   138 (struct
```
```   139   open Sum;
```
```   140   val mk_bal = HOLogic.mk_binop "op -";
```
```   141   val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
```
```   142   val uncancel_tac = gen_uncancel_tac diff_cancel;
```
```   143 end);
```
```   144
```
```   145
```
```   146
```
```   147 (** prepare nat_cancel simprocs **)
```
```   148
```
```   149 val nat_cancel_sums_add = map prep_simproc
```
```   150   [("nateq_cancel_sums",
```
```   151      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),
```
```   152    ("natless_cancel_sums",
```
```   153      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc),
```
```   154    ("natle_cancel_sums",
```
```   155      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)];
```
```   156
```
```   157 val nat_cancel_sums = nat_cancel_sums_add @
```
```   158   [prep_simproc ("natdiff_cancel_sums",
```
```   159     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)];
```
```   160
```
```   161 end;
```
```   162
```
```   163 open ArithData;
```
```   164
```
```   165
```
```   166 (*---------------------------------------------------------------------------*)
```
```   167 (* 2. Linear arithmetic                                                      *)
```
```   168 (*---------------------------------------------------------------------------*)
```
```   169
```
```   170 (* Parameters data for general linear arithmetic functor *)
```
```   171
```
```   172 structure LA_Logic: LIN_ARITH_LOGIC =
```
```   173 struct
```
```   174 val ccontr = ccontr;
```
```   175 val conjI = conjI;
```
```   176 val neqE = linorder_neqE;
```
```   177 val notI = notI;
```
```   178 val sym = sym;
```
```   179 val not_lessD = linorder_not_less RS iffD1;
```
```   180 val not_leD = linorder_not_le RS iffD1;
```
```   181
```
```   182
```
```   183 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
```
```   184
```
```   185 val mk_Trueprop = HOLogic.mk_Trueprop;
```
```   186
```
```   187 fun neg_prop(TP\$(Const("Not",_)\$t)) = TP\$t
```
```   188   | neg_prop(TP\$t) = TP \$ (Const("Not",HOLogic.boolT-->HOLogic.boolT)\$t);
```
```   189
```
```   190 fun is_False thm =
```
```   191   let val _ \$ t = #prop(rep_thm thm)
```
```   192   in t = Const("False",HOLogic.boolT) end;
```
```   193
```
```   194 fun is_nat(t) = fastype_of1 t = HOLogic.natT;
```
```   195
```
```   196 fun mk_nat_thm sg t =
```
```   197   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
```
```   198   in instantiate ([],[(cn,ct)]) le0 end;
```
```   199
```
```   200 end;
```
```   201
```
```   202
```
```   203 (* arith theory data *)
```
```   204
```
```   205 structure ArithTheoryDataArgs =
```
```   206 struct
```
```   207   val name = "HOL/arith";
```
```   208   type T = {splits: thm list, inj_consts: (string * typ)list, discrete: (string * bool) list, presburger: (int -> tactic) option};
```
```   209
```
```   210   val empty = {splits = [], inj_consts = [], discrete = [], presburger = None};
```
```   211   val copy = I;
```
```   212   val prep_ext = I;
```
```   213   fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
```
```   214              {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
```
```   215    {splits = Drule.merge_rules (splits1, splits2),
```
```   216     inj_consts = merge_lists inj_consts1 inj_consts2,
```
```   217     discrete = merge_alists discrete1 discrete2,
```
```   218     presburger = (case presburger1 of None => presburger2 | p => p)};
```
```   219   fun print _ _ = ();
```
```   220 end;
```
```   221
```
```   222 structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
```
```   223
```
```   224 fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
```
```   225   {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm);
```
```   226
```
```   227 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
```
```   228   {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
```
```   229
```
```   230 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
```
```   231   {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
```
```   232
```
```   233
```
```   234 structure LA_Data_Ref: LIN_ARITH_DATA =
```
```   235 struct
```
```   236
```
```   237 (* Decomposition of terms *)
```
```   238
```
```   239 fun nT (Type("fun",[N,_])) = N = HOLogic.natT
```
```   240   | nT _ = false;
```
```   241
```
```   242 fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
```
```   243                            | Some n => (overwrite(p,(t,ratadd(n,m))), i));
```
```   244
```
```   245 exception Zero;
```
```   246
```
```   247 fun rat_of_term(numt,dent) =
```
```   248   let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent
```
```   249   in if den = 0 then raise Zero else int_ratdiv(num,den) end;
```
```   250
```
```   251 (* Warning: in rare cases number_of encloses a non-numeral,
```
```   252    in which case dest_binum raises TERM; hence all the handles below.
```
```   253    Same for Suc-terms that turn out not to be numerals -
```
```   254    although the simplifier should eliminate those anyway...
```
```   255 *)
```
```   256
```
```   257 fun number_of_Sucs (Const("Suc",_) \$ n) = number_of_Sucs n + 1
```
```   258   | number_of_Sucs t = if HOLogic.is_zero t then 0
```
```   259                        else raise TERM("number_of_Sucs",[])
```
```   260
```
```   261 (* decompose nested multiplications, bracketing them to the right and combining all
```
```   262    their coefficients
```
```   263 *)
```
```   264
```
```   265 fun demult inj_consts =
```
```   266 let
```
```   267 fun demult((mC as Const("op *",_)) \$ s \$ t,m) = ((case s of
```
```   268         Const("Numeral.number_of",_)\$n
```
```   269         => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
```
```   270       | Const("uminus",_)\$(Const("Numeral.number_of",_)\$n)
```
```   271         => demult(t,ratmul(m,rat_of_int(~(HOLogic.dest_binum n))))
```
```   272       | Const("Suc",_) \$ _
```
```   273         => demult(t,ratmul(m,rat_of_int(number_of_Sucs s)))
```
```   274       | Const("op *",_) \$ s1 \$ s2 => demult(mC \$ s1 \$ (mC \$ s2 \$ t),m)
```
```   275       | Const("HOL.divide",_) \$ numt \$ (Const("Numeral.number_of",_)\$dent) =>
```
```   276           let val den = HOLogic.dest_binum dent
```
```   277           in if den = 0 then raise Zero
```
```   278              else demult(mC \$ numt \$ t,ratmul(m, ratinv(rat_of_int den)))
```
```   279           end
```
```   280       | _ => atomult(mC,s,t,m)
```
```   281       ) handle TERM _ => atomult(mC,s,t,m))
```
```   282   | demult(atom as Const("HOL.divide",_) \$ t \$ (Const("Numeral.number_of",_)\$dent), m) =
```
```   283       (let val den = HOLogic.dest_binum dent
```
```   284        in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
```
```   285        handle TERM _ => (Some atom,m))
```
```   286   | demult(Const("0",_),m) = (None, rat_of_int 0)
```
```   287   | demult(Const("1",_),m) = (None, m)
```
```   288   | demult(t as Const("Numeral.number_of",_)\$n,m) =
```
```   289       ((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
```
```   290        handle TERM _ => (Some t,m))
```
```   291   | demult(Const("uminus",_)\$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
```
```   292   | demult(t as Const f \$ x, m) =
```
```   293       (if f mem inj_consts then Some x else Some t,m)
```
```   294   | demult(atom,m) = (Some atom,m)
```
```   295
```
```   296 and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')
```
```   297                             | (Some t',m') => (Some(mC \$ atom \$ t'),m'))
```
```   298 in demult end;
```
```   299
```
```   300 fun decomp2 inj_consts (rel,lhs,rhs) =
```
```   301 let
```
```   302 (* Turn term into list of summand * multiplicity plus a constant *)
```
```   303 fun poly(Const("op +",_) \$ s \$ t, m, pi) = poly(s,m,poly(t,m,pi))
```
```   304   | poly(all as Const("op -",T) \$ s \$ t, m, pi) =
```
```   305       if nT T then add_atom(all,m,pi)
```
```   306       else poly(s,m,poly(t,ratneg m,pi))
```
```   307   | poly(Const("uminus",_) \$ t, m, pi) = poly(t,ratneg m,pi)
```
```   308   | poly(Const("0",_), _, pi) = pi
```
```   309   | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
```
```   310   | poly(Const("Suc",_)\$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
```
```   311   | poly(t as Const("op *",_) \$ _ \$ _, m, pi as (p,i)) =
```
```   312       (case demult inj_consts (t,m) of
```
```   313          (None,m') => (p,ratadd(i,m))
```
```   314        | (Some u,m') => add_atom(u,m',pi))
```
```   315   | poly(t as Const("HOL.divide",_) \$ _ \$ _, m, pi as (p,i)) =
```
```   316       (case demult inj_consts (t,m) of
```
```   317          (None,m') => (p,ratadd(i,m'))
```
```   318        | (Some u,m') => add_atom(u,m',pi))
```
```   319   | poly(all as (Const("Numeral.number_of",_)\$t,m,(p,i))) =
```
```   320       ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
```
```   321        handle TERM _ => add_atom all)
```
```   322   | poly(all as Const f \$ x, m, pi) =
```
```   323       if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
```
```   324   | poly x  = add_atom x;
```
```   325
```
```   326 val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0))
```
```   327 and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0))
```
```   328
```
```   329   in case rel of
```
```   330        "op <"  => Some(p,i,"<",q,j)
```
```   331      | "op <=" => Some(p,i,"<=",q,j)
```
```   332      | "op ="  => Some(p,i,"=",q,j)
```
```   333      | _       => None
```
```   334   end handle Zero => None;
```
```   335
```
```   336 fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
```
```   337   | negate None = None;
```
```   338
```
```   339 fun of_lin_arith_sort sg U =
```
```   340   Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"])
```
```   341
```
```   342 (* FIXME: "discrete" should only contain discrete types *)
```
```   343 fun allows_lin_arith sg discrete (U as Type(D,[])) =
```
```   344       if of_lin_arith_sort sg U
```
```   345       then (true, case assoc(discrete,D) of None => false
```
```   346                   | Some d => d)
```
```   347       else (* special cases *)
```
```   348            (case assoc(discrete,D) of None => (false,false)
```
```   349             | Some d => (true,d))
```
```   350   | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false);
```
```   351
```
```   352 fun decomp1 (sg,discrete,inj_consts) (T,xxx) =
```
```   353   (case T of
```
```   354      Type("fun",[U,_]) =>
```
```   355        (case allows_lin_arith sg discrete U of
```
```   356           (true,d) => (case decomp2 inj_consts xxx of None => None
```
```   357                        | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d))
```
```   358         | (false,_) => None)
```
```   359    | _ => None);
```
```   360
```
```   361 fun decomp2 data (_\$(Const(rel,T)\$lhs\$rhs)) = decomp1 data (T,(rel,lhs,rhs))
```
```   362   | decomp2 data (_\$(Const("Not",_)\$(Const(rel,T)\$lhs\$rhs))) =
```
```   363       negate(decomp1 data (T,(rel,lhs,rhs)))
```
```   364   | decomp2 data _ = None
```
```   365
```
```   366 fun decomp sg =
```
```   367   let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
```
```   368   in decomp2 (sg,discrete,inj_consts) end
```
```   369
```
```   370 fun number_of(n,T) = HOLogic.number_of_const T \$ (HOLogic.mk_bin n)
```
```   371
```
```   372 end;
```
```   373
```
```   374
```
```   375 structure Fast_Arith =
```
```   376   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
```
```   377
```
```   378 val fast_arith_tac    = Fast_Arith.lin_arith_tac false
```
```   379 and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
```
```   380 and trace_arith    = Fast_Arith.trace
```
```   381 and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit;
```
```   382
```
```   383 local
```
```   384
```
```   385 val isolateSuc =
```
```   386   let val thy = theory "Nat"
```
```   387   in prove_goal thy "Suc(i+j) = i+j + Suc 0"
```
```   388      (fn _ => [simp_tac (simpset_of thy) 1])
```
```   389   end;
```
```   390
```
```   391 (* reduce contradictory <= to False.
```
```   392    Most of the work is done by the cancel tactics.
```
```   393 *)
```
```   394 val add_rules =
```
```   395  [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
```
```   396   One_nat_def,isolateSuc];
```
```   397
```
```   398 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
```
```   399  (fn prems => [cut_facts_tac prems 1,
```
```   400                blast_tac (claset() addIs [add_mono]) 1]))
```
```   401 ["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
```
```   402  "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
```
```   403  "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
```
```   404  "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::pordered_ab_semigroup_add)"
```
```   405 ];
```
```   406
```
```   407 val mono_ss = simpset() addsimps
```
```   408                 [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
```
```   409
```
```   410 val add_mono_thms_ordered_field =
```
```   411   map (fn s => prove_goal (the_context ()) s
```
```   412                  (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
```
```   413     ["(i<j) & (k=l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
```
```   414      "(i=j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
```
```   415      "(i<j) & (k<=l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
```
```   416      "(i<=j) & (k<l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
```
```   417      "(i<j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
```
```   418
```
```   419 in
```
```   420
```
```   421 val init_lin_arith_data =
```
```   422  Fast_Arith.setup @
```
```   423  [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} =>
```
```   424    {add_mono_thms = add_mono_thms @
```
```   425     add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
```
```   426     mult_mono_thms = mult_mono_thms,
```
```   427     inj_thms = inj_thms,
```
```   428     lessD = lessD @ [Suc_leI],
```
```   429     simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
```
```   430   ArithTheoryData.init, arith_discrete ("nat", true)];
```
```   431
```
```   432 end;
```
```   433
```
```   434 val fast_nat_arith_simproc =
```
```   435   Simplifier.simproc (Theory.sign_of (the_context ())) "fast_nat_arith"
```
```   436     ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
```
```   437
```
```   438
```
```   439 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
```
```   440 useful to detect inconsistencies among the premises for subgoals which are
```
```   441 *not* themselves (in)equalities, because the latter activate
```
```   442 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
```
```   443 solver all the time rather than add the additional check. *)
```
```   444
```
```   445
```
```   446 (* arith proof method *)
```
```   447
```
```   448 (* FIXME: K true should be replaced by a sensible test to speed things up
```
```   449    in case there are lots of irrelevant terms involved;
```
```   450    elimination of min/max can be optimized:
```
```   451    (max m n + k <= r) = (m+k <= r & n+k <= r)
```
```   452    (l <= min m n + k) = (l <= m+k & l <= n+k)
```
```   453 *)
```
```   454 local
```
```   455
```
```   456 fun raw_arith_tac ex i st =
```
```   457   refute_tac (K true)
```
```   458    (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
```
```   459    ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
```
```   460    i st;
```
```   461
```
```   462 fun presburger_tac i st =
```
```   463   (case ArithTheoryData.get_sg (sign_of_thm st) of
```
```   464      {presburger = Some tac, ...} =>
```
```   465        (tracing "Simple arithmetic decision procedure failed.\nNow trying full Presburger arithmetic..."; tac i st)
```
```   466    | _ => no_tac st);
```
```   467
```
```   468 in
```
```   469
```
```   470 val simple_arith_tac = FIRST' [fast_arith_tac,
```
```   471   ObjectLogic.atomize_tac THEN' raw_arith_tac true];
```
```   472
```
```   473 val arith_tac = FIRST' [fast_arith_tac,
```
```   474   ObjectLogic.atomize_tac THEN' raw_arith_tac true,
```
```   475   presburger_tac];
```
```   476
```
```   477 val silent_arith_tac = FIRST' [fast_arith_tac,
```
```   478   ObjectLogic.atomize_tac THEN' raw_arith_tac false,
```
```   479   presburger_tac];
```
```   480
```
```   481 fun arith_method prems =
```
```   482   Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
```
```   483
```
```   484 end;
```
```   485
```
```   486
```
```   487 (* theory setup *)
```
```   488
```
```   489 val arith_setup =
```
```   490  [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
```
```   491   init_lin_arith_data @
```
```   492   [Simplifier.change_simpset_of (op addSolver)
```
```   493    (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
```
```   494   Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
```
```   495   Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
```
```   496     "decide linear arithmethic")],
```
```   497   Attrib.add_attributes [("arith_split",
```
```   498     (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
```
```   499     "declaration of split rules for arithmetic procedure")]];
```