author haftmann Thu, 16 Nov 2017 11:30:23 +0100 changeset 67078 6a85b8a9c28c parent 67077 8fa951baba0d child 67079 02483f568c52
removed overambitious simp rules from e7e54a0b9197
```--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Tue Nov 14 23:07:47 2017 +0100
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Nov 16 11:30:23 2017 +0100
@@ -20,7 +20,7 @@
"normalize_quot (a, 0) = (0, 1)"
by (simp add: normalize_quot_def)

-lemma normalize_quot_proj [simp]:
+lemma normalize_quot_proj:
"fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
"snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
@@ -275,8 +275,7 @@
have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
using assms(1,2) d
-    by (auto simp: normalized_fracts_def ac_simps)
-      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
+    by (auto simp add: normalized_fracts_def ac_simps dvd_div_unit_iff elim: coprime_imp_coprime)
qed fact+

lemma quot_of_fract_inverse:```