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