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) \ 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 \ nat \ 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) \ GCD \ g dvd x \ 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) \ GCD \ d dvd x \ d dvd y \ 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) \ GCD \ (x,y,g') \ GCD \ 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 (*>*)