summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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