src/HOL/Computational_Algebra/Polynomial_Factorial.thy
changeset 67051 e7e54a0b9197
parent 66840 0d689d71dbdc
child 68790 851a9d9746c6
     1.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -171,7 +171,7 @@
     1.4    hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
     1.5    hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
     1.6    moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
     1.7 -    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
     1.8 +    by (simp_all add: a_def b_def coprime_quot_of_fract [of c] ac_simps
     1.9            normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
    1.10    ultimately show ?thesis by (intro that[of a b])
    1.11  qed
    1.12 @@ -513,9 +513,12 @@
    1.13     from fract_poly_smult_eqE[OF this] guess a b . note ab = this
    1.14     hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
    1.15     with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
    1.16 -   hence "normalize b = gcd a b" by simp
    1.17 -   also from ab(3) have "\<dots> = 1" .
    1.18 -   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
    1.19 +   then have "normalize b = gcd a b"
    1.20 +     by simp
    1.21 +   with \<open>coprime a b\<close> have "normalize b = 1"
    1.22 +     by simp
    1.23 +   then have "a = 1" "is_unit b"
    1.24 +     by (simp_all add: a normalize_1_iff)
    1.25     
    1.26     note eq
    1.27     also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
    1.28 @@ -676,7 +679,8 @@
    1.29      from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
    1.30      from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
    1.31      with assms content_e have "a = normalize b" by (simp add: ab(4))
    1.32 -    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
    1.33 +    with ab have ab': "a = 1" "is_unit b"
    1.34 +      by (simp_all add: normalize_1_iff)
    1.35      with ab ab' have "c' = to_fract b" by auto
    1.36      from this and \<open>is_unit b\<close> show ?thesis by (rule that)
    1.37    qed