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
```