src/Provers/Arith/cancel_numerals.ML
changeset 8799 89e9deef4bcb
parent 8779 2d4afbc46801
child 9191 300bd596d696
--- a/src/Provers/Arith/cancel_numerals.ML	Fri May 05 17:49:34 2000 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Fri May 05 17:49:54 2000 +0200
@@ -37,9 +37,10 @@
   val bal_add2: 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;
 
 
@@ -85,16 +86,17 @@
 				      newshape(n2,terms2')))
   in
 
-      if n2<=n1 then 
-	  Data.prove_conv 
-	     [Data.subst_tac reshape, rtac Data.bal_add1 1,
-	      Data.numeral_simp_tac] sg
-	     (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
-      else
-	  Data.prove_conv 
-	     [Data.subst_tac reshape, rtac Data.bal_add2 1,
-	      Data.numeral_simp_tac] sg
-	     (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))
+      apsome Data.simplify_meta_eq
+       (if n2<=n1 then 
+	    Data.prove_conv 
+	       [Data.trans_tac reshape, rtac Data.bal_add1 1,
+		Data.numeral_simp_tac] sg
+	       (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
+	else
+	    Data.prove_conv 
+	       [Data.trans_tac reshape, rtac Data.bal_add2 1,
+		Data.numeral_simp_tac] sg
+	       (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2'))))
   end
   handle TERM _ => None
        | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)