src/Provers/Arith/combine_numerals.ML
changeset 8799 89e9deef4bcb
parent 8774 ad5026ff0c16
child 8816 31b4fb3d8d60
--- a/src/Provers/Arith/combine_numerals.ML	Fri May 05 17:49:34 2000 +0200
+++ b/src/Provers/Arith/combine_numerals.ML	Fri May 05 17:49:54 2000 +0200
@@ -27,9 +27,10 @@
   val left_distrib: thm
   (*proof tools*)
   val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
-  val subst_tac: thm option -> tactic
-  val norm_tac: tactic
-  val numeral_simp_tac: tactic
+  val trans_tac: thm option -> tactic (*applies the initial lemma*)
+  val norm_tac: tactic                (*proves the initial lemma*)
+  val numeral_simp_tac: tactic        (*proves the final theorem*)
+  val simplify_meta_eq: thm -> thm    (*simplifies the final theorem*)
 end;
 
 
@@ -76,10 +77,11 @@
 			 Data.mk_sum ([Data.mk_coeff(m,u),
 				       Data.mk_coeff(n,u)] @ terms))
   in
-      Data.prove_conv 
-        [Data.subst_tac reshape, rtac Data.left_distrib 1,
-	 Data.numeral_simp_tac] sg
-	(t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms))
+      apsome Data.simplify_meta_eq
+	 (Data.prove_conv 
+	    [Data.trans_tac reshape, rtac Data.left_distrib 1,
+	     Data.numeral_simp_tac] sg
+	    (t, Data.mk_sum (Data.mk_coeff(m+n,u) :: terms)))
   end
   handle TERM _ => None
        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)