Euclid's algorithm proof in Isabelle

GCD.thy

theory GCD
imports Main
begin

fun gcd :: "nat ⇒ nat ⇒ nat" where
"gcd m 0 = m" |
"gcd m n = gcd n (m mod n)"


theorem gcd_dvd_both: "(gcd m n dvd m) ∧ (gcd m n dvd n)"
apply (induct_tac m n rule: "gcd.induct")
apply (case_tac "n = 0")
apply (simp_all)
apply (blast dest: dvd_mod_imp_dvd)
done

theorem gcd_greatest: "k dvd m ⟶ k dvd n ⟶ k dvd gcd m n"
apply (induct_tac m n rule: "gcd.induct")
apply (case_tac "n = 0")
apply (simp_all add: dvd_mod)
done

end