src/HOL/Tools/arith_data.ML
author haftmann
Thu, 12 Mar 2009 18:01:26 +0100
changeset 30496 7cdcc9dd95cb
parent 29302 eb782d1dc07c
child 30518 07b45c1aa788
permissions -rw-r--r--
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement

(*  Title:      HOL/arith_data.ML
    Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow

Common arithmetic proof auxiliary.
*)

signature ARITH_DATA =
sig
  val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
  val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
  val simp_all_tac: thm list -> simpset -> tactic
  val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
    -> simproc
end;

structure Arith_Data: ARITH_DATA =
struct

fun prove_conv_nohyps tacs ctxt (t, u) =
  if t aconv u then NONE
  else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
  in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;

fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;

fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
  mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
      (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    (K (EVERY [expand_tac, norm_tac ss]))));

fun simp_all_tac rules =
  let val ss0 = HOL_ss addsimps rules
  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;

fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
  Simplifier.simproc (the_context ()) name pats proc;

end;