# HG changeset patch
# User haftmann
# Date 1450795139 -3600
# Node ID 58b153bfa737cd6dafd14775f8d59eca066c7bd3
# Parent  ad710de5c57664eacb07bc84aeff9badd6e92f23
tuned proofs and augmented some lemmas

diff -r ad710de5c576 -r 58b153bfa737 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Dec 22 17:41:46 2015 +0100
+++ b/src/HOL/GCD.thy	Tue Dec 22 15:38:59 2015 +0100
@@ -133,7 +133,15 @@
   then show ?thesis
     by (auto intro: associated_eqI)
 qed
-    
+
+lemma gcd_left_idem [simp]:
+  "gcd a (gcd a b) = gcd a b"
+  by (auto intro: associated_eqI)
+
+lemma gcd_right_idem [simp]:
+  "gcd (gcd a b) b = gcd a b"
+  unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
+
 lemma coprime_1_left [simp]:
   "coprime 1 a"
   by (rule associated_eqI) simp_all
@@ -252,6 +260,10 @@
   assume ?Q then show ?P by auto
 qed
 
+lemma lcm_eq_1_iff [simp]:
+  "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
+  by (auto intro: associated_eqI)
+
 lemma unit_factor_lcm :
   "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
@@ -281,6 +293,14 @@
     by (auto intro: associated_eqI)
 qed
 
+lemma lcm_left_idem [simp]:
+  "lcm a (lcm a b) = lcm a b"
+  by (auto intro: associated_eqI)
+
+lemma lcm_right_idem [simp]:
+  "lcm (lcm a b) b = lcm a b"
+  unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
+
 lemma gcd_mult_lcm [simp]:
   "gcd a b * lcm a b = normalize a * normalize b"
   by (simp add: lcm_gcd normalize_mult)
@@ -836,14 +856,9 @@
  apply (auto intro: gcd_greatest)
 done
 
-interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
-  + 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)"
-apply standard
-apply (auto intro: dvd_antisym dvd_trans)[2]
-apply (metis dvd.dual_order.refl gcd_unique_nat)+
-done
-
-interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" ..
+interpretation gcd_nat:
+  semilattice_neutr_order gcd "0::nat" Rings.dvd "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
+  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd.antisym dvd_trans)
 
 lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
 lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
@@ -1875,43 +1890,48 @@
 lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
 
+lemma (in semiring_gcd) comp_fun_idem_gcd:
+  "comp_fun_idem gcd"
+  by standard (simp_all add: fun_eq_iff ac_simps)
+
+lemma (in semiring_gcd) comp_fun_idem_lcm:
+  "comp_fun_idem lcm"
+  by standard (simp_all add: fun_eq_iff ac_simps)
+
 lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
-proof qed (auto simp add: gcd_ac_nat)
+  by (fact comp_fun_idem_gcd)
 
 lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
-proof qed (auto simp add: gcd_ac_int)
+  by (fact comp_fun_idem_gcd)
 
 lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
-proof qed (auto simp add: lcm_ac_nat)
+  by (fact comp_fun_idem_lcm)
 
 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
-proof qed (auto simp add: lcm_ac_int)
-
+  by (fact comp_fun_idem_lcm)
 
-(* FIXME introduce selimattice_bot/top and derive the following lemmas in there: *)
-
-lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
-by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
+lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+  by (fact lcm_eq_0_iff)
 
-lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
-by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
+lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
+  by (fact lcm_eq_0_iff)
 
-lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
-by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)
-
-lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
-by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
+lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
+  by (simp only: lcm_eq_1_iff) simp
+  
+lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+  by auto
 
 
 subsection \<open>The complete divisibility lattice\<close>
 
-interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+interpretation gcd_semilattice_nat: semilattice_inf gcd Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   by standard simp_all
 
-interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+interpretation lcm_semilattice_nat: semilattice_sup lcm Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   by standard simp_all
 
-interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
+interpretation gcd_lcm_lattice_nat: lattice gcd Rings.dvd "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
 
 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
@@ -1982,19 +2002,6 @@
 declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
 declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
 
-lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
-  by (fact Lcm_nat_empty)
-
-lemma Lcm_insert_nat [simp]:
-  shows "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
-  by (fact gcd_lcm_complete_lattice_nat.Sup_insert)
-
-lemma Lcm0_iff[simp]: "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 : M"
-by(induct rule:finite_ne_induct) auto
-
-lemma Lcm_eq_0[simp]: "finite (M::nat set) \<Longrightarrow> 0 : M \<Longrightarrow> Lcm M = 0"
-by (metis Lcm0_iff empty_iff)
-
 instance nat :: semiring_Gcd
 proof
   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
@@ -2031,6 +2038,22 @@
       simp add: unit_factor_Gcd uf)
 qed
 
+lemma Lcm_empty_nat:
+  "Lcm {} = (1::nat)"
+  by (fact Lcm_empty)
+
+lemma Lcm_insert_nat [simp]:
+  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
+  by (fact Lcm_insert)
+
+lemma Lcm_eq_0 [simp]:
+  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
+  by (rule Lcm_eq_0_I)
+
+lemma Lcm0_iff [simp]:
+  "finite (M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
+  by (induct rule: finite_ne_induct) auto
+
 text\<open>Alternative characterizations of Gcd:\<close>
 
 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})"
@@ -2088,11 +2111,7 @@
 lemma mult_inj_if_coprime_nat:
   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
-apply (auto simp add: inj_on_def simp del: One_nat_def)
-apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
-apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
-             dvd.neq_le_trans dvd_triv_right mult.commute)
-done
+  by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
 
 text\<open>Nitpick:\<close>
 
@@ -2147,18 +2166,18 @@
 qed
 
 lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
-  by (simp add: Lcm_int_def)
+  by (fact Lcm_empty)
 
 lemma Lcm_insert_int [simp]:
-  shows "Lcm (insert (n::int) N) = lcm n (Lcm N)"
-  by (simp add: Lcm_int_def lcm_int_def)
+  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
+  by (fact Lcm_insert)
 
 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
   by (fact dvd_int_unfold_dvd_nat)
 
 lemma dvd_Lcm_int [simp]:
   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
-  using assms by (simp add: Lcm_int_def dvd_int_iff)
+  using assms by (fact dvd_Lcm)
 
 lemma Lcm_dvd_int [simp]:
   fixes M :: "int set"