# HG changeset patch # User haftmann # Date 1491392860 -7200 # Node ID 6f9c6ae27984a787f4e64d7358272d625128d551 # Parent a8d868477bc01deed32c46ff5c14562e3280b717 tuned diff -r a8d868477bc0 -r 6f9c6ae27984 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:38 2017 +0200 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Apr 05 13:47:40 2017 +0200 @@ -16,8 +16,8 @@ subsection \Various facts about polynomials\ -lemma prod_mset_const_poly: "prod_mset (image_mset (\x. [:f x:]) A) = [:prod_mset (image_mset f A):]" - by (induction A) (simp_all add: one_poly_def mult_ac) +lemma prod_mset_const_poly: " (\x\#A. [:f x:]) = [:prod_mset (image_mset f A):]" + by (induct A) (simp_all add: one_poly_def ac_simps) lemma irreducible_const_poly_iff: fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}" @@ -169,13 +169,14 @@ lemma prod_mset_fract_poly: "prod_mset (image_mset (\x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))" - by (induction A) (simp_all add: mult_ac) + by (induct A) (simp_all add: one_poly_def ac_simps) lemma is_unit_fract_poly_iff: "p dvd 1 \ fract_poly p dvd 1 \ content p = 1" proof safe assume A: "p dvd 1" - with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp + with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)" + by simp from A show "content p = 1" by (auto simp: is_unit_poly_iff normalize_1_iff) next