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.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"*)
```