--- a/src/HOL/Tools/nat_arith.ML Fri Jul 27 17:57:31 2012 +0200
+++ b/src/HOL/Tools/nat_arith.ML Fri Jul 27 17:59:18 2012 +0200
@@ -1,17 +1,19 @@
(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
+ Author: Brian Huffman
Basic arithmetic for natural numbers.
*)
signature NAT_ARITH =
sig
+ val cancel_diff_conv: conv
+ val cancel_eq_conv: conv
+ val cancel_le_conv: conv
+ val cancel_less_conv: conv
+ (* legacy functions: *)
val mk_sum: term list -> term
val mk_norm_sum: term list -> term
val dest_sum: term -> term list
- val nateq_cancel_sums: simpset -> cterm -> thm option
- val natless_cancel_sums: simpset -> cterm -> thm option
- val natle_cancel_sums: simpset -> cterm -> thm option
- val natdiff_cancel_sums: simpset -> cterm -> thm option
end;
structure Nat_Arith: NAT_ARITH =
@@ -42,55 +44,58 @@
SOME (t, u) => dest_sum t @ dest_sum u
| NONE => [tm]));
+val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
+ by (simp only: add_ac)}
+val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
+ by (simp only: add_ac)}
+val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
+ by (simp only: add_Suc_right)}
+val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
+ by (simp only: add_0_right)}
-(** cancel common summands **)
+val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
-structure CommonCancelSums =
-struct
- val mk_sum = mk_norm_sum;
- val dest_sum = dest_sum;
- val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
- val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
- @{thm Nat.add_0}, @{thm Nat.add_0_right}];
- val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
- fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
-end;
+fun move_to_front path = Conv.every_conv
+ [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
+ Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
-structure EqCancelSums = CancelSumsFun
-(struct
- open CommonCancelSums;
- val mk_bal = HOLogic.mk_eq;
- val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
- val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
-end);
+fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
+ add_atoms (add1::path) x #> add_atoms (add2::path) y
+ | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
+ add_atoms (suc1::path) x
+ | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
+ | add_atoms path x = cons (x, path)
+
+fun atoms t = add_atoms [] t []
+
+exception Cancel
-structure LessCancelSums = CancelSumsFun
-(struct
- open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
- val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
-end);
+fun find_common ord xs ys =
+ let
+ fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
+ (case ord (x, y) of
+ EQUAL => (px, py)
+ | LESS => find xs' ys
+ | GREATER => find xs ys')
+ | find _ _ = raise Cancel
+ fun ord' ((x, _), (y, _)) = ord (x, y)
+ in
+ find (sort ord' xs) (sort ord' ys)
+ end
-structure LeCancelSums = CancelSumsFun
-(struct
- open CommonCancelSums;
- val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
- val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
- val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
-end);
+fun cancel_conv rule ct =
+ let
+ val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
+ val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
+ val lconv = move_to_front lpath
+ val rconv = move_to_front rpath
+ val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
+ val conv = conv1 then_conv Conv.rewr_conv rule
+ in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
-structure DiffCancelSums = CancelSumsFun
-(struct
- open CommonCancelSums;
- val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
- val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
- val cancel_rule = mk_meta_eq @{thm diff_cancel};
-end);
-
-fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
-fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
-fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
-fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
+val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
+val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
+val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
+val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
end;