section \<open>The Euclidean Algorithm - Inductively\<close>

text \<open>
In this project you will develop and verify an inductive specification of the
Euclidean algorithm.

(Adapted from \<^url>\<open>http://isabelle.in.tum.de/exercises/proj/euclid/ex.pdf\<close>)
\<close>

theory Project_GCD
  imports Main
begin

text \<open>
Define the set \<open>gcd\<close> of triples \<open>(a,b,g)\<close> such that \<open>g\<close> is the greatest
common divisor of \<open>a\<close> and \<open>b\<close> 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).
\<close>

inductive_set gcd :: "(nat \<times> nat \<times> nat) set"

text \<open>
Show that the greatest common divisor as given by \<open>gcd\<close> is indeed a divisor.
\<close>
lemma gcd_divides: "(a, b, g) \<in> gcd \<Longrightarrow> g dvd a \<and> g dvd b"
  sorry


subsection \<open>Soundness\<close>

text \<open>
Show that the greatest common divisor as given by \<open>gcd\<close> is greater than or
equal to any other common divisor.
\<close>
lemma gcd_greatest:
  assumes "(a, b, g) \<in> gcd"
    and "0 < a \<or> 0 < b"
    and "d dvd a"
    and "d dvd b"
  shows "d \<le> g"
  sorry

subsection \<open>Completeness\<close>

text \<open>
So far, you have only shown that \<open>gcd\<close> is correct, but there might still
be values \<open>a\<close> and \<open>b\<close> such that there is no \<open>g\<close> with \<open>(a,b,g) \<in> gcd\<close>.

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.)
\<close>
lemma gcd_defined_aux:
  "a + b \<le> n \<Longrightarrow> \<exists>g. (a, b, g) \<in> gcd"
  sorry

lemma gcd_defined: "\<exists>g. (a, b, g) \<in> gcd"
  sorry

end