src/HOL/arith_data.ML
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24095 785c3cd7fcb5
child 25484 4c98517601ce
permissions -rw-r--r--
moved Finite_Set before Datatype
     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 (*** cancellation of common terms ***)
     9 
    10 structure NatArithUtils =
    11 struct
    12 
    13 (** abstract syntax of structure nat: 0, Suc, + **)
    14 
    15 (* mk_sum, mk_norm_sum *)
    16 
    17 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    18 
    19 fun mk_sum [] = HOLogic.zero
    20   | mk_sum [t] = t
    21   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    22 
    23 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    24 fun mk_norm_sum ts =
    25   let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    26     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    27   end;
    28 
    29 
    30 (* dest_sum *)
    31 
    32 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    33 
    34 fun dest_sum tm =
    35   if HOLogic.is_zero tm then []
    36   else
    37     (case try HOLogic.dest_Suc tm of
    38       SOME t => HOLogic.Suc_zero :: dest_sum t
    39     | NONE =>
    40         (case try dest_plus tm of
    41           SOME (t, u) => dest_sum t @ dest_sum u
    42         | NONE => [tm]));
    43 
    44 
    45 
    46 (** generic proof tools **)
    47 
    48 (* prove conversions *)
    49 
    50 fun prove_conv expand_tac norm_tac ss tu =  (* FIXME avoid standard *)
    51   mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    52       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    53     (K (EVERY [expand_tac, norm_tac ss]))));
    54 
    55 
    56 (* rewriting *)
    57 
    58 fun simp_all_tac rules =
    59   let val ss0 = HOL_ss addsimps rules
    60   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    61 
    62 fun prep_simproc (name, pats, proc) =
    63   Simplifier.simproc (the_context ()) name pats proc;
    64 
    65 end;
    66 
    67 
    68 
    69 (** ArithData **)
    70 
    71 signature ARITH_DATA =
    72 sig
    73   val nat_cancel_sums_add: simproc list
    74   val nat_cancel_sums: simproc list
    75   val arith_data_setup: Context.generic -> Context.generic
    76 end;
    77 
    78 structure ArithData: ARITH_DATA =
    79 struct
    80 
    81 open NatArithUtils;
    82 
    83 
    84 (** cancel common summands **)
    85 
    86 structure Sum =
    87 struct
    88   val mk_sum = mk_norm_sum;
    89   val dest_sum = dest_sum;
    90   val prove_conv = prove_conv;
    91   val norm_tac1 = simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    92     @{thm "add_0"}, @{thm "add_0_right"}];
    93   val norm_tac2 = simp_all_tac @{thms add_ac};
    94   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    95 end;
    96 
    97 fun gen_uncancel_tac rule ct =
    98   rtac (instantiate' [] [NONE, SOME ct] (rule RS @{thm subst_equals})) 1;
    99 
   100 
   101 (* nat eq *)
   102 
   103 structure EqCancelSums = CancelSumsFun
   104 (struct
   105   open Sum;
   106   val mk_bal = HOLogic.mk_eq;
   107   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   108   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
   109 end);
   110 
   111 
   112 (* nat less *)
   113 
   114 structure LessCancelSums = CancelSumsFun
   115 (struct
   116   open Sum;
   117   val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   118   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   119   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   120 end);
   121 
   122 
   123 (* nat le *)
   124 
   125 structure LeCancelSums = CancelSumsFun
   126 (struct
   127   open Sum;
   128   val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   129   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   130   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   131 end);
   132 
   133 
   134 (* nat diff *)
   135 
   136 structure DiffCancelSums = CancelSumsFun
   137 (struct
   138   open Sum;
   139   val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   140   val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   141   val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   142 end);
   143 
   144 
   145 (* prepare nat_cancel simprocs *)
   146 
   147 val nat_cancel_sums_add = map prep_simproc
   148   [("nateq_cancel_sums",
   149      ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"],
   150      K EqCancelSums.proc),
   151    ("natless_cancel_sums",
   152      ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"],
   153      K LessCancelSums.proc),
   154    ("natle_cancel_sums",
   155      ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"],
   156      K LeCancelSums.proc)];
   157 
   158 val nat_cancel_sums = nat_cancel_sums_add @
   159   [prep_simproc ("natdiff_cancel_sums",
   160     ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"],
   161     K DiffCancelSums.proc)];
   162 
   163 val arith_data_setup =
   164   Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   165 
   166 
   167 (* FIXME dead code *)
   168 (* antisymmetry:
   169    combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y
   170 
   171 local
   172 val antisym = mk_meta_eq order_antisym
   173 val not_lessD = @{thm linorder_not_less} RS iffD1
   174 fun prp t thm = (#prop(rep_thm thm) = t)
   175 in
   176 fun antisym_eq prems thm =
   177   let
   178     val r = #prop(rep_thm thm);
   179   in
   180     case r of
   181       Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
   182         let val r' = Tr $ (c $ t $ s)
   183         in
   184           case Library.find_first (prp r') prems of
   185             NONE =>
   186               let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
   187               in case Library.find_first (prp r') prems of
   188                    NONE => []
   189                  | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
   190               end
   191           | SOME thm' => [thm' RS (thm RS antisym)]
   192         end
   193     | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
   194         let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
   195         in
   196           case Library.find_first (prp r') prems of
   197             NONE =>
   198               let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
   199               in case Library.find_first (prp r') prems of
   200                    NONE => []
   201                  | SOME thm' =>
   202                      [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
   203               end
   204           | SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
   205         end
   206     | _ => []
   207   end
   208   handle THM _ => []
   209 end;
   210 *)
   211 
   212 end;
   213 
   214 open ArithData;