make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests

--- a/src/HOL/Tools/arith_data.ML	Thu Jul 19 22:21:59 2012 +0200
+++ b/src/HOL/Tools/arith_data.ML	Fri Jul 20 10:53:25 2012 +0200
@@ -112,7 +112,8 @@
 
 fun simp_all_tac rules =
   let val ss0 = HOL_ss addsimps rules
-  in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
+      val safe_simp_tac = generic_simp_tac true (false, false, false)
+  in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 fun simplify_meta_eq rules =
   let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}

--- a/src/HOL/Tools/nat_arith.ML	Thu Jul 19 22:21:59 2012 +0200
+++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 20 10:53:25 2012 +0200
@@ -49,13 +49,11 @@
 struct
   val mk_sum = mk_norm_sum;
   val dest_sum = dest_sum;
-  val prove_conv = Arith_Data.prove_conv2;
+  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
     @{thm Nat.add_0}, @{thm Nat.add_0_right}];
   val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
-  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
-    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
 end;
 
 structure EqCancelSums = CancelSumsFun
@@ -63,7 +61,7 @@
   open CommonCancelSums;
   val mk_bal = HOLogic.mk_eq;
   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
+  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
 end);
 
 structure LessCancelSums = CancelSumsFun
@@ -71,7 +69,7 @@
   open CommonCancelSums;
   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
+  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
 end);
 
 structure LeCancelSums = CancelSumsFun
@@ -79,7 +77,7 @@
   open CommonCancelSums;
   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
+  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
 end);
 
 structure DiffCancelSums = CancelSumsFun
@@ -87,7 +85,7 @@
   open CommonCancelSums;
   val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
   val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
-  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
+  val cancel_rule = mk_meta_eq @{thm diff_cancel};
 end);
 
 val nat_cancel_sums_add =

--- a/src/HOL/ex/Simproc_Tests.thy	Thu Jul 19 22:21:59 2012 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Jul 20 10:53:25 2012 +0200
@@ -5,14 +5,14 @@
 header {* Testing of arithmetic simprocs *}
 
 theory Simproc_Tests
-imports (*Main*) "../Numeral_Simprocs"
+imports Main
 begin
 
 text {*
-  This theory tests the various simprocs defined in
-  @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
-  are derived from commented-out code originally found in
-  @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
+  This theory tests the various simprocs defined in @{file
+  "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
+  Many of the tests are derived from commented-out code originally
+  found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
 *}
 
 subsection {* ML bindings *}
@@ -21,6 +21,29 @@
   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
 *}
 
+subsection {* Cancellation simprocs from @{text Nat.thy} *}
+
+notepad begin
+  fix a b c d :: nat
+  {
+    assume "b = Suc c" have "a + b = Suc (c + a)"
+      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact
+  next
+    assume "b < Suc c" have "a + b < Suc (c + a)"
+      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact
+  next
+    assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
+      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact
+  next
+    assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
+      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact
+  }
+end
+
+schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
+  by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0)
+(* TODO: test more simprocs with schematic variables *)
+
 subsection {* Abelian group cancellation simprocs *}
 
 notepad begin

--- a/src/Provers/Arith/cancel_sums.ML	Thu Jul 19 22:21:59 2012 +0200
+++ b/src/Provers/Arith/cancel_sums.ML	Fri Jul 20 10:53:25 2012 +0200
@@ -13,12 +13,12 @@
   (*abstract syntax*)
   val mk_sum: term list -> term
   val dest_sum: term -> term list
+  val mk_plus: term * term -> term
   val mk_bal: term * term -> term
   val dest_bal: term -> term * term
   (*rules*)
-  val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
   val norm_tac: simpset -> tactic            (*AC0 etc.*)
-  val uncancel_tac: cterm -> tactic          (*apply A ~~ B  ==  x + A ~~ x + B*)
+  val cancel_rule: thm                       (* x + A ~~ x + B == A ~~ B *)
 end;
 
 signature CANCEL_SUMS =
@@ -46,14 +46,6 @@
       | GREATER => cons2 u (cancel (t :: ts) us vs));
 
 
-(* uncancel *)
-
-fun uncancel_sums_tac _ [] = all_tac
-  | uncancel_sums_tac thy (t :: ts) =
-      Data.uncancel_tac (Thm.cterm_of thy t) THEN
-      uncancel_sums_tac thy ts;
-
-
 (* the simplification procedure *)
 
 fun proc ss t =
@@ -66,9 +58,21 @@
         val (ts', us', vs) = cancel ts us [];
       in
         if null vs then NONE
-        else SOME
-          (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss
-            (t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
+        else
+          let
+            val cert = Thm.cterm_of thy
+            val t' = Data.mk_sum ts'
+            val u' = Data.mk_sum us'
+            val v = Data.mk_sum vs
+            val t1 = Data.mk_bal (Data.mk_plus (v, t'), Data.mk_plus (v, u'))
+            val t2 = Data.mk_bal (t', u')
+            val goal1 = Thm.cterm_of thy (Logic.mk_equals (t, t1))
+            val goal2 = Thm.cterm_of thy (Logic.mk_equals (t1, t2))
+            val thm1 = Goal.prove_internal [] goal1 (K (Data.norm_tac ss))
+            val thm2 = Goal.prove_internal [] goal2 (K (rtac Data.cancel_rule 1))
+          in
+            SOME (Thm.transitive thm1 thm2)
+          end
       end);
 
 end;