# HG changeset patch
# User huffman
# Date 1320849214 -3600
# Node ID 1006cba234e3be5682a8bfe4e3c5c473d7cc0eb9
# Parent  958d19d3405bf152ab01dbc8c379956249f9b064# Parent  d17556b9a89bb38d390e575bae21cf20104266f7
merged

diff -r d17556b9a89b -r 1006cba234e3 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 11:35:09 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 15:33:34 2011 +0100
@@ -103,8 +103,8 @@
   {* fn phi => Numeral_Simprocs.combine_numerals *}
 
 simproc_setup field_combine_numerals
-  ("(i::'a::{field_inverse_zero, number_ring}) + j"
-  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
+  ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
+  |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
 
 simproc_setup inteq_cancel_numerals
@@ -141,8 +141,8 @@
   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
 
 simproc_setup ring_eq_cancel_numeral_factor
-  ("(l::'a::{idom,number_ring}) * m = n"
-  |"(l::'a::{idom,number_ring}) = m * n") =
+  ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
+  |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
 
 simproc_setup ring_less_cancel_numeral_factor
@@ -156,14 +156,14 @@
   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
 
 simproc_setup int_div_cancel_numeral_factors
-  ("((l::'a::{semiring_div,number_ring}) * m) div n"
-  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
+  ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
+  |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
 
 simproc_setup divide_cancel_numeral_factor
-  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
-  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
-  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
+  ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
+  |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
+  |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
 
 simproc_setup ring_eq_cancel_factor
@@ -202,6 +202,30 @@
 
 use "Tools/nat_numeral_simprocs.ML"
 
+simproc_setup nateq_cancel_numerals
+  ("(l::nat) + m = n" | "(l::nat) = m + n" |
+   "(l::nat) * m = n" | "(l::nat) = m * n" |
+   "Suc m = n" | "m = Suc n") =
+  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *}
+
+simproc_setup natless_cancel_numerals
+  ("(l::nat) + m < n" | "(l::nat) < m + n" |
+   "(l::nat) * m < n" | "(l::nat) < m * n" |
+   "Suc m < n" | "m < Suc n") =
+  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *}
+
+simproc_setup natle_cancel_numerals
+  ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
+   "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
+   "Suc m \<le> n" | "m \<le> Suc n") =
+  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *}
+
+simproc_setup natdiff_cancel_numerals
+  ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
+   "(l::nat) * m - n" | "(l::nat) - m * n" |
+   "Suc m - n" | "m - Suc n") =
+  {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
+
 declaration {* 
   K (Lin_Arith.add_simps (@{thms neg_simps} @ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}])
   #> Lin_Arith.add_simps (@{thms ring_distribs} @ [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1},
@@ -222,7 +246,12 @@
        @{simproc inteq_cancel_numerals},
        @{simproc intless_cancel_numerals},
        @{simproc intle_cancel_numerals}]
-  #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
+  #> Lin_Arith.add_simprocs
+      [Nat_Numeral_Simprocs.combine_numerals,
+       @{simproc nateq_cancel_numerals},
+       @{simproc natless_cancel_numerals},
+       @{simproc natle_cancel_numerals},
+       @{simproc natdiff_cancel_numerals}])
 *}
 
 end
diff -r d17556b9a89b -r 1006cba234e3 src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Nov 09 11:35:09 2011 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Nov 09 15:33:34 2011 +0100
@@ -6,7 +6,10 @@
 signature NAT_NUMERAL_SIMPROCS =
 sig
   val combine_numerals: simproc
-  val cancel_numerals: simproc list
+  val eq_cancel_numerals: simpset -> cterm -> thm option
+  val less_cancel_numerals: simpset -> cterm -> thm option
+  val le_cancel_numerals: simpset -> cterm -> thm option
+  val diff_cancel_numerals: simpset -> cterm -> thm option
   val cancel_factors: simproc list
   val cancel_numeral_factors: simproc list
 end;
