src/HOL/Tools/arith_data.ML
author wenzelm
Thu Jan 01 23:31:49 2009 +0100 (2009-01-01)
changeset 29302 eb782d1dc07c
parent 28952 15a4b2cf8c34
child 30496 7cdcc9dd95cb
permissions -rw-r--r--
normalized some ML type/val aliases;
     1 (*  Title:      HOL/arith_data.ML
     2     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     3 
     4 Basic arithmetic proof tools.
     5 *)
     6 
     7 signature ARITH_DATA =
     8 sig
     9   val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    10   val simp_all_tac: thm list -> simpset -> tactic
    11 
    12   val mk_sum: term list -> term
    13   val mk_norm_sum: term list -> term
    14   val dest_sum: term -> term list
    15 
    16   val nat_cancel_sums_add: simproc list
    17   val nat_cancel_sums: simproc list
    18   val setup: Context.generic -> Context.generic
    19 end;
    20 
    21 structure ArithData: ARITH_DATA =
    22 struct
    23 
    24 (** generic proof tools **)
    25 
    26 (* prove conversions *)
    27 
    28 fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    29   mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    30       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    31     (K (EVERY [expand_tac, norm_tac ss]))));
    32 
    33 (* rewriting *)
    34 
    35 fun simp_all_tac rules =
    36   let val ss0 = HOL_ss addsimps rules
    37   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    38 
    39 
    40 (** abstract syntax of structure nat: 0, Suc, + **)
    41 
    42 local
    43 
    44 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    45 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    46 
    47 in
    48 
    49 fun mk_sum [] = HOLogic.zero
    50   | mk_sum [t] = t
    51   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    52 
    53 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    54 fun mk_norm_sum ts =
    55   let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    56     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    57   end;
    58 
    59 
    60 fun dest_sum tm =
    61   if HOLogic.is_zero tm then []
    62   else
    63     (case try HOLogic.dest_Suc tm of
    64       SOME t => HOLogic.Suc_zero :: dest_sum t
    65     | NONE =>
    66         (case try dest_plus tm of
    67           SOME (t, u) => dest_sum t @ dest_sum u
    68         | NONE => [tm]));
    69 
    70 end;
    71 
    72 
    73 (** cancel common summands **)
    74 
    75 structure Sum =
    76 struct
    77   val mk_sum = mk_norm_sum;
    78   val dest_sum = dest_sum;
    79   val prove_conv = prove_conv;
    80   val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    81     @{thm "add_0"}, @{thm "add_0_right"}];
    82   val norm_tac2 = simp_all_tac @{thms add_ac};
    83   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    84 end;
    85 
    86 fun gen_uncancel_tac rule ct =
    87   rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
    88 
    89 
    90 (* nat eq *)
    91 
    92 structure EqCancelSums = CancelSumsFun
    93 (struct
    94   open Sum;
    95   val mk_bal = HOLogic.mk_eq;
    96   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    97   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    98 end);
    99 
   100 
   101 (* nat less *)
   102 
   103 structure LessCancelSums = CancelSumsFun
   104 (struct
   105   open Sum;
   106   val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   107   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   108   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   109 end);
   110 
   111 
   112 (* nat le *)
   113 
   114 structure LeCancelSums = CancelSumsFun
   115 (struct
   116   open Sum;
   117   val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   118   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   119   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   120 end);
   121 
   122 
   123 (* nat diff *)
   124 
   125 structure DiffCancelSums = CancelSumsFun
   126 (struct
   127   open Sum;
   128   val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   129   val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   130   val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   131 end);
   132 
   133 
   134 (* prepare nat_cancel simprocs *)
   135 
   136 val nat_cancel_sums_add =
   137   [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
   138      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
   139      (K EqCancelSums.proc),
   140    Simplifier.simproc (the_context ()) "natless_cancel_sums"
   141      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   142      (K LessCancelSums.proc),
   143    Simplifier.simproc (the_context ()) "natle_cancel_sums"
   144      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   145      (K LeCancelSums.proc)];
   146 
   147 val nat_cancel_sums = nat_cancel_sums_add @
   148   [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
   149     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   150     (K DiffCancelSums.proc)];
   151 
   152 val setup =
   153   Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   154 
   155 end;