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