@@ -195,29 +198,10 @@
   val bal_add2 = @{thm nat_diff_add_eq2} RS trans
 );
 
-
-val cancel_numerals =
-  map (Numeral_Simprocs.prep_simproc @{theory})
-   [("nateq_cancel_numerals",
-     ["(l::nat) + m = n", "(l::nat) = m + n",
-      "(l::nat) * m = n", "(l::nat) = m * n",
-      "Suc m = n", "m = Suc n"],
-     K EqCancelNumerals.proc),
-    ("natless_cancel_numerals",
-     ["(l::nat) + m < n", "(l::nat) < m + n",
-      "(l::nat) * m < n", "(l::nat) < m * n",
-      "Suc m < n", "m < Suc n"],
-     K LessCancelNumerals.proc),
-    ("natle_cancel_numerals",
-     ["(l::nat) + m <= n", "(l::nat) <= m + n",
-      "(l::nat) * m <= n", "(l::nat) <= m * n",
-      "Suc m <= n", "m <= Suc n"],
-     K LeCancelNumerals.proc),
-    ("natdiff_cancel_numerals",
-     ["((l::nat) + m) - n", "(l::nat) - (m + n)",
-      "(l::nat) * m - n", "(l::nat) - m * n",
-      "Suc m - n", "m - Suc n"],
-     K DiffCancelNumerals.proc)];
+fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct)
+fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct)
+fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct)
+fun diff_cancel_numerals ss ct = DiffCancelNumerals.proc ss (term_of ct)
 
 
 (*** Applying CombineNumeralsFun ***)
@@ -424,7 +408,6 @@
 end;
 
 
-Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
 Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
@@ -436,57 +419,6 @@
 set simp_trace;
 fun test s = (Goal s; by (Simp_tac 1));
 
-(*cancel_numerals*)
-test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
-test "(2*length xs < 2*length xs + j)";
-test "(2*length xs < length xs * 2 + j)";
-test "2*u = (u::nat)";
-test "2*u = Suc (u)";
-test "(i + j + 12 + (k::nat)) - 15 = y";
-test "(i + j + 12 + (k::nat)) - 5 = y";
-test "Suc u - 2 = y";
-test "Suc (Suc (Suc u)) - 2 = y";
-test "(i + j + 2 + (k::nat)) - 1 = y";
-test "(i + j + 1 + (k::nat)) - 2 = y";
-
-test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
-test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
-test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
-test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
-test "Suc ((u*v)*4) - v*3*u = w";
-test "Suc (Suc ((u*v)*3)) - v*3*u = w";
-
-test "(i + j + 12 + (k::nat)) = u + 15 + y";
-test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
-test "(i + j + 12 + (k::nat)) = u + 5 + y";
-(*Suc*)
-test "(i + j + 12 + k) = Suc (u + y)";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
-test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
-test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
-test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
-test "2*y + 3*z + 2*u = Suc (u)";
-test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
-test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)";
-test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
-test "(2*n*m) < (3*(m*n)) + (u::nat)";
-
-test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
- 
-test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
-
-test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
-
-test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
-
-
-(*negative numerals: FAIL*)
-test "(i + j + -23 + (k::nat)) < u + 15 + y";
-test "(i + j + 3 + (k::nat)) < u + -15 + y";
-test "(i + j + -12 + (k::nat)) - 15 = y";
-test "(i + j + 12 + (k::nat)) - -15 = y";
-test "(i + j + -12 + (k::nat)) - -15 = y";
-
 (*combine_numerals*)
 test "k + 3*k = (u::nat)";
 test "Suc (i + 3) = u";
diff -r d17556b9a89b -r 1006cba234e3 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 09 11:35:09 2011 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 09 15:33:34 2011 +0100
@@ -178,6 +178,17 @@
 val add_0s =  @{thms add_0s};
 val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
 
