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