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