src/HOL/GCD.thy
 changeset 60596 54168997757f parent 60580 7e741e22d7fc child 60597 2da9b632069b
```     1.1 --- a/src/HOL/GCD.thy	Sat Jun 27 00:10:24 2015 +0200
1.2 +++ b/src/HOL/GCD.thy	Sat Jun 27 20:20:32 2015 +0200
1.3 @@ -756,10 +756,10 @@
1.4  done
1.5
1.6  lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
1.7 -  by (induct n, simp_all add: power_Suc coprime_mult_nat)
1.8 +  by (induct n) (simp_all add: coprime_mult_nat)
1.9
1.10  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
1.11 -  by (induct n, simp_all add: power_Suc coprime_mult_int)
1.12 +  by (induct n) (simp_all add: coprime_mult_int)
1.13
1.14  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
1.15    by (simp add: coprime_exp_nat gcd_nat.commute)
1.16 @@ -888,7 +888,7 @@
1.17      have "a' dvd a'^n" by (simp add: m)
1.18      with th0 have "a' dvd b'^n"
1.19        using dvd_trans[of a' "a'^n" "b'^n"] by simp
1.20 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute power_Suc)
1.21 +    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
1.22      from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
1.23      have "a' dvd b'" by (subst (asm) mult.commute, blast)
1.24      hence "a'*?g dvd b'*?g" by simp
1.25 @@ -1500,6 +1500,18 @@
1.26
1.27  end
1.28
1.29 +class semiring_Gcd = semiring_gcd + Gcd +
1.30 +  assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1.31 +    and dvd_Gcd: "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
1.32 +    and Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
1.33 +begin
1.34 +
1.35 +lemma Gcd_empty [simp]:
1.36 +  "Gcd {} = 0"
1.37 +  by (rule dvd_0_left, rule dvd_Gcd) simp
1.38 +
1.39 +end
1.40 +
1.41  lemma dvd_Lcm_nat [simp]:
1.42    fixes M :: "nat set"
1.43    assumes "m \<in> M"
1.44 @@ -1559,32 +1571,27 @@
1.45  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
1.46    by (fact Lcm_nat_empty)
1.47
1.48 -lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
1.49 -  by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
1.50 -
1.51  lemma Lcm_insert_nat [simp]:
1.52    shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
1.53    by (fact gcd_lcm_complete_lattice_nat.Sup_insert)
1.54
1.55 -lemma Gcd_insert_nat [simp]:
1.56 -  shows "Gcd (insert (n::nat) N) = gcd n (Gcd N)"
1.57 -  by (fact gcd_lcm_complete_lattice_nat.Inf_insert)
1.58 -
1.59  lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
1.60  by(induct rule:finite_ne_induct) auto
1.61
1.62  lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
1.63  by (metis Lcm0_iff empty_iff)
1.64
1.65 -lemma Gcd_dvd_nat [simp]:
1.66 -  fixes M :: "nat set"
1.67 -  assumes "m \<in> M" shows "Gcd M dvd m"
1.68 -  using assms by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
1.69 -
1.70 -lemma dvd_Gcd_nat[simp]:
1.71 -  fixes M :: "nat set"
1.72 -  assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
1.73 -  using assms by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
1.74 +instance nat :: semiring_Gcd
1.75 +proof
1.76 +  show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
1.77 +    using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
1.78 +next
1.79 +  show "n dvd Gcd N" if "\<forall>m\<in>N. n dvd m" for N and n :: nat
1.80 +    using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
1.81 +next
1.82 +  show "Gcd (insert n N) = gcd n (Gcd N)" for N and n :: nat
1.83 +    by simp
1.84 +qed
1.85
1.86  text{* Alternative characterizations of Gcd: *}
1.87
1.88 @@ -1592,12 +1599,12 @@
1.89  apply(rule antisym)
1.90   apply(rule Max_ge)
1.91    apply (metis all_not_in_conv finite_divisors_nat finite_INT)
1.92 - apply simp
1.93 + apply (simp add: Gcd_dvd)
1.94  apply (rule Max_le_iff[THEN iffD2])
1.95    apply (metis all_not_in_conv finite_divisors_nat finite_INT)
1.96   apply fastforce
1.97  apply clarsimp
1.98 -apply (metis Gcd_dvd_nat Max_in dvd_0_left dvd_Gcd_nat dvd_imp_le linorder_antisym_conv3 not_less0)
1.99 +apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
1.100  done
1.101
1.102  lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
1.103 @@ -1676,17 +1683,10 @@
1.104  lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
1.106
1.107 -lemma Gcd_empty_int [simp]: "Gcd {} = (0::int)"
1.108 -  by (simp add: Gcd_int_def)
1.109 -
1.110  lemma Lcm_insert_int [simp]:
1.111    shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
1.112    by (simp add: Lcm_int_def lcm_int_def)
1.113
1.114 -lemma Gcd_insert_int [simp]:
1.115 -  shows "Gcd (insert (n::int) N) = gcd n (Gcd N)"
1.116 -  by (simp add: Gcd_int_def gcd_int_def)
1.117 -
1.118  lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
1.120
1.121 @@ -1699,16 +1699,9 @@
1.122    assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
1.123    using assms by (simp add: Lcm_int_def dvd_int_iff)
1.124
1.125 -lemma Gcd_dvd_int [simp]:
1.126 -  fixes M :: "int set"
1.127 -  assumes "m \<in> M" shows "Gcd M dvd m"
1.128 -  using assms by (simp add: Gcd_int_def dvd_int_iff)
1.129 -
1.130 -lemma dvd_Gcd_int[simp]:
1.131 -  fixes M :: "int set"
1.132 -  assumes "\<forall>m\<in>M. n dvd m" shows "n dvd Gcd M"
1.133 -  using assms by (simp add: Gcd_int_def dvd_int_iff)
1.134 -
1.135 +instance int :: semiring_Gcd
1.136 +  by intro_classes (simp_all add: Gcd_int_def gcd_int_def dvd_int_iff Gcd_dvd dvd_Gcd)
1.137 +
1.138  lemma Lcm_set_int [code, code_unfold]:
1.139    "Lcm (set xs) = fold lcm xs (1::int)"
1.140    by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
1.141 @@ -1728,5 +1721,16 @@
1.142    and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
1.143    and gcd_greatest_int = gcd_greatest [where ?'a = int]
1.144
1.145 +lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
1.146 +  and dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
1.147 +
1.148 +lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
1.149 +  and dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
1.150 +
1.151 +lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
1.152 +  and Gcd_insert_nat = Gcd_insert [where ?'a = nat]
1.153 +
1.154 +lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
1.155 +  and Gcd_insert_int = Gcd_insert [where ?'a = int]
1.156 +
1.157  end
1.158 -
```