# HG changeset patch
# User haftmann
# Date 1260276057 -3600
# Node ID 829eb528b2267fc80c64d33355f87d3e67afd69d
# Parent  7996b488a9b509a3019531a9f71076a28e91c78b
resorted code equations from "old" number theory version

diff -r 7996b488a9b5 -r 829eb528b226 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Dec 07 23:06:03 2009 +0100
+++ b/src/HOL/GCD.thy	Tue Dec 08 13:40:57 2009 +0100
@@ -25,7 +25,7 @@
 *)
 
 
-header {* GCD *}
+header {* Greates common divisor and least common multiple *}
 
 theory GCD
 imports Fact Parity
@@ -33,7 +33,7 @@
 
 declare One_nat_def [simp del]
 
-subsection {* gcd *}
+subsection {* GCD and LCM definitions *}
 
 class gcd = zero + one + dvd +
 
@@ -50,11 +50,7 @@
 
 end
 
-
-(* definitions for the natural numbers *)
-
 instantiation nat :: gcd
-
 begin
 
 fun
@@ -72,11 +68,7 @@
 
 end
 
-
-(* definitions for the integers *)
-
 instantiation int :: gcd
-
 begin
 
 definition
@@ -94,8 +86,7 @@
 end
 
 
-subsection {* Set up Transfer *}
-
+subsection {* Transfer setup *}
 
 lemma transfer_nat_int_gcd:
   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
@@ -125,7 +116,7 @@
     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
 
 
-subsection {* GCD *}
+subsection {* GCD properties *}
 
 (* was gcd_induct *)
 lemma gcd_nat_induct:
@@ -547,6 +538,10 @@
 apply simp
 done
 
+lemma gcd_code_int [code]:
+  "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
+  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+
 
 subsection {* Coprimality *}
 
@@ -1225,9 +1220,9 @@
 qed
 
 
-subsection {* LCM *}
+subsection {* LCM properties *}
 
-lemma lcm_altdef_int: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
+lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
   by (simp add: lcm_int_def lcm_nat_def zdiv_int
     zmult_int [symmetric] gcd_int_def)
 
@@ -1443,6 +1438,7 @@
 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)
 
+
 subsubsection {* The complete divisibility lattice *}