resorted code equations from "old" number theory version
authorhaftmann
Tue Dec 08 13:40:57 2009 +0100 (2009-12-08)
changeset 34030829eb528b226
parent 34025 7996b488a9b5
child 34031 f7480c5a34e8
resorted code equations from "old" number theory version
src/HOL/GCD.thy
     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.7 -header {* GCD *}
     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