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 (*>*)