src/HOL/Tools/arith_data.ML
author wenzelm
Sat, 16 Aug 2014 14:32:26 +0200
changeset 57952 1a9a6dfc255f
parent 51717 9e7d1c139569
child 57955 f28337c2c0a8
permissions -rw-r--r--
updated to named_theorems;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30878
309bfab064e9 tuned comment
haftmann
parents: 30722
diff changeset
     1
(*  Title:      HOL/Tools/arith_data.ML
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
     2
    Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     3
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
     4
Common arithmetic proof auxiliary and legacy.
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     5
*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     6
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
     7
signature ARITH_DATA =
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
     8
sig
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
     9
  val arith_tac: Proof.context -> int -> tactic
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    10
  val verbose_arith_tac: Proof.context -> int -> tactic
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    11
  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    12
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    13
  val mk_number: typ -> int -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    14
  val mk_sum: typ -> term list -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    15
  val long_mk_sum: typ -> term list -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    16
  val dest_sum: term -> term list
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    17
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    18
  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    19
  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
    20
  val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
    21
  val simp_all_tac: thm list -> Proof.context -> tactic
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
    22
  val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    23
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    24
  val setup: theory -> theory
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    25
end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    26
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    27
structure Arith_Data: ARITH_DATA =
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    28
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    29
57952
1a9a6dfc255f updated to named_theorems;
wenzelm
parents: 51717
diff changeset
    30
(* slot for plugging in tactics *)
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    31
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33359
diff changeset
    32
structure Arith_Tactics = Theory_Data
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    33
(
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    34
  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    35
  val empty = [];
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    36
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33359
diff changeset
    37
  fun merge data : T = AList.merge (op =) (K true) data;
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    38
);
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    39
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    40
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    41
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    42
fun gen_arith_tac verbose ctxt =
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    43
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41539
diff changeset
    44
    val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt);
49387
167708456269 dropped some unused identifiers
haftmann
parents: 48372
diff changeset
    45
    fun invoke (_, (_, tac)) k st = tac verbose ctxt k st;
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    46
  in FIRST' (map invoke (rev tactics)) end;
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    47
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    48
val arith_tac = gen_arith_tac false;
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    49
val verbose_arith_tac = gen_arith_tac true;
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    50
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30686
diff changeset
    51
val setup =
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30686
diff changeset
    52
  Method.setup @{binding arith}
33554
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33522
diff changeset
    53
    (Scan.succeed (fn ctxt =>
57952
1a9a6dfc255f updated to named_theorems;
wenzelm
parents: 51717
diff changeset
    54
      METHOD (fn facts =>
1a9a6dfc255f updated to named_theorems;
wenzelm
parents: 51717
diff changeset
    55
        HEADGOAL
1a9a6dfc255f updated to named_theorems;
wenzelm
parents: 51717
diff changeset
    56
        (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
1a9a6dfc255f updated to named_theorems;
wenzelm
parents: 51717
diff changeset
    57
          THEN' verbose_arith_tac ctxt))))
30722
623d4831c8cf simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents: 30686
diff changeset
    58
    "various arithmetic decision procedures";
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    59
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    60
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    61
(* some specialized syntactic operations *)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    62
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45620
diff changeset
    63
fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 45620
diff changeset
    64
  | mk_number T n = HOLogic.mk_number T n;
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    65
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    66
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    67
50107
289181e3e524 tuned signature;
wenzelm
parents: 49387
diff changeset
    68
fun mk_minus t =
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    69
  let val T = Term.fastype_of t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    70
  in Const (@{const_name Groups.uminus}, T --> T) $ t end;
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    71
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    72
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
44945
haftmann
parents: 42361
diff changeset
    73
fun mk_sum T [] = mk_number T 0
haftmann
parents: 42361
diff changeset
    74
  | mk_sum T [t, u] = mk_plus (t, u)
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    75
  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    76
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    77
(*this version ALWAYS includes a trailing zero*)
44945
haftmann
parents: 42361
diff changeset
    78
fun long_mk_sum T [] = mk_number T 0
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    79
  | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    80
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    81
(*decompose additions AND subtractions as a sum*)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    82
fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
44945
haftmann
parents: 42361
diff changeset
    83
      dest_summing (pos, t, dest_summing (pos, u, ts))
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    84
  | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) =
44945
haftmann
parents: 42361
diff changeset
    85
      dest_summing (pos, t, dest_summing (not pos, u, ts))
haftmann
parents: 42361
diff changeset
    86
  | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts;
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    87
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    88
fun dest_sum t = dest_summing (true, t, []);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    89
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    90
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    91
(* various auxiliary and legacy *)
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30518
diff changeset
    92
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    93
fun prove_conv_nohyps tacs ctxt (t, u) =
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    94
  if t aconv u then NONE
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    95
  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    96
  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    97
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    98
fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    99
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   100
fun prove_conv2 expand_tac norm_tac ctxt tu = (* FIXME avoid Drule.export_without_context *)
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   101
  mk_meta_eq (Drule.export_without_context (Goal.prove ctxt [] []
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   102
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   103
    (K (EVERY [expand_tac, norm_tac ctxt]))));
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   104
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   105
fun simp_all_tac rules ctxt =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   106
  ALLGOALS (safe_simp_tac (put_simpset HOL_ss ctxt addsimps rules));
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   107
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   108
fun simplify_meta_eq rules ctxt =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   109
  simplify (put_simpset HOL_basic_ss ctxt addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2})
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 50107
diff changeset
   110
    o mk_meta_eq;
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   111
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   112
end;