src/HOL/Computational_Algebra/Factorial_Ring.thy
changeset 66938 c78ff0aeba4c
parent 66453 cc19f7ca2ed6
child 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
     1.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Oct 30 13:18:44 2017 +0000
     1.3 @@ -1424,7 +1424,7 @@
     1.4    define A where "A = Abs_multiset f"
     1.5    from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
     1.6    with S(2) have nz: "n \<noteq> 0" by auto
     1.7 -  from S_eq \<open>finite S\<close> have count_A: "count A x = f x" for x
     1.8 +  from S_eq \<open>finite S\<close> have count_A: "count A = f"
     1.9      unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
    1.10    from S_eq count_A have set_mset_A: "set_mset A = S"
    1.11      by (simp only: set_mset_def)
    1.12 @@ -1452,7 +1452,8 @@
    1.13      also from S(1) p
    1.14      have "image_mset (multiplicity p) A = image_mset (\<lambda>q. if p = q then 1 else 0) A"
    1.15        by (intro image_mset_cong) (auto simp: set_mset_A multiplicity_self prime_multiplicity_other)
    1.16 -    also have "sum_mset \<dots> = f p" by (simp add: sum_mset_delta' count_A)
    1.17 +    also have "sum_mset \<dots> = f p"
    1.18 +      by (simp add: semiring_1_class.sum_mset_delta' count_A)
    1.19      finally show "f p = multiplicity p n" ..
    1.20    qed
    1.21  qed