src/HOL/arith_data.ML
author paulson
Tue Sep 01 15:05:36 1998 +0200 (1998-09-01)
changeset 5418 a895ab904b85
parent 5353 0526ade4a23b
child 5429 0833486c23ce
permissions -rw-r--r--
Replaced Suc_diff_n by Suc_diff_le
     1 (*  Title:      HOL/arith_data.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4 
     5 Setup various arithmetic proof procedures.
     6 *)
     7 
     8 signature ARITH_DATA =
     9 sig
    10   val nat_cancel_sums: simproc list
    11   val nat_cancel_factor: simproc list
    12   val nat_cancel: simproc list
    13 end;
    14 
    15 structure ArithData: ARITH_DATA =
    16 struct
    17 
    18 
    19 (** abstract syntax of structure nat: 0, Suc, + **)
    20 
    21 (* mk_sum, mk_norm_sum *)
    22 
    23 val one = HOLogic.mk_nat 1;
    24 val mk_plus = HOLogic.mk_binop "op +";
    25 
    26 fun mk_sum [] = HOLogic.zero
    27   | mk_sum [t] = t
    28   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    29 
    30 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    31 fun mk_norm_sum ts =
    32   let val (ones, sums) = partition (equal one) ts in
    33     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    34   end;
    35 
    36 
    37 (* dest_sum *)
    38 
    39 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    40 
    41 fun dest_sum tm =
    42   if HOLogic.is_zero tm then []
    43   else
    44     (case try HOLogic.dest_Suc tm of
    45       Some t => one :: dest_sum t
    46     | None =>
    47         (case try dest_plus tm of
    48           Some (t, u) => dest_sum t @ dest_sum u
    49         | None => [tm]));
    50 
    51 
    52 (** generic proof tools **)
    53 
    54 (* prove conversions *)
    55 
    56 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    57 
    58 fun prove_conv expand_tac norm_tac sg (t, u) =
    59   meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
    60     (K [expand_tac, norm_tac]))
    61   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    62     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    63 
    64 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    65   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    66 
    67 
    68 (* rewriting *)
    69 
    70 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
    71 
    72 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    73 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    74 
    75 
    76 
    77 (** cancel common summands **)
    78 
    79 structure Sum =
    80 struct
    81   val mk_sum = mk_norm_sum;
    82   val dest_sum = dest_sum;
    83   val prove_conv = prove_conv;
    84   val norm_tac = simp_all add_rules THEN simp_all add_ac;
    85 end;
    86 
    87 fun gen_uncancel_tac rule ct =
    88   rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
    89 
    90 
    91 (* nat eq *)
    92 
    93 structure EqCancelSums = CancelSumsFun
    94 (struct
    95   open Sum;
    96   val mk_bal = HOLogic.mk_eq;
    97   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    98   val uncancel_tac = gen_uncancel_tac add_left_cancel;
    99 end);
   100 
   101 
   102 (* nat less *)
   103 
   104 structure LessCancelSums = CancelSumsFun
   105 (struct
   106   open Sum;
   107   val mk_bal = HOLogic.mk_binrel "op <";
   108   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   109   val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   110 end);
   111 
   112 
   113 (* nat le *)
   114 
   115 structure LeCancelSums = CancelSumsFun
   116 (struct
   117   open Sum;
   118   val mk_bal = HOLogic.mk_binrel "op <=";
   119   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   120   val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   121 end);
   122 
   123 
   124 (* nat diff *)
   125 
   126 structure DiffCancelSums = CancelSumsFun
   127 (struct
   128   open Sum;
   129   val mk_bal = HOLogic.mk_binop "op -";
   130   val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   131   val uncancel_tac = gen_uncancel_tac diff_cancel;
   132 end);
   133 
   134 
   135 
   136 (** cancel common factor **)
   137 
   138 structure Factor =
   139 struct
   140   val mk_sum = mk_norm_sum;
   141   val dest_sum = dest_sum;
   142   val prove_conv = prove_conv;
   143   val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   144 end;
   145 
   146 fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   147 
   148 fun gen_multiply_tac rule k =
   149   if k > 0 then
   150     rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   151   else no_tac;
   152 
   153 
   154 (* nat eq *)
   155 
   156 structure EqCancelFactor = CancelFactorFun
   157 (struct
   158   open Factor;
   159   val mk_bal = HOLogic.mk_eq;
   160   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   161   val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   162 end);
   163 
   164 
   165 (* nat less *)
   166 
   167 structure LessCancelFactor = CancelFactorFun
   168 (struct
   169   open Factor;
   170   val mk_bal = HOLogic.mk_binrel "op <";
   171   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   172   val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   173 end);
   174 
   175 
   176 (* nat le *)
   177 
   178 structure LeCancelFactor = CancelFactorFun
   179 (struct
   180   open Factor;
   181   val mk_bal = HOLogic.mk_binrel "op <=";
   182   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   183   val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   184 end);
   185 
   186 
   187 
   188 (** prepare nat_cancel simprocs **)
   189 
   190 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   191 val prep_pats = map prep_pat;
   192 
   193 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   194 
   195 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   196 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   197 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   198 val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   199 
   200 val nat_cancel_sums = map prep_simproc
   201   [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   202    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   203    ("natle_cancel_sums", le_pats, LeCancelSums.proc),
   204    ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   205 
   206 val nat_cancel_factor = map prep_simproc
   207   [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   208    ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   209    ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   210 
   211 val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   212 
   213 
   214 end;
   215 
   216 
   217 open ArithData;
   218 
   219 
   220 context Arith.thy;
   221 Addsimprocs nat_cancel;
   222 
   223 
   224 (*This proof requires natdiff_cancel_sums*)
   225 goal Arith.thy "!!n::nat. m<n --> m<l --> (l-n) < (l-m)";
   226 by (induct_tac "l" 1);
   227 by (Simp_tac 1);
   228 by (Clarify_tac 1);
   229 by (etac less_SucE 1);
   230 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
   231 				      Suc_diff_le]) 1);
   232 by (Clarify_tac 1);
   233 by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
   234 qed_spec_mp "diff_less_mono2";