Setup various arithmetic proof procedures.
authorwenzelm
Wed Nov 26 16:44:25 1997 +0100 (1997-11-26)
changeset 429581132a38996a
parent 4294 7fe9723d579b
child 4296 aa84d9c62454
Setup various arithmetic proof procedures.
src/HOL/arith_data.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/arith_data.ML	Wed Nov 26 16:44:25 1997 +0100
     1.3 @@ -0,0 +1,194 @@
     1.4 +(*  Title:      HOL/arith_data.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.7 +
     1.8 +Setup various arithmetic proof procedures.
     1.9 +*)
    1.10 +
    1.11 +signature ARITH_DATA =
    1.12 +sig
    1.13 +  val nat_cancel: simproc list
    1.14 +end;
    1.15 +
    1.16 +structure ArithData (* FIXME :ARITH_DATA *) =
    1.17 +struct
    1.18 +
    1.19 +
    1.20 +(** abstract syntax of structure nat: 0, Suc, + **)
    1.21 +
    1.22 +(* mk_sum *)
    1.23 +
    1.24 +val mk_plus = HOLogic.mk_binop "op +";
    1.25 +
    1.26 +fun mk_sum [] = HOLogic.zero
    1.27 +  | mk_sum [t] = t
    1.28 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.29 +
    1.30 +
    1.31 +(* dest_sum *)
    1.32 +
    1.33 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    1.34 +val one = HOLogic.mk_nat 1;
    1.35 +
    1.36 +fun dest_sum tm =
    1.37 +  if HOLogic.is_zero tm then []
    1.38 +  else
    1.39 +    (case try HOLogic.dest_Suc tm of
    1.40 +      Some t => one :: dest_sum t
    1.41 +    | None =>
    1.42 +        (case try dest_plus tm of
    1.43 +          Some (t, u) => dest_sum t @ dest_sum u
    1.44 +        | None => [tm]));
    1.45 +
    1.46 +
    1.47 +(** generic proof tools **)
    1.48 +
    1.49 +(* prove conversions *)
    1.50 +
    1.51 +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    1.52 +
    1.53 +fun prove_conv expand_tac norm_tac sg (t, u) =
    1.54 +  mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
    1.55 +    (K [expand_tac, norm_tac]))
    1.56 +  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.57 +    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    1.58 +
    1.59 +val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    1.60 +  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    1.61 +
    1.62 +
    1.63 +(* rewriting *)
    1.64 +
    1.65 +fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
    1.66 +
    1.67 +val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    1.68 +val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    1.69 +
    1.70 +
    1.71 +
    1.72 +(** cancel common summands **)
    1.73 +
    1.74 +structure Sum =
    1.75 +struct
    1.76 +  val mk_sum = mk_sum;
    1.77 +  val dest_sum = dest_sum;
    1.78 +  val prove_conv = prove_conv;
    1.79 +  val norm_tac = simp_all add_rules THEN simp_all add_ac;
    1.80 +end;
    1.81 +
    1.82 +fun gen_uncancel_tac rule ct =
    1.83 +  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
    1.84 +
    1.85 +
    1.86 +(* nat eq *)
    1.87 +
    1.88 +structure EqCancelSums = CancelSumsFun
    1.89 +(struct
    1.90 +  open Sum;
    1.91 +  val mk_bal = HOLogic.mk_eq;
    1.92 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    1.93 +  val uncancel_tac = gen_uncancel_tac add_left_cancel;
    1.94 +end);
    1.95 +
    1.96 +
    1.97 +(* nat less *)
    1.98 +
    1.99 +structure LessCancelSums = CancelSumsFun
   1.100 +(struct
   1.101 +  open Sum;
   1.102 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.103 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.104 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   1.105 +end);
   1.106 +
   1.107 +
   1.108 +(* nat le *)
   1.109 +
   1.110 +structure LeCancelSums = CancelSumsFun
   1.111 +(struct
   1.112 +  open Sum;
   1.113 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.114 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.115 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   1.116 +end);
   1.117 +
   1.118 +
   1.119 +(* nat diff *)
   1.120 +
   1.121 +(* FIXME *)
   1.122 +
   1.123 +
   1.124 +
   1.125 +(** cancel common factor **)
   1.126 +
   1.127 +structure Factor =
   1.128 +struct
   1.129 +  val mk_sum = mk_sum;
   1.130 +  val dest_sum = dest_sum;
   1.131 +  val prove_conv = prove_conv;
   1.132 +  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   1.133 +end;
   1.134 +
   1.135 +fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   1.136 +
   1.137 +fun gen_multiply_tac rule k =
   1.138 +  if k > 0 then
   1.139 +    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   1.140 +  else no_tac;
   1.141 +
   1.142 +
   1.143 +(* nat eq *)
   1.144 +
   1.145 +structure EqCancelFactor = CancelFactorFun
   1.146 +(struct
   1.147 +  open Factor;
   1.148 +  val mk_bal = HOLogic.mk_eq;
   1.149 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.150 +  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   1.151 +end);
   1.152 +
   1.153 +
   1.154 +(* nat less *)
   1.155 +
   1.156 +structure LessCancelFactor = CancelFactorFun
   1.157 +(struct
   1.158 +  open Factor;
   1.159 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.160 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.161 +  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   1.162 +end);
   1.163 +
   1.164 +
   1.165 +(* nat le *)
   1.166 +
   1.167 +structure LeCancelFactor = CancelFactorFun
   1.168 +(struct
   1.169 +  open Factor;
   1.170 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.171 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.172 +  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   1.173 +end);
   1.174 +
   1.175 +
   1.176 +
   1.177 +(** prepare nat_cancel simprocs **)
   1.178 +
   1.179 +fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   1.180 +val prep_pats = map prep_pat;
   1.181 +
   1.182 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.183 +
   1.184 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   1.185 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   1.186 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   1.187 +
   1.188 +val nat_cancel = map prep_simproc
   1.189 +  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   1.190 +   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   1.191 +   ("natle_cancel_factor", le_pats, LeCancelFactor.proc),
   1.192 +   ("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   1.193 +   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   1.194 +   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
   1.195 +
   1.196 +
   1.197 +end;