Isabelle coursework exercises
Copyright By PowCoder代写 加微信 powcoder
Autumn term 2022
There are four tasks, all worth the same number of marks. They appear in
roughly increasing order of difficulty. The first three tasks are independent from
each other, so failure to complete one task should have no bearing on later tasks.
Task 4 builds on Task 3. Tasks labelled (?) are expected to be reasonably straight-
forward. Tasks labelled (??) should be manageable but may require quite a bit
of thinking, and it may be necessary to consult additional sources of information,
such as the Isabelle manual and Stack Overflow. Tasks labelled (???) are more
ambitious still.
Marking principles. It is not expected that students will complete all parts of
all the tasks. Partial credit will be given to partial answers. If you are unable
to complete a proof, partial credit will be given for explaining your thinking
process in the form of (*comments*) in the Isabelle file.
Submission process. You are expected to produce a single Isabelle theory
file called YourName.thy. This file should contain all of the definitions and
proofs for all of the tasks below that you have attempted.
Plagiarism policy. You are allowed to consult the coursework tasks from pre-
vious years – the questions and model solutions for these are available. You
are allowed to consult internet sources like Isabelle tutorials. You are allowed
to work together with the other student in your pair. You are allowed to ask
questions on Stack Overflow or the Isabelle mailing list, but make your ques-
tions generic (e.g. “Why isn’t the subst method working as I expected?”);
please don’t ask for solutions to these specific tasks! And please don’t share
your answers to these tasks outside of your own pair. If you would like to
share your answers to these tasks publicly, e.g. on a public GitHub repo, you
are welcome to do so, but please check with me first, because some students
may still be working on the coursework with an extended deadline.
Task 1 (?) This task is about designing circuitry that implements binary addition,
and proving that the circuitry is correct.
Consider the following fulladder function, which takes three Boolean
inputs (a, b, and cin) and uses two half-adders and an OR gate to produce
two Boolean outputs (cout and s):
1 fulladder (a,b,cin) = (
2 let (tmp1, tmp2) = halfadder(a,b) in
3 let (tmp3, s) = halfadder(cin, tmp2) in
4 let cout = tmp1 | tmp3 in
5 (cout, s))
Provide a suitable definition of halfadder, and then use Isabelle to prove
that fulladder is correct, in the sense that
2× cout+ s = a+ b+ cin.
Task 2 (??) Prove the following theorem in Isabelle:
Theorem. Raising any natural number to its fifth power does
not change its last (decimal) digit. In other words: n5 mod 10 =
Also prove that the theorem does not apply to sixth powers.
Task 3 (??) This task builds on the circuit datatype from the worksheet. We
shall add an extra optimisation that exploits the following Boolean identi-
The following function, called opt_ident, traverses a given circuit look-
ing for opportunities to apply those identities (in the left-to-right direction).
Each time the identity is applied, one gate is removed from the circuit, thus
reducing its area.
1 fun opt_ident where
2 “opt_ident (NOT c) = NOT (opt_ident c)”
3 | “opt_ident (AND c1 c2) = (
4 let c1’ = opt_ident c1 in
5 let c2’ = opt_ident c2 in
6 if c1’ = c2’ then c1’ else AND c1’ c2’)”
7 | “opt_ident (OR c1 c2) = (
8 let c1’ = opt_ident c1 in
9 let c2’ = opt_ident c2 in
10 if c1’ = c2’ then c1’ else OR c1’ c2’)”
11 | “opt_ident TRUE = TRUE”
12 | “opt_ident FALSE = FALSE”
13 | “opt_ident (INPUT i) = INPUT i”
Use Isabelle to prove that opt_ident is correct. That is, prove for any cir-
cuit c that opt_ident(c) has the same input/output behaviour as c. Also
prove that opt_ident never increases circuit area (as measured by count-
ing the number of gates).
Task 4 (???) This task also builds on the circuit datatype from the worksheet.
By adapting opt_ident from the previous task or otherwise, implement
a function called opt_redundancy that exploits the following Boolean
identities:
a ∨ (a ∧ b) ≡ a
(a ∧ b) ∨ a ≡ a
a ∧ (a ∨ b) ≡ a
(a ∨ b) ∧ a ≡ a
Use Isabelle to prove that opt_redundancy is correct. Also prove that it
never increases circuit area.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com