# HG changeset patch
# User huffman
# Date 1241062432 25200
# Node ID 020efcbfe2d84d8a37162947018437a883ecc972
# Parent  6d2188134536e38439731ef8ac763063f8fe71cc
add semiring_assoc_fold simproc for unsigned numerals

diff -r 6d2188134536 -r 020efcbfe2d8 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Wed Apr 29 17:57:16 2009 -0700
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 20:33:52 2009 -0700
@@ -911,7 +911,7 @@
 
 subsection {* Simplification Procedures *}
 
-text {* Reorientation of equalities *}
+subsubsection {* Reorientation of equalities *}
 
 setup {*
   ReorientProc.add
@@ -923,6 +923,51 @@
 
 simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
 
+subsubsection {* Constant folding for multiplication in semirings *}
+
+context semiring_numeral
+begin
+
+lemma mult_of_num_commute: "x * of_num n = of_num n * x"
+by (induct n)
+  (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right)
+
+definition
+  "commutes_with a b \<longleftrightarrow> a * b = b * a"
+
+lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a"
+unfolding commutes_with_def .
+
+lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)"
+unfolding commutes_with_def by (simp only: mult_assoc [symmetric])
+
+lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x"
+unfolding commutes_with_def by (simp_all add: mult_of_num_commute)
+
+lemmas mult_ac_numeral =
+  mult_assoc
+  commutes_with_commute
+  commutes_with_left_commute
+  commutes_with_numeral
+
+end
+
+ML {*
+structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
+struct
+  val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral}
+  val eq_reflection = eq_reflection
+  fun is_numeral (Const(@{const_name of_num}, _) $ _) = true
+    | is_numeral _ = false;
+end;
+
+structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
+*}
+
+simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") =
+  {* fn phi => fn ss => fn ct =>
+    Semiring_Times_Assoc.proc ss (Thm.term_of ct) *}
+
 
 subsection {* Toy examples *}