src/HOL/Tools/arith_data.ML
author wenzelm
Thu Jul 02 17:34:14 2009 +0200 (2009-07-02)
changeset 31902 862ae16a799d
parent 30878 309bfab064e9
child 32155 e2bf2f73b0c8
permissions -rw-r--r--
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
haftmann@30878
     1
(*  Title:      HOL/Tools/arith_data.ML
wenzelm@24095
     2
    Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
wenzelm@9436
     3
haftmann@30496
     4
Common arithmetic proof auxiliary.
wenzelm@9436
     5
*)
wenzelm@9436
     6
haftmann@26101
     7
signature ARITH_DATA =
haftmann@26101
     8
sig
haftmann@30686
     9
  val arith_tac: Proof.context -> int -> tactic
haftmann@30686
    10
  val verbose_arith_tac: Proof.context -> int -> tactic
haftmann@30686
    11
  val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
haftmann@30686
    12
  val get_arith_facts: Proof.context -> thm list
haftmann@30686
    13
haftmann@30496
    14
  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
haftmann@30496
    15
  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
haftmann@30496
    16
  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
wenzelm@29302
    17
  val simp_all_tac: thm list -> simpset -> tactic
haftmann@30518
    18
  val simplify_meta_eq: thm list -> simpset -> thm -> thm
haftmann@30518
    19
  val trans_tac: thm option -> tactic
haftmann@30496
    20
  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
haftmann@30496
    21
    -> simproc
haftmann@30686
    22
haftmann@30686
    23
  val setup: theory -> theory
haftmann@26101
    24
end;
wenzelm@9436
    25
haftmann@30496
    26
structure Arith_Data: ARITH_DATA =
wenzelm@9436
    27
struct
wenzelm@9436
    28
haftmann@30878
    29
(* slots for plugging in arithmetic facts and tactics *)
haftmann@30686
    30
wenzelm@31902
    31
structure Arith_Facts = Named_Thms
wenzelm@31902
    32
(
haftmann@30686
    33
  val name = "arith"
haftmann@30686
    34
  val description = "arith facts - only ground formulas"
haftmann@30686
    35
);
haftmann@30686
    36
haftmann@30686
    37
val get_arith_facts = Arith_Facts.get;
haftmann@30686
    38
haftmann@30686
    39
structure Arith_Tactics = TheoryDataFun
haftmann@30686
    40
(
haftmann@30686
    41
  type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
haftmann@30686
    42
  val empty = [];
haftmann@30686
    43
  val copy = I;
haftmann@30686
    44
  val extend = I;
haftmann@30686
    45
  fun merge _ = AList.merge (op =) (K true);
haftmann@30686
    46
);
haftmann@30686
    47
haftmann@30686
    48
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
haftmann@30686
    49
haftmann@30686
    50
fun gen_arith_tac verbose ctxt =
haftmann@30686
    51
  let
haftmann@30686
    52
    val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
haftmann@30686
    53
    fun invoke (_, (name, tac)) k st = (if verbose
haftmann@30686
    54
      then warning ("Trying " ^ name ^ "...") else ();
haftmann@30686
    55
      tac verbose ctxt k st);
haftmann@30686
    56
  in FIRST' (map invoke (rev tactics)) end;
haftmann@30686
    57
haftmann@30686
    58
val arith_tac = gen_arith_tac false;
haftmann@30686
    59
val verbose_arith_tac = gen_arith_tac true;
haftmann@30686
    60
wenzelm@30722
    61
val setup =
wenzelm@30722
    62
  Arith_Facts.setup #>
wenzelm@30722
    63
  Method.setup @{binding arith}
wenzelm@30722
    64
    (Args.bang_facts >> (fn prems => fn ctxt =>
wenzelm@30722
    65
      METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
wenzelm@30722
    66
        THEN' verbose_arith_tac ctxt))))
wenzelm@30722
    67
    "various arithmetic decision procedures";
haftmann@30686
    68
haftmann@30686
    69
haftmann@30686
    70
(* various auxiliary and legacy *)
haftmann@30686
    71
haftmann@30496
    72
fun prove_conv_nohyps tacs ctxt (t, u) =
haftmann@30496
    73
  if t aconv u then NONE
haftmann@30496
    74
  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
haftmann@30496
    75
  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
haftmann@26101
    76
haftmann@30496
    77
fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
haftmann@26101
    78
haftmann@30496
    79
fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
haftmann@26101
    80
  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
haftmann@26101
    81
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
haftmann@26101
    82
    (K (EVERY [expand_tac, norm_tac ss]))));
haftmann@26101
    83
haftmann@26101
    84
fun simp_all_tac rules =
haftmann@26101
    85
  let val ss0 = HOL_ss addsimps rules
haftmann@26101
    86
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
haftmann@26101
    87
haftmann@30518
    88
fun simplify_meta_eq rules =
haftmann@30518
    89
  let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
haftmann@30518
    90
  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
haftmann@30518
    91
haftmann@30518
    92
fun trans_tac NONE  = all_tac
haftmann@30518
    93
  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
haftmann@30518
    94
haftmann@30496
    95
fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
haftmann@30496
    96
  Simplifier.simproc (the_context ()) name pats proc;
wenzelm@9436
    97
wenzelm@24095
    98
end;