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.105    by (simp add: Lcm_int_def)
   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.119    by (simp add: zdvd_int)
   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 -