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.153        simp add: unit_factor_Gcd uf)
   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"