src/Provers/Arith/cancel_numerals.ML
changeset 20114 a1bb4bc68ff3
parent 20044 92cc2f4c7335
child 24630 351a308ab58d
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Wed Jul 12 21:19:14 2006 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Wed Jul 12 21:19:17 2006 +0200
     1.3 @@ -36,8 +36,7 @@
     1.4    val bal_add1: thm
     1.5    val bal_add2: thm
     1.6    (*proof tools*)
     1.7 -  val prove_conv: tactic list -> Proof.context ->
     1.8 -                  thm list -> string list -> term * term -> thm option
     1.9 +  val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    1.10    val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
    1.11    val norm_tac: simpset -> tactic                (*proves the initial lemma*)
    1.12    val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
    1.13 @@ -69,41 +68,41 @@
    1.14  (*the simplification procedure*)
    1.15  fun proc ss t =
    1.16    let
    1.17 -      val ctxt = Simplifier.the_context ss;
    1.18 -      val hyps = prems_of_ss ss;
    1.19 -      (*first freeze any Vars in the term to prevent flex-flex problems*)
    1.20 -      val (t', xs) = Term.adhoc_freeze_vars t;
    1.21 -      val (t1,t2) = Data.dest_bal t'
    1.22 -      val terms1 = Data.dest_sum t1
    1.23 -      and terms2 = Data.dest_sum t2
    1.24 -      val u = find_common (terms1,terms2)
    1.25 -      val (n1, terms1') = Data.find_first_coeff u terms1
    1.26 -      and (n2, terms2') = Data.find_first_coeff u terms2
    1.27 -      and T = Term.fastype_of u
    1.28 -      fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
    1.29 -      val reshape =  (*Move i*u to the front and put j*u into standard form
    1.30 +    val ctxt = Simplifier.the_context ss
    1.31 +    val prems = prems_of_ss ss
    1.32 +    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
    1.33 +    val export = singleton (Variable.export ctxt' ctxt)
    1.34 +
    1.35 +    val (t1,t2) = Data.dest_bal t'
    1.36 +    val terms1 = Data.dest_sum t1
    1.37 +    and terms2 = Data.dest_sum t2
    1.38 +
    1.39 +    val u = find_common (terms1, terms2)
    1.40 +    val (n1, terms1') = Data.find_first_coeff u terms1
    1.41 +    and (n2, terms2') = Data.find_first_coeff u terms2
    1.42 +    and T = Term.fastype_of u
    1.43 +
    1.44 +    fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms)
    1.45 +    val reshape =  (*Move i*u to the front and put j*u into standard form
    1.46                         i + #m + j + k == #m + i + (j + k) *)
    1.47 -            if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.48 -                raise TERM("cancel_numerals", [])
    1.49 -            else Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
    1.50 -                        (t',
    1.51 -                         Data.mk_bal (newshape(n1,terms1'),
    1.52 -                                      newshape(n2,terms2')))
    1.53 +        if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
    1.54 +          raise TERM("cancel_numerals", [])
    1.55 +        else Data.prove_conv [Data.norm_tac ss] ctxt prems
    1.56 +          (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2')))
    1.57    in
    1.58 -      Option.map (Data.simplify_meta_eq ss)
    1.59 -       (if n2<=n1 then
    1.60 -            Data.prove_conv
    1.61 -               [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.62 -                Data.numeral_simp_tac ss] ctxt hyps xs
    1.63 -               (t', Data.mk_bal (newshape(n1-n2,terms1'),
    1.64 -                                 Data.mk_sum T terms2'))
    1.65 -        else
    1.66 -            Data.prove_conv
    1.67 -               [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    1.68 -                Data.numeral_simp_tac ss] ctxt hyps xs
    1.69 -               (t', Data.mk_bal (Data.mk_sum T terms1',
    1.70 -                                 newshape(n2-n1,terms2'))))
    1.71 +    Option.map (export o Data.simplify_meta_eq ss)
    1.72 +      (if n2 <= n1 then
    1.73 +         Data.prove_conv
    1.74 +           [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
    1.75 +            Data.numeral_simp_tac ss] ctxt prems
    1.76 +           (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2'))
    1.77 +       else
    1.78 +         Data.prove_conv
    1.79 +           [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
    1.80 +            Data.numeral_simp_tac ss] ctxt prems
    1.81 +           (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2'))))
    1.82    end
    1.83 +  (* FIXME avoid handling of generic exceptions *)
    1.84    handle TERM _ => NONE
    1.85         | TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
    1.86                               Undeclared type constructor "Numeral.bin"*)