src/HOL/Tools/arith_data.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 35761 c4a698ee83b4
child 38715 6513ea67d95d
permissions -rw-r--r--
tuned titles
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
  val get_arith_facts: Proof.context -> thm 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
    13
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    14
  val mk_number: typ -> int -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    15
  val mk_sum: typ -> term list -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    16
  val long_mk_sum: typ -> term list -> term
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    17
  val dest_sum: term -> term list
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    18
30496
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_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
    20
  val prove_conv: tactic list -> Proof.context -> thm list -> 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
    21
  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
29302
eb782d1dc07c normalized some ML type/val aliases;
wenzelm
parents: 28952
diff changeset
    22
  val simp_all_tac: thm list -> simpset -> tactic
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
    23
  val simplify_meta_eq: thm list -> simpset -> thm -> thm
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
    24
  val trans_tac: thm option -> tactic
32155
e2bf2f73b0c8 more @{theory} antiquotations;
wenzelm
parents: 31902
diff changeset
    25
  val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    26
    -> simproc
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
    27
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
    28
  val setup: theory -> theory
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
    29
end;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    30
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
    31
structure Arith_Data: ARITH_DATA =
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    32
struct
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    33
30878
309bfab064e9 tuned comment
haftmann
parents: 30722
diff changeset
    34
(* slots for plugging in arithmetic facts and 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
    35
31902
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30878
diff changeset
    36
structure Arith_Facts = Named_Thms
862ae16a799d renamed NamedThmsFun to Named_Thms;
wenzelm
parents: 30878
diff changeset
    37
(
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
  val name = "arith"
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
  val description = "arith facts - only ground formulas"
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
);
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
val get_arith_facts = Arith_Facts.get;
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
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33359
diff changeset
    44
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
    45
(
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
  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
    47
  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
    48
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33359
diff changeset
    49
  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
    50
);
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
    51
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
    52
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
    53
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
    54
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
    55
  let
35761
c4a698ee83b4 reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents: 35636
diff changeset
    56
    val tactics = Arith_Tactics.get (ProofContext.theory_of ctxt);
c4a698ee83b4 reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents: 35636
diff changeset
    57
    fun invoke (_, (name, tac)) k st =
c4a698ee83b4 reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
wenzelm
parents: 35636
diff changeset
    58
     (if verbose then warning ("Trying " ^ name ^ "...") else ();
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
      tac verbose ctxt k st);
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
  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
    61
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
    62
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
    63
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
    64
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
    65
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
    66
  Arith_Facts.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
    67
  Method.setup @{binding arith}
33554
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33522
diff changeset
    68
    (Scan.succeed (fn ctxt =>
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33522
diff changeset
    69
      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
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
    70
        THEN' verbose_arith_tac ctxt))))
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
    71
    "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
    72
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
    73
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    74
(* some specialized syntactic operations *)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    75
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    76
fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    77
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    78
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    79
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    80
fun mk_minus t = 
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    81
  let val T = Term.fastype_of t
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    82
  in Const (@{const_name Groups.uminus}, T --> T) $ t end;
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    83
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    84
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    85
fun mk_sum T []        = mk_number T 0
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    86
  | mk_sum T [t,u]     = mk_plus (t, u)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    87
  | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    88
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    89
(*this version ALWAYS includes a trailing zero*)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    90
fun long_mk_sum T []        = mk_number T 0
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    91
  | 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
    92
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    93
(*decompose additions AND subtractions as a sum*)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35021
diff changeset
    94
fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    95
        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
    96
  | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) =
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    97
        dest_summing (pos, t, dest_summing (not pos, u, ts))
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    98
  | dest_summing (pos, t, ts) =
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    99
        if pos then t::ts else mk_minus t :: ts;
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
   100
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
   101
fun dest_sum t = dest_summing (true, t, []);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
   102
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
   103
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
   104
(* 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
   105
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
   106
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
   107
  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
   108
  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
   109
  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   110
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29302
diff changeset
   111
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
   112
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34974
diff changeset
   113
fun prove_conv2 expand_tac norm_tac ss tu = (* FIXME avoid Drule.export_without_context *)
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34974
diff changeset
   114
  mk_meta_eq (Drule.export_without_context (Goal.prove (Simplifier.the_context ss) [] []
26101
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   115
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   116
    (K (EVERY [expand_tac, norm_tac ss]))));
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   117
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   118
fun simp_all_tac rules =
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   119
  let val ss0 = HOL_ss addsimps rules
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   120
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
a657683e902a tuned structures in arith_data.ML
haftmann
parents: 25484
diff changeset
   121
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   122
fun simplify_meta_eq rules =
35410
1ea89d2a1bd4 more antiquotations;
wenzelm
parents: 35267
diff changeset
   123
  let val ss0 = HOL_basic_ss addeqcongs [@{thm eq_cong2}] addsimps rules
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   124
  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   125
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   126
fun trans_tac NONE  = all_tac
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   127
  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   128
32155
e2bf2f73b0c8 more @{theory} antiquotations;
wenzelm
parents: 31902
diff changeset
   129
fun prep_simproc thy (name, pats, proc) =
e2bf2f73b0c8 more @{theory} antiquotations;
wenzelm
parents: 31902
diff changeset
   130
  Simplifier.simproc thy name pats proc;
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
   131
24095
785c3cd7fcb5 moved lin_arith stuff to Tools/lin_arith.ML;
wenzelm
parents: 24076
diff changeset
   132
end;