section \<open>BIGNAT - Specification and Verification\<close>

text \<open>
Hardware platforms have a limit on the largest number they can represent.
This is usually fixed by the bit lengths of registers and ALUs used.

In order to be able to perform calculations that require arbitrarily large
numbers, the provided arithmetic operations need to be extended in order for
them to work on an abstract data type representing numbers of arbitrary size.

In this project you will build and verify an implementation for BIGNAT,
an abstract data type representing natural numbers of arbitrary size.

(Adapted from \<^url>\<open>http://isabelle.in.tum.de/exercises/proj/bignat/ex.pdf\<close>)
\<close>

theory Project_BIGNAT
  imports Main
begin

subsection \<open>Representation\<close>

text \<open>
A BIGNAT is represented by a list of natural numbers in a range supported by
the target machine. In our case, this will be all natural numbers smaller than
a given base \<open>b\<close>.

Note: Natural numbers in Isabelle are of arbitrary size.
\<close>

type_synonym bignat = "nat list"

text \<open>
Define a function \<open>valid\<close> that takes a base and checks if a given BIGNAT
is valid.
\<close>
fun valid :: "nat \<Rightarrow> bignat \<Rightarrow> bool"
  where
    "valid b n = undefined"

text \<open>
Define a function \<open>val\<close> that takes a BIGNAT and its corresponding base,
and returns the natural number represented by the BIGNAT.
\<close>
fun val :: "nat \<Rightarrow> bignat \<Rightarrow> nat"
  where
    "val b n = undefined"


subsection \<open>Addition\<close>

text \<open>
Define a function \<open>add\<close> that adds two BIGNATs with the same base.
Make sure that your algorithm preserves the validity of the BIGNAT
representation.
\<close>
fun add :: "nat \<Rightarrow> bignat \<Rightarrow> bignat \<Rightarrow> bignat"
  where
    "add b m n = undefined"

text \<open>
Using @{const val}, verify formally that your @{const add} function computes
the sum of two BIGNATs correctly.
\<close>
lemma val_add: "val b (add b m n) = val b m + val b n"
  sorry

text \<open>
Using @{const valid}, verify formally that your function @{const add} preserves
the validity of the BIGNAT representation.
\<close>
lemma valid_add:
  assumes "valid b m" and "valid b n"
  shows "valid b (add b m n)"
  sorry


subsection \<open>Multiplication\<close>

text \<open>
Define a function \<open>mult\<close> that multiplies two BIGNATs with the same base.
You may use @{const add}, but not so often as to make the solution trivial.
Make sure that your algorithm preserves the validity of the BIGNAT
representation.
\<close>
fun mult :: "nat \<Rightarrow> bignat \<Rightarrow> bignat \<Rightarrow> bignat"
  where
    "mult b m n = undefined"

text \<open>
Using \<open>val\<close>, verify formally that your @{const mult} function computes the
product of two BIGNATs correctly.
\<close>
lemma val_mult: "val b (mult b m n) = val b m * val b n"
  sorry

text \<open>
Using \<open>valid\<close>, verify formally that your @{const mult} function preserves
the validity of the BIGNAT representation.
\<close>
lemma valid_mult:
  assumes "valid b m" and "valid b n"
  shows "valid b (mult b m n)"
  sorry

end