src/HOL/arith_data.ML
author wenzelm
Wed Nov 26 17:52:53 1997 +0100 (1997-11-26)
changeset 4309 c98f44948d86
parent 4295 81132a38996a
child 4310 cad4f24be60b
permissions -rw-r--r--
separate lists of simprocs;
     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 *)
    22 
    23 val mk_plus = HOLogic.mk_binop "op +";
    24 
    25 fun mk_sum [] = HOLogic.zero
    26   | mk_sum [t] = t
    27   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    28 
    29 
    30 (* dest_sum *)
    31 
    32 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    33 val one = HOLogic.mk_nat 1;
    34 
    35 fun dest_sum tm =
    36   if HOLogic.is_zero tm then []
    37   else
    38     (case try HOLogic.dest_Suc tm of
    39       Some t => one :: dest_sum t
    40     | None =>
    41         (case try dest_plus tm of
    42           Some (t, u) => dest_sum t @ dest_sum u
    43         | None => [tm]));
    44 
    45 
    46 (** generic proof tools **)
    47 
    48 (* prove conversions *)
    49 
    50 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    51 
    52 fun prove_conv expand_tac norm_tac sg (t, u) =
    53   mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
    54     (K [expand_tac, norm_tac]))
    55   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    56     (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    57 
    58 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    59   (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    60 
    61 
    62 (* rewriting *)
    63 
    64 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
    65 
    66 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    67 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    68 
    69 
    70 
    71 (** cancel common summands **)
    72 
    73 structure Sum =
    74 struct
    75   val mk_sum = mk_sum;
    76   val dest_sum = dest_sum;
    77   val prove_conv = prove_conv;
    78   val norm_tac = simp_all add_rules THEN simp_all add_ac;
    79 end;
    80 
    81 fun gen_uncancel_tac rule ct =
    82   rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
    83 
    84 
    85 (* nat eq *)
    86 
    87 structure EqCancelSums = CancelSumsFun
    88 (struct
    89   open Sum;
    90   val mk_bal = HOLogic.mk_eq;
    91   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    92   val uncancel_tac = gen_uncancel_tac add_left_cancel;
    93 end);
    94 
    95 
    96 (* nat less *)
    97 
    98 structure LessCancelSums = CancelSumsFun
    99 (struct
   100   open Sum;
   101   val mk_bal = HOLogic.mk_binrel "op <";
   102   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   103   val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   104 end);
   105 
   106 
   107 (* nat le *)
   108 
   109 structure LeCancelSums = CancelSumsFun
   110 (struct
   111   open Sum;
   112   val mk_bal = HOLogic.mk_binrel "op <=";
   113   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   114   val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   115 end);
   116 
   117 
   118 (* nat diff *)
   119 
   120 (* FIXME *)
   121 
   122 
   123 
   124 (** cancel common factor **)
   125 
   126 structure Factor =
   127 struct
   128   val mk_sum = mk_sum;
   129   val dest_sum = dest_sum;
   130   val prove_conv = prove_conv;
   131   val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   132 end;
   133 
   134 fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   135 
   136 fun gen_multiply_tac rule k =
   137   if k > 0 then
   138     rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   139   else no_tac;
   140 
   141 
   142 (* nat eq *)
   143 
   144 structure EqCancelFactor = CancelFactorFun
   145 (struct
   146   open Factor;
   147   val mk_bal = HOLogic.mk_eq;
   148   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   149   val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   150 end);
   151 
   152 
   153 (* nat less *)
   154 
   155 structure LessCancelFactor = CancelFactorFun
   156 (struct
   157   open Factor;
   158   val mk_bal = HOLogic.mk_binrel "op <";
   159   val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   160   val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   161 end);
   162 
   163 
   164 (* nat le *)
   165 
   166 structure LeCancelFactor = CancelFactorFun
   167 (struct
   168   open Factor;
   169   val mk_bal = HOLogic.mk_binrel "op <=";
   170   val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   171   val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   172 end);
   173 
   174 
   175 
   176 (** prepare nat_cancel simprocs **)
   177 
   178 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   179 val prep_pats = map prep_pat;
   180 
   181 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   182 
   183 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   184 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   185 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   186 
   187 val nat_cancel_sums = map prep_simproc
   188   [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   189    ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   190    ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
   191 
   192 val nat_cancel_factor = map prep_simproc
   193   [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   194    ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   195    ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   196 
   197 val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   198 
   199 
   200 end;