src/HOL/arith_data.ML
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 20280 ad9fbbd01535
child 20412 40757f475eb0
permissions -rw-r--r--
simplified code generator setup
     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 "HOL.plus";
    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) = List.partition (equal one) ts in
    29     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    30   end;
    31 
    32 (* dest_sum *)
    33 
    34 val dest_plus = HOLogic.dest_bin "HOL.plus" HOLogic.natT;
    35 
    36 fun dest_sum tm =
    37   if HOLogic.is_zero tm then []
    38   else
    39     (case try HOLogic.dest_Suc tm of
    40       SOME t => one :: dest_sum t
    41     | NONE =>
    42         (case try dest_plus tm of
    43           SOME (t, u) => dest_sum t @ dest_sum u
    44         | NONE => [tm]));
    45 
    46 (** generic proof tools **)
    47 
    48 (* prove conversions *)
    49 
    50 fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    51   mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    52       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    53     (K (EVERY [expand_tac, norm_tac ss]))));
    54 
    55 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    56   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    57 
    58 (* rewriting *)
    59 
    60 fun simp_all_tac rules =
    61   let val ss0 = HOL_ss addsimps rules
    62   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    63 
    64 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    65 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    66 
    67 fun prep_simproc (name, pats, proc) =
    68   Simplifier.simproc (the_context ()) name pats proc;
    69 
    70 end;  (* NatArithUtils *)
    71 
    72 
    73 signature ARITH_DATA =
    74 sig
    75   val nat_cancel_sums_add: simproc list
    76   val nat_cancel_sums: simproc list
    77 end;
    78 
    79 
    80 structure ArithData: ARITH_DATA =
    81 struct
    82 
    83 open NatArithUtils;
    84 
    85 (** cancel common summands **)
    86 
    87 structure Sum =
    88 struct
    89   val mk_sum = mk_norm_sum;
    90   val dest_sum = dest_sum;
    91   val prove_conv = prove_conv;
    92   val norm_tac1 = simp_all_tac add_rules;
    93   val norm_tac2 = simp_all_tac add_ac;
    94   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    95 end;
    96 
    97 fun gen_uncancel_tac rule ct =
    98   rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1;
    99 
   100 (* nat eq *)
   101 
   102 structure EqCancelSums = CancelSumsFun
   103 (struct
   104   open Sum;
   105   val mk_bal = HOLogic.mk_eq;
   106   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   107   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
   108 end);
   109 
   110 (* nat less *)
   111 
   112 structure LessCancelSums = CancelSumsFun
   113 (struct
   114   open Sum;
   115   val mk_bal = HOLogic.mk_binrel "Orderings.less";
   116   val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
   117   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
   118 end);
   119 
   120 (* nat le *)
   121 
   122 structure LeCancelSums = CancelSumsFun
   123 (struct
   124   open Sum;
   125   val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
   126   val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
   127   val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
   128 end);
   129 
   130 (* nat diff *)
   131 
   132 structure DiffCancelSums = CancelSumsFun
   133 (struct
   134   open Sum;
   135   val mk_bal = HOLogic.mk_binop "HOL.minus";
   136   val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
   137   val uncancel_tac = gen_uncancel_tac diff_cancel;
   138 end);
   139 
   140 (** prepare nat_cancel simprocs **)
   141 
   142 val nat_cancel_sums_add = map prep_simproc
   143   [("nateq_cancel_sums",
   144      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
   145      K EqCancelSums.proc),
   146    ("natless_cancel_sums",
   147      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
   148      K LessCancelSums.proc),
   149    ("natle_cancel_sums",
   150      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
   151      K LeCancelSums.proc)];
   152 
   153 val nat_cancel_sums = nat_cancel_sums_add @
   154   [prep_simproc ("natdiff_cancel_sums",
   155     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
   156     K DiffCancelSums.proc)];
   157 
   158 end;  (* ArithData *)
   159 
   160 open ArithData;
   161 
   162 
   163 (*---------------------------------------------------------------------------*)
   164 (* 2. Linear arithmetic                                                      *)
   165 (*---------------------------------------------------------------------------*)
   166 
   167 (* Parameters data for general linear arithmetic functor *)
   168 
   169 structure LA_Logic: LIN_ARITH_LOGIC =
   170 struct
   171 
   172 val ccontr = ccontr;
   173 val conjI = conjI;
   174 val notI = notI;
   175 val sym = sym;
   176 val not_lessD = linorder_not_less RS iffD1;
   177 val not_leD = linorder_not_le RS iffD1;
   178 
   179 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   180 
   181 val mk_Trueprop = HOLogic.mk_Trueprop;
   182 
   183 fun atomize thm = case #prop(rep_thm thm) of
   184     Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) =>
   185     atomize(thm RS conjunct1) @ atomize(thm RS conjunct2)
   186   | _ => [thm];
   187 
   188 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   189   | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
   190 
   191 fun is_False thm =
   192   let val _ $ t = #prop(rep_thm thm)
   193   in t = Const("False",HOLogic.boolT) end;
   194 
   195 fun is_nat(t) = fastype_of1 t = HOLogic.natT;
   196 
   197 fun mk_nat_thm sg t =
   198   let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   199   in instantiate ([],[(cn,ct)]) le0 end;
   200 
   201 end;  (* LA_Logic *)
   202 
   203 
   204 (* arith theory data *)
   205 
   206 structure ArithTheoryData = TheoryDataFun
   207 (struct
   208   val name = "HOL/arith";
   209   type T = {splits: thm list,
   210             inj_consts: (string * typ) list,
   211             discrete: string list,
   212             presburger: (int -> tactic) option};
   213   val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE};
   214   val copy = I;
   215   val extend = I;
   216   fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1},
   217              {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) =
   218    {splits = Drule.merge_rules (splits1, splits2),
   219     inj_consts = merge_lists inj_consts1 inj_consts2,
   220     discrete = merge_lists discrete1 discrete2,
   221     presburger = (case presburger1 of NONE => presburger2 | p => p)};
   222   fun print _ _ = ();
   223 end);
   224 
   225 val arith_split_add = Thm.declaration_attribute (fn thm =>
   226   Context.map_theory (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   227     {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger})));
   228 
   229 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   230   {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger});
   231 
   232 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} =>
   233   {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger});
   234 
   235 
   236 signature HOL_LIN_ARITH_DATA =
   237 sig
   238   include LIN_ARITH_DATA
   239   val fast_arith_split_limit : int ref
   240 end;
   241 
   242 structure LA_Data_Ref: HOL_LIN_ARITH_DATA =
   243 struct
   244 
   245 (* internal representation of linear (in-)equations *)
   246 type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
   247 
   248 (* Decomposition of terms *)
   249 
   250 fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
   251   | nT _                      = false;
   252 
   253 fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
   254              (term * Rat.rat) list * Rat.rat =
   255   case AList.lookup (op =) p t of NONE   => ((t, m) :: p, i)
   256                                 | SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i);
   257 
   258 exception Zero;
   259 
   260 fun rat_of_term (numt : term, dent : term) : Rat.rat =
   261 let
   262   val num = HOLogic.dest_binum numt
   263   val den = HOLogic.dest_binum dent
   264 in
   265   if den = 0 then raise Zero else Rat.rat_of_quotient (num, den)
   266 end;
   267 
   268 (* Warning: in rare cases number_of encloses a non-numeral,
   269    in which case dest_binum raises TERM; hence all the handles below.
   270    Same for Suc-terms that turn out not to be numerals -
   271    although the simplifier should eliminate those anyway ...
   272 *)
   273 fun number_of_Sucs (Const ("Suc", _) $ n) : int =
   274       number_of_Sucs n + 1
   275   | number_of_Sucs t =
   276       if HOLogic.is_zero t then 0 else raise TERM ("number_of_Sucs", []);
   277 
   278 (* decompose nested multiplications, bracketing them to the right and combining
   279    all their coefficients
   280 *)
   281 fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
   282 let
   283   fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
   284     (case s of
   285       Const ("Numeral.number_of", _) $ n =>
   286         demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
   287     | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
   288         demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n))))
   289     | Const("Suc", _) $ _ =>
   290         demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s)))
   291     | Const ("HOL.times", _) $ s1 $ s2 =>
   292         demult (mC $ s1 $ (mC $ s2 $ t), m)
   293     | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
   294         let
   295           val den = HOLogic.dest_binum dent
   296         in
   297           if den = 0 then
   298             raise Zero
   299           else
   300             demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
   301         end
   302     | _ =>
   303         atomult (mC, s, t, m)
   304     ) handle TERM _ => atomult (mC, s, t, m)
   305   )
   306     | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
   307       (let
   308         val den = HOLogic.dest_binum dent
   309       in
   310         if den = 0 then
   311           raise Zero
   312         else
   313           demult (t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
   314       end
   315         handle TERM _ => (SOME atom, m))
   316     | demult (Const ("0", _), m) = (NONE, Rat.rat_of_int 0)
   317     | demult (Const ("1", _), m) = (NONE, m)
   318     | demult (t as Const ("Numeral.number_of", _) $ n, m) =
   319         ((NONE, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
   320           handle TERM _ => (SOME t,m))
   321     | demult (Const ("HOL.uminus", _) $ t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1)))
   322     | demult (t as Const f $ x, m) =
   323         (if f mem inj_consts then SOME x else SOME t, m)
   324     | demult (atom, m) = (SOME atom, m)
   325 and
   326   atomult (mC, atom, t, m) = (
   327     case demult (t, m) of (NONE, m')    => (SOME atom, m')
   328                         | (SOME t', m') => (SOME (mC $ atom $ t'), m')
   329   )
   330 in demult end;
   331 
   332 fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
   333             ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
   334 let
   335   (* Turn term into list of summand * multiplicity plus a constant *)
   336   fun poly (Const ("HOL.plus", _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
   337         poly (s, m, poly (t, m, pi))
   338     | poly (all as Const ("HOL.minus", T) $ s $ t, m, pi) =
   339         if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
   340     | poly (all as Const ("HOL.uminus", T) $ t, m, pi) =
   341         if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
   342     | poly (Const ("0", _), _, pi) =
   343         pi
   344     | poly (Const ("1", _), m, (p, i)) =
   345         (p, Rat.add (i, m))
   346     | poly (Const ("Suc", _) $ t, m, (p, i)) =
   347         poly (t, m, (p, Rat.add (i, m)))
   348     | poly (all as Const ("HOL.times", _) $ _ $ _, m, pi as (p, i)) =
   349         (case demult inj_consts (all, m) of
   350            (NONE,   m') => (p, Rat.add (i, m'))
   351          | (SOME u, m') => add_atom u m' pi)
   352     | poly (all as Const ("HOL.divide", _) $ _ $ _, m, pi as (p, i)) =
   353         (case demult inj_consts (all, m) of
   354            (NONE,   m') => (p, Rat.add (i, m'))
   355          | (SOME u, m') => add_atom u m' pi)
   356     | poly (all as Const ("Numeral.number_of", _) $ t, m, pi as (p, i)) =
   357         ((p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum t))))
   358          handle TERM _ => add_atom all m pi)
   359     | poly (all as Const f $ x, m, pi) =
   360         if f mem inj_consts then poly (x, m, pi) else add_atom all m pi
   361     | poly (all, m, pi) =
   362         add_atom all m pi
   363   val (p, i) = poly (lhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0))
   364   val (q, j) = poly (rhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0))
   365 in
   366   case rel of
   367     "Orderings.less"    => SOME (p, i, "<", q, j)
   368   | "Orderings.less_eq" => SOME (p, i, "<=", q, j)
   369   | "op ="              => SOME (p, i, "=", q, j)
   370   | _                   => NONE
   371 end handle Zero => NONE;
   372 
   373 fun of_lin_arith_sort sg (U : typ) : bool =
   374   Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"])
   375 
   376 fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
   377   if of_lin_arith_sort sg U then
   378     (true, D mem discrete)
   379   else (* special cases *)
   380     if D mem discrete then  (true, true)  else  (false, false)
   381   | allows_lin_arith sg discrete U =
   382   (of_lin_arith_sort sg U, false);
   383 
   384 fun decomp_typecheck (sg, discrete, inj_consts) (T : typ, xxx) : decompT option =
   385   case T of
   386     Type ("fun", [U, _]) =>
   387       (case allows_lin_arith sg discrete U of
   388         (true, d) =>
   389           (case decomp0 inj_consts xxx of
   390             NONE                   => NONE
   391           | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d))
   392       | (false, _) =>
   393           NONE)
   394   | _ => NONE;
   395 
   396 fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
   397   | negate NONE                        = NONE;
   398 
   399 fun decomp_negation data (_ $ (Const (rel, T) $ lhs $ rhs)) : decompT option =
   400       decomp_typecheck data (T, (rel, lhs, rhs))
   401   | decomp_negation data (_ $ (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
   402       negate (decomp_typecheck data (T, (rel, lhs, rhs)))
   403   | decomp_negation data _ =
   404       NONE;
   405 
   406 fun decomp sg : term -> decompT option =
   407 let
   408   val {discrete, inj_consts, ...} = ArithTheoryData.get sg
   409 in
   410   decomp_negation (sg, discrete, inj_consts)
   411 end;
   412 
   413 fun domain_is_nat (_ $ (Const (_, T) $ _ $ _))                      = nT T
   414   | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T
   415   | domain_is_nat _                                                 = false;
   416 
   417 fun number_of (n : IntInf.int, T : typ) =
   418   HOLogic.number_of_const T $ (HOLogic.mk_binum n);
   419 
   420 (*---------------------------------------------------------------------------*)
   421 (* code that performs certain goal transformations for linear arithmetic     *)
   422 (*---------------------------------------------------------------------------*)
   423 
   424 (* A "do nothing" variant of pre_decomp and pre_tac:
   425 
   426 fun pre_decomp sg Ts termitems = [termitems];
   427 fun pre_tac i = all_tac;
   428 *)
   429 
   430 (*---------------------------------------------------------------------------*)
   431 (* the following code performs splitting of certain constants (e.g. min,     *)
   432 (* max) in a linear arithmetic problem; similar to what split_tac later does *)
   433 (* to the proof state                                                        *)
   434 (*---------------------------------------------------------------------------*)
   435 
   436 val fast_arith_split_limit = ref 9;
   437 
   438 (* checks if splitting with 'thm' is implemented                             *)
   439 
   440 fun is_split_thm (thm : thm) : bool =
   441   case concl_of thm of _ $ (_ $ (_ $ lhs) $ _) => (
   442     (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
   443     case head_of lhs of
   444       Const (a, _) => a mem_string ["Orderings.max",
   445                                     "Orderings.min",
   446                                     "HOL.abs",
   447                                     "HOL.minus",
   448                                     "IntDef.nat",
   449                                     "Divides.op mod",
   450                                     "Divides.op div"]
   451     | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
   452                                  Display.string_of_thm thm);
   453                        false))
   454   | _ => (warning ("Lin. Arith.: wrong format for split rule " ^
   455                    Display.string_of_thm thm);
   456           false);
   457 
   458 (* substitute new for occurrences of old in a term, incrementing bound       *)
   459 (* variables as needed when substituting inside an abstraction               *)
   460 
   461 fun subst_term ([] : (term * term) list) (t : term) = t
   462   | subst_term pairs                     t          =
   463       (case AList.lookup (op aconv) pairs t of
   464         SOME new =>
   465           new
   466       | NONE     =>
   467           (case t of Abs (a, T, body) =>
   468             let val pairs' = map (pairself (incr_boundvars 1)) pairs
   469             in  Abs (a, T, subst_term pairs' body)  end
   470           | t1 $ t2                   =>
   471             subst_term pairs t1 $ subst_term pairs t2
   472           | _ => t));
   473 
   474 (* approximates the effect of one application of split_tac (followed by NNF  *)
   475 (* normalization) on the subgoal represented by '(Ts, terms)'; returns a     *)
   476 (* list of new subgoals (each again represented by a typ list for bound      *)
   477 (* variables and a term list for premises), or NONE if split_tac would fail  *)
   478 (* on the subgoal                                                            *)
   479 
   480 (* FIXME: currently only the effect of certain split theorems is reproduced  *)
   481 (*        (which is why we need 'is_split_thm').  A more canonical           *)
   482 (*        implementation should analyze the right-hand side of the split     *)
   483 (*        theorem that can be applied, and modify the subgoal accordingly.   *)
   484 (*        Or even better, the splitter should be extended to provide         *)
   485 (*        splitting on terms as well as splitting on theorems (where the     *)
   486 (*        former can have a faster implementation as it does not need to be  *)
   487 (*        proof-producing).                                                  *)
   488 
   489 fun split_once_items (sg : theory) (Ts : typ list, terms : term list) :
   490                      (typ list * term list) list option =
   491 let
   492   (* takes a list  [t1, ..., tn]  to the term                                *)
   493   (*   tn' --> ... --> t1' --> False  ,                                      *)
   494   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   495   (* term list -> term *)
   496   fun REPEAT_DETERM_etac_rev_mp terms' =
   497     fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const
   498   val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg))
   499   val cmap       = Splitter.cmap_of_split_thms split_thms
   500   val splits     = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms)
   501 in
   502   if length splits > !fast_arith_split_limit then (
   503     tracing ("fast_arith_split_limit exceeded (current value is " ^
   504               string_of_int (!fast_arith_split_limit) ^ ")");
   505     NONE
   506   ) else (
   507   case splits of [] =>
   508     (* split_tac would fail: no possible split *)
   509     NONE
   510   | ((_, _, _, split_type, split_term) :: _) => (
   511     (* ignore all but the first possible split *)
   512     case strip_comb split_term of
   513     (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
   514       (Const ("Orderings.max", _), [t1, t2]) =>
   515       let
   516         val rev_terms     = rev terms
   517         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   518         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   519         val t1_leq_t2     = Const ("Orderings.less_eq",
   520                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   521         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   522         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   523         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
   524         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
   525       in
   526         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   527       end
   528     (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
   529     | (Const ("Orderings.min", _), [t1, t2]) =>
   530       let
   531         val rev_terms     = rev terms
   532         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   533         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   534         val t1_leq_t2     = Const ("Orderings.less_eq",
   535                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   536         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   537         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   538         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
   539         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
   540       in
   541         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   542       end
   543     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
   544     | (Const ("HOL.abs", _), [t1]) =>
   545       let
   546         val rev_terms   = rev terms
   547         val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   548         val terms2      = map (subst_term [(split_term, Const ("HOL.uminus",
   549                             split_type --> split_type) $ t1)]) rev_terms
   550         val zero        = Const ("0", split_type)
   551         val zero_leq_t1 = Const ("Orderings.less_eq",
   552                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   553         val t1_lt_zero  = Const ("Orderings.less",
   554                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   555         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   556         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   557         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   558       in
   559         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   560       end
   561     (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
   562     | (Const ("HOL.minus", _), [t1, t2]) =>
   563       let
   564         (* "d" in the above theorem becomes a new bound variable after NNF   *)
   565         (* transformation, therefore some adjustment of indices is necessary *)
   566         val rev_terms       = rev terms
   567         val zero            = Const ("0", split_type)
   568         val d               = Bound 0
   569         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
   570         val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
   571                                 (map (incr_boundvars 1) rev_terms)
   572         val t1'             = incr_boundvars 1 t1
   573         val t2'             = incr_boundvars 1 t2
   574         val t1_lt_t2        = Const ("Orderings.less",
   575                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   576         val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   577                                 (Const ("HOL.plus",
   578                                   split_type --> split_type --> split_type) $ t2' $ d)
   579         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   580         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
   581         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
   582       in
   583         SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
   584       end
   585     (* ?P (nat ?i) = ((ALL n. ?i = int n --> ?P n) & (?i < 0 --> ?P 0)) *)
   586     | (Const ("IntDef.nat", _), [t1]) =>
   587       let
   588         val rev_terms   = rev terms
   589         val zero_int    = Const ("0", HOLogic.intT)
   590         val zero_nat    = Const ("0", HOLogic.natT)
   591         val n           = Bound 0
   592         val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
   593                             (map (incr_boundvars 1) rev_terms)
   594         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
   595         val t1'         = incr_boundvars 1 t1
   596         val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   597                             (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
   598         val t1_lt_zero  = Const ("Orderings.less",
   599                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   600         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   601         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
   602         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   603       in
   604         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
   605       end
   606     (* "?P ((?n::nat) mod (number_of ?k)) =
   607          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
   608            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
   609     | (Const ("Divides.op mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
   610       let
   611         val rev_terms               = rev terms
   612         val zero                    = Const ("0", split_type)
   613         val i                       = Bound 1
   614         val j                       = Bound 0
   615         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
   616         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)])
   617                                         (map (incr_boundvars 2) rev_terms)
   618         val t1'                     = incr_boundvars 2 t1
   619         val t2'                     = incr_boundvars 2 t2
   620         val t2_eq_zero              = Const ("op =",
   621                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   622         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   623                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   624         val j_lt_t2                 = Const ("Orderings.less",
   625                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   626         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   627                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
   628                                          (Const ("HOL.times",
   629                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   630         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   631         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   632         val subgoal2                = (map HOLogic.mk_Trueprop
   633                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   634                                           @ terms2 @ [not_false]
   635       in
   636         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
   637       end
   638     (* "?P ((?n::nat) div (number_of ?k)) =
   639          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
   640            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
   641     | (Const ("Divides.op div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
   642       let
   643         val rev_terms               = rev terms
   644         val zero                    = Const ("0", split_type)
   645         val i                       = Bound 1
   646         val j                       = Bound 0
   647         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
   648         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)])
   649                                         (map (incr_boundvars 2) rev_terms)
   650         val t1'                     = incr_boundvars 2 t1
   651         val t2'                     = incr_boundvars 2 t2
   652         val t2_eq_zero              = Const ("op =",
   653                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   654         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   655                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   656         val j_lt_t2                 = Const ("Orderings.less",
   657                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   658         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   659                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
   660                                          (Const ("HOL.times",
   661                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   662         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   663         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   664         val subgoal2                = (map HOLogic.mk_Trueprop
   665                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   666                                           @ terms2 @ [not_false]
   667       in
   668         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
   669       end
   670     (* "?P ((?n::int) mod (number_of ?k)) =
   671          ((iszero (number_of ?k) --> ?P ?n) &
   672           (neg (number_of (bin_minus ?k)) -->
   673             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
   674           (neg (number_of ?k) -->
   675             (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
   676     | (Const ("Divides.op mod",
   677         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
   678       let
   679         val rev_terms               = rev terms
   680         val zero                    = Const ("0", split_type)
   681         val i                       = Bound 1
   682         val j                       = Bound 0
   683         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
   684         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, j)])
   685                                         (map (incr_boundvars 2) rev_terms)
   686         val t1'                     = incr_boundvars 2 t1
   687         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
   688         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
   689         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
   690                                         (number_of $
   691                                           (Const ("Numeral.bin_minus",
   692                                             HOLogic.binT --> HOLogic.binT) $ k'))
   693         val zero_leq_j              = Const ("Orderings.less_eq",
   694                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
   695         val j_lt_t2                 = Const ("Orderings.less",
   696                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   697         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   698                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
   699                                          (Const ("HOL.times",
   700                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   701         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
   702         val t2_lt_j                 = Const ("Orderings.less",
   703                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   704         val j_leq_zero              = Const ("Orderings.less_eq",
   705                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
   706         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   707         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
   708         val subgoal2                = (map HOLogic.mk_Trueprop [neg_minus_k, zero_leq_j])
   709                                         @ hd terms2_3
   710                                         :: (if tl terms2_3 = [] then [not_false] else [])
   711                                         @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
   712                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   713         val subgoal3                = (map HOLogic.mk_Trueprop [neg_t2, t2_lt_j])
   714                                         @ hd terms2_3
   715                                         :: (if tl terms2_3 = [] then [not_false] else [])
   716                                         @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
   717                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   718         val Ts'                     = split_type :: split_type :: Ts
   719       in
   720         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
   721       end
   722     (* "?P ((?n::int) div (number_of ?k)) =
   723          ((iszero (number_of ?k) --> ?P 0) &
   724           (neg (number_of (bin_minus ?k)) -->
   725             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
   726           (neg (number_of ?k) -->
   727             (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
   728     | (Const ("Divides.op div",
   729         Type ("fun", [Type ("IntDef.int", []), _])), [t1, t2 as (number_of $ k)]) =>
   730       let
   731         val rev_terms               = rev terms
   732         val zero                    = Const ("0", split_type)
   733         val i                       = Bound 1
   734         val j                       = Bound 0
   735         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
   736         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
   737                                         (map (incr_boundvars 2) rev_terms)
   738         val t1'                     = incr_boundvars 2 t1
   739         val (t2' as (_ $ k'))       = incr_boundvars 2 t2
   740         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
   741         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
   742                                         (number_of $
   743                                           (Const ("Numeral.bin_minus",
   744                                             HOLogic.binT --> HOLogic.binT) $ k'))
   745         val zero_leq_j              = Const ("Orderings.less_eq",
   746                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
   747         val j_lt_t2                 = Const ("Orderings.less",
   748                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   749         val t1_eq_t2_times_i_plus_j = Const ("op =",
   750                                         split_type --> split_type --> HOLogic.boolT) $ t1' $
   751                                        (Const ("HOL.plus", split_type --> split_type --> split_type) $
   752                                          (Const ("HOL.times",
   753                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   754         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
   755         val t2_lt_j                 = Const ("Orderings.less",
   756                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   757         val j_leq_zero              = Const ("Orderings.less_eq",
   758                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
   759         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   760         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
   761         val subgoal2                = (HOLogic.mk_Trueprop neg_minus_k)
   762                                         :: terms2_3
   763                                         @ not_false
   764                                         :: (map HOLogic.mk_Trueprop
   765                                              [zero_leq_j, j_lt_t2, t1_eq_t2_times_i_plus_j])
   766         val subgoal3                = (HOLogic.mk_Trueprop neg_t2)
   767                                         :: terms2_3
   768                                         @ not_false
   769                                         :: (map HOLogic.mk_Trueprop
   770                                              [t2_lt_j, j_leq_zero, t1_eq_t2_times_i_plus_j])
   771         val Ts'                     = split_type :: split_type :: Ts
   772       in
   773         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
   774       end
   775     (* this will only happen if a split theorem can be applied for which no  *)
   776     (* code exists above -- in which case either the split theorem should be *)
   777     (* implemented above, or 'is_split_thm' should be modified to filter it  *)
   778     (* out                                                                   *)
   779     | (t, ts) => (
   780       warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^
   781                " (with " ^ Int.toString (length ts) ^
   782                " argument(s)) not implemented; proof reconstruction is likely to fail");
   783       NONE
   784     ))
   785   )
   786 end;
   787 
   788 (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
   789 (* terms in the same way as filter_prems_tac does                            *)
   790 
   791 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
   792 let
   793   fun filter_prems (t, (left, right)) =
   794     if  p t  then  (left, right @ [t])  else  (left @ right, [])
   795   val (left, right) = foldl filter_prems ([], []) terms
   796 in
   797   right @ left
   798 end;
   799 
   800 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
   801 (* subgoal that has 'terms' as premises                                      *)
   802 
   803 fun negated_term_occurs_positively (terms : term list) : bool =
   804   List.exists
   805     (fn (Trueprop $ (Const ("Not", _) $ t)) => member (op aconv) terms (Trueprop $ t)
   806       | _                                   => false)
   807     terms;
   808 
   809 fun pre_decomp sg (Ts : typ list, terms : term list) : (typ list * term list) list =
   810 let
   811   (* repeatedly split (including newly emerging subgoals) until no further   *)
   812   (* splitting is possible                                                   *)
   813   fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
   814     | split_loop (subgoal::subgoals)                = (
   815         case split_once_items sg subgoal of
   816           SOME new_subgoals => split_loop (new_subgoals @ subgoals)
   817         | NONE              => subgoal :: split_loop subgoals
   818       )
   819   fun is_relevant t  = isSome (decomp sg t)
   820   (* filter_prems_tac is_relevant: *)
   821   val relevant_terms = filter_prems_tac_items is_relevant terms
   822   (* split_tac, NNF normalization: *)
   823   val split_goals    = split_loop [(Ts, relevant_terms)]
   824   (* necessary because split_once_tac may normalize terms: *)
   825   val beta_eta_norm  = map (apsnd (map (Envir.eta_contract o Envir.beta_norm))) split_goals
   826   (* TRY (etac notE) THEN eq_assume_tac: *)
   827   val result         = List.filter (not o negated_term_occurs_positively o snd) beta_eta_norm
   828 in
   829   result
   830 end;
   831 
   832 (* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
   833 (* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
   834 (* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
   835 (* performs NNF-normalization of ~P, and eliminates conjunctions,            *)
   836 (* disjunctions and existential quantifiers from the premises, possibly (in  *)
   837 (* the case of disjunctions) resulting in several new subgoals, each of the  *)
   838 (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
   839 (* !fast_arith_split_limit splits are possible.                              *)
   840 
   841 fun split_once_tac (split_thms : thm list) (i : int) : tactic =
   842 let
   843   val nnf_simpset =
   844     empty_ss setmkeqTrue mk_eq_True
   845     setmksimps (mksimps mksimps_pairs)
   846     addsimps [imp_conv_disj, iff_conv_conj_imp, de_Morgan_disj, de_Morgan_conj, 
   847       not_all, not_ex, not_not]
   848   fun prem_nnf_tac i st =
   849     full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st
   850   fun cond_split_tac i st =
   851     let
   852       val subgoal = Logic.nth_prem (i, Thm.prop_of st)
   853       val Ts      = rev (map snd (Logic.strip_params subgoal))
   854       val concl   = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
   855       val cmap    = Splitter.cmap_of_split_thms split_thms
   856       val splits  = Splitter.split_posns cmap (theory_of_thm st) Ts concl
   857     in
   858       if length splits > !fast_arith_split_limit then
   859         no_tac st
   860       else
   861         split_tac split_thms i st
   862     end
   863 in
   864   EVERY' [
   865     REPEAT_DETERM o etac rev_mp,
   866     cond_split_tac,
   867     rtac ccontr,
   868     prem_nnf_tac,
   869     TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
   870   ] i
   871 end;
   872 
   873 (* remove irrelevant premises, then split the i-th subgoal (and all new      *)
   874 (* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
   875 (* subgoals and finally attempt to solve them by finding an immediate        *)
   876 (* contradiction (i.e. a term and its negation) in their premises.           *)
   877 
   878 fun pre_tac i st =
   879 let
   880   val sg            = theory_of_thm st
   881   val split_thms    = filter is_split_thm (#splits (ArithTheoryData.get sg))
   882   fun is_relevant t = isSome (decomp sg t)
   883 in
   884   DETERM (
   885     TRY (filter_prems_tac is_relevant i)
   886       THEN (
   887         (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
   888           THEN_ALL_NEW
   889             ((fn j => PRIMITIVE
   890                         (Drule.fconv_rule
   891                           (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
   892               THEN'
   893             (TRY o (etac notE THEN' eq_assume_tac)))
   894       ) i
   895   ) st
   896 end;
   897 
   898 end;  (* LA_Data_Ref *)
   899 
   900 
   901 structure Fast_Arith =
   902   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
   903 
   904 val fast_arith_tac         = Fast_Arith.lin_arith_tac false;
   905 val fast_ex_arith_tac      = Fast_Arith.lin_arith_tac;
   906 val trace_arith            = Fast_Arith.trace;
   907 val fast_arith_neq_limit   = Fast_Arith.fast_arith_neq_limit;
   908 val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit;
   909 
   910 local
   911 
   912 (* reduce contradictory <= to False.
   913    Most of the work is done by the cancel tactics.
   914 *)
   915 val add_rules =
   916  [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
   917   One_nat_def,
   918   order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
   919   zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
   920 
   921 val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
   922  (fn prems => [cut_facts_tac prems 1,
   923                blast_tac (claset() addIs [add_mono]) 1]))
   924 ["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   925  "(i  = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   926  "(i <= j) & (k  = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)",
   927  "(i  = j) & (k  = l) ==> i + k  = j + (l::'a::pordered_ab_semigroup_add)"
   928 ];
   929 
   930 val mono_ss = simpset() addsimps
   931                 [add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
   932 
   933 val add_mono_thms_ordered_field =
   934   map (fn s => prove_goal (the_context ()) s
   935                  (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
   936     ["(i<j) & (k=l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   937      "(i=j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   938      "(i<j) & (k<=l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   939      "(i<=j) & (k<l)  ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)",
   940      "(i<j) & (k<l)   ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"];
   941 
   942 in
   943 
   944 val init_lin_arith_data =
   945  Fast_Arith.setup #>
   946  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
   947    {add_mono_thms = add_mono_thms @
   948     add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
   949     mult_mono_thms = mult_mono_thms,
   950     inj_thms = inj_thms,
   951     lessD = lessD @ [Suc_leI],
   952     neqE = [linorder_neqE_nat,
   953       get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
   954     simpset = HOL_basic_ss addsimps add_rules
   955                    addsimprocs [ab_group_add_cancel.sum_conv,
   956                                 ab_group_add_cancel.rel_conv]
   957                    (*abel_cancel helps it work in abstract algebraic domains*)
   958                    addsimprocs nat_cancel_sums_add}) #>
   959   ArithTheoryData.init #>
   960   arith_discrete "nat";
   961 
   962 end;
   963 
   964 val fast_nat_arith_simproc =
   965   Simplifier.simproc (the_context ()) "fast_nat_arith"
   966     ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
   967 
   968 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   969 useful to detect inconsistencies among the premises for subgoals which are
   970 *not* themselves (in)equalities, because the latter activate
   971 fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
   972 solver all the time rather than add the additional check. *)
   973 
   974 
   975 (* arith proof method *)
   976 
   977 local
   978 
   979 fun raw_arith_tac ex i st =
   980   (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
   981      decomp sg"?) to speed things up in case there are lots of irrelevant
   982      terms involved; elimination of min/max can be optimized:
   983      (max m n + k <= r) = (m+k <= r & n+k <= r)
   984      (l <= min m n + k) = (l <= m+k & l <= n+k)
   985   *)
   986   refute_tac (K true)
   987     (* Splitting is also done inside fast_arith_tac, but not completely --   *)
   988     (* split_tac may use split theorems that have not been implemented in    *)
   989     (* fast_arith_tac (cf. pre_decomp and split_once_items above), and       *)
   990     (* fast_arith_split_limit may trigger.                                   *)
   991     (* Therefore splitting outside of fast_arith_tac may allow us to prove   *)
   992     (* some goals that fast_arith_tac alone would fail on.                   *)
   993     (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st))))
   994     (fast_ex_arith_tac ex)
   995     i st;
   996 
   997 fun presburger_tac i st =
   998   (case ArithTheoryData.get (Thm.theory_of_thm st) of
   999      {presburger = SOME tac, ...} =>
  1000        (warning "Trying full Presburger arithmetic ..."; tac i st)
  1001    | _ => no_tac st);
  1002 
  1003 in
  1004 
  1005   val simple_arith_tac = FIRST' [fast_arith_tac,
  1006     ObjectLogic.atomize_tac THEN' raw_arith_tac true];
  1007 
  1008   val arith_tac = FIRST' [fast_arith_tac,
  1009     ObjectLogic.atomize_tac THEN' raw_arith_tac true,
  1010     presburger_tac];
  1011 
  1012   val silent_arith_tac = FIRST' [fast_arith_tac,
  1013     ObjectLogic.atomize_tac THEN' raw_arith_tac false,
  1014     presburger_tac];
  1015 
  1016   fun arith_method prems =
  1017     Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
  1018 
  1019 end;
  1020 
  1021 (* antisymmetry:
  1022    combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
  1023 
  1024 local
  1025 val antisym = mk_meta_eq order_antisym
  1026 val not_lessD = linorder_not_less RS iffD1
  1027 fun prp t thm = (#prop(rep_thm thm) = t)
  1028 in
  1029 fun antisym_eq prems thm =
  1030   let
  1031     val r = #prop(rep_thm thm);
  1032   in
  1033     case r of
  1034       Tr $ ((c as Const("Orderings.less_eq",T)) $ s $ t) =>
  1035         let val r' = Tr $ (c $ t $ s)
  1036         in
  1037           case Library.find_first (prp r') prems of
  1038             NONE =>
  1039               let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ s $ t))
  1040               in case Library.find_first (prp r') prems of
  1041                    NONE => []
  1042                  | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
  1043               end
  1044           | SOME thm' => [thm' RS (thm RS antisym)]
  1045         end
  1046     | Tr $ (Const("Not",_) $ (Const("Orderings.less",T) $ s $ t)) =>
  1047         let val r' = Tr $ (Const("Orderings.less_eq",T) $ s $ t)
  1048         in
  1049           case Library.find_first (prp r') prems of
  1050             NONE =>
  1051               let val r' = Tr $ (HOLogic.Not $ (Const("Orderings.less",T) $ t $ s))
  1052               in case Library.find_first (prp r') prems of
  1053                    NONE => []
  1054                  | SOME thm' =>
  1055                      [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
  1056               end
  1057           | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
  1058         end
  1059     | _ => []
  1060   end
  1061   handle THM _ => []
  1062 end;
  1063 *)
  1064 
  1065 (* theory setup *)
  1066 
  1067 val arith_setup =
  1068   init_lin_arith_data #>
  1069   (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
  1070     addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
  1071     addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
  1072   Method.add_methods
  1073     [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
  1074       "decide linear arithmethic")] #>
  1075   Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
  1076     "declaration of split rules for arithmetic procedure")];