theory GreatestCommonDivisor
imports Main
begin
fun gcd :: "nat \ nat \ nat" where
"gcd a b =
(if a = 0 then
b
else if b = 0 then
a
else if a > b then
gcd (a - b) b
else
gcd a (b - a))"
definition
greatest_common_divisor :: "nat \ nat \ nat \ bool" where
"greatest_common_divisor p m n \ p dvd m \ p dvd n \
(\d. d dvd m \ d dvd n \ d dvd p)"
declare greatest_common_divisor_def[simp]
theorem gcd_correct:
assumes n: "n = a + b"
shows "greatest_common_divisor (gcd a b) a b"
using n apply (induct n arbitrary: a b rule: nat_less_induct)
proof -
fix n a b
assume IH: "\mx xa.
m = x + xa \ greatest_common_divisor (gcd x xa) x xa"
and n: "n = a + b"
show "greatest_common_divisor (gcd a b) a b"
proof (cases "a = 0")
assume a: "a = 0"
hence g: "gcd a b = b" by simp
have x: "b dvd 0" by simp
have y: "b dvd b" by simp
have z: "\ d. d dvd 0 \ d dvd b \ d dvd b" by simp
from x y z have "greatest_common_divisor b 0 b" by simp
with a show ?thesis by simp
next
assume az: "a \ 0"
show "greatest_common_divisor (gcd a b) a b"
proof (cases "b = 0")
assume b: "b = 0"
with az have g: "gcd a b = a" by (case_tac a) auto
have x: "a dvd a" by simp
have y: "a dvd 0" by simp
have z: "\ d. d dvd a \ d dvd 0 \ d dvd a" by simp
from x y z have "greatest_common_divisor a a 0" by simp
with b g show ?thesis by simp
next
assume bz: "b \ 0"
have "a > b \ a \ b" by arith
thus "greatest_common_divisor (gcd a b) a b"
proof
assume ba: "b < a"
from az bz ba have g: "gcd a b = gcd (a - b) b"
apply (case_tac a) apply auto done
let ?M = "(a - b) + b"
from bz ba n have mn: "?M < n" by simp
from mn IH
have "greatest_common_divisor (gcd (a - b) b) (a - b) b"
by blast
with g have d: "greatest_common_divisor (gcd a b) (a - b) b"
by (simp only: g)
from d have dab: "(gcd a b) dvd (a - b)"
by (simp only: greatest_common_divisor_def)
from d have db: "(gcd a b) dvd b"
by (simp only: greatest_common_divisor_def)
from ba have ba2: "b \ a" by simp
from dab db ba2 have x: "(gcd a b) dvd a" by (rule dvd_diffD)
have z: "\ d. d dvd a \ d dvd b \ d dvd (gcd a b)"
proof clarify
fix d assume da: "d dvd a" and db: "d dvd b"
from d have gr: "\ k. k dvd (a - b) \ k dvd b \ k dvd (gcd a b)"
by (simp only: greatest_common_divisor_def, blast)
from da db have dab: "d dvd (a - b)" by (rule nat_dvd_diff)
from gr dab db show "d dvd (gcd a b)" by simp
qed
from x db z show ?thesis by simp
next
assume ab: "a \ b"
from az bz ab have g: "gcd a b = gcd a (b - a)"by (case_tac a) auto
let ?M = "a + (b - a)"
from az ab n have mn: "?M < n" by simp
from mn IH
have "greatest_common_divisor (gcd a (b - a)) a (b - a)" by blast
with g have g2: "greatest_common_divisor (gcd a b) a (b - a)"
by (simp only: greatest_common_divisor_def) blast
from g2 have gcd_div_a: "gcd a b dvd a"
by (simp only: greatest_common_divisor_def)
from g2 ab have gcd_div_b: "gcd a b dvd b"
apply (simp only: greatest_common_divisor_def)
apply (rule dvd_diffD) apply blast+ done
have greatest: "\d. d dvd a \ d dvd b \ d dvd gcd a b"
proof clarify
fix d assume diva: "d dvd a" and divb: "d dvd b"
from divb diva have divba: "d dvd (b - a)" by (rule nat_dvd_diff)
from divba diva g2 show "d dvd (gcd a b)"
by (simp only: greatest_common_divisor_def)
qed
from gcd_div_a gcd_div_b greatest show ?thesis
by (simp only: greatest_common_divisor_def) blast
qed
qed
qed
qed
end