(* Title: HOL/Tools/arith_data.ML Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
Common arithmetic proof auxiliary and legacy.
*)
signature ARITH_DATA = sig val arith_tac: Proof.context -> int -> tactic val add_tactic: string -> (Proof.context -> int -> tactic) -> theory -> theory
val mk_number: typ -> int -> term val mk_sum: typ -> term list -> term val long_mk_sum: typ -> term list -> term val dest_sum: term -> term list
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 -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm val simp_all_tac: thm list -> Proof.context -> tactic val simplify_meta_eq: thm list -> Proof.context -> thm -> thm end;
structure Arith_Data: ARITH_DATA = struct
(* slot for plugging in tactics *)
structure Arith_Tactics = Theory_Data
( type T = (serial * (string * (Proof.context -> int -> tactic))) list; val empty = []; fun merge data : T = AList.merge (op =) (K true) data;
);
fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
fun arith_tac ctxt = let val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt); fun invoke (_, (_, tac)) k st = tac ctxt k st; in FIRST' (map invoke (rev tactics)) end;
fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
| mk_number T n = HOLogic.mk_number T n;
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) fun mk_sum T [] = mk_number T 0
| mk_sum T [t, u] = \<^Const>\<open>plus T for t u\<close>
| mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>mk_sum T ts\<close>\<close>;
(*this version ALWAYS includes a trailing zero*) fun long_mk_sum T [] = mk_number T 0
| long_mk_sum T (t :: ts) = \<^Const>\<open>plus T for t \<open>long_mk_sum T ts\<close>\<close>;
(*decompose additions AND subtractions as a sum*) fun dest_summing pos \<^Const_>\<open>plus _ for t u\<close> ts = dest_summing pos t (dest_summing pos u ts)
| dest_summing pos \<^Const_>\<open>minus _ for t u\<close> ts = dest_summing pos t (dest_summing (not pos) u ts)
| dest_summing pos t ts = (if pos then t else \<^Const>\<open>uminus \<open>fastype_of t\<close> for t\<close>) :: ts;
fun dest_sum t = dest_summing true t [];
(* various auxiliary and legacy *)
fun prove_conv_nohyps tacs ctxt (t, u) = if t aconv u then NONE elseletval eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
