src/Provers/Arith/cancel_numeral_factor.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 61144 5e94dfead1c2
child 70315 2f9623aa1eeb
permissions -rw-r--r--
more robust sorted_entries;
paulson@10537
     1
(*  Title:      Provers/Arith/cancel_numeral_factor.ML
paulson@10537
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@10537
     3
    Copyright   2000  University of Cambridge
paulson@10537
     4
paulson@10537
     5
Cancel common coefficients in balanced expressions:
paulson@10537
     6
paulson@10537
     7
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
paulson@10537
     8
paulson@10537
     9
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
paulson@10537
    10
and d = gcd(m,m') and n=m/d and n'=m'/d.
paulson@10537
    11
paulson@10537
    12
It works by (a) massaging both sides to bring gcd(m,m') to the front:
paulson@10537
    13
paulson@10537
    14
     u*#m ~~ u'*#m'  ==  #d*(#n*u) ~~ #d*(#n'*u')
paulson@10537
    15
paulson@10537
    16
(b) then using the rule "cancel" to reach #n*u ~~ #n'*u'.
paulson@10537
    17
*)
paulson@10537
    18
paulson@10537
    19
signature CANCEL_NUMERAL_FACTOR_DATA =
paulson@10537
    20
sig
paulson@10537
    21
  (*abstract syntax*)
paulson@10537
    22
  val mk_bal: term * term -> term
paulson@10537
    23
  val dest_bal: term -> term * term
wenzelm@24630
    24
  val mk_coeff: int * term -> term
wenzelm@24630
    25
  val dest_coeff: term -> int * term
paulson@10537
    26
  (*rules*)
paulson@10537
    27
  val cancel: thm
paulson@10537
    28
  val neg_exchanges: bool  (*true if a negative coeff swaps the two operands,
paulson@10537
    29
                             as with < and <= but not = and div*)
paulson@10537
    30
  (*proof tools*)
wenzelm@20114
    31
  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
wenzelm@59530
    32
  val trans_tac: Proof.context -> thm option -> tactic  (*applies the initial lemma*)
wenzelm@51717
    33
  val norm_tac: Proof.context -> tactic              (*proves the initial lemma*)
wenzelm@51717
    34
  val numeral_simp_tac: Proof.context -> tactic      (*proves the final theorem*)
wenzelm@51717
    35
  val simplify_meta_eq: Proof.context -> thm -> thm  (*simplifies the final theorem*)
paulson@10537
    36
end;
paulson@10537
    37
paulson@10537
    38
paulson@10537
    39
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
wenzelm@61144
    40
  sig val proc: Proof.context -> cterm -> thm option end =
paulson@10537
    41
struct
paulson@10537
    42
paulson@10537
    43
(*the simplification procedure*)
wenzelm@61144
    44
fun proc ctxt ct =
wenzelm@15027
    45
  let
wenzelm@51717
    46
    val prems = Simplifier.prems_of ctxt;
wenzelm@61144
    47
    val t = Thm.term_of ct;
wenzelm@20114
    48
    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
wenzelm@20114
    49
    val export = singleton (Variable.export ctxt' ctxt)
wenzelm@51717
    50
    (* FIXME ctxt vs. ctxt' *)
wenzelm@20114
    51
wenzelm@20114
    52
    val (t1,t2) = Data.dest_bal t'
wenzelm@20114
    53
    val (m1, t1') = Data.dest_coeff t1
wenzelm@20114
    54
    and (m2, t2') = Data.dest_coeff t2
wenzelm@20114
    55
    val d = (*if both are negative, also divide through by ~1*)
wenzelm@20114
    56
      if (m1<0 andalso m2<=0) orelse
haftmann@23261
    57
         (m1<=0 andalso m2<0) then ~ (abs (Integer.gcd m1 m2)) else abs (Integer.gcd m1 m2)
wenzelm@20114
    58
    val _ = if d=1 then   (*trivial, so do nothing*)
wenzelm@20114
    59
              raise TERM("cancel_numeral_factor", [])
wenzelm@20114
    60
            else ()
wenzelm@20114
    61
    fun newshape (i,t) = Data.mk_coeff(d, Data.mk_coeff(i,t))
wenzelm@20114
    62
    val n1 = m1 div d and n2 = m2 div d
wenzelm@20114
    63
    val rhs = if d<0 andalso Data.neg_exchanges
wenzelm@20114
    64
              then Data.mk_bal (Data.mk_coeff(n2,t2'), Data.mk_coeff(n1,t1'))
wenzelm@20114
    65
              else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
wenzelm@20114
    66
    val reshape =  (*Move d to the front and put the rest into standard form
wenzelm@20114
    67
                       i * #m * j == #d * (#n * (j * k)) *)
wenzelm@51717
    68
      Data.prove_conv [Data.norm_tac ctxt] ctxt prems
wenzelm@20114
    69
        (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
paulson@10537
    70
  in
wenzelm@51717
    71
    Option.map (export o Data.simplify_meta_eq ctxt)
wenzelm@20114
    72
      (Data.prove_conv
wenzelm@60754
    73
         [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1,
wenzelm@51717
    74
          Data.numeral_simp_tac ctxt] ctxt prems (t', rhs))
paulson@10537
    75
  end
wenzelm@20114
    76
  (* FIXME avoid handling of generic exceptions *)
skalberg@15531
    77
  handle TERM _ => NONE
skalberg@15531
    78
       | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
wenzelm@20114
    79
                             Undeclared type constructor "Numeral.bin"*)
paulson@10537
    80
paulson@10537
    81
end;