src/HOL/Tools/lin_arith.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66610 98b7ba7b1e9a
child 67149 e61557884799
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/lin_arith.ML
     2     Author:     Tjark Weber and Tobias Nipkow, TU Muenchen
     3 
     4 HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
     5 *)
     6 
     7 signature LIN_ARITH =
     8 sig
     9   val pre_tac: Proof.context -> int -> tactic
    10   val simple_tac: Proof.context -> int -> tactic
    11   val tac: Proof.context -> int -> tactic
    12   val simproc: Proof.context -> cterm -> thm option
    13   val add_inj_thms: thm list -> Context.generic -> Context.generic
    14   val add_lessD: thm -> Context.generic -> Context.generic
    15   val add_simps: thm list -> Context.generic -> Context.generic
    16   val add_simprocs: simproc list -> Context.generic -> Context.generic
    17   val add_inj_const: string * typ -> Context.generic -> Context.generic
    18   val add_discrete_type: string -> Context.generic -> Context.generic
    19   val set_number_of: (Proof.context -> typ -> int -> cterm) -> Context.generic -> Context.generic
    20   val setup: Context.generic -> Context.generic
    21   val global_setup: theory -> theory
    22   val split_limit: int Config.T
    23   val neq_limit: int Config.T
    24   val trace: bool Config.T
    25 end;
    26 
    27 structure Lin_Arith: LIN_ARITH =
    28 struct
    29 
    30 (* Parameters data for general linear arithmetic functor *)
    31 
    32 structure LA_Logic: LIN_ARITH_LOGIC =
    33 struct
    34 
    35 val ccontr = @{thm ccontr};
    36 val conjI = conjI;
    37 val notI = notI;
    38 val sym = sym;
    39 val trueI = TrueI;
    40 val not_lessD = @{thm linorder_not_less} RS iffD1;
    41 val not_leD = @{thm linorder_not_le} RS iffD1;
    42 
    43 fun mk_Eq thm = thm RS @{thm Eq_FalseI} handle THM _ => thm RS @{thm Eq_TrueI};
    44 
    45 val mk_Trueprop = HOLogic.mk_Trueprop;
    46 
    47 fun atomize thm = case Thm.prop_of thm of
    48     Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
    49     atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
    50   | _ => [thm];
    51 
    52 fun neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
    53   | neg_prop ((TP as Const(@{const_name Trueprop}, _)) $ t) = TP $ (HOLogic.Not $t)
    54   | neg_prop t = raise TERM ("neg_prop", [t]);
    55 
    56 fun is_False thm =
    57   let val _ $ t = Thm.prop_of thm
    58   in t = @{term False} end;
    59 
    60 fun is_nat t = (fastype_of1 t = HOLogic.natT);
    61 
    62 fun mk_nat_thm thy t =
    63   let val ct = Thm.global_cterm_of thy t
    64   in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end;
    65 
    66 end;
    67 
    68 
    69 (* arith context data *)
    70 
    71 structure Lin_Arith_Data = Generic_Data
    72 (
    73   type T = {splits: thm list,
    74             inj_consts: (string * typ) list,
    75             discrete: string list};
    76   val empty = {splits = [], inj_consts = [], discrete = []};
    77   val extend = I;
    78   fun merge
    79    ({splits = splits1, inj_consts = inj_consts1, discrete = discrete1},
    80     {splits = splits2, inj_consts = inj_consts2, discrete = discrete2}) : T =
    81    {splits = Thm.merge_thms (splits1, splits2),
    82     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
    83     discrete = Library.merge (op =) (discrete1, discrete2)};
    84 );
    85 
    86 val get_arith_data = Lin_Arith_Data.get o Context.Proof;
    87 
    88 fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
    89   {splits = update Thm.eq_thm_prop thm splits,
    90    inj_consts = inj_consts, discrete = discrete});
    91 
    92 fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
    93   {splits = splits, inj_consts = inj_consts,
    94    discrete = update (op =) d discrete});
    95 
    96 fun add_inj_const c = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
    97   {splits = splits, inj_consts = update (op =) c inj_consts,
    98    discrete = discrete});
    99 
   100 val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
   101 val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
   102 val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false);
   103 
   104 
   105 structure LA_Data: LIN_ARITH_DATA =
   106 struct
   107 
   108 val neq_limit = neq_limit;
   109 val trace = trace;
   110 
   111 
   112 (* Decomposition of terms *)
   113 
   114 (*internal representation of linear (in-)equations*)
   115 type decomp =
   116   ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
   117 
   118 fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
   119   | nT _                      = false;
   120 
   121 fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
   122              (term * Rat.rat) list * Rat.rat =
   123   case AList.lookup Envir.aeconv p t of
   124       NONE   => ((t, m) :: p, i)
   125     | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
   126 
   127 (* decompose nested multiplications, bracketing them to the right and combining
   128    all their coefficients
   129 
   130    inj_consts: list of constants to be ignored when encountered
   131                (e.g. arithmetic type conversions that preserve value)
   132 
   133    m: multiplicity associated with the entire product
   134 
   135    returns either (SOME term, associated multiplicity) or (NONE, constant)
   136 *)
   137 fun of_field_sort thy U = Sign.of_sort thy (U, @{sort inverse});
   138 
   139 fun demult thy (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
   140 let
   141   fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) =
   142       (case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 =>
   143         (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
   144         demult (mC $ s1 $ (mC $ s2 $ t), m)
   145       | _ =>
   146         (* product 's * t', where either factor can be 'NONE' *)
   147         (case demult (s, m) of
   148           (SOME s', m') =>
   149             (case demult (t, m') of
   150               (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
   151             | (NONE,    m'') => (SOME s', m''))
   152         | (NONE,    m') => demult (t, m')))
   153     | demult (atom as (mC as Const (@{const_name Rings.divide}, T)) $ s $ t, m) =
   154       (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
   155          become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
   156          if we choose to do so here, the simpset used by arith must be able to
   157          perform the same simplifications. *)
   158       (* quotient 's / t', where the denominator t can be NONE *)
   159       (* Note: will raise Div iff m' is @0 *)
   160       if of_field_sort thy (domain_type T) then
   161         let
   162           val (os',m') = demult (s, m);
   163           val (ot',p) = demult (t, @1)
   164         in (case (os',ot') of
   165             (SOME s', SOME t') => SOME (mC $ s' $ t')
   166           | (SOME s', NONE) => SOME s'
   167           | (NONE, SOME t') =>
   168                SOME (mC $ Const (@{const_name Groups.one}, domain_type (snd (dest_Const mC))) $ t')
   169           | (NONE, NONE) => NONE,
   170           Rat.mult m' (Rat.inv p))
   171         end
   172       else (SOME atom, m)
   173     (* terms that evaluate to numeric constants *)
   174     | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m)
   175     | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
   176     | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
   177     (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
   178       in which case dest_numeral raises TERM; hence all the handles below.
   179       Same for Suc-terms that turn out not to be numerals -
   180       although the simplifier should eliminate those anyway ...*)
   181     | demult (t as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ n, m) =
   182       ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_numeral n)))
   183         handle TERM _ => (SOME t, m))
   184     | demult (t as Const (@{const_name Suc}, _) $ _, m) =
   185       ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_nat t)))
   186         handle TERM _ => (SOME t, m))
   187     (* injection constants are ignored *)
   188     | demult (t as Const f $ x, m) =
   189       if member (op =) inj_consts f then demult (x, m) else (SOME t, m)
   190     (* everything else is considered atomic *)
   191     | demult (atom, m) = (SOME atom, m)
   192 in demult end;
   193 
   194 fun decomp0 thy (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
   195             ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
   196 let
   197   (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
   198      summands and associated multiplicities, plus a constant 'i' (with implicit
   199      multiplicity 1) *)
   200   fun poly (Const (@{const_name Groups.plus}, _) $ s $ t,
   201         m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
   202     | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) =
   203         if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi))
   204     | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) =
   205         if nT T then add_atom all m pi else poly (t, ~ m, pi)
   206     | poly (Const (@{const_name Groups.zero}, _), _, pi) =
   207         pi
   208     | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
   209         (p, Rat.add i m)
   210     | poly (all as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ t, m, pi as (p, i)) =
   211         (let val k = HOLogic.dest_numeral t
   212         in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end
   213         handle TERM _ => add_atom all m pi)
   214     | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
   215         poly (t, m, (p, Rat.add i m))
   216     | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
   217         (case demult thy inj_consts (all, m) of
   218            (NONE,   m') => (p, Rat.add i m')
   219          | (SOME u, m') => add_atom u m' pi)
   220     | poly (all as Const (@{const_name Rings.divide}, T) $ _ $ _, m, pi as (p, i)) =
   221         if of_field_sort thy (domain_type T) then 
   222           (case demult thy inj_consts (all, m) of
   223              (NONE,   m') => (p, Rat.add i m')
   224            | (SOME u, m') => add_atom u m' pi)
   225         else add_atom all m pi
   226     | poly (all as Const f $ x, m, pi) =
   227         if member (op =) inj_consts f then poly (x, m, pi) else add_atom all m pi
   228     | poly (all, m, pi) =
   229         add_atom all m pi
   230   val (p, i) = poly (lhs, @1, ([], @0))
   231   val (q, j) = poly (rhs, @1, ([], @0))
   232 in
   233   case rel of
   234     @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
   235   | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   236   | @{const_name HOL.eq}            => SOME (p, i, "=", q, j)
   237   | _                   => NONE
   238 end handle General.Div => NONE;
   239 
   240 fun of_lin_arith_sort thy U =
   241   Sign.of_sort thy (U, @{sort Rings.linordered_idom});
   242 
   243 fun allows_lin_arith thy (discrete : string list) (U as Type (D, [])) : bool * bool =
   244       if of_lin_arith_sort thy U then (true, member (op =) discrete D)
   245       else if member (op =) discrete D then (true, true) else (false, false)
   246   | allows_lin_arith sg _ U = (of_lin_arith_sort sg U, false);
   247 
   248 fun decomp_typecheck thy (discrete, inj_consts) (T : typ, xxx) : decomp option =
   249   case T of
   250     Type ("fun", [U, _]) =>
   251       (case allows_lin_arith thy discrete U of
   252         (true, d) =>
   253           (case decomp0 thy inj_consts xxx of
   254             NONE                   => NONE
   255           | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d))
   256       | (false, _) =>
   257           NONE)
   258   | _ => NONE;
   259 
   260 fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
   261   | negate NONE                        = NONE;
   262 
   263 fun decomp_negation thy data
   264       ((Const (@{const_name Trueprop}, _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
   265       decomp_typecheck thy data (T, (rel, lhs, rhs))
   266   | decomp_negation thy data
   267       ((Const (@{const_name Trueprop}, _)) $ (Const (@{const_name Not}, _) $ (Const (rel, T) $ lhs $ rhs))) =
   268       negate (decomp_typecheck thy data (T, (rel, lhs, rhs)))
   269   | decomp_negation _ _ _ =
   270       NONE;
   271 
   272 fun decomp ctxt : term -> decomp option =
   273   let
   274     val thy = Proof_Context.theory_of ctxt
   275     val {discrete, inj_consts, ...} = get_arith_data ctxt
   276   in decomp_negation thy (discrete, inj_consts) end;
   277 
   278 fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T
   279   | domain_is_nat (_ $ (Const (@{const_name Not}, _) $ (Const (_, T) $ _ $ _))) = nT T
   280   | domain_is_nat _ = false;
   281 
   282 
   283 (* Abstraction of terms *)
   284 
   285 (*
   286   Abstract terms contain only arithmetic operators and relations.
   287 
   288   When constructing an abstract term for an arbitrary term, non-arithmetic sub-terms
   289   are replaced by fresh variables which are declared in the context. Constructing
   290   an abstract term from an arbitrary term follows the strategy of decomp.
   291 *)
   292 
   293 fun apply t u = t $ u
   294 
   295 fun with2 f c t u cx = f t cx ||>> f u |>> (fn (t, u) => c $ t $ u)
   296 
   297 fun abstract_atom (t as Free _) cx = (t, cx)
   298   | abstract_atom (t as Const _) cx = (t, cx)
   299   | abstract_atom t (cx as (terms, ctxt)) =
   300       (case AList.lookup Envir.aeconv terms t of
   301         SOME u => (u, cx)
   302       | NONE =>
   303           let
   304             val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
   305             val u = Free (n, fastype_of t)
   306           in (u, ((t, u) :: terms, ctxt')) end)
   307 
   308 fun abstract_num t cx = if can HOLogic.dest_number t then (t, cx) else abstract_atom t cx
   309 
   310 fun is_field_sort (_, ctxt) T = of_field_sort (Proof_Context.theory_of ctxt) (domain_type T)
   311 
   312 fun is_inj_const (_, ctxt) f =
   313   let val {inj_consts, ...} = get_arith_data ctxt
   314   in member (op =) inj_consts f end
   315 
   316 fun abstract_arith ((c as Const (@{const_name Groups.plus}, _)) $ u1 $ u2) cx =
   317       with2 abstract_arith c u1 u2 cx
   318   | abstract_arith (t as (c as Const (@{const_name Groups.minus}, T)) $ u1 $ u2) cx =
   319       if nT T then abstract_atom t cx else with2 abstract_arith c u1 u2 cx
   320   | abstract_arith (t as (c as Const (@{const_name Groups.uminus}, T)) $ u) cx =
   321       if nT T then abstract_atom t cx else abstract_arith u cx |>> apply c
   322   | abstract_arith ((c as Const (@{const_name Suc}, _)) $ u) cx = abstract_arith u cx |>> apply c
   323   | abstract_arith ((c as Const (@{const_name Groups.times}, _)) $ u1 $ u2) cx =
   324       with2 abstract_arith c u1 u2 cx
   325   | abstract_arith (t as (c as Const (@{const_name Rings.divide}, T)) $ u1 $ u2) cx =
   326       if is_field_sort cx T then with2 abstract_arith c u1 u2 cx else abstract_atom t cx
   327   | abstract_arith (t as (c as Const f) $ u) cx =
   328       if is_inj_const cx f then abstract_arith u cx |>> apply c else abstract_num t cx
   329   | abstract_arith t cx = abstract_num t cx
   330 
   331 fun is_lin_arith_rel @{const_name Orderings.less} = true
   332   | is_lin_arith_rel @{const_name Orderings.less_eq} = true
   333   | is_lin_arith_rel @{const_name HOL.eq} = true
   334   | is_lin_arith_rel _ = false
   335 
   336 fun is_lin_arith_type (_, ctxt) T =
   337   let val {discrete, ...} = get_arith_data ctxt
   338   in fst (allows_lin_arith (Proof_Context.theory_of ctxt) discrete T) end
   339 
   340 fun abstract_rel (t as (r as Const (rel, Type ("fun", [U, _]))) $ lhs $ rhs) cx =
   341       if is_lin_arith_rel rel andalso is_lin_arith_type cx U then with2 abstract_arith r lhs rhs cx
   342       else abstract_atom t cx
   343   | abstract_rel t cx = abstract_atom t cx
   344 
   345 fun abstract_neg ((c as Const (@{const_name Not}, _)) $ t) cx = abstract_rel t cx |>> apply c
   346   | abstract_neg t cx = abstract_rel t cx
   347 
   348 fun abstract ((c as Const (@{const_name Trueprop}, _)) $ t) cx = abstract_neg t cx |>> apply c
   349   | abstract t cx = abstract_atom t cx
   350 
   351 
   352 (*---------------------------------------------------------------------------*)
   353 (* the following code performs splitting of certain constants (e.g., min,    *)
   354 (* max) in a linear arithmetic problem; similar to what split_tac later does *)
   355 (* to the proof state                                                        *)
   356 (*---------------------------------------------------------------------------*)
   357 
   358 (* checks if splitting with 'thm' is implemented                             *)
   359 
   360 fun is_split_thm ctxt thm =
   361   (case Thm.concl_of thm of _ $ (_ $ (_ $ lhs) $ _) =>
   362     (* Trueprop $ ((op =) $ (?P $ lhs) $ rhs) *)
   363     (case head_of lhs of
   364       Const (a, _) =>
   365         member (op =)
   366          [@{const_name Orderings.max},
   367           @{const_name Orderings.min},
   368           @{const_name Groups.abs},
   369           @{const_name Groups.minus},
   370           "Int.nat" (*DYNAMIC BINDING!*),
   371           @{const_name Rings.modulo},
   372           @{const_name Rings.divide}] a
   373     | _ =>
   374       (if Context_Position.is_visible ctxt then
   375         warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
   376        else (); false))
   377   | _ =>
   378     (if Context_Position.is_visible ctxt then
   379       warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
   380      else (); false));
   381 
   382 (* substitute new for occurrences of old in a term, incrementing bound       *)
   383 (* variables as needed when substituting inside an abstraction               *)
   384 
   385 fun subst_term ([] : (term * term) list) (t : term) = t
   386   | subst_term pairs                     t          =
   387       (case AList.lookup Envir.aeconv pairs t of
   388         SOME new =>
   389           new
   390       | NONE     =>
   391           (case t of Abs (a, T, body) =>
   392             let val pairs' = map (apply2 (incr_boundvars 1)) pairs
   393             in  Abs (a, T, subst_term pairs' body)  end
   394           | t1 $ t2 => subst_term pairs t1 $ subst_term pairs t2
   395           | _ => t));
   396 
   397 (* approximates the effect of one application of split_tac (followed by NNF  *)
   398 (* normalization) on the subgoal represented by '(Ts, terms)'; returns a     *)
   399 (* list of new subgoals (each again represented by a typ list for bound      *)
   400 (* variables and a term list for premises), or NONE if split_tac would fail  *)
   401 (* on the subgoal                                                            *)
   402 
   403 (* FIXME: currently only the effect of certain split theorems is reproduced  *)
   404 (*        (which is why we need 'is_split_thm').  A more canonical           *)
   405 (*        implementation should analyze the right-hand side of the split     *)
   406 (*        theorem that can be applied, and modify the subgoal accordingly.   *)
   407 (*        Or even better, the splitter should be extended to provide         *)
   408 (*        splitting on terms as well as splitting on theorems (where the     *)
   409 (*        former can have a faster implementation as it does not need to be  *)
   410 (*        proof-producing).                                                  *)
   411 
   412 fun split_once_items ctxt (Ts : typ list, terms : term list) :
   413                      (typ list * term list) list option =
   414 let
   415   val thy = Proof_Context.theory_of ctxt
   416   (* takes a list  [t1, ..., tn]  to the term                                *)
   417   (*   tn' --> ... --> t1' --> False  ,                                      *)
   418   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   419   fun REPEAT_DETERM_etac_rev_mp tms =
   420     fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms)
   421       @{term False}
   422   val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
   423   val cmap        = Splitter.cmap_of_split_thms split_thms
   424   val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
   425   val splits      = Splitter.split_posns cmap thy Ts goal_tm
   426   val split_limit = Config.get ctxt split_limit
   427 in
   428   if length splits > split_limit then (
   429     tracing ("linarith_split_limit exceeded (current value is " ^
   430       string_of_int split_limit ^ ")");
   431     NONE
   432   ) else case splits of
   433     [] =>
   434     (* split_tac would fail: no possible split *)
   435     NONE
   436   | (_, _::_, _, _, _) :: _ =>
   437     (* disallow a split that involves non-locally bound variables (except    *)
   438     (* when bound by outermost meta-quantifiers)                             *)
   439     NONE
   440   | (_, [], _, split_type, split_term) :: _ =>
   441     (* ignore all but the first possible split                               *)
   442     (case strip_comb split_term of
   443     (* ?P (max ?i ?j) = ((?i <= ?j --> ?P ?j) & (~ ?i <= ?j --> ?P ?i)) *)
   444       (Const (@{const_name Orderings.max}, _), [t1, t2]) =>
   445       let
   446         val rev_terms     = rev terms
   447         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   448         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   449         val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   450                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   451         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   452         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   453         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms2 @ [not_false]
   454         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms1 @ [not_false]
   455       in
   456         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   457       end
   458     (* ?P (min ?i ?j) = ((?i <= ?j --> ?P ?i) & (~ ?i <= ?j --> ?P ?j)) *)
   459     | (Const (@{const_name Orderings.min}, _), [t1, t2]) =>
   460       let
   461         val rev_terms     = rev terms
   462         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   463         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   464         val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   465                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   466         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   467         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   468         val subgoal1      = (HOLogic.mk_Trueprop t1_leq_t2) :: terms1 @ [not_false]
   469         val subgoal2      = (HOLogic.mk_Trueprop not_t1_leq_t2) :: terms2 @ [not_false]
   470       in
   471         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   472       end
   473     (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
   474     | (Const (@{const_name Groups.abs}, _), [t1]) =>
   475       let
   476         val rev_terms   = rev terms
   477         val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   478         val terms2      = map (subst_term [(split_term, Const (@{const_name Groups.uminus},
   479                             split_type --> split_type) $ t1)]) rev_terms
   480         val zero        = Const (@{const_name Groups.zero}, split_type)
   481         val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
   482                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   483         val t1_lt_zero  = Const (@{const_name Orderings.less},
   484                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   485         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   486         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   487         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   488       in
   489         SOME [(Ts, subgoal1), (Ts, subgoal2)]
   490       end
   491     (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
   492     | (Const (@{const_name Groups.minus}, _), [t1, t2]) =>
   493       let
   494         (* "d" in the above theorem becomes a new bound variable after NNF   *)
   495         (* transformation, therefore some adjustment of indices is necessary *)
   496         val rev_terms       = rev terms
   497         val zero            = Const (@{const_name Groups.zero}, split_type)
   498         val d               = Bound 0
   499         val terms1          = map (subst_term [(split_term, zero)]) rev_terms
   500         val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
   501                                 (map (incr_boundvars 1) rev_terms)
   502         val t1'             = incr_boundvars 1 t1
   503         val t2'             = incr_boundvars 1 t2
   504         val t1_lt_t2        = Const (@{const_name Orderings.less},
   505                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   506         val t1_eq_t2_plus_d = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   507                                 (Const (@{const_name Groups.plus},
   508                                   split_type --> split_type --> split_type) $ t2' $ d)
   509         val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   510         val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
   511         val subgoal2        = (HOLogic.mk_Trueprop t1_eq_t2_plus_d) :: terms2 @ [not_false]
   512       in
   513         SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)]
   514       end
   515     (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *)
   516     | (Const ("Int.nat", _), (*DYNAMIC BINDING!*) [t1]) =>
   517       let
   518         val rev_terms   = rev terms
   519         val zero_int    = Const (@{const_name Groups.zero}, HOLogic.intT)
   520         val zero_nat    = Const (@{const_name Groups.zero}, HOLogic.natT)
   521         val n           = Bound 0
   522         val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
   523                             (map (incr_boundvars 1) rev_terms)
   524         val terms2      = map (subst_term [(split_term, zero_nat)]) rev_terms
   525         val t1'         = incr_boundvars 1 t1
   526         val t1_eq_nat_n = Const (@{const_name HOL.eq}, HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   527                             (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   528         val t1_lt_zero  = Const (@{const_name Orderings.less},
   529                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   530         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   531         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
   532         val subgoal2    = (HOLogic.mk_Trueprop t1_lt_zero) :: terms2 @ [not_false]
   533       in
   534         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
   535       end
   536     (* ?P ((?n::nat) mod (numeral ?k)) =
   537          ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) -->
   538            (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *)
   539     | (Const (@{const_name Rings.modulo}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   540       let
   541         val rev_terms               = rev terms
   542         val zero                    = Const (@{const_name Groups.zero}, split_type)
   543         val i                       = Bound 1
   544         val j                       = Bound 0
   545         val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
   546         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, j)])
   547                                         (map (incr_boundvars 2) rev_terms)
   548         val t1'                     = incr_boundvars 2 t1
   549         val t2'                     = incr_boundvars 2 t2
   550         val t2_eq_zero              = Const (@{const_name HOL.eq},
   551                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   552         val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
   553                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   554         val j_lt_t2                 = Const (@{const_name Orderings.less},
   555                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   556         val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   557                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   558                                          (Const (@{const_name Groups.times},
   559                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   560         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   561         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   562         val subgoal2                = (map HOLogic.mk_Trueprop
   563                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   564                                           @ terms2 @ [not_false]
   565       in
   566         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
   567       end
   568     (* ?P ((?n::nat) div (numeral ?k)) =
   569          ((numeral ?k = 0 --> ?P 0) & (~ (numeral ?k = 0) -->
   570            (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P i))) *)
   571     | (Const (@{const_name Rings.divide}, Type ("fun", [@{typ nat}, _])), [t1, t2]) =>
   572       let
   573         val rev_terms               = rev terms
   574         val zero                    = Const (@{const_name Groups.zero}, split_type)
   575         val i                       = Bound 1
   576         val j                       = Bound 0
   577         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
   578         val terms2                  = map (subst_term [(incr_boundvars 2 split_term, i)])
   579                                         (map (incr_boundvars 2) rev_terms)
   580         val t1'                     = incr_boundvars 2 t1
   581         val t2'                     = incr_boundvars 2 t2
   582         val t2_eq_zero              = Const (@{const_name HOL.eq},
   583                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   584         val t2_neq_zero             = HOLogic.mk_not (Const (@{const_name HOL.eq},
   585                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   586         val j_lt_t2                 = Const (@{const_name Orderings.less},
   587                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   588         val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   589                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   590                                          (Const (@{const_name Groups.times},
   591                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   592         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   593         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   594         val subgoal2                = (map HOLogic.mk_Trueprop
   595                                         [t2_neq_zero, j_lt_t2, t1_eq_t2_times_i_plus_j])
   596                                           @ terms2 @ [not_false]
   597       in
   598         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
   599       end
   600     (* ?P ((?n::int) mod (numeral ?k)) =
   601          ((numeral ?k = 0 --> ?P ?n) &
   602           (0 < numeral ?k -->
   603             (ALL i j.
   604               0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P j)) &
   605           (numeral ?k < 0 -->
   606             (ALL i j.
   607               numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *)
   608     | (Const (@{const_name Rings.modulo},
   609         Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
   610       let
   611         val rev_terms               = rev terms
   612         val zero                    = Const (@{const_name Groups.zero}, 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_3                = 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 (@{const_name HOL.eq},
   621                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   622         val zero_lt_t2              = Const (@{const_name Orderings.less},
   623                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
   624         val t2_lt_zero              = Const (@{const_name Orderings.less},
   625                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
   626         val zero_leq_j              = Const (@{const_name Orderings.less_eq},
   627                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
   628         val j_leq_zero              = Const (@{const_name Orderings.less_eq},
   629                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
   630         val j_lt_t2                 = Const (@{const_name Orderings.less},
   631                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   632         val t2_lt_j                 = Const (@{const_name Orderings.less},
   633                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   634         val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   635                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   636                                          (Const (@{const_name Groups.times},
   637                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   638         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   639         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   640         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
   641                                         @ hd terms2_3
   642                                         :: (if tl terms2_3 = [] then [not_false] else [])
   643                                         @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
   644                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   645         val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
   646                                         @ hd terms2_3
   647                                         :: (if tl terms2_3 = [] then [not_false] else [])
   648                                         @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
   649                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   650         val Ts'                     = split_type :: split_type :: Ts
   651       in
   652         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
   653       end
   654     (* ?P ((?n::int) div (numeral ?k)) =
   655          ((numeral ?k = 0 --> ?P 0) &
   656           (0 < numeral ?k -->
   657             (ALL i j.
   658               0 <= j & j < numeral ?k & ?n = numeral ?k * i + j --> ?P i)) &
   659           (numeral ?k < 0 -->
   660             (ALL i j.
   661               numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *)
   662     | (Const (@{const_name Rings.divide},
   663         Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) =>
   664       let
   665         val rev_terms               = rev terms
   666         val zero                    = Const (@{const_name Groups.zero}, split_type)
   667         val i                       = Bound 1
   668         val j                       = Bound 0
   669         val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
   670         val terms2_3                = map (subst_term [(incr_boundvars 2 split_term, i)])
   671                                         (map (incr_boundvars 2) rev_terms)
   672         val t1'                     = incr_boundvars 2 t1
   673         val t2'                     = incr_boundvars 2 t2
   674         val t2_eq_zero              = Const (@{const_name HOL.eq},
   675                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   676         val zero_lt_t2              = Const (@{const_name Orderings.less},
   677                                         split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
   678         val t2_lt_zero              = Const (@{const_name Orderings.less},
   679                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
   680         val zero_leq_j              = Const (@{const_name Orderings.less_eq},
   681                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
   682         val j_leq_zero              = Const (@{const_name Orderings.less_eq},
   683                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
   684         val j_lt_t2                 = Const (@{const_name Orderings.less},
   685                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   686         val t2_lt_j                 = Const (@{const_name Orderings.less},
   687                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
   688         val t1_eq_t2_times_i_plus_j = Const (@{const_name HOL.eq}, split_type --> split_type --> HOLogic.boolT) $ t1' $
   689                                        (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
   690                                          (Const (@{const_name Groups.times},
   691                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
   692         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ @{term False})
   693         val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
   694         val subgoal2                = (map HOLogic.mk_Trueprop [zero_lt_t2, zero_leq_j])
   695                                         @ hd terms2_3
   696                                         :: (if tl terms2_3 = [] then [not_false] else [])
   697                                         @ (map HOLogic.mk_Trueprop [j_lt_t2, t1_eq_t2_times_i_plus_j])
   698                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   699         val subgoal3                = (map HOLogic.mk_Trueprop [t2_lt_zero, t2_lt_j])
   700                                         @ hd terms2_3
   701                                         :: (if tl terms2_3 = [] then [not_false] else [])
   702                                         @ (map HOLogic.mk_Trueprop [j_leq_zero, t1_eq_t2_times_i_plus_j])
   703                                         @ (if tl terms2_3 = [] then [] else tl terms2_3 @ [not_false])
   704         val Ts'                     = split_type :: split_type :: Ts
   705       in
   706         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
   707       end
   708     (* this will only happen if a split theorem can be applied for which no  *)
   709     (* code exists above -- in which case either the split theorem should be *)
   710     (* implemented above, or 'is_split_thm' should be modified to filter it  *)
   711     (* out                                                                   *)
   712     | (t, ts) =>
   713       (if Context_Position.is_visible ctxt then
   714         warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
   715           " (with " ^ string_of_int (length ts) ^
   716           " argument(s)) not implemented; proof reconstruction is likely to fail")
   717        else (); NONE))
   718 end;  (* split_once_items *)
   719 
   720 (* remove terms that do not satisfy 'p'; change the order of the remaining   *)
   721 (* terms in the same way as filter_prems_tac does                            *)
   722 
   723 fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
   724   let
   725     fun filter_prems t (left, right) =
   726       if p t then (left, right @ [t]) else (left @ right, [])
   727     val (left, right) = fold filter_prems terms ([], [])
   728   in
   729     right @ left
   730   end;
   731 
   732 (* return true iff TRY (etac notE) THEN eq_assume_tac would succeed on a     *)
   733 (* subgoal that has 'terms' as premises                                      *)
   734 
   735 fun negated_term_occurs_positively (terms : term list) : bool =
   736   exists
   737     (fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
   738       member Envir.aeconv terms (Trueprop $ t)
   739       | _ => false)
   740     terms;
   741 
   742 fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list =
   743   let
   744     (* repeatedly split (including newly emerging subgoals) until no further   *)
   745     (* splitting is possible                                                   *)
   746     fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
   747       | split_loop (subgoal::subgoals) =
   748           (case split_once_items ctxt subgoal of
   749             SOME new_subgoals => split_loop (new_subgoals @ subgoals)
   750           | NONE => subgoal :: split_loop subgoals)
   751     fun is_relevant t  = is_some (decomp ctxt t)
   752     (* filter_prems_tac is_relevant: *)
   753     val relevant_terms = filter_prems_tac_items is_relevant terms
   754     (* split_tac, NNF normalization: *)
   755     val split_goals = split_loop [(Ts, relevant_terms)]
   756     (* necessary because split_once_tac may normalize terms: *)
   757     val beta_eta_norm = map (apsnd (map (Envir.eta_contract o Envir.beta_norm)))
   758       split_goals
   759     (* TRY (etac notE) THEN eq_assume_tac: *)
   760     val result = filter_out (negated_term_occurs_positively o snd) beta_eta_norm
   761   in
   762     result
   763   end;
   764 
   765 (* takes the i-th subgoal  [| A1; ...; An |] ==> B  to                       *)
   766 (* An --> ... --> A1 --> B,  performs splitting with the given 'split_thms'  *)
   767 (* (resulting in a different subgoal P), takes  P  to  ~P ==> False,         *)
   768 (* performs NNF-normalization of ~P, and eliminates conjunctions,            *)
   769 (* disjunctions and existential quantifiers from the premises, possibly (in  *)
   770 (* the case of disjunctions) resulting in several new subgoals, each of the  *)
   771 (* general form  [| Q1; ...; Qm |] ==> False.  Fails if more than            *)
   772 (* !split_limit splits are possible.                              *)
   773 
   774 local
   775   fun nnf_simpset ctxt =
   776     (empty_simpset ctxt
   777       |> Simplifier.set_mkeqTrue mk_eq_True
   778       |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   779     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
   780       @{thm de_Morgan_conj}, not_all, not_ex, not_not]
   781   fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt)
   782 in
   783 
   784 fun split_once_tac ctxt split_thms =
   785   let
   786     val thy = Proof_Context.theory_of ctxt
   787     val cond_split_tac = SUBGOAL (fn (subgoal, i) =>
   788       let
   789         val Ts = rev (map snd (Logic.strip_params subgoal))
   790         val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal)
   791         val cmap = Splitter.cmap_of_split_thms split_thms
   792         val splits = Splitter.split_posns cmap thy Ts concl
   793       in
   794         if null splits orelse length splits > Config.get ctxt split_limit then
   795           no_tac
   796         else if null (#2 (hd splits)) then
   797           split_tac ctxt split_thms i
   798         else
   799           (* disallow a split that involves non-locally bound variables      *)
   800           (* (except when bound by outermost meta-quantifiers)               *)
   801           no_tac
   802       end)
   803   in
   804     EVERY' [
   805       REPEAT_DETERM o eresolve_tac ctxt [rev_mp],
   806       cond_split_tac,
   807       resolve_tac ctxt @{thms ccontr},
   808       prem_nnf_tac ctxt,
   809       TRY o REPEAT_ALL_NEW
   810         (DETERM o (eresolve_tac ctxt [conjE, exE] ORELSE' eresolve_tac ctxt [disjE]))
   811     ]
   812   end;
   813 
   814 end;  (* local *)
   815 
   816 (* remove irrelevant premises, then split the i-th subgoal (and all new      *)
   817 (* subgoals) by using 'split_once_tac' repeatedly.  Beta-eta-normalize new   *)
   818 (* subgoals and finally attempt to solve them by finding an immediate        *)
   819 (* contradiction (i.e., a term and its negation) in their premises.          *)
   820 
   821 fun pre_tac ctxt i =
   822   let
   823     val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
   824     fun is_relevant t = is_some (decomp ctxt t)
   825   in
   826     DETERM (
   827       TRY (filter_prems_tac ctxt is_relevant i)
   828         THEN (
   829           (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms))
   830             THEN_ALL_NEW
   831               (CONVERSION Drule.beta_eta_conversion
   832                 THEN'
   833               (TRY o (eresolve_tac ctxt [notE] THEN' eq_assume_tac)))
   834         ) i
   835     )
   836   end;
   837 
   838 end;  (* LA_Data *)
   839 
   840 
   841 val pre_tac = LA_Data.pre_tac;
   842 
   843 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
   844 
   845 val add_inj_thms = Fast_Arith.add_inj_thms;
   846 val add_lessD = Fast_Arith.add_lessD;
   847 val add_simps = Fast_Arith.add_simps;
   848 val add_simprocs = Fast_Arith.add_simprocs;
   849 val set_number_of = Fast_Arith.set_number_of;
   850 
   851 val simple_tac = Fast_Arith.lin_arith_tac;
   852 
   853 (* reduce contradictory <= to False.
   854    Most of the work is done by the cancel tactics. *)
   855 
   856 val init_arith_data =
   857   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, number_of, ...} =>
   858    {add_mono_thms =
   859       map Thm.trim_context @{thms add_mono_thms_linordered_semiring add_mono_thms_linordered_field}
   860         @ add_mono_thms,
   861     mult_mono_thms =
   862       map Thm.trim_context
   863         (@{thms mult_strict_left_mono mult_left_mono} @
   864           [@{lemma "a = b ==> c * a = c * b" by (rule arg_cong)}]) @ mult_mono_thms,
   865     inj_thms = inj_thms,
   866     lessD = lessD,
   867     neqE = map Thm.trim_context @{thms linorder_neqE_nat linorder_neqE_linordered_idom} @ neqE,
   868     simpset =
   869       put_simpset HOL_basic_ss @{context} |> Simplifier.add_cong @{thm if_weak_cong} |> simpset_of,
   870     number_of = number_of});
   871 
   872 (* FIXME !?? *)
   873 fun add_arith_facts ctxt =
   874   Simplifier.add_prems (rev (Named_Theorems.get ctxt @{named_theorems arith})) ctxt;
   875 
   876 val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
   877 
   878 
   879 (* generic refutation procedure *)
   880 
   881 (* parameters:
   882 
   883    test: term -> bool
   884    tests if a term is at all relevant to the refutation proof;
   885    if not, then it can be discarded. Can improve performance,
   886    esp. if disjunctions can be discarded (no case distinction needed!).
   887 
   888    prep_tac: int -> tactic
   889    A preparation tactic to be applied to the goal once all relevant premises
   890    have been moved to the conclusion.
   891 
   892    ref_tac: int -> tactic
   893    the actual refutation tactic. Should be able to deal with goals
   894    [| A1; ...; An |] ==> False
   895    where the Ai are atomic, i.e. no top-level &, | or EX
   896 *)
   897 
   898 local
   899   fun nnf_simpset ctxt =
   900     (empty_simpset ctxt
   901       |> Simplifier.set_mkeqTrue mk_eq_True
   902       |> Simplifier.set_mksimps (mksimps mksimps_pairs))
   903     addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
   904       @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
   905   fun prem_nnf_tac ctxt = full_simp_tac (nnf_simpset ctxt);
   906 in
   907 
   908 fun refute_tac ctxt test prep_tac ref_tac =
   909   let val refute_prems_tac =
   910         REPEAT_DETERM
   911               (eresolve_tac ctxt [@{thm conjE}, @{thm exE}] 1 ORELSE
   912                filter_prems_tac ctxt test 1 ORELSE
   913                eresolve_tac ctxt @{thms disjE} 1) THEN
   914         (DETERM (eresolve_tac ctxt @{thms notE} 1 THEN eq_assume_tac 1) ORELSE
   915          ref_tac 1);
   916   in EVERY'[TRY o filter_prems_tac ctxt test,
   917             REPEAT_DETERM o eresolve_tac ctxt @{thms rev_mp}, prep_tac,
   918               resolve_tac ctxt @{thms ccontr}, prem_nnf_tac ctxt,
   919             SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
   920   end;
   921 
   922 end;
   923 
   924 
   925 (* arith proof method *)
   926 
   927 local
   928 
   929 fun raw_tac ctxt =
   930   (* FIXME: K true should be replaced by a sensible test (perhaps "is_some o
   931      decomp sg"? -- but note that the test is applied to terms already before
   932      they are split/normalized) to speed things up in case there are lots of
   933      irrelevant terms involved; elimination of min/max can be optimized:
   934      (max m n + k <= r) = (m+k <= r & n+k <= r)
   935      (l <= min m n + k) = (l <= m+k & l <= n+k)
   936   *)
   937   refute_tac ctxt (K true)
   938     (* Splitting is also done inside simple_tac, but not completely --    *)
   939     (* split_tac may use split theorems that have not been implemented in *)
   940     (* simple_tac (cf. pre_decomp and split_once_items above), and        *)
   941     (* split_limit may trigger.                                           *)
   942     (* Therefore splitting outside of simple_tac may allow us to prove    *)
   943     (* some goals that simple_tac alone would fail on.                    *)
   944     (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
   945     (Fast_Arith.lin_arith_tac ctxt);
   946 
   947 in
   948 
   949 fun tac ctxt =
   950   FIRST' [simple_tac ctxt,
   951     Object_Logic.full_atomize_tac ctxt THEN'
   952     (REPEAT_DETERM o resolve_tac ctxt [impI]) THEN' raw_tac ctxt];
   953 
   954 end;
   955 
   956 
   957 (* context setup *)
   958 
   959 val global_setup =
   960   map_theory_simpset (fn ctxt => ctxt
   961     addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))) #>
   962   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
   963     "declaration of split rules for arithmetic procedure" #>
   964   Method.setup @{binding linarith}
   965     (Scan.succeed (fn ctxt =>
   966       METHOD (fn facts =>
   967         HEADGOAL
   968           (Method.insert_tac ctxt
   969             (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
   970           THEN' tac ctxt)))) "linear arithmetic" #>
   971   Arith_Data.add_tactic "linear arithmetic" tac;
   972 
   973 val setup =
   974   init_arith_data
   975   #> add_discrete_type @{type_name nat}
   976   #> add_lessD @{thm Suc_leI}
   977   #> add_simps (@{thms simp_thms} @ @{thms ring_distribs} @ [@{thm if_True}, @{thm if_False},
   978       @{thm minus_diff_eq},
   979       @{thm add_0_left}, @{thm add_0_right}, @{thm order_less_irrefl},
   980       @{thm zero_neq_one}, @{thm zero_less_one}, @{thm zero_le_one},
   981       @{thm zero_neq_one} RS not_sym, @{thm not_one_le_zero}, @{thm not_one_less_zero}])
   982   #> add_simps [@{thm add_Suc}, @{thm add_Suc_right}, @{thm nat.inject},
   983       @{thm Suc_le_mono}, @{thm Suc_less_eq}, @{thm Zero_not_Suc},
   984       @{thm Suc_not_Zero}, @{thm le_0_eq}, @{thm One_nat_def}]
   985   #> add_simprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
   986       @{simproc group_cancel_eq}, @{simproc group_cancel_le},
   987       @{simproc group_cancel_less}]
   988      (*abel_cancel helps it work in abstract algebraic domains*)
   989   #> add_simprocs [@{simproc nateq_cancel_sums},@{simproc natless_cancel_sums},
   990       @{simproc natle_cancel_sums}];
   991 
   992 end;