src/HOL/GCD.thy
changeset 54867 c21a2465cac1
parent 54489 03ff4d1e6784
child 56166 9a241bc276cd
     1.1 --- a/src/HOL/GCD.thy	Wed Dec 25 22:35:29 2013 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Dec 26 22:47:49 2013 +0100
     1.3 @@ -197,14 +197,14 @@
     1.4    by (simp add: lcm_int_def)
     1.5  
     1.6  (* was gcd_0, etc. *)
     1.7 -lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
     1.8 +lemma gcd_0_nat: "gcd (x::nat) 0 = x"
     1.9    by simp
    1.10  
    1.11  (* was igcd_0, etc. *)
    1.12  lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
    1.13    by (unfold gcd_int_def, auto)
    1.14  
    1.15 -lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
    1.16 +lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
    1.17    by simp
    1.18  
    1.19  lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
    1.20 @@ -243,7 +243,7 @@
    1.21  lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
    1.22    and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
    1.23    apply (induct m n rule: gcd_nat_induct)
    1.24 -  apply (simp_all add: gcd_non_0_nat)
    1.25 +  apply (simp_all add: gcd_non_0_nat gcd_0_nat)
    1.26    apply (blast dest: dvd_mod_imp_dvd)
    1.27  done
    1.28  
    1.29 @@ -278,7 +278,7 @@
    1.30    by (rule zdvd_imp_le, auto)
    1.31  
    1.32  lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.33 -by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
    1.34 +by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
    1.35  
    1.36  lemma gcd_greatest_int:
    1.37    "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
    1.38 @@ -307,25 +307,6 @@
    1.39  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
    1.40    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
    1.41  
    1.42 -interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.43 -proof
    1.44 -qed (auto intro: dvd_antisym dvd_trans)
    1.45 -
    1.46 -interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.47 -proof
    1.48 -qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    1.49 -
    1.50 -lemmas gcd_assoc_nat = gcd_nat.assoc
    1.51 -lemmas gcd_commute_nat = gcd_nat.commute
    1.52 -lemmas gcd_left_commute_nat = gcd_nat.left_commute
    1.53 -lemmas gcd_assoc_int = gcd_int.assoc
    1.54 -lemmas gcd_commute_int = gcd_int.commute
    1.55 -lemmas gcd_left_commute_int = gcd_int.left_commute
    1.56 -
    1.57 -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    1.58 -
    1.59 -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    1.60 -
    1.61  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
    1.62      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.63    apply auto
    1.64 @@ -343,18 +324,40 @@
    1.65   apply (auto intro: gcd_greatest_int)
    1.66  done
    1.67  
    1.68 +interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.69 +  + 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.70 +apply default
    1.71 +apply (auto intro: dvd_antisym dvd_trans)[4]
    1.72 +apply (metis dvd.dual_order.refl gcd_unique_nat)
    1.73 +apply (auto intro: dvdI elim: dvdE)
    1.74 +done
    1.75 +
    1.76 +interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.77 +proof
    1.78 +qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    1.79 +
    1.80 +lemmas gcd_assoc_nat = gcd_nat.assoc
    1.81 +lemmas gcd_commute_nat = gcd_nat.commute
    1.82 +lemmas gcd_left_commute_nat = gcd_nat.left_commute
    1.83 +lemmas gcd_assoc_int = gcd_int.assoc
    1.84 +lemmas gcd_commute_int = gcd_int.commute
    1.85 +lemmas gcd_left_commute_int = gcd_int.left_commute
    1.86 +
    1.87 +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    1.88 +
    1.89 +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    1.90 +
    1.91  lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    1.92 -by (metis dvd.eq_iff gcd_unique_nat)
    1.93 +  by (fact gcd_nat.absorb1)
    1.94  
    1.95  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
    1.96 -by (metis dvd.eq_iff gcd_unique_nat)
    1.97 +  by (fact gcd_nat.absorb2)
    1.98  
    1.99 -lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   1.100 -by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
   1.101 +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   1.102 +  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   1.103  
   1.104 -lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   1.105 -by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   1.106 -
   1.107 +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   1.108 +  by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   1.109  
   1.110  text {*
   1.111    \medskip Multiplication laws
   1.112 @@ -1391,12 +1394,17 @@
   1.113    by (auto intro: dvd_antisym [transferred] lcm_least_int)
   1.114  
   1.115  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.116 +  + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
   1.117  proof
   1.118    fix n m p :: nat
   1.119    show "lcm (lcm n m) p = lcm n (lcm m p)"
   1.120      by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
   1.121    show "lcm m n = lcm n m"
   1.122      by (simp add: lcm_nat_def gcd_commute_nat field_simps)
   1.123 +  show "lcm m m = m"
   1.124 +    by (metis dvd.order_refl lcm_unique_nat)
   1.125 +  show "lcm m 1 = m"
   1.126 +    by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
   1.127  qed
   1.128  
   1.129  interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
   1.130 @@ -1478,10 +1486,6 @@
   1.131  
   1.132  subsection {* The complete divisibility lattice *}
   1.133  
   1.134 -lemma semilattice_neutr_set_lcm_one_nat:
   1.135 -  "semilattice_neutr_set lcm (1::nat)"
   1.136 -  by default simp_all
   1.137 -
   1.138  interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
   1.139  proof
   1.140    case goal3 thus ?case by(metis gcd_unique_nat)
   1.141 @@ -1508,28 +1512,19 @@
   1.142  definition
   1.143    "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
   1.144  
   1.145 +interpretation semilattice_neutr_set lcm "1::nat" ..
   1.146 +
   1.147  lemma Lcm_nat_infinite:
   1.148    "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
   1.149    by (simp add: Lcm_nat_def)
   1.150  
   1.151  lemma Lcm_nat_empty:
   1.152    "Lcm {} = (1::nat)"
   1.153 -proof -
   1.154 -  interpret semilattice_neutr_set lcm "1::nat"
   1.155 -    by (fact semilattice_neutr_set_lcm_one_nat)
   1.156 -  show ?thesis by (simp add: Lcm_nat_def)
   1.157 -qed
   1.158 +  by (simp add: Lcm_nat_def)
   1.159  
   1.160  lemma Lcm_nat_insert:
   1.161    "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
   1.162 -proof (cases "finite M")
   1.163 -  interpret semilattice_neutr_set lcm "1::nat"
   1.164 -    by (fact semilattice_neutr_set_lcm_one_nat)
   1.165 -  case True
   1.166 -  then show ?thesis by (simp add: Lcm_nat_def)
   1.167 -next
   1.168 -  case False then show ?thesis by (simp add: Lcm_nat_infinite)
   1.169 -qed
   1.170 +  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
   1.171  
   1.172  definition
   1.173    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   1.174 @@ -1587,7 +1582,7 @@
   1.175  qed
   1.176  
   1.177  lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
   1.178 -  by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
   1.179 +  by (fact Lcm_nat_empty)
   1.180  
   1.181  lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
   1.182    by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
   1.183 @@ -1688,6 +1683,7 @@
   1.184  lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
   1.185  by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
   1.186  
   1.187 +
   1.188  subsubsection {* Setwise gcd and lcm for integers *}
   1.189  
   1.190  instantiation int :: Gcd