section \<open>Assessed Exercise I: Euler's totient function\<close>

(*<*)theory Totient_ex
  imports "HOL-Computational_Algebra.Computational_Algebra"
begin(*>*)

text\<open>
Euler's totient function, written $\phi(n)$, denotes the number of integers 1, 2, \ldots,~$n$ that are coprime to
the positive integer~$n$. 
So for example $\phi(1)=\phi(2)=1$ and $\phi(3)=\phi(4)=2$. 
The totient function is fundamental to number theory and this exercise establishes some of its elementary properties. 
See Baker, \emph{A Concise Introduction to the Theory of Numbers} (Cambridge University Press, 1984), page 9. 
Other books on elementary number theory will also cover this function.
\<close>

text \<open>\begin{task}
Define the totient function @{text \<phi>} of type @{typ"nat \<Rightarrow> nat"} as described above.
Note that the cardinality of a finite set can be expressed using the built-in function @{term card},
and the two-argument predicate @{term coprime} is also available.
Greek letters can be inserted using the Symbols palette, but you may give the function the name
@{text phi} if you prefer.

Then prove the following two facts.
\points{5}
\end{task}
\<close>
(*<*)consts \<phi> :: "nat \<Rightarrow> nat"(*>*) 
lemma phi_1: "\<phi> 1 = 1"
(*<*) oops (*>*) 
  
lemma phi_2: "\<phi> 2 = 1"
(*<*) oops (*>*) 
  
text \<open>\begin{task}
The following exercise establishes an alternative characterisation of the totient function.
\points{10}
\end{task}
\<close>
lemma phi_altdef: "\<phi>(n) = card {m. coprime m n \<and> m < n}"
(*<*) oops (*>*) 

text \<open>\begin{task}
Among the other straightforward properties of the totient function is that $\phi(p)=p-1$
if $p$ is prime.
\points{10}
\end{task}
\<close>
lemma phi_prime [simp]:
  assumes "prime p" shows "\<phi> p = (p-1)"
(*<*) oops (*>*) 

text \<open>\begin{task}
The result above can be generalised to $\phi(p^j)=p^j-p^{j-1}$, where $p$ is prime and $j>0$.
\points{25}
\end{task}
\<close>
lemma phi_prime_power [simp]:
  assumes "prime p" "j > 0" shows "\<phi> (p ^ j) = p ^ j - p ^ (j-1)"
(*<*) oops (*>*) 

text \<open>
\noindent\emph{Hint}: none of these proofs require induction. Typically they involve manipulations of sets of positive integers,
perhaps using equational reasoning.
\newpage\<close>

(*<*)
end
(*>*)