removed overambitious simp rules from e7e54a0b9197
authorhaftmann
Thu Nov 16 11:30:23 2017 +0100 (19 months ago)
changeset 670786a85b8a9c28c
parent 67077 8fa951baba0d
child 67079 02483f568c52
removed overambitious simp rules from e7e54a0b9197
src/HOL/Computational_Algebra/Normalized_Fraction.thy
     1.1 --- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Tue Nov 14 23:07:47 2017 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Thu Nov 16 11:30:23 2017 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    "normalize_quot (a, 0) = (0, 1)"
     1.5    by (simp add: normalize_quot_def)
     1.6  
     1.7 -lemma normalize_quot_proj [simp]:
     1.8 +lemma normalize_quot_proj:
     1.9    "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
    1.10    "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
    1.11    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')
    1.12 @@ -275,8 +275,7 @@
    1.13    have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
    1.14    thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
    1.15      using assms(1,2) d
    1.16 -    by (auto simp: normalized_fracts_def ac_simps)
    1.17 -      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
    1.18 +    by (auto simp add: normalized_fracts_def ac_simps dvd_div_unit_iff elim: coprime_imp_coprime)
    1.19  qed fact+
    1.20    
    1.21  lemma quot_of_fract_inverse: