src/HOL/GCD.thy
 changeset 61913 58b153bfa737 parent 61856 4b1b85f38944 child 61929 b8e242e52c97
```     1.1 --- a/src/HOL/GCD.thy	Tue Dec 22 17:41:46 2015 +0100
1.2 +++ b/src/HOL/GCD.thy	Tue Dec 22 15:38:59 2015 +0100
1.3 @@ -133,7 +133,15 @@
1.4    then show ?thesis
1.5      by (auto intro: associated_eqI)
1.6  qed
1.7 -
1.8 +
1.9 +lemma gcd_left_idem [simp]:
1.10 +  "gcd a (gcd a b) = gcd a b"
1.11 +  by (auto intro: associated_eqI)
1.12 +
1.13 +lemma gcd_right_idem [simp]:
1.14 +  "gcd (gcd a b) b = gcd a b"
1.15 +  unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
1.16 +
1.17  lemma coprime_1_left [simp]:
1.18    "coprime 1 a"
1.19    by (rule associated_eqI) simp_all
1.20 @@ -252,6 +260,10 @@
1.21    assume ?Q then show ?P by auto
1.22  qed
1.23
1.24 +lemma lcm_eq_1_iff [simp]:
1.25 +  "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
1.26 +  by (auto intro: associated_eqI)
1.27 +
1.28  lemma unit_factor_lcm :
1.29    "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
1.30    by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
1.31 @@ -281,6 +293,14 @@
1.32      by (auto intro: associated_eqI)
1.33  qed
1.34
1.35 +lemma lcm_left_idem [simp]:
1.36 +  "lcm a (lcm a b) = lcm a b"
1.37 +  by (auto intro: associated_eqI)
1.38 +
1.39 +lemma lcm_right_idem [simp]:
1.40 +  "lcm (lcm a b) b = lcm a b"
1.41 +  unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
1.42 +
1.43  lemma gcd_mult_lcm [simp]:
1.44    "gcd a b * lcm a b = normalize a * normalize b"
1.45    by (simp add: lcm_gcd normalize_mult)
1.46 @@ -836,14 +856,9 @@
1.47   apply (auto intro: gcd_greatest)
1.48  done
1.49
1.50 -interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.51 -  + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
1.52 -apply standard
1.53 -apply (auto intro: dvd_antisym dvd_trans)[2]
1.54 -apply (metis dvd.dual_order.refl gcd_unique_nat)+
1.55 -done
1.56 -
1.57 -interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" ..
1.58 +interpretation gcd_nat:
1.59 +  semilattice_neutr_order gcd "0::nat" Rings.dvd "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
1.60 +  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd.antisym dvd_trans)
1.61
1.62  lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
1.63  lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
1.64 @@ -1875,43 +1890,48 @@
1.65  lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
1.66  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
1.67
1.68 +lemma (in semiring_gcd) comp_fun_idem_gcd:
1.69 +  "comp_fun_idem gcd"
1.70 +  by standard (simp_all add: fun_eq_iff ac_simps)
1.71 +
1.72 +lemma (in semiring_gcd) comp_fun_idem_lcm:
1.73 +  "comp_fun_idem lcm"
1.74 +  by standard (simp_all add: fun_eq_iff ac_simps)
1.75 +
1.76  lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
1.77 -proof qed (auto simp add: gcd_ac_nat)
1.78 +  by (fact comp_fun_idem_gcd)
1.79
1.80  lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
1.81 -proof qed (auto simp add: gcd_ac_int)
1.82 +  by (fact comp_fun_idem_gcd)
1.83
1.84  lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
1.85 -proof qed (auto simp add: lcm_ac_nat)
1.86 +  by (fact comp_fun_idem_lcm)
1.87
1.88  lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
1.89 -proof qed (auto simp add: lcm_ac_int)
1.90 -
1.91 +  by (fact comp_fun_idem_lcm)
1.92
1.93 -(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
1.94 -
1.95 -lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1.96 -by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
1.97 +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1.98 +  by (fact lcm_eq_0_iff)
1.99
1.100 -lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1.101 -by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
1.102 +lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
1.103 +  by (fact lcm_eq_0_iff)
1.104
1.105 -lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
1.106 -by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
1.107 -
1.108 -lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
1.109 -by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
1.110 +lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
1.111 +  by (simp only: lcm_eq_1_iff) simp
1.112 +
1.113 +lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
1.114 +  by auto
1.115
1.116
1.117  subsection \<open>The complete divisibility lattice\<close>
1.118
1.119 -interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.120 +interpretation gcd_semilattice_nat: semilattice_inf gcd Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.121    by standard simp_all
1.122
1.123 -interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.124 +interpretation lcm_semilattice_nat: semilattice_sup lcm Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.125    by standard simp_all
1.126
1.127 -interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
1.128 +interpretation gcd_lcm_lattice_nat: lattice gcd Rings.dvd "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
1.129
1.130  text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
1.131  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
1.132 @@ -1982,19 +2002,6 @@
1.133  declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
1.134  declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
1.135
1.136 -lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
1.137 -  by (fact Lcm_nat_empty)
1.138 -
1.139 -lemma Lcm_insert_nat [simp]:
1.140 -  shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
1.141 -  by (fact gcd_lcm_complete_lattice_nat.Sup_insert)
1.142 -
1.143 -lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
1.144 -by(induct rule:finite_ne_induct) auto
1.145 -
1.146 -lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
1.147 -by (metis Lcm0_iff empty_iff)
1.148 -
1.149  instance nat :: semiring_Gcd
1.150  proof
1.151    show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
1.152 @@ -2031,6 +2038,22 @@
1.154  qed
1.155
1.156 +lemma Lcm_empty_nat:
1.157 +  "Lcm {} = (1::nat)"
1.158 +  by (fact Lcm_empty)
1.159 +
1.160 +lemma Lcm_insert_nat [simp]:
1.161 +  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
1.162 +  by (fact Lcm_insert)
1.163 +
1.164 +lemma Lcm_eq_0 [simp]:
1.165 +  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
1.166 +  by (rule Lcm_eq_0_I)
1.167 +
1.168 +lemma Lcm0_iff [simp]:
1.169 +  "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
1.170 +  by (induct rule: finite_ne_induct) auto
1.171 +
1.172  text\<open>Alternative characterizations of Gcd:\<close>
1.173
1.174  lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
1.175 @@ -2088,11 +2111,7 @@
1.176  lemma mult_inj_if_coprime_nat:
1.177    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
1.178     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
1.179 -apply (auto simp add: inj_on_def simp del: One_nat_def)
1.180 -apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
1.181 -apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
1.182 -             dvd.neq_le_trans dvd_triv_right mult.commute)
1.183 -done
1.184 +  by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
1.185
1.186  text\<open>Nitpick:\<close>
1.187
1.188 @@ -2147,18 +2166,18 @@
1.189  qed
1.190
1.191  lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
1.192 -  by (simp add: Lcm_int_def)
1.193 +  by (fact Lcm_empty)
1.194
1.195  lemma Lcm_insert_int [simp]:
1.196 -  shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
1.197 -  by (simp add: Lcm_int_def lcm_int_def)
1.198 +  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
1.199 +  by (fact Lcm_insert)
1.200
1.201  lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
1.202    by (fact dvd_int_unfold_dvd_nat)
1.203
1.204  lemma dvd_Lcm_int [simp]:
1.205    fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
1.206 -  using assms by (simp add: Lcm_int_def dvd_int_iff)
1.207 +  using assms by (fact dvd_Lcm)
1.208
1.209  lemma Lcm_dvd_int [simp]:
1.210    fixes M :: "int set"
```