header {* Assessed Exercise I: Greatest Common Divisors *}

(*<*)
theory euclid_ex 
  imports "~~/src/HOL/Number_Theory/Primes" 
begin
(*>*)

(*Note that this theory is based upon Isabelle's theory of prime
numbers, which will be loaded automatically.*)


text {*
The greatest common divisor of two natural
numbers can be computed by a binary version of Euclid's
algorithm:

\begin{itemize}
\item The GCD of $x$ and 0 is $x$.

\item If the GCD of $x$ and $y$ is $z$, then the GCD of $2x$ and $2y$ is $2z$.

\item The GCD of $2x$ and $y$ is the same as that of $x$ and $y$ if $y$ is odd.

\item The GCD of $x$ and $y$ is the same as that of $x-y$ and $y$ if $y\le x$.

\item The GCD of $x$ and $y$ is the same as the GCD of $y$ and $x$.
\end{itemize} 
Note that frequently more than one of these cases is
applicable, so it is not immediately obvious that they express a
function.

\begin{task} 
Define inductively the set @{text GCD} such that
@{text "(x,y,g) \<in> GCD"} means @{text g} is the greatest common divisor
of @{text x} und @{text y}, as specified by the description above.
\end{task}
*}
(*<*)
consts GCD :: "(nat \<times> nat \<times> nat) set"
(*>*)
text {*\begin{task} Show that the GCD of @{text x} und @{text y} is
really a divisor of both numbers:\end{task} 
*}
lemma GCD_divides: "(x,y,g) \<in> GCD \<Longrightarrow> g dvd x \<and> g dvd y"
(*<*)oops(*>*)
text {* \begin{task} Show that the GCD of @{text x} und @{text y} is
really the greatest common divisor of both numbers, with respect to
the divides relation. Hint: consider using the predicate @{text coprime},
which belongs to the theory @{text GCD}. This theory will be present in your
session because it is an ancestor of theory @{text Prime}.\end{task} 
*}
lemma GCD_greatest_dvd:
  "(x,y,g) \<in> GCD \<Longrightarrow> d dvd x \<Longrightarrow> d dvd y \<Longrightarrow> d dvd g"
(*<*)oops(*>*)

text {* \begin{task} Show that, despite its apparent non-determinism,
the relation @{text GCD} is deterministic and therefore defines a
function:\end{task} 
*}
lemma GCD_unique: 
  "(x,y,g) \<in> GCD \<Longrightarrow> (x,y,g') \<in> GCD \<Longrightarrow> g = g'"
(*<*)oops(*>*)

text {*Hint: first, prove a lemma establishing a connection between
the relation @{text GCD} and the function @{text gcd}, which belongs
to the theory @{text GCD}. This theory provides many lemmas that can
help you complete this exercise.  *}

text {*
\newpage*}

(*<*) end (*>*)