src/HOL/Arith.ML
changeset 5983 79e301a6a51b
parent 5771 7c2c8cf20221
child 6055 fdf4638bf726
     1.1 --- a/src/HOL/Arith.ML	Fri Nov 27 16:54:59 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Fri Nov 27 17:00:30 1998 +0100
     1.3 @@ -154,6 +154,7 @@
     1.4  Goal "n <= ((m + n)::nat)";
     1.5  by (induct_tac "m" 1);
     1.6  by (ALLGOALS Simp_tac);
     1.7 +by (etac le_SucI 1);
     1.8  qed "le_add2";
     1.9  
    1.10  Goal "n <= ((n + m)::nat)";
    1.11 @@ -184,6 +185,7 @@
    1.12  Goal "i+j < (k::nat) --> i<k";
    1.13  by (induct_tac "j" 1);
    1.14  by (ALLGOALS Asm_simp_tac);
    1.15 +by(blast_tac (claset() addDs [Suc_lessD]) 1);
    1.16  qed_spec_mp "add_lessD1";
    1.17  
    1.18  Goal "~ (i+j < (i::nat))";
    1.19 @@ -605,6 +607,311 @@
    1.20  qed "mult_eq_self_implies_10";
    1.21  
    1.22  
    1.23 +
    1.24 +
    1.25 +(*---------------------------------------------------------------------------*)
    1.26 +(* Various arithmetic proof procedures                                       *)
    1.27 +(*---------------------------------------------------------------------------*)
    1.28 +
    1.29 +(*---------------------------------------------------------------------------*)
    1.30 +(* 1. Cancellation of common terms                                           *)
    1.31 +(*---------------------------------------------------------------------------*)
    1.32 +
    1.33 +(*  Title:      HOL/arith_data.ML
    1.34 +    ID:         $Id$
    1.35 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
    1.36 +
    1.37 +Setup various arithmetic proof procedures.
    1.38 +*)
    1.39 +
    1.40 +signature ARITH_DATA =
    1.41 +sig
    1.42 +  val nat_cancel_sums: simproc list
    1.43 +  val nat_cancel_factor: simproc list
    1.44 +  val nat_cancel: simproc list
    1.45 +end;
    1.46 +
    1.47 +structure ArithData: ARITH_DATA =
    1.48 +struct
    1.49 +
    1.50 +
    1.51 +(** abstract syntax of structure nat: 0, Suc, + **)
    1.52 +
    1.53 +(* mk_sum, mk_norm_sum *)
    1.54 +
    1.55 +val one = HOLogic.mk_nat 1;
    1.56 +val mk_plus = HOLogic.mk_binop "op +";
    1.57 +
    1.58 +fun mk_sum [] = HOLogic.zero
    1.59 +  | mk_sum [t] = t
    1.60 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.61 +
    1.62 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    1.63 +fun mk_norm_sum ts =
    1.64 +  let val (ones, sums) = partition (equal one) ts in
    1.65 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    1.66 +  end;
    1.67 +
    1.68 +
    1.69 +(* dest_sum *)
    1.70 +
    1.71 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
    1.72 +
    1.73 +fun dest_sum tm =
    1.74 +  if HOLogic.is_zero tm then []
    1.75 +  else
    1.76 +    (case try HOLogic.dest_Suc tm of
    1.77 +      Some t => one :: dest_sum t
    1.78 +    | None =>
    1.79 +        (case try dest_plus tm of
    1.80 +          Some (t, u) => dest_sum t @ dest_sum u
    1.81 +        | None => [tm]));
    1.82 +
    1.83 +
    1.84 +(** generic proof tools **)
    1.85 +
    1.86 +(* prove conversions *)
    1.87 +
    1.88 +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    1.89 +
    1.90 +fun prove_conv expand_tac norm_tac sg (t, u) =
    1.91 +  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
    1.92 +    (K [expand_tac, norm_tac]))
    1.93 +  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
    1.94 +    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
    1.95 +
    1.96 +val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
    1.97 +  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
    1.98 +
    1.99 +
   1.100 +(* rewriting *)
   1.101 +
   1.102 +fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   1.103 +
   1.104 +val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   1.105 +val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   1.106 +
   1.107 +
   1.108 +
   1.109 +(** cancel common summands **)
   1.110 +
   1.111 +structure Sum =
   1.112 +struct
   1.113 +  val mk_sum = mk_norm_sum;
   1.114 +  val dest_sum = dest_sum;
   1.115 +  val prove_conv = prove_conv;
   1.116 +  val norm_tac = simp_all add_rules THEN simp_all add_ac;
   1.117 +end;
   1.118 +
   1.119 +fun gen_uncancel_tac rule ct =
   1.120 +  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   1.121 +
   1.122 +
   1.123 +(* nat eq *)
   1.124 +
   1.125 +structure EqCancelSums = CancelSumsFun
   1.126 +(struct
   1.127 +  open Sum;
   1.128 +  val mk_bal = HOLogic.mk_eq;
   1.129 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.130 +  val uncancel_tac = gen_uncancel_tac add_left_cancel;
   1.131 +end);
   1.132 +
   1.133 +
   1.134 +(* nat less *)
   1.135 +
   1.136 +structure LessCancelSums = CancelSumsFun
   1.137 +(struct
   1.138 +  open Sum;
   1.139 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.140 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.141 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   1.142 +end);
   1.143 +
   1.144 +
   1.145 +(* nat le *)
   1.146 +
   1.147 +structure LeCancelSums = CancelSumsFun
   1.148 +(struct
   1.149 +  open Sum;
   1.150 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.151 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.152 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   1.153 +end);
   1.154 +
   1.155 +
   1.156 +(* nat diff *)
   1.157 +
   1.158 +structure DiffCancelSums = CancelSumsFun
   1.159 +(struct
   1.160 +  open Sum;
   1.161 +  val mk_bal = HOLogic.mk_binop "op -";
   1.162 +  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   1.163 +  val uncancel_tac = gen_uncancel_tac diff_cancel;
   1.164 +end);
   1.165 +
   1.166 +
   1.167 +
   1.168 +(** cancel common factor **)
   1.169 +
   1.170 +structure Factor =
   1.171 +struct
   1.172 +  val mk_sum = mk_norm_sum;
   1.173 +  val dest_sum = dest_sum;
   1.174 +  val prove_conv = prove_conv;
   1.175 +  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   1.176 +end;
   1.177 +
   1.178 +fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
   1.179 +
   1.180 +fun gen_multiply_tac rule k =
   1.181 +  if k > 0 then
   1.182 +    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   1.183 +  else no_tac;
   1.184 +
   1.185 +
   1.186 +(* nat eq *)
   1.187 +
   1.188 +structure EqCancelFactor = CancelFactorFun
   1.189 +(struct
   1.190 +  open Factor;
   1.191 +  val mk_bal = HOLogic.mk_eq;
   1.192 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.193 +  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   1.194 +end);
   1.195 +
   1.196 +
   1.197 +(* nat less *)
   1.198 +
   1.199 +structure LessCancelFactor = CancelFactorFun
   1.200 +(struct
   1.201 +  open Factor;
   1.202 +  val mk_bal = HOLogic.mk_binrel "op <";
   1.203 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.204 +  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   1.205 +end);
   1.206 +
   1.207 +
   1.208 +(* nat le *)
   1.209 +
   1.210 +structure LeCancelFactor = CancelFactorFun
   1.211 +(struct
   1.212 +  open Factor;
   1.213 +  val mk_bal = HOLogic.mk_binrel "op <=";
   1.214 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.215 +  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   1.216 +end);
   1.217 +
   1.218 +
   1.219 +
   1.220 +(** prepare nat_cancel simprocs **)
   1.221 +
   1.222 +fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
   1.223 +val prep_pats = map prep_pat;
   1.224 +
   1.225 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.226 +
   1.227 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   1.228 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   1.229 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   1.230 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   1.231 +
   1.232 +val nat_cancel_sums = map prep_simproc
   1.233 +  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   1.234 +   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   1.235 +   ("natle_cancel_sums", le_pats, LeCancelSums.proc),
   1.236 +   ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   1.237 +
   1.238 +val nat_cancel_factor = map prep_simproc
   1.239 +  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   1.240 +   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   1.241 +   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   1.242 +
   1.243 +val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   1.244 +
   1.245 +
   1.246 +end;
   1.247 +
   1.248 +open ArithData;
   1.249 +
   1.250 +Addsimprocs nat_cancel;
   1.251 +
   1.252 +(*---------------------------------------------------------------------------*)
   1.253 +(* 2. Linear arithmetic                                                      *)
   1.254 +(*---------------------------------------------------------------------------*)
   1.255 +
   1.256 +(* Parameter data for general linear arithmetic functor *)
   1.257 +structure Nat_LA_Data: LIN_ARITH_DATA =
   1.258 +struct
   1.259 +val ccontr = ccontr;
   1.260 +val conjI = conjI;
   1.261 +val lessD = Suc_leI;
   1.262 +val nat_neqE = nat_neqE;
   1.263 +val notI = notI;
   1.264 +val not_leD = not_leE RS Suc_leI;
   1.265 +val not_lessD = leI;
   1.266 +val sym = sym;
   1.267 +
   1.268 +val nat = Type("nat",[]);
   1.269 +
   1.270 +fun nnb T = T = Type("fun",[nat,Type("fun",[nat,Type("bool",[])])])
   1.271 +
   1.272 +(* Turn term into list of summand * multiplicity plus a constant *)
   1.273 +fun poly(Const("Suc",_)$t, (p,i)) = poly(t, (p,i+1))
   1.274 +  | poly(Const("op +",Type("fun",[Type("nat",[]),_])) $ s $ t, pi) =
   1.275 +      poly(s,poly(t,pi))
   1.276 +  | poly(t,(p,i)) =
   1.277 +      if t = Const("0",nat) then (p,i)
   1.278 +      else (case assoc(p,t) of None => ((t,1)::p,i)
   1.279 +            | Some m => (overwrite(p,(t,m+1)), i))
   1.280 +
   1.281 +fun decomp2(rel,T,lhs,rhs) =
   1.282 +  if not(nnb T) then None else
   1.283 +  let val (p,i) = poly(lhs,([],0)) and (q,j) = poly(rhs,([],0))
   1.284 +  in case rel of
   1.285 +       "op <"  => Some(p,i,"<",q,j)
   1.286 +     | "op <=" => Some(p,i,"<=",q,j)
   1.287 +     | "op ="  => Some(p,i,"=",q,j)
   1.288 +     | _       => None
   1.289 +  end;
   1.290 +
   1.291 +fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j)
   1.292 +  | negate None = None;
   1.293 +
   1.294 +fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs)
   1.295 +  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   1.296 +      negate(decomp2(rel,T,lhs,rhs))
   1.297 +  | decomp _ = None
   1.298 +(* reduce contradictory <= to False.
   1.299 +   Most of the work is done by the cancel tactics.
   1.300 +*)
   1.301 +val add_rules = [Zero_not_Suc,Suc_not_Zero,le_0_eq];
   1.302 +
   1.303 +val cancel_sums_ss = HOL_basic_ss addsimps add_rules
   1.304 +                                  addsimprocs nat_cancel_sums;
   1.305 +
   1.306 +val simp = simplify cancel_sums_ss;
   1.307 +
   1.308 +val add_mono_thms = map (fn s => prove_goal Arith.thy s
   1.309 + (fn prems => [cut_facts_tac prems 1,
   1.310 +               blast_tac (claset() addIs [add_le_mono]) 1]))
   1.311 +["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.312 + "(i = j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.313 + "(i <= j) & (k = l) ==> i + k <= j + (l::nat)",
   1.314 + "(i = j) & (k = l) ==> i + k <= j + (l::nat)"
   1.315 +];
   1.316 +
   1.317 +end;
   1.318 +
   1.319 +structure Fast_Nat_Arith = Fast_Lin_Arith(Nat_LA_Data);
   1.320 +
   1.321 +simpset_ref () := (simpset() addSolver Fast_Nat_Arith.cut_lin_arith_tac);
   1.322 +
   1.323 +(*---------------------------------------------------------------------------*)
   1.324 +(* End of proof procedures. Now go and USE them!                             *)
   1.325 +(*---------------------------------------------------------------------------*)
   1.326 +
   1.327 +
   1.328  (*** Subtraction laws -- mostly from Clemens Ballarin ***)
   1.329  
   1.330  Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
   1.331 @@ -628,7 +935,7 @@
   1.332    by (dres_inst_tac [("k","k")] add_less_mono1 1);
   1.333    by (Asm_full_simp_tac 1);
   1.334   by (rotate_tac 1 1);
   1.335 - by (asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
   1.336 + by (Asm_full_simp_tac 1);
   1.337  by (etac add_less_imp_less_diff 1);
   1.338  qed "less_diff_conv";
   1.339  
   1.340 @@ -736,3 +1043,35 @@
   1.341  by (dtac not_leE 1);
   1.342  by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
   1.343  qed_spec_mp "diff_le_mono2";
   1.344 +
   1.345 +
   1.346 +(*This proof requires natdiff_cancel_sums*)
   1.347 +Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)";
   1.348 +by (induct_tac "l" 1);
   1.349 +by (Simp_tac 1);
   1.350 +by (Clarify_tac 1);
   1.351 +by (etac less_SucE 1);
   1.352 +by (Clarify_tac 2);
   1.353 +by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2);
   1.354 +by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
   1.355 +				      Suc_diff_le, less_imp_le]) 1);
   1.356 +qed_spec_mp "diff_less_mono2";
   1.357 +
   1.358 +(** Elimination of `-' on nat due to John Harrison **)
   1.359 +(*This proof requires natle_cancel_sums*)
   1.360 +
   1.361 +Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
   1.362 +by(case_tac "a <= b" 1);
   1.363 +by(Auto_tac);
   1.364 +by(eres_inst_tac [("x","b-a")] allE 1);
   1.365 +by(Auto_tac);
   1.366 +qed "nat_diff_split";
   1.367 +
   1.368 +(*
   1.369 +This is an example of the power of nat_diff_split. Many of the `-' thms in
   1.370 +Arith.ML could take advantage of this, but would need to be moved.
   1.371 +*)
   1.372 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
   1.373 +by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.374 +qed_spec_mp "diffs0_imp_equal";
   1.375 +