section \The Euclidean Algorithm - Inductively\ text \ In this project you will develop and verify an inductive specification of the Euclidean algorithm. (Adapted from \<^url>\http://isabelle.in.tum.de/exercises/proj/euclid/ex.pdf\) \ theory Project_GCD imports Main begin text \ Define the set \gcd\ of triples \(a,b,g)\ such that \g\ is the greatest common divisor of \a\ and \b\ inductively. Your definition should closely follow the Euclidean algorithm, which repeatedly subtracts the smaller from the larger number, until one of them is zero (at this point, the other number is the greatest common divisor). \ inductive_set gcd :: "(nat \ nat \ nat) set" text \ Show that the greatest common divisor as given by \gcd\ is indeed a divisor. \ lemma gcd_divides: "(a, b, g) \ gcd \ g dvd a \ g dvd b" sorry subsection \Soundness\ text \ Show that the greatest common divisor as given by \gcd\ is greater than or equal to any other common divisor. \ lemma gcd_greatest: assumes "(a, b, g) \ gcd" and "0 < a \ 0 < b" and "d dvd a" and "d dvd b" shows "d \ g" sorry subsection \Completeness\ text \ So far, you have only shown that \gcd\ is correct, but there might still be values \a\ and \b\ such that there is no \g\ with \(a,b,g) \ gcd\. Thus, show completeness of your specification. First prove the following result by course-of-value recursion, that is, using @{thm nat_less_induct}. (Inside the induction make a case analysis corresponding to the different clauses of the algorithm.) \ lemma gcd_defined_aux: "a + b \ n \ \g. (a, b, g) \ gcd" sorry lemma gcd_defined: "\g. (a, b, g) \ gcd" sorry end