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