src/HOL/Tools/nat_arith.ML
changeset 48560 e0875d956a6b
parent 48559 686cc7c47589
child 48561 12aa0cb2b447
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:57:31 2012 +0200
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 27 17:59:18 2012 +0200
     1.3 @@ -1,17 +1,19 @@
     1.4  (* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     1.5 +   Author: Brian Huffman
     1.6  
     1.7  Basic arithmetic for natural numbers.
     1.8  *)
     1.9  
    1.10  signature NAT_ARITH =
    1.11  sig
    1.12 +  val cancel_diff_conv: conv
    1.13 +  val cancel_eq_conv: conv
    1.14 +  val cancel_le_conv: conv
    1.15 +  val cancel_less_conv: conv
    1.16 +  (* legacy functions: *)
    1.17    val mk_sum: term list -> term
    1.18    val mk_norm_sum: term list -> term
    1.19    val dest_sum: term -> term list
    1.20 -  val nateq_cancel_sums: simpset -> cterm -> thm option
    1.21 -  val natless_cancel_sums: simpset -> cterm -> thm option
    1.22 -  val natle_cancel_sums: simpset -> cterm -> thm option
    1.23 -  val natdiff_cancel_sums: simpset -> cterm -> thm option
    1.24  end;
    1.25  
    1.26  structure Nat_Arith: NAT_ARITH =
    1.27 @@ -42,55 +44,58 @@
    1.28            SOME (t, u) => dest_sum t @ dest_sum u
    1.29          | NONE => [tm]));
    1.30  
    1.31 +val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    1.32 +      by (simp only: add_ac)}
    1.33 +val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
    1.34 +      by (simp only: add_ac)}
    1.35 +val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
    1.36 +      by (simp only: add_Suc_right)}
    1.37 +val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    1.38 +      by (simp only: add_0_right)}
    1.39  
    1.40 -(** cancel common summands **)
    1.41 +val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
    1.42  
    1.43 -structure CommonCancelSums =
    1.44 -struct
    1.45 -  val mk_sum = mk_norm_sum;
    1.46 -  val dest_sum = dest_sum;
    1.47 -  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    1.48 -  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    1.49 -    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
    1.50 -  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    1.51 -  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    1.52 -end;
    1.53 +fun move_to_front path = Conv.every_conv
    1.54 +    [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    1.55 +     Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
    1.56  
    1.57 -structure EqCancelSums = CancelSumsFun
    1.58 -(struct
    1.59 -  open CommonCancelSums;
    1.60 -  val mk_bal = HOLogic.mk_eq;
    1.61 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    1.62 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
    1.63 -end);
    1.64 +fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    1.65 +      add_atoms (add1::path) x #> add_atoms (add2::path) y
    1.66 +  | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
    1.67 +      add_atoms (suc1::path) x
    1.68 +  | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
    1.69 +  | add_atoms path x = cons (x, path)
    1.70 +
    1.71 +fun atoms t = add_atoms [] t []
    1.72 +
    1.73 +exception Cancel
    1.74  
    1.75 -structure LessCancelSums = CancelSumsFun
    1.76 -(struct
    1.77 -  open CommonCancelSums;
    1.78 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    1.79 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    1.80 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
    1.81 -end);
    1.82 +fun find_common ord xs ys =
    1.83 +  let
    1.84 +    fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    1.85 +        (case ord (x, y) of
    1.86 +          EQUAL => (px, py)
    1.87 +        | LESS => find xs' ys
    1.88 +        | GREATER => find xs ys')
    1.89 +      | find _ _ = raise Cancel
    1.90 +    fun ord' ((x, _), (y, _)) = ord (x, y)
    1.91 +  in
    1.92 +    find (sort ord' xs) (sort ord' ys)
    1.93 +  end
    1.94  
    1.95 -structure LeCancelSums = CancelSumsFun
    1.96 -(struct
    1.97 -  open CommonCancelSums;
    1.98 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    1.99 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   1.100 -  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
   1.101 -end);
   1.102 +fun cancel_conv rule ct =
   1.103 +  let
   1.104 +    val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
   1.105 +    val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
   1.106 +    val lconv = move_to_front lpath
   1.107 +    val rconv = move_to_front rpath
   1.108 +    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
   1.109 +    val conv = conv1 then_conv Conv.rewr_conv rule
   1.110 +  in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
   1.111  
   1.112 -structure DiffCancelSums = CancelSumsFun
   1.113 -(struct
   1.114 -  open CommonCancelSums;
   1.115 -  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
   1.116 -  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
   1.117 -  val cancel_rule = mk_meta_eq @{thm diff_cancel};
   1.118 -end);
   1.119 -
   1.120 -fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
   1.121 -fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
   1.122 -fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
   1.123 -fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
   1.124 +val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
   1.125 +val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
   1.126 +val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
   1.127 +val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
   1.128  
   1.129  end;