src/HOL/Tools/arith_data.ML
 author wenzelm Sun, 01 Mar 2009 23:36:12 +0100 changeset 30190 479806475f3c parent 29302 eb782d1dc07c child 30496 7cdcc9dd95cb permissions -rw-r--r--
use long names for old-style fold combinators;
```
(*  Title:      HOL/arith_data.ML
Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow

Basic arithmetic proof tools.
*)

signature ARITH_DATA =
sig
val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val simp_all_tac: thm list -> simpset -> tactic

val mk_sum: term list -> term
val mk_norm_sum: term list -> term
val dest_sum: term -> term list

val nat_cancel_sums: simproc list
val setup: Context.generic -> Context.generic
end;

structure ArithData: ARITH_DATA =
struct

(** generic proof tools **)

(* prove conversions *)

fun prove_conv 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]))));

(* rewriting *)

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

(** abstract syntax of structure nat: 0, Suc, + **)

local

val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;

in

fun mk_sum [] = HOLogic.zero
| mk_sum [t] = t
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);

(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
fun mk_norm_sum ts =
let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
end;

fun dest_sum tm =
if HOLogic.is_zero tm then []
else
(case try HOLogic.dest_Suc tm of
SOME t => HOLogic.Suc_zero :: dest_sum t
| NONE =>
(case try dest_plus tm of
SOME (t, u) => dest_sum t @ dest_sum u
| NONE => [tm]));

end;

(** cancel common summands **)

structure Sum =
struct
val mk_sum = mk_norm_sum;
val dest_sum = dest_sum;
val prove_conv = prove_conv;
val norm_tac2 = simp_all_tac @{thms add_ac};
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
end;

fun gen_uncancel_tac rule ct =
rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;

(* nat eq *)

structure EqCancelSums = CancelSumsFun
(struct
open Sum;
val mk_bal = HOLogic.mk_eq;
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
end);

(* nat less *)

structure LessCancelSums = CancelSumsFun
(struct
open Sum;
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
end);

(* nat le *)

structure LeCancelSums = CancelSumsFun
(struct
open Sum;
val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
end);

(* nat diff *)

structure DiffCancelSums = CancelSumsFun
(struct
open Sum;
val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
end);

(* prepare nat_cancel simprocs *)

[Simplifier.simproc (the_context ()) "nateq_cancel_sums"
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
(K EqCancelSums.proc),
Simplifier.simproc (the_context ()) "natless_cancel_sums"
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
(K LessCancelSums.proc),
Simplifier.simproc (the_context ()) "natle_cancel_sums"
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
(K LeCancelSums.proc)];