src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60686 ea5bc46c11e6
parent 60685 cb21b7022b00
child 60687 33dbbcb6a8a3
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:34 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:39 2015 +0200
     1.3 @@ -1363,8 +1363,17 @@
     1.4    by (simp add: gcd_0)
     1.5  
     1.6  subclass semiring_gcd
     1.7 -  by unfold_locales (simp_all add: gcd_greatest_iff)
     1.8 -  
     1.9 +  apply standard
    1.10 +  using gcd_right_idem
    1.11 +  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
    1.12 +  done
    1.13 +
    1.14 +subclass semiring_Gcd
    1.15 +  by standard (simp_all add: Gcd_greatest)
    1.16 +
    1.17 +subclass semiring_Lcm
    1.18 +  by standard (simp add: Lcm_Gcd)
    1.19 +
    1.20  end
    1.21  
    1.22  text \<open>
    1.23 @@ -1382,7 +1391,7 @@
    1.24  lemma euclid_ext_gcd [simp]:
    1.25    "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
    1.26    by (induct a b rule: gcd_eucl_induct)
    1.27 -    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
    1.28 +    (simp_all add: euclid_ext_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
    1.29  
    1.30  lemma euclid_ext_gcd' [simp]:
    1.31    "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
    1.32 @@ -1453,9 +1462,6 @@
    1.33  definition [simp]:
    1.34    "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
    1.35  
    1.36 -definition [simp]:
    1.37 -  "unit_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
    1.38 -
    1.39  instance proof
    1.40  qed simp_all
    1.41  
    1.42 @@ -1467,11 +1473,8 @@
    1.43  definition [simp]:
    1.44    "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
    1.45  
    1.46 -definition [simp]:
    1.47 -  "unit_factor_int = (sgn :: int \<Rightarrow> int)"
    1.48 -
    1.49  instance
    1.50 -by standard (auto simp add: abs_mult nat_mult_distrib sgn_times split: abs_split)
    1.51 +by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
    1.52  
    1.53  end
    1.54