src/Provers/Arith/combine_numerals.ML
 changeset 20114 a1bb4bc68ff3 parent 20044 92cc2f4c7335 child 23058 c722004c5a22
```--- a/src/Provers/Arith/combine_numerals.ML	Wed Jul 12 21:19:14 2006 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Wed Jul 12 21:19:17 2006 +0200
@@ -27,7 +27,7 @@
(*rules*)
val left_distrib: thm
(*proof tools*)
-  val prove_conv: tactic list -> Proof.context -> string list -> term * term -> thm option
+  val prove_conv: tactic list -> Proof.context -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic                (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic        (*proves the final theorem*)
@@ -38,56 +38,57 @@
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
val proc: simpset -> term -> thm option
-  end
+  end
=
struct

(*Remove the first occurrence of #m*u from the term list*)
fun remove (_, _, []) = (*impossible, since #m*u was found by find_repeated*)
-      raise TERM("combine_numerals: remove", [])
+      raise TERM("combine_numerals: remove", [])
| remove (m, u, t::terms) =
case try Data.dest_coeff t of
-	  SOME(n,v) => if m=n andalso u aconv v then terms
-		       else t :: remove (m, u, terms)
-	| NONE      =>  t :: remove (m, u, terms);
+          SOME(n,v) => if m=n andalso u aconv v then terms
+                       else t :: remove (m, u, terms)
+        | NONE      =>  t :: remove (m, u, terms);

(*a left-to-right scan of terms, seeking another term of the form #n*u, where
#m*u is already in terms for some m*)
-fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
+fun find_repeated (tab, _, []) = raise TERM("find_repeated", [])
| find_repeated (tab, past, t::terms) =
case try Data.dest_coeff t of
-	  SOME(n,u) =>
-	      (case Termtab.lookup tab u of
-		  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
-		| NONE => find_repeated (Termtab.update (u, n) tab,
-					 t::past,  terms))
-	| NONE => find_repeated (tab, t::past, terms);
+          SOME(n,u) =>
+              (case Termtab.lookup tab u of
+                  SOME m => (u, m, n, rev (remove (m,u,past)) @ terms)
+                | NONE => find_repeated (Termtab.update (u, n) tab,
+                                         t::past,  terms))
+        | NONE => find_repeated (tab, t::past, terms);

(*the simplification procedure*)
fun proc ss t =
let
-      val ctxt = Simplifier.the_context ss;
-      (*first freeze any Vars in the term to prevent flex-flex problems*)
-      val (t', xs) = Term.adhoc_freeze_vars t
-      val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
-      val T = Term.fastype_of u
-      val reshape =  (*Move i*u to the front and put j*u into standard form
-		       i + #m + j + k == #m + i + (j + k) *)
-	    if m=0 orelse n=0 then   (*trivial, so do nothing*)
-		raise TERM("combine_numerals", [])
-	    else Data.prove_conv [Data.norm_tac ss] ctxt xs
-			(t',
-			 Data.mk_sum T ([Data.mk_coeff(m,u),
-				         Data.mk_coeff(n,u)] @ terms))
+    val ctxt = Simplifier.the_context ss;
+    val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    val export = singleton (Variable.export ctxt' ctxt)
+
+    val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
+    val T = Term.fastype_of u
+
+    val reshape =  (*Move i*u to the front and put j*u into standard form
+                       i + #m + j + k == #m + i + (j + k) *)
+      if m=0 orelse n=0 then   (*trivial, so do nothing*)
+        raise TERM("combine_numerals", [])
+      else Data.prove_conv [Data.norm_tac ss] ctxt
+        (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms))
in
-      Option.map (Data.simplify_meta_eq ss)
-	 (Data.prove_conv
-	    [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
-	     Data.numeral_simp_tac ss] ctxt xs
-	    (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
+    Option.map (export o Data.simplify_meta_eq ss)
+      (Data.prove_conv
+         [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+          Data.numeral_simp_tac ss] ctxt
+         (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
+  (* FIXME avoid handling of generic exceptions *)
handle TERM _ => NONE
| TYPE _ => NONE;   (*Typically (if thy doesn't include Numeral)
-			     Undeclared type constructor "Numeral.bin"*)
+                             Undeclared type constructor "Numeral.bin"*)

end;```