1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Nov 29 10:22:38 2000 +0100
1.3 @@ -0,0 +1,87 @@
1.4 +(* Title: Provers/Arith/cancel_numeral_factor.ML
1.5 + ID: $Id$
1.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 + Copyright 2000 University of Cambridge
1.8 +
1.9 +Cancel common coefficients in balanced expressions:
1.10 +
1.11 + u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
1.12 +
1.13 +where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
1.14 +and d = gcd(m,m') and n=m/d and n'=m'/d.
1.15 +
1.16 +It works by (a) massaging both sides to bring gcd(m,m') to the front:
1.17 +
1.18 + u*#m ~~ u'*#m' == #d*(#n*u) ~~ #d*(#n'*u')
1.19 +
1.20 +(b) then using the rule "cancel" to reach #n*u ~~ #n'*u'.
1.21 +*)
1.22 +
1.23 +signature CANCEL_NUMERAL_FACTOR_DATA =
1.24 +sig
1.25 + (*abstract syntax*)
1.26 + val mk_bal: term * term -> term
1.27 + val dest_bal: term -> term * term
1.28 + val mk_coeff: int * term -> term
1.29 + val dest_coeff: term -> int * term
1.30 + (*rules*)
1.31 + val cancel: thm
1.32 + val neg_exchanges: bool (*true if a negative coeff swaps the two operands,
1.33 + as with < and <= but not = and div*)
1.34 + (*proof tools*)
1.35 + val prove_conv: tactic list -> Sign.sg ->
1.36 + thm list -> term * term -> thm option
1.37 + val trans_tac: thm option -> tactic (*applies the initial lemma*)
1.38 + val norm_tac: tactic (*proves the initial lemma*)
1.39 + val numeral_simp_tac: tactic (*proves the final theorem*)
1.40 + val simplify_meta_eq: thm -> thm (*simplifies the final theorem*)
1.41 +end;
1.42 +
1.43 +
1.44 +functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
1.45 + sig
1.46 + val proc: Sign.sg -> thm list -> term -> thm option
1.47 + end
1.48 +=
1.49 +struct
1.50 +
1.51 +
1.52 +(* greatest common divisor *)
1.53 +fun gcd (0, n) = abs n
1.54 + | gcd (m, n) = gcd (n mod m, m);
1.55 +
1.56 +(*the simplification procedure*)
1.57 +fun proc sg hyps t =
1.58 + let (*first freeze any Vars in the term to prevent flex-flex problems*)
1.59 + val rand_s = gensym"_"
1.60 + fun mk_inst (var as Var((a,i),T)) =
1.61 + (var, Free((a ^ rand_s ^ string_of_int i), T))
1.62 + val t' = subst_atomic (map mk_inst (term_vars t)) t
1.63 + val (t1,t2) = Data.dest_bal t'
1.64 + val (m1, t1') = Data.dest_coeff t1
1.65 + and (m2, t2') = Data.dest_coeff t2
1.66 + val d = (*if both are negative, also divide through by ~1*)
1.67 + if m1<0 andalso m2<0 then ~ (gcd(m1,m2)) else gcd(m1,m2)
1.68 + val _ = if d=1 then (*trivial, so do nothing*)
1.69 + raise TERM("cancel_numeral_factor", [])
1.70 + else ()
1.71 + fun newshape (i,t) = Data.mk_coeff(d, Data.mk_coeff(i,t))
1.72 + val n1 = m1 div d and n2 = m2 div d
1.73 + val rhs = if d<0 andalso Data.neg_exchanges
1.74 + then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1'))
1.75 + else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
1.76 + val reshape = (*Move d to the front and put the rest into standard form
1.77 + i * #m * j == #d * (#n * (j * k)) *)
1.78 + Data.prove_conv [Data.norm_tac] sg hyps
1.79 + (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
1.80 + in
1.81 + apsome Data.simplify_meta_eq
1.82 + (Data.prove_conv
1.83 + [Data.trans_tac reshape, rtac Data.cancel 1,
1.84 + Data.numeral_simp_tac] sg hyps (t', rhs))
1.85 + end
1.86 + handle TERM _ => None
1.87 + | TYPE _ => None; (*Typically (if thy doesn't include Numeral)
1.88 + Undeclared type constructor "Numeral.bin"*)
1.89 +
1.90 +end;