src/HOL/GCD.thy
 changeset 34030 829eb528b226 parent 33946 fcc20072df9a child 34221 3ae38d4b090c
```     1.1 --- a/src/HOL/GCD.thy	Mon Dec 07 23:06:03 2009 +0100
1.2 +++ b/src/HOL/GCD.thy	Tue Dec 08 13:40:57 2009 +0100
1.3 @@ -25,7 +25,7 @@
1.4  *)
1.5
1.6
1.8 +header {* Greates common divisor and least common multiple *}
1.9
1.10  theory GCD
1.11  imports Fact Parity
1.12 @@ -33,7 +33,7 @@
1.13
1.14  declare One_nat_def [simp del]
1.15
1.16 -subsection {* gcd *}
1.17 +subsection {* GCD and LCM definitions *}
1.18
1.19  class gcd = zero + one + dvd +
1.20
1.21 @@ -50,11 +50,7 @@
1.22
1.23  end
1.24
1.25 -
1.26 -(* definitions for the natural numbers *)
1.27 -
1.28  instantiation nat :: gcd
1.29 -
1.30  begin
1.31
1.32  fun
1.33 @@ -72,11 +68,7 @@
1.34
1.35  end
1.36
1.37 -
1.38 -(* definitions for the integers *)
1.39 -
1.40  instantiation int :: gcd
1.41 -
1.42  begin
1.43
1.44  definition
1.45 @@ -94,8 +86,7 @@
1.46  end
1.47
1.48
1.49 -subsection {* Set up Transfer *}
1.50 -
1.51 +subsection {* Transfer setup *}
1.52
1.53  lemma transfer_nat_int_gcd:
1.54    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
1.55 @@ -125,7 +116,7 @@
1.56      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
1.57
1.58
1.59 -subsection {* GCD *}
1.60 +subsection {* GCD properties *}
1.61
1.62  (* was gcd_induct *)
1.63  lemma gcd_nat_induct:
1.64 @@ -547,6 +538,10 @@
1.65  apply simp
1.66  done
1.67
1.68 +lemma gcd_code_int [code]:
1.69 +  "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
1.70 +  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
1.71 +
1.72
1.73  subsection {* Coprimality *}
1.74
1.75 @@ -1225,9 +1220,9 @@
1.76  qed
1.77
1.78
1.79 -subsection {* LCM *}
1.80 +subsection {* LCM properties *}
1.81
1.82 -lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1.83 +lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
1.84    by (simp add: lcm_int_def lcm_nat_def zdiv_int
1.85      zmult_int [symmetric] gcd_int_def)
1.86
1.87 @@ -1443,6 +1438,7 @@
1.88  lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
1.89  by (auto simp add: abs_mult_self trans [OF lcm_unique_int eq_commute, symmetric] zmult_eq_1_iff)
1.90
1.91 +
1.92  subsubsection {* The complete divisibility lattice *}
1.93
1.94
```