section \<open>Assessed Exercise II: The Binary Euclidean Algorithm\<close>

(*<*)
theory Euclid_ex
  imports Main
begin
(*>*)

text \<open>
The greatest common divisor of two natural
numbers can be computed efficiently using a binary version of Euclid's algorithm.
It eliminates common factors of two (which in hardware can be done efficiently by shifting),
and given two odd numbers it subtracts them, producing another even number.

\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}
This algorithm is actually nondeterministic, in that the steps can be applied in any order.
However the result is unique because a pair of positive integers has exactly one greatest common divisor.

\begin{task} Inductively define the set @{text BinaryGCD} such that
@{term "(x,y,g) \<in> BinaryGCD"} means @{term g} is computed from @{term x} and @{term y} as specified by the description above.
\points{5}
\end{task}
\<close>
consts  BinaryGCD :: "(nat \<times> nat \<times> nat) set"

text \<open>\begin{task} Show that the @{term BinaryGCD} of @{term x} and @{term y} is
really the greatest common divisor of both numbers, with respect to
the divides relation. Hint: it may help to consider whether @{term d} is even or odd.
Be careful to choose the right form of induction, and justify your choice in your write-up.
\points{15}
\end{task}
\<close>
lemma GCD_greatest_divisor:
  "(x,y,g) \<in> BinaryGCD \<Longrightarrow> d dvd x \<Longrightarrow> d dvd y \<Longrightarrow> d dvd g"
(*<*)oops(*>*)

text \<open>\begin{task}
Prove the following statement.
In the form given (assuming @{term n} to be odd), it can be proved directly by induction.
\points{10}
\end{task}
\<close>
lemma GCD_mult:
  "(x,y,g) \<in> BinaryGCD \<Longrightarrow> odd n \<Longrightarrow> (n*x,n*y,n*g) \<in> BinaryGCD"
(*<*)oops(*>*)

text \<open>
\noindent\emph{Remark}: the theorem above actually holds for all @{term n}, but the simplest way of proving it
is probably to prove that  @{term BinaryGCD} corresponds exactly to the true @{term gcd} function
and then to use properties of the latter.

\begin{task}
How do we know that @{term BinaryGCD} can compute a result for all values of @{term a} and @{term b}?
To prove it requires a carefully formulated induction, as shown in the theorem statement below.
We need course-of-values induction (expressed by the theorem @{text less_induct}),
which allows us to assume the induction formula for everything smaller than @{term n}.
(Why doesn't standard induction work here?)

Hint: the algorithm is complete even if the steps @{text GCDEven} and @{text GCDOdd} are deleted.
They merely improve performance, so your proof can ignore them. You will still need to
consider various cases corresponding to the remaining steps of the algorithm.
\points{20}
\end{task}
\<close>

lemma GCD_defined_aux: "a+b \<le> n \<Longrightarrow> \<exists>g. (a, b, g) \<in> BinaryGCD"
(*<*)oops(*>*)

text \<open>Armed with this lemma, the completeness statement is trivial.\<close>

theorem GCD_defined: "\<exists>g. (a, b, g) \<in> BinaryGCD"

(*<*)oops

end (*>*)