+(* For post-simplification of the rhs of simproc-generated rules *)
+val post_simps =
+    [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
+     @{thm add_0_left}, @{thm add_0_right},
+     @{thm mult_zero_left}, @{thm mult_zero_right},
+     @{thm mult_1_left}, @{thm mult_1_right},
+     @{thm mult_minus1}, @{thm mult_minus1_right}]
+
+val field_post_simps =
+    post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
+                      
 (*Simplify inverse Numeral1, a/Numeral1*)
 val inverse_1s = [@{thm inverse_numeral_1}];
 val divide_1s = [@{thm divide_numeral_1}];
@@ -235,7 +246,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
   val prove_conv = Arith_Data.prove_conv
 end;
 
@@ -287,7 +298,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
 end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
@@ -314,7 +325,7 @@
 
   val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
-  val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s)
+  val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
 end;
 
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
@@ -356,8 +367,7 @@
     [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   val simplify_meta_eq = Arith_Data.simplify_meta_eq
-    [@{thm Nat.add_0}, @{thm Nat.add_0_right}, @{thm mult_zero_left},
-      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
+    ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
   val prove_conv = Arith_Data.prove_conv
 end
 
diff -r d17556b9a89b -r 1006cba234e3 src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 11:35:09 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 15:33:34 2011 +0100
@@ -24,323 +24,305 @@
 
 subsection {* @{text int_combine_numerals} *}
 
-lemma assumes "10 + (2 * l + oo) = uu"
-  shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-3 + (i + (j + k)) = y"
-  shows "(i + j + 12 + (k::int)) - 15 = y"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "7 + (i + (j + k)) = y"
-  shows "(i + j + 12 + (k::int)) - 5 = y"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-4 * (u * v) + (2 * x + y) = w"
-  shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
-  shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
-  shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
-  shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "Numeral0 * b + (a + - c) = d"
-  shows "a + -(b+c) + b = (d::int)"
-apply (simp only: minus_add_distrib)
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-2 * b + (a + - c) = d"
-  shows "a + -(b+c) - b = (d::int)"
-apply (simp only: minus_add_distrib)
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
-  shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "-27 + (i + (j + k)) = y"
-  shows "(i + j + -12 + (k::int)) - 15 = y"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "27 + (i + (j + k)) = y"
-  shows "(i + j + 12 + (k::int)) - -15 = y"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
-lemma assumes "3 + (i + (j + k)) = y"
-  shows "(i + j + -12 + (k::int)) - -15 = y"
-by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
-
+notepad begin
+  fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
+  {
+    assume "10 + (2 * l + oo) = uu"
+    have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-3 + (i + (j + k)) = y"
+    have "(i + j + 12 + k) - 15 = y"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "7 + (i + (j + k)) = y"
+    have "(i + j + 12 + k) - 5 = y"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-4 * (u * v) + (2 * x + y) = w"
+    have "(2*x - (u*v) + y) - v*3*u = w"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "2 * x * u * v + y = w"
+    have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "3 * (u * v) + (2 * x * u * v + y) = w"
+    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
+    have "u*v - (x*u*v + (u*v)*4 + y) = w"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "a + - c = d"
+    have "a + -(b+c) + b = d"
+      apply (simp only: minus_add_distrib)
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-2 * b + (a + - c) = d"
+    have "a + -(b+c) - b = d"
+      apply (simp only: minus_add_distrib)
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-7 + (i + (j + (k + (- u + - y)))) = z"
+    have "(i + j + -2 + k) - (u + 5 + y) = z"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "-27 + (i + (j + k)) = y"
+    have "(i + j + -12 + k) - 15 = y"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "27 + (i + (j + k)) = y"
+    have "(i + j + 12 + k) - -15 = y"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  next
+    assume "3 + (i + (j + k)) = y"
+    have "(i + j + -12 + k) - -15 = y"
+      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
+  }
+end
 
 subsection {* @{text inteq_cancel_numerals} *}
 
-lemma assumes "u = Numeral0" shows "2*u = (u::int)"
-by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
+notepad begin
+  fix i j k u vv w y z w' y' z' :: "'a::number_ring"
+  {
+    assume "u = 0" have "2*u = u"
+      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
-
-lemma assumes "i + (j + k) = 3 + (u + y)"
-  shows "(i + j + 12 + (k::int)) = u + 15 + y"
-by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
-
-lemma assumes "7 + (j + (i + k)) = y"
-  shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
-by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
-
-lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
-  shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
-by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
-
+  next
+    assume "i + (j + k) = 3 + (u + y)"
+    have "(i + j + 12 + k) = u + 15 + y"
+      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
+  next
+    assume "7 + (j + (i + k)) = y"
+    have "(i + j*2 + 12 + k) = j + 5 + y"
+      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
+  next
+    assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
+    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
+      by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
+  }
+end
 
 subsection {* @{text intless_cancel_numerals} *}
 
-lemma assumes "y < 2 * b" shows "y - b < (b::int)"
-by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
-
-lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
-by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
-
-lemma assumes "i + (j + k) < 8 + (u + y)"
-  shows "(i + j + -3 + (k::int)) < u + 5 + y"
-by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
-
-lemma assumes "9 + (i + (j + k)) < u + y"
-  shows "(i + j + 3 + (k::int)) < u + -6 + y"
-by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
-
+notepad begin
+  fix b c i j k u y :: "'a::{linordered_idom,number_ring}"
+  {
+    assume "y < 2 * b" have "y - b < b"
+      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
+  next
+    assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
+      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
+  next
+    assume "i + (j + k) < 8 + (u + y)"
+    have "(i + j + -3 + k) < u + 5 + y"
+      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
+  next
+    assume "9 + (i + (j + k)) < u + y"
+    have "(i + j + 3 + k) < u + -6 + y"
+      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
+  }
+end
 
 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
-lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
+notepad begin
+  fix x y :: "'a::{idom,ring_char_0,number_ring}"
+  {
+    assume "3*x = 4*y" have "9*x = 12 * y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "-3*x = 4*y" have "-99*x = 132 * y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "111*x = -44*y" have "999*x = -396 * y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "11*x = 9*y" have "-99*x = -81 * y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "2*x = y" have "-2 * x = -1 * y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "2*x = y" have "-2 * x = -y"
+      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
+  }
+end
 
 subsection {* @{text int_div_cancel_numeral_factors} *}
 
-lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
-by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
-
-lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
-by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
-
-lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
-by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
-
-lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
-by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
-
-lemma assumes "(2*x) div (Numeral1*y) = z"
-  shows "(-2 * x) div (-1 * (y::int)) = z"
-by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
-
+notepad begin
+  fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}"
+  {
+    assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
+      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
+  next
+    assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
+      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
+  next
+    assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
+      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
+  next
+    assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
+      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
+  next
+    assume "(2*x) div y = z"
+    have "(-2 * x) div (-1 * y) = z"
+      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
+  }
+end
 
 subsection {* @{text ring_less_cancel_numeral_factor} *}
 
-lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
-lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
-by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
-
+notepad begin
+  fix x y :: "'a::{linordered_idom,number_ring}"
+  {
+    assume "3*x < 4*y" have "9*x < 12 * y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "-3*x < 4*y" have "-99*x < 132 * y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "111*x < -44*y" have "999*x < -396 * y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "9*y < 11*x" have "-99*x < -81 * y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "y < 2*x" have "-2 * x < -y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "23*y < x" have "-x < -23 * y"
+      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
+  }
+end
 
 subsection {* @{text ring_le_cancel_numeral_factor} *}
 
-lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
-by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
-
-
-subsection {* @{text ring_eq_cancel_numeral_factor} *}
-
-lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
-lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
-
+notepad begin
+  fix x y :: "'a::{linordered_idom,number_ring}"
+  {
+    assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "23*y \<le> x" have "-x \<le> -23 * y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "y \<le> 0" have "0 \<le> y * -2"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
+      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
+  }
+end
 
 subsection {* @{text divide_cancel_numeral_factor} *}
 
-lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
-by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
-
-lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z"
-by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
-
-lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z"
-by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
-
-lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z"
-by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
-
-lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z"
-by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
-
+notepad begin
+  fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
+  {
+    assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
+      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
+  next
+    assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
+      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
+  next
+    assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
+      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
+  next
+    assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
+      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
+  next
+    assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
+      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
+  }
+end
 
 subsection {* @{text ring_eq_cancel_factor} *}
 
-lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
-lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
-by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
-
+notepad begin
+  fix a b c d k x y :: "'a::idom"
+  {
+    assume "k = 0 \<or> x = y" have "x*k = k*y"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> 1 = y" have "k = k*y"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  next
+    assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  next
+    assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> x = y" have "x*k = k*y"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  next
+    assume "k = 0 \<or> 1 = y" have "k = k*y"
+      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
+  }
+end
 
 subsection {* @{text int_div_cancel_factor} *}
 
-lemma assumes "(if k = 0 then 0 else x div y) = uu"
-  shows "(x*k) div (k*(y::int)) = (uu::int)"
-by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
-
-lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
-  shows "(k) div (k*(y::int)) = (uu::int)"
-by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
-
-lemma assumes "(if b = 0 then 0 else a * c) = uu"
-  shows "(a*(b*c)) div ((b::int)) = (uu::int)"
-by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
-
-lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
-  shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
-by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
-
+notepad begin
+  fix a b c d k uu x y :: "'a::semiring_div"
+  {
+    assume "(if k = 0 then 0 else x div y) = uu"
+    have "(x*k) div (k*y) = uu"
+      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
+  next
+    assume "(if k = 0 then 0 else 1 div y) = uu"
+    have "(k) div (k*y) = uu"
+      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
+  next
+    assume "(if b = 0 then 0 else a * c) = uu"
+    have "(a*(b*c)) div b = uu"
+      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
+  next
+    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
+    have "(a*(b*c)) div (d*b*(x*a)) = uu"
+      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
+  }
+end
 
 subsection {* @{text divide_cancel_factor} *}
 
-lemma assumes "(if k = 0 then 0 else x / y) = uu"
-  shows "(x*k) / (k*(y::rat)) = (uu::rat)"
-by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
-
-lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
-  shows "(k) / (k*(y::rat)) = (uu::rat)"
-by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
-
-lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
-  shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
-by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
-
-lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
-  shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
-by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
+notepad begin
+  fix a b c d k uu x y :: "'a::field_inverse_zero"
+  {
+    assume "(if k = 0 then 0 else x / y) = uu"
+    have "(x*k) / (k*y) = uu"
+      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
+  next
+    assume "(if k = 0 then 0 else 1 / y) = uu"
+    have "(k) / (k*y) = uu"
+      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
+  next
+    assume "(if b = 0 then 0 else a * c / 1) = uu"
+    have "(a*(b*c)) / b = uu"
+      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
+  next
+    assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
+    have "(a*(b*c)) / (d*b*(x*a)) = uu"
+      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
+  }
+end
 
 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
 oops -- "FIXME: need simproc to cover this case"
@@ -348,41 +330,234 @@
 
 subsection {* @{text linordered_ring_less_cancel_factor} *}
 
-lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
-by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
-
-lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
-by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
-
-lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
-by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
-
-lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
-by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
-
+notepad begin
+  fix x y z :: "'a::linordered_idom"
+  {
+    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
+      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  next
+    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
+      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  next
+    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
+      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  next
+    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
+      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
+  }
+end
 
 subsection {* @{text linordered_ring_le_cancel_factor} *}
 
-lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
-by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
-
-lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
-by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
-
+notepad begin
+  fix x y z :: "'a::linordered_idom"
+  {
+    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
+      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
+  next
+    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
+      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
+  }
+end
 
 subsection {* @{text field_combine_numerals} *}
 
-lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
-by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
-
-lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
-by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
-
-lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
-by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+notepad begin
+  fix x y z uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
+  {
+    assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
+      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+  next
+    assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
+      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+  next
+    assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
+      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+  next
+    assume "y + z = uu"
+    have "x / 2 + y - 3 * x / 6 + z = uu"
+      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+  next
+    assume "1 / 15 * x + y = uu"
+    have "7 * x / 5 + y - 4 * x / 3 = uu"
+      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
+  }
+end
 
 lemma "2/3 * (x::rat) + x / 3 = uu"
 apply (tactic {* test [@{simproc field_combine_numerals}] *})?
 oops -- "FIXME: test fails"
 
+subsection {* @{text nateq_cancel_numerals} *}
+
+notepad begin
+  fix i j k l oo u uu vv w y z w' y' z' :: "nat"
+  {
+    assume "Suc 0 * u = 0" have "2*u = (u::nat)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "i + (j + k) = 3 * Suc 0 + (u + y)"
+    have "(i + j + 12 + k) = u + 15 + y"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "7 * Suc 0 + (i + (j + k)) = u + y"
+    have "(i + j + 12 + k) = u + 5 + y"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "11 * Suc 0 + (i + (j + k)) = u + y"
+    have "(i + j + 12 + k) = Suc (u + y)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "i + (j + k) = 2 * Suc 0 + (u + y)"
+    have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
+    have "2*y + 3*z + 2*u = Suc (u)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
+    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
+      2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
+    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
+      2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  next
+    assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
+    have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
+      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
+  }
 end
+
+subsection {* @{text natless_cancel_numerals} *}
+
+notepad begin
+  fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
+  fix c i j k l oo u uu vv w y z w' y' z' :: "nat"
+  {
+    assume "0 < j" have "(2*length xs < 2*length xs + j)"
+      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
+  next
+    assume "0 < j" have "(2*length xs < length xs * 2 + j)"
+      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
+  next
+    assume "i + (j + k) < u + y"
+    have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
+      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
+  next
+    assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
+      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
+  next
+    (* FIXME: negative numerals fail
+    have "(i + j + -23 + (k::nat)) < u + 15 + y"
+      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
+      sorry
+    have "(i + j + 3 + (k::nat)) < u + -15 + y"
+      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
+      sorry*)
+  }
+end
+
+subsection {* @{text natle_cancel_numerals} *}
+
+notepad begin
+  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
+  fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
+  {
+    assume "u + y \<le> 36 * Suc 0 + (i + (j + k))"
+    have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)"
+      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
+  next
+    assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0"
+    have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)"
+      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
+  next
+    assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1"
+      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
+  next
+    assume "5 + length l3 = 0"
+    have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \<le> length (compT P E A ST mxr e))"
+      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
+  next
+    assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0"
+    have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \<le> length (compT P E A ST mxr e))"
+      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
+  }
+end
+
+subsection {* @{text natdiff_cancel_numerals} *}
+
+notepad begin
+  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
+  fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
+  {
+    assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
+    have "(i + j + 2 + k) - 1 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "i + (j + k) - Suc 0 * Suc 0 = y"
+    have "(i + j + 1 + k) - 2 = y"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "2 * x + y - 2 * (u * v) = w"
+    have "(2*x + (u*v) + y) - v*3*u = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "2 * x * u * v + (5 + y) - 0 = w"
+    have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
+    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
+    have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "Suc (Suc 0 * (u * v)) - 0 = w"
+    have "Suc ((u*v)*4) - v*3*u = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
+    have "(i + j + 32 + k) - (u + 15 + y) = zz"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
+      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
+  next
+    (* FIXME: negative numerals fail
+    have "(i + j + -12 + k) - 15 = y"
+      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
+      sorry
+    have "(i + j + 12 + k) - -15 = y"
+      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
+      sorry
+    have "(i + j + -12 + k) - -15 = y"
+      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
+      sorry*)
+  }
+end
+
+end