# HG changeset patch
# User huffman
# Date 1320849204 -3600
# Node ID 958d19d3405bf152ab01dbc8c379956249f9b064
# Parent  62bc9474d04b9a9e3a2c3d624cccab2cf931d600
tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1

diff -r 62bc9474d04b -r 958d19d3405b src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 09 11:44:42 2011 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Nov 09 15:33:24 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 62bc9474d04b -r 958d19d3405b src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 11:44:42 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 15:33:24 2011 +0100
@@ -43,7 +43,7 @@
     have "(2*x - (u*v) + y) - v*3*u = w"
       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   next
-    assume "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
+    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
@@ -55,7 +55,7 @@
     have "u*v - (x*u*v + (u*v)*4 + y) = w"
       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   next
-    assume "Numeral0 * b + (a + - c) = d"
+    assume "a + - c = d"
     have "a + -(b+c) + b = d"
       apply (simp only: minus_add_distrib)
       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
@@ -88,7 +88,7 @@
 notepad begin
   fix i j k u vv w y z w' y' z' :: "'a::number_ring"
   {
-    assume "u = Numeral0" have "2*u = u"
+    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 *)
   next
@@ -144,10 +144,10 @@
     assume "11*x = 9*y" have "-99*x = -81 * y"
       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   next
-    assume "2*x = Numeral1*y" have "-2 * x = -1 * y"
+    assume "2*x = y" have "-2 * x = -1 * y"
       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   next
-    assume "2*x = Numeral1*y" have "-2 * x = -y"
+    assume "2*x = y" have "-2 * x = -y"
       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   }
 end
@@ -169,7 +169,7 @@
     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 (Numeral1*y) = z"
+    assume "(2*x) div y = z"
     have "(-2 * x) div (-1 * y) = z"
       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   }
@@ -192,10 +192,10 @@
     assume "9*y < 11*x" have "-99*x < -81 * y"
       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   next
-    assume "Numeral1*y < 2*x" have "-2 * x < -y"
+    assume "y < 2*x" have "-2 * x < -y"
       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   next
-    assume "23*y < Numeral1*x" have "-x < -23 * y"
+    assume "23*y < x" have "-x < -23 * y"
       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   }
 end
@@ -217,16 +217,16 @@
     assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   next
-    assume "Numeral1*y \<le> 2*x" have "-2 * x \<le> -1 * y"
+    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> Numeral1*x" have "-x \<le> -23 * y"
+    assume "23*y \<le> x" have "-x \<le> -23 * y"
       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   next
-    assume "Numeral1*y \<le> Numeral0" have "0 \<le> y * -2"
+    assume "y \<le> 0" have "0 \<le> y * -2"
       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   next
-    assume "-1*x \<le> Numeral1*y" have "- (2 * x) \<le> 2*y"
+    assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   }
 end
@@ -248,7 +248,7 @@
     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) / (Numeral1*y) = z" have "(-2 * x) / (-1 * y) = z"
+    assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   }
 end
@@ -363,7 +363,7 @@
 subsection {* @{text field_combine_numerals} *}
 
 notepad begin
-  fix x uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
+  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
@@ -373,6 +373,14 @@
   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