1.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 29 17:57:16 2009 -0700
     1.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 20:33:52 2009 -0700
     1.3 @@ -911,7 +911,7 @@
     1.4  
     1.5  subsection {* Simplification Procedures *}
     1.6  
     1.7 -text {* Reorientation of equalities *}
     1.8 +subsubsection {* Reorientation of equalities *}
     1.9  
    1.10  setup {*
    1.11    ReorientProc.add
    1.12 @@ -923,6 +923,51 @@
    1.13  
    1.14  simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
    1.15  
    1.16 +subsubsection {* Constant folding for multiplication in semirings *}
    1.17 +
    1.18 +context semiring_numeral
    1.19 +begin
    1.20 +
    1.21 +lemma mult_of_num_commute: "x * of_num n = of_num n * x"
    1.22 +by (induct n)
    1.23 +  (simp_all only: of_num.simps left_distrib right_distrib mult_1_left mult_1_right)
    1.24 +
    1.25 +definition
    1.26 +  "commutes_with a b \<longleftrightarrow> a * b = b * a"
    1.27 +
    1.28 +lemma commutes_with_commute: "commutes_with a b \<Longrightarrow> a * b = b * a"
    1.29 +unfolding commutes_with_def .
    1.30 +
    1.31 +lemma commutes_with_left_commute: "commutes_with a b \<Longrightarrow> a * (b * c) = b * (a * c)"
    1.32 +unfolding commutes_with_def by (simp only: mult_assoc [symmetric])
    1.33 +
    1.34 +lemma commutes_with_numeral: "commutes_with x (of_num n)" "commutes_with (of_num n) x"
    1.35 +unfolding commutes_with_def by (simp_all add: mult_of_num_commute)
    1.36 +
    1.37 +lemmas mult_ac_numeral =
    1.38 +  mult_assoc
    1.39 +  commutes_with_commute
    1.40 +  commutes_with_left_commute
    1.41 +  commutes_with_numeral
    1.42 +
    1.43 +end
    1.44 +
    1.45 +ML {*
    1.46 +structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
    1.47 +struct
    1.48 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral}
    1.49 +  val eq_reflection = eq_reflection
    1.50 +  fun is_numeral (Const(@{const_name of_num}, _) $ _) = true
    1.51 +    | is_numeral _ = false;
    1.52 +end;
    1.53 +
    1.54 +structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
    1.55 +*}
    1.56 +
    1.57 +simproc_setup semiring_assoc_fold' ("(a::'a::semiring_numeral) * b") =
    1.58 +  {* fn phi => fn ss => fn ct =>
    1.59 +    Semiring_Times_Assoc.proc ss (Thm.term_of ct) *}
    1.60 +
    1.61  
    1.62  subsection {* Toy examples *}
    1.63