supleed2/ELEC70056-HSV-CW1
1
0
Fork 0
mirror of https://github.com/supleed2/ELEC70056-HSV-CW1.git synced 2024-12-22 13:45:48 +00:00
Code Issues Packages Projects Releases Wiki Activity

finalised cw for 2021

Browse source
This commit is contained in:
John Wickerson 2021-11-01 06:34:44 +00:00
commit 0e8514ef99
26 changed files with 1832 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
README.md Normal file
View file

@ -0,0 +1,5 @@
# Hardware & Software Verification
This is the homepage of the above-named module, which is offered to MSc and 4th-year MEng students at Imperial College London.
The module is run by Dr John Wickerson (software) and Professor Pete Harrod (hardware).

BIN
dafny/2019/dafny_exercises_2019.pdf Normal file
View file

Binary file not shown.

175
dafny/2019/solutions_2019.dfy Normal file
View file

@ -0,0 +1,175 @@
// Dafny coursework solutions
// Autumn term, 2019
//
// Authors: John Wickerson and Matt Windsor
predicate sorted_between(A:array<int>, lo:int, hi:int)
reads A
requires 0 <= lo <= hi <= A.Length
{
forall m,n :: lo <= m < n < hi ==> A[m] <= A[n]
}
// Task 1
predicate sorted(A:array<int>)
reads A
{
sorted_between(A,0,A.Length)
}
predicate partitioned(A:array<int>, index:int)
reads A
requires 0 <= index <= A.Length
{
forall i,j :: 0 <= i < index <= j < A.Length ==> A[i] <= A[j]
}
// Task 2
method bubble_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant partitioned(A, A.Length - i)
invariant sorted_between(A, A.Length - i, A.Length)
decreases A.Length - i
{
var j := 1;
while j < A.Length - i
invariant 0 <= i <= A.Length
invariant 0 < j <= A.Length - i
invariant partitioned(A, A.Length - i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant forall m :: 0 <= m < j-1 ==> A[m] <= A[j-1]
decreases A.Length - j
{
if A[j-1] > A[j] {
A[j-1], A[j] := A[j], A[j-1];
}
j := j+1;
}
i := i+1;
}
}
// Task 3
method selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant sorted_between(A, 0, i)
invariant partitioned(A, i)
decreases A.Length - i
{
var k := i;
var j := i+1;
while j < A.Length
invariant 0 <= i <= k < j <= A.Length
invariant sorted_between(A, 0, i)
invariant partitioned(A, i)
invariant forall n :: i <= n < j ==> A[k] <= A[n]
decreases A.Length - j
{
if A[k] > A[j] {
k := j;
}
j := j+1;
}
A[k], A[i] := A[i], A[k];
i := i + 1;
}
}
// Task 4
method insertion_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant sorted_between(A, 0, i)
decreases A.Length - i
{
var j := i;
var tmp := A[j];
while 1 <= j && tmp < A[j-1]
invariant 0 <= j <= i <= A.Length
invariant forall l :: j <= l < i ==> tmp < A[l]
invariant sorted_between(A, 0, i)
invariant j < i ==> sorted_between(A, 0, i+1)
decreases j
{
A[j] := A[j-1];
j := j-1;
}
A[j] := tmp;
i := i+1;
}
}
// Task 5
method shellsort(A:array<int>)
modifies A
ensures sorted(A)
{
var stride := A.Length / 2;
while 0 < stride
invariant 0 <= stride
invariant stride == 0 ==> sorted(A)
decreases stride
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant stride==1 ==> sorted_between(A, 0, i)
decreases A.Length - i
{
var j := i;
var tmp := A[j];
while stride <= j && tmp < A[j-stride]
invariant 0 <= j <= i <= A.Length
invariant stride==1 ==> forall l :: j <= l < i ==> tmp < A[l]
invariant stride==1 ==> sorted_between(A, 0, i)
invariant stride==1 ==> j < i ==> sorted_between(A, 0, i+1)
decreases j
{
A[j] := A[j-stride];
j := j-stride;
}
A[j] := tmp;
i := i+1;
}
stride := stride / 2;
}
}
// Task 6
method john_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant forall j :: 0 <= j < i ==> A[j] == 42
decreases A.Length - i
{
A[i] := 42;
i := i + 1;
}
}
method Main() {
var A:array<int> := new int[7] [4,0,1,9,7,1,2];
print "Before: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
bubble_sort(A);
print "After: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
}

110
dafny/2019/tasks_2019.dfy Normal file
View file

@ -0,0 +1,110 @@
// Dafny coursework tasks
// Autumn term, 2019
//
// Authors: John Wickerson and Matt Windsor
// Task 1
predicate sorted(A:array<int>)
reads A
{
forall m,n :: 0 <= m < n < A.Length ==> A[m] <= A[n]
}
// Task 2
method bubble_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length {
var j := 1;
while j < A.Length - i {
if A[j-1] > A[j] {
A[j-1], A[j] := A[j], A[j-1];
}
j := j+1;
}
i := i+1;
}
}
// Task 3
method selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length {
var k := i;
var j := i+1;
while j < A.Length {
if A[k] > A[j] {
k := j;
}
j := j+1;
}
A[k], A[i] := A[i], A[k];
i := i + 1;
}
}
// Task 4
method insertion_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length {
var j := i;
var tmp := A[j];
while 1 <= j && tmp < A[j-1] {
A[j] := A[j-1];
j := j-1;
}
A[j] := tmp;
i := i+1;
}
}
// Task 5
method shellsort(A:array<int>)
modifies A
ensures sorted(A)
{
var stride := A.Length / 2;
while 0 < stride {
var i := 0;
while i < A.Length {
var j := i;
var tmp := A[j];
while stride <= j && tmp < A[j-stride] {
A[j] := A[j-stride];
j := j-stride;
}
A[j] := tmp;
i := i+1;
}
stride := stride / 2;
}
}
// Task 6
method john_sort(A:array<int>)
modifies A
ensures sorted(A)
{
var i := 0;
while i < A.Length {
A[i] := 42;
i := i + 1;
}
}
method Main() {
var A:array<int> := new int[7] [4,0,1,9,7,1,2];
print "Before: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
bubble_sort(A);
print "After: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
}

BIN
dafny/2020/dafny_exercises_2020.pdf Normal file
View file

Binary file not shown.

200
dafny/2020/solutions_2020.dfy Normal file
View file

@ -0,0 +1,200 @@
// Dafny coursework solutions
// Autumn term, 2020
//
// Authors: John Wickerson and Matt Windsor
// Task 1
predicate zeroes(A:array<int>)
reads A
{
forall i :: 0 <= i < A.Length ==> A[i] == 0
}
method resetArray(A:array<int>)
ensures zeroes(A)
modifies A
{
var i := 0;
while i < A.Length
invariant 0 <= i <= A.Length
invariant forall j :: 0 <= j < i ==> A[j] == 0
decreases A.Length - i
{
A[i] := 0;
i := i + 1;
}
}
predicate sorted_between(A:array<int>, lo:int, hi:int)
reads A
{
forall m,n :: 0 <= lo <= m < n < hi <= A.Length ==> A[m] <= A[n]
}
predicate sorted(A:array<int>)
reads A
{
sorted_between(A,0,A.Length)
}
predicate partitioned(A:array<int>, index:int)
reads A
{
forall i,j :: 0 <= i < index <= j < A.Length ==> A[i] <= A[j]
}
// Task 2
method backwards_selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := A.Length;
while 0 < i
invariant 0 <= i <= A.Length
invariant sorted_between(A, i, A.Length)
invariant partitioned(A, i)
decreases i
{
var max := 0;
var j := 1;
while j < i
invariant 0 <= max < j <= i
invariant forall n :: 0 <= n < j ==> A[n] <= A[max]
decreases i - j
{
if A[max] < A[j] {
max := j;
}
j := j+1;
}
A[max], A[i-1] := A[i-1], A[max];
i := i - 1;
}
}
// Task 3
method recursive_selection_sort_inner(A:array<int>, i:int)
requires 0 <= i <= A.Length
requires sorted_between(A, 0, i)
requires partitioned(A, i)
ensures sorted(A)
modifies A
decreases A.Length - i
{
if i == A.Length {
return;
}
var k := i;
var j := i + 1;
while j < A.Length
invariant 0 <= i <= k < j <= A.Length
invariant forall n :: i <= n < j ==> A[k] <= A[n]
decreases A.Length - j
{
if A[k] > A[j] {
k := j;
}
j := j+1;
}
A[k], A[i] := A[i], A[k];
recursive_selection_sort_inner(A, i + 1);
}
method recursive_selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
recursive_selection_sort_inner(A, 0);
}
// Task 4
method bubble_sort_with_early_stop(A:array<int>)
ensures sorted(A)
modifies A
{
var stable := false;
var i := 0;
while !stable
invariant 0 <= i <= A.Length + 1
invariant partitioned(A, A.Length - i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant if stable then sorted(A) else i < A.Length + 1
decreases A.Length - i
{
var j := 0;
stable := true;
while j + 1 < A.Length - i
invariant 0 <= i <= A.Length
invariant 0 < A.Length ==> 0 <= j < A.Length
invariant partitioned(A, A.Length - i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant if stable then sorted_between(A, 0, j + 1) else i < A.Length
invariant forall m :: 0 <= m < j < A.Length ==> A[m] <= A[j]
invariant A.Length - i <= j ==> partitioned(A, A.Length - i - 1)
decreases A.Length - j
{
if A[j+1] < A[j] {
A[j], A[j+1] := A[j+1], A[j];
stable := false;
}
j := j+1;
}
i := i+1;
}
}
// Task 5
method cocktail_shaker_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length / 2
invariant i <= A.Length
invariant partitioned(A, A.Length - i)
invariant partitioned(A, i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant sorted_between(A, 0, i)
decreases A.Length - i
{
var j := i;
while j < A.Length - i - 1
invariant j < A.Length - i
invariant partitioned(A, A.Length - i)
invariant partitioned(A, i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant sorted_between(A, 0, i)
invariant forall m :: 0 <= m < j ==> A[m] <= A[j]
decreases A.Length - j
{
if A[j+1] < A[j] {
A[j], A[j+1] := A[j+1], A[j];
}
j := j+1;
}
while i < j
invariant i <= j < A.Length - i
invariant partitioned(A, A.Length - i)
invariant partitioned(A, A.Length - i - 1)
invariant partitioned(A, i)
invariant sorted_between(A, A.Length - i, A.Length)
invariant sorted_between(A, 0, i)
invariant forall m :: j < m < A.Length ==> A[j] <= A[m]
decreases j
{
if A[j-1] > A[j] {
A[j-1], A[j] := A[j], A[j-1];
}
j := j-1;
}
i := i+1;
}
}
method Main() {
var A:array<int> := new int[7] [4,0,1,9,7,1,2];
print "Before: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
recursive_selection_sort(A);
print "After: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
}

122
dafny/2020/tasks_2020.dfy Normal file
View file

@ -0,0 +1,122 @@
// Dafny coursework tasks
// Autumn term, 2020
//
// Authors: John Wickerson and Matt Windsor
predicate sorted(A:array<int>)
reads A
{
forall m,n :: 0 <= m < n < A.Length ==> A[m] <= A[n]
}
// Task 1
method resetArray(A:array<int>)
ensures zeroes(A)
modifies A
{
var i := 0;
while i < A.Length {
A[i] := 0;
i := i + 1;
}
}
// Task 2
method backwards_selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := A.Length;
while 0 < i {
var max := 0;
var j := 1;
while j < i {
if A[max] < A[j] {
max := j;
}
j := j+1;
}
A[max], A[i-1] := A[i-1], A[max];
i := i - 1;
}
}
// Task 3
method recursive_selection_sort_inner(A:array<int>, i:int)
modifies A
{
if i == A.Length {
return;
}
var k := i;
var j := i + 1;
while j < A.Length {
if A[k] > A[j] {
k := j;
}
j := j+1;
}
A[k], A[i] := A[i], A[k];
recursive_selection_sort_inner(A, i + 1);
}
method recursive_selection_sort(A:array<int>)
ensures sorted(A)
modifies A
{
recursive_selection_sort_inner(A, 0);
}
// Task 4
method bubble_sort_with_early_stop(A:array<int>)
ensures sorted(A)
modifies A
{
var stable := false;
var i := 0;
while !stable {
var j := 0;
stable := true;
while j + 1 < A.Length - i {
if A[j+1] < A[j] {
A[j], A[j+1] := A[j+1], A[j];
stable := false;
}
j := j+1;
}
i := i+1;
}
}
// Task 5
method cocktail_shaker_sort(A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length / 2 {
var j := i;
while j < A.Length - i - 1 {
if A[j+1] < A[j] {
A[j], A[j+1] := A[j+1], A[j];
}
j := j+1;
}
while i < j {
if A[j-1] > A[j] {
A[j-1], A[j] := A[j], A[j-1];
}
j := j-1;
}
i := i+1;
}
}
method Main() {
var A:array<int> := new int[7] [4,0,1,9,7,1,2];
print "Before: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
recursive_selection_sort(A);
print "After: ", A[0], A[1], A[2], A[3],
A[4], A[5], A[6], "\n";
}

BIN
dafny/2021/dafny_exercises_2021.pdf Normal file
View file

Binary file not shown.

162
dafny/2021/tasks_2021.dfy Normal file
View file

@ -0,0 +1,162 @@
// Dafny coursework tasks
// Autumn term, 2021
//
// Authors: John Wickerson
predicate sorted(A:array<int>)
reads A
{
forall m,n :: 0 <= m < n < A.Length ==> A[m] <= A[n]
}
// Task 1. Difficulty: *
method create_multiples_of_two(A:array<int>)
ensures forall n :: 0 <= n < A.Length ==> A[n] == 2*n
modifies A
{
// ...
}
// Task 2. Difficulty: **
method exchange_sort (A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length - 1 {
var j := i + 1;
while j < A.Length {
if A[i] > A[j] {
A[i], A[j] := A[j], A[i];
}
j := j + 1;
}
i := i + 1;
}
}
// Task 3. Difficulty: **
method fung_sort (A:array<int>)
ensures sorted(A)
modifies A
{
var i := 0;
while i < A.Length {
var j := 0;
while j < A.Length {
if A[i] < A[j] {
A[i], A[j] := A[j], A[i];
}
j := j+1;
}
i := i+1;
}
}
// Task 4. Difficulty: ***
predicate odd_sorted(A:array<int>, hi:int)
reads A
{
forall i :: 0 <= i ==> 2*i+2 < hi <= A.Length ==> A[2*i + 1] <= A[2*i+2]
}
method odd_even_sort(A:array<int>)
ensures sorted(A)
modifies A
decreases *
{
var is_sorted := false;
while !is_sorted {
is_sorted := true;
var i := 0;
while 2*i+2 < A.Length {
if A[2*i+2] < A[2*i+1] {
A[2*i+1], A[2*i+2] := A[2*i+2], A[2*i+1];
is_sorted := false;
}
i := i+1;
}
i := 0;
while 2*i+1 < A.Length {
if A[2*i+1] < A[2*i] {
A[2*i], A[2*i+1] := A[2*i+1], A[2*i];
is_sorted := false;
}
i := i+1;
}
}
}
// Task 5. Difficulty: ***
method bubble_sort3(A:array<int>)
ensures sorted(A)
modifies A
decreases *
{
var stable := false;
while !stable {
stable := true;
var j := 0;
while 2*j+2 <= A.Length {
if 2*j+2 == A.Length {
if A[2*j+1] < A[2*j] {
A[2*j+1], A[2*j] := A[2*j], A[2*j+1];
stable := false;
}
} else {
if A[2*j+1] < A[2*j] {
A[2*j+1], A[2*j] := A[2*j], A[2*j+1];
stable := false;
}
if A[2*j+2] < A[2*j+1] {
A[2*j+2], A[2*j+1] := A[2*j+1], A[2*j+2];
stable := false;
}
if A[2*j+1] < A[2*j] {
A[2*j+1], A[2*j] := A[2*j], A[2*j+1];
stable := false;
}
}
j := j + 1;
}
}
}
// Task 6. Difficulty: *
function method get_min(a:int, b:int) : int
{
if a <= b then a else b
}
method sort3(a:int, b:int, c:int) returns (min:int, mid:int, max:int)
ensures min in {a,b,c}
ensures mid in {a,b,c}
ensures max in {a,b,c}
ensures a in {min, mid, max}
ensures b in {min, mid, max}
ensures c in {min, mid, max}
ensures min <= mid <= max
{
min := get_min(a, get_min(b,c));
max := -get_min(-a, get_min(-b,-c));
mid := a + b + c - max - min;
}
method print_array(A:array<int>)
{
var i := 0;
while i < A.Length {
print A[i];
i := i + 1;
}
}
method Main()
decreases *
{
var A:array<int> := new int[7] [4,0,1,9,7,1,2];
print "Before: "; print_array(A); print "\n";
exchange_sort(A);
print "After: "; print_array(A); print "\n";
}

BIN
dafny/dafny.pdf Normal file
View file

Binary file not shown.

71
dafny/dafny_worksheet.dfy Normal file
View file

@ -0,0 +1,71 @@
// Source code to accompany Dafny worksheet
//
// Author: John Wickerson
method triangle(n:int) returns (t:int)
requires n >=0
ensures t == n * (n+1) / 2
{
t := 0;
var i := 0;
while i < n
invariant i <= n
invariant t == i * (i+1) / 2
decreases n - i
{
i := i+1;
t := t+i;
}
return t;
}
method max (a:int, b:int) returns (r:int)
ensures r >= a
ensures r >= b
ensures r == a || r == b
{
if a>b {
return a;
} else {
return b;
}
}
predicate contains_upto(A:array<int>, hi:int, v:int)
reads A
requires hi <= A.Length
{
exists j :: 0 <= j < hi && v == A[j]
}
predicate contains(A:array<int>, v:int)
reads A
{
contains_upto(A, A.Length, v)
}
method maxarray (A:array<int>) returns (r:int)
requires A.Length > 0
ensures contains(A, r)
ensures forall j :: 0 <= j < A.Length ==> r >= A[j]
{
r := A[0];
var i := 1;
while i < A.Length
invariant 1 <= i <= A.Length
invariant contains_upto(A, i, r)
invariant forall j :: 0 <= j < i ==> r >= A[j]
decreases A.Length - i
{
if r < A[i] {
r := A[i];
}
i := i+1;
}
assert i == A.Length;
}
method Main() {
var m:int := max(3,5);
print m, "\n";
}

21
isabelle/2019/HSV_tasks_2019.thy Normal file
View file

@ -0,0 +1,21 @@
theory HSV_tasks_2019 imports Main begin
datatype "circuit" =
NOT "circuit"
| AND "circuit" "circuit"
| OR "circuit" "circuit"
| TRUE
| FALSE
| INPUT "int"
section \<open>Starting point for Task 8\<close>
text \<open>The following function calculates the area of a circuit (i.e. number of gates).\<close>
fun area :: "circuit \<Rightarrow> nat" where
"area (NOT c) = 1 + area c"
| "area (AND c1 c2) = 1 + area c1 + area c2"
| "area (OR c1 c2) = 1 + area c1 + area c2"
| "area _ = 0"
end

392
isabelle/2019/HSV_tasks_2019_solutions.thy Normal file
View file

@ -0,0 +1,392 @@
theory HSV_tasks_2019_solutions imports Complex_Main begin
section \<open>Task 1: proving that 2 * sqrt 2 is irrational.\<close>
(* The following theorem is copied from Chapter 3 of the worksheet *)
theorem sqrt2_irrational: "sqrt 2 \<notin> \<rat>"
proof auto
assume "sqrt 2 \<in> \<rat>"
then obtain m n where
"n \<noteq> 0" and "\<bar>sqrt 2\<bar> = real m / real n" and "coprime m n"
by (rule Rats_abs_nat_div_natE)
hence "\<bar>sqrt 2\<bar>^2 = (real m / real n)^2" by auto
hence "2 = (real m / real n)^2" by simp
hence "2 = (real m)^2 / (real n)^2" unfolding power_divide by auto
hence "2 * (real n)^2 = (real m)^2"
by (simp add: nonzero_eq_divide_eq `n \<noteq> 0`)
hence "real (2 * n^2) = (real m)^2" by auto
hence *: "2 * n^2 = m^2"
using of_nat_power_eq_of_nat_cancel_iff by blast
hence "even (m^2)" by presburger
hence "even m" by simp
then obtain m' where "m = 2 * m'" by auto
with * have "2 * n^2 = (2 * m')^2" by auto
hence "2 * n^2 = 4 * m'^2" by simp
hence "n^2 = 2 * m'^2" by simp
hence "even (n^2)" by presburger
hence "even n" by simp
with `even m` and `coprime m n` show False by auto
qed
theorem "2 * sqrt 2 \<notin> \<rat>"
proof auto
assume *: "2 * sqrt 2 \<in> \<rat>"
have "2 \<in> \<rat>" by simp
with * have "2 * sqrt 2 / 2 \<in> \<rat>" using Rats_divide by blast
hence "sqrt 2 \<in> \<rat>" by simp
with sqrt2_irrational show False by simp
qed
section \<open>Task 2: L-numbers.\<close>
fun L :: "nat \<Rightarrow> nat" where
"L n = (if n < 2 then n else 2 + L (n - 1))"
value "L 0" (* should be 0 *)
value "L 1" (* should be 1 *)
value "L 2" (* should be 3 *)
value "L 3" (* should be 5 *)
lemma L_helper: "L (Suc n) = 2 * (Suc n) - 1"
apply (induct n)
apply simp+
done
theorem "L n = (if n = 0 then 0 else 2 * n - 1)"
apply (cases n)
apply simp
using L_helper apply auto
done
section \<open>Task 3: Pyramidal numbers.\<close>
fun py :: "nat \<Rightarrow> nat" where
"py n = (if n = 0 then 0 else n^2 + py (n-1))"
value "py 0" (* 0 *)
value "py 1" (* 1 *)
value "py 2" (* 5 *)
value "py 3" (* 14 *)
value "py 4" (* 30 *)
value "py 5" (* 55 *)
value "py 6" (* 91 *)
theorem "py n = ((2 * n + 1) * (n + 1) * n) div 6"
proof (induct n)
case 0
thus ?case by simp
next
case (Suc n)
assume IH: "py n = ((2 * n + 1) * (n + 1) * n) div 6" (* induction hypothesis *)
have "py (Suc n) = (Suc n)^2 + py n" by simp
also have "... = (Suc n)^2 + ((2 * n + 1) * (n + 1) * n) div 6" using IH by simp
also have "... = (6 * (n + 1)^2 + (2 * n + 1) * (n + 1) * n) div 6" by simp
also have "... = (6 * (n^2 + 2*n + 1) + (2 * n + 1) * (n + 1) * n) div 6"
by (metis Suc_eq_plus1 add_Suc mult_2 one_add_one plus_1_eq_Suc power2_sum power_one)
also have "... = (2 * n * n + 4 * n + 3 * n + 6) * (n + 1) div 6"
by (simp add: add_mult_distrib power2_eq_square distrib_right)
also have "... = (2 * n * (n + 2) + 3 * (n + 2)) * (n + 1) div 6"
by (smt add.assoc distrib_right mult.commute mult_2_right numeral_Bit0)
also have "... = (2 * n + 3) * (n + 2) * (n + 1) div 6"
by (simp add: distrib_right)
also have "... = (2 * Suc n + 1) * (Suc n + 1) * Suc n div 6"
by (metis One_nat_def Suc_1 Suc_eq_plus1 add_Suc_shift distrib_left mult_2 numeral_3_eq_3)
finally show "py (Suc n) = (2 * Suc n + 1) * (Suc n + 1) * Suc n div 6" by assumption
qed
section \<open>Task 4: the opt_NOT optimisation leaves no consecutive NOTs in the circuit.\<close>
datatype "circuit" =
NOT "circuit"
| AND "circuit" "circuit"
| OR "circuit" "circuit"
| TRUE
| FALSE
| INPUT "int"
text \<open>Simulates a circuit given a valuation for each input wire\<close>
fun simulate where
"simulate (AND c1 c2) \<rho> = ((simulate c1 \<rho>) \<and> (simulate c2 \<rho>))"
| "simulate (OR c1 c2) \<rho> = ((simulate c1 \<rho>) \<or> (simulate c2 \<rho>))"
| "simulate (NOT c) \<rho> = (\<not> (simulate c \<rho>))"
| "simulate TRUE \<rho> = True"
| "simulate FALSE \<rho> = False"
| "simulate (INPUT i) \<rho> = \<rho> i"
text \<open>A function that optimises a circuit by removing pairs of consecutive NOT gates\<close>
fun opt_NOT where
"opt_NOT (NOT (NOT c)) = opt_NOT c"
| "opt_NOT (NOT c) = NOT (opt_NOT c)"
| "opt_NOT (AND c1 c2) = AND (opt_NOT c1) (opt_NOT c2)"
| "opt_NOT (OR c1 c2) = OR (opt_NOT c1) (opt_NOT c2)"
| "opt_NOT TRUE = TRUE"
| "opt_NOT FALSE = FALSE"
| "opt_NOT (INPUT i) = INPUT i"
text \<open>We can prove that the optimiser does its job: that the optimised
circuit has no consecutive NOT gates.\<close>
fun has_double_NOT where
"has_double_NOT (NOT (NOT c)) = True"
| "has_double_NOT (NOT c) = has_double_NOT c"
| "has_double_NOT (AND c1 c2) = (has_double_NOT c1 \<or> has_double_NOT c2)"
| "has_double_NOT (OR c1 c2) = (has_double_NOT c1 \<or> has_double_NOT c2)"
| "has_double_NOT _ = False"
theorem opt_NOT_is_complete: "\<not> has_double_NOT (opt_NOT c)"
by (induct c rule: opt_NOT.induct, auto)
section \<open>Task 5: Removing NOT-NOT is idempotent.\<close>
text \<open>We can prove that the optimiser is 'idempotent': applying it twice is the
same as applying it just once.\<close>
theorem opt_NOT_is_idempotent: "opt_NOT (opt_NOT c) = opt_NOT c"
by (induct c rule: opt_NOT.induct, auto)
section \<open>Task 6: Applying De Morgan's laws is sound.\<close>
text \<open>Optimising based on De Morgan's laws\<close>
fun opt_DM where
"opt_DM (NOT c) = NOT (opt_DM c)"
| "opt_DM (AND (NOT c1) (NOT c2)) = NOT (OR (opt_DM c1) (opt_DM c2))"
| "opt_DM (AND c1 c2) = AND (opt_DM c1) (opt_DM c2)"
| "opt_DM (OR (NOT c1) (NOT c2)) = NOT (AND (opt_DM c1) (opt_DM c2))"
| "opt_DM (OR c1 c2) = OR (opt_DM c1) (opt_DM c2)"
| "opt_DM TRUE = TRUE"
| "opt_DM FALSE = FALSE"
| "opt_DM (INPUT i) = INPUT i"
theorem opt_DM_is_sound: "simulate (opt_DM c) \<rho> = simulate c \<rho>"
by (induct rule: opt_DM.induct, auto)
text \<open>The following non-theorem is easily contradicted, e.g.
using c = AND (NOT (NOT TRUE)) (NOT (NOT TRUE)). Therefore,
opt_DM isn't idempotent.\<close>
theorem opt_DM_is_idempotent: "opt_DM (opt_DM c) = opt_DM c"
oops
section \<open>Task 7: Applying both optimisations successively is sound.\<close>
(* The following theorem was provided in the worksheet *)
theorem opt_NOT_is_sound: "simulate (opt_NOT c) \<rho> = simulate c \<rho>"
by (induct rule: opt_NOT.induct, auto)
theorem both_sound: "simulate (opt_DM (opt_NOT c)) \<rho> = simulate c \<rho>"
apply (subst opt_DM_is_sound)
apply (subst opt_NOT_is_sound)
apply auto
done
section \<open>Task 8: Neither optimisation increases the circuit's area.\<close>
text \<open>The following function calculates the area of a circuit (i.e. number of gates).\<close>
fun area :: "circuit \<Rightarrow> nat" where
"area (NOT c) = 1 + area c"
| "area (AND c1 c2) = 1 + area c1 + area c2"
| "area (OR c1 c2) = 1 + area c1 + area c2"
| "area _ = 0"
theorem opt_NOT_doesnt_increase_area: "area (opt_NOT c) \<le> area c"
by (induct rule: opt_NOT.induct, auto)
theorem opt_DM_doesnt_increase_area: "area (opt_DM c) \<le> area c"
by (induct rule: opt_DM.induct, auto)
section \<open>Task 9: Neither optimisation increases the circuit's delay.\<close>
text \<open>Delay (assuming all gates have a delay of 1, and constants and inputs are instantaneous)\<close>
fun delay :: "circuit \<Rightarrow> nat" where
"delay (NOT c) = 1 + delay c"
| "delay (AND c1 c2) = 1 + max (delay c1) (delay c2)"
| "delay (OR c1 c2) = 1 + max (delay c1) (delay c2)"
| "delay _ = 0"
text \<open>We can prove that our optimisations never increase the maximum delay of a circuit.\<close>
theorem opt_NOT_doesnt_increase_delay: "delay (opt_NOT c) \<le> delay c"
by (induct rule: opt_NOT.induct, auto)
theorem opt_DM_doesnt_increase_delay: "delay (opt_DM c) \<le> delay c"
by (induct rule: opt_DM.induct, auto)
section \<open>Task 10: Constant folding.\<close>
text \<open>Here is an optimiser that performs 'constant folding': wherever it sees a gate with
constants (TRUE and FALSE) as inputs, it tries to replace the gate with TRUE, FALSE, or the other
input depending on the logical behaviour of the gate.
For instance, it replaces NOT FALSE with TRUE, AND FALSE c with FALSE for all inputs c, and
OR c FALSE with c.
This optimiser is somewhat more complicated than the other optimisers: it has a lot of rules, and
needs to do analysis on the results of recursively applying itself.
First, we define how it translates NOT gates, AND gates, and OR gates:\<close>
fun opt_CF_NOT where
"opt_CF_NOT TRUE = FALSE"
| "opt_CF_NOT FALSE = TRUE"
| "opt_CF_NOT c = NOT c"
fun opt_CF_AND where
"opt_CF_AND TRUE c2 = c2"
| "opt_CF_AND c1 TRUE = c1"
| "opt_CF_AND FALSE _ = FALSE"
| "opt_CF_AND _ FALSE = FALSE"
| "opt_CF_AND c1 c2 = AND c1 c2"
fun opt_CF_OR where
"opt_CF_OR FALSE c2 = c2"
| "opt_CF_OR c1 FALSE = c1"
| "opt_CF_OR TRUE _ = TRUE"
| "opt_CF_OR _ TRUE = TRUE"
| "opt_CF_OR c1 c2 = OR c1 c2"
text \<open>The actual optimiser just runs the above rewrites on each NOT, AND, and OR gate.\<close>
fun opt_CF where
"opt_CF (NOT c) = opt_CF_NOT (opt_CF c)"
| "opt_CF (AND c1 c2) = opt_CF_AND (opt_CF c1) (opt_CF c2)"
| "opt_CF (OR c1 c2) = opt_CF_OR (opt_CF c1) (opt_CF c2)"
| "opt_CF x = x"
text \<open>To prove the constant folder sound, first consider the soundness of the sub-cases.\<close>
lemma opt_CF_NOT_is_sound: "simulate (opt_CF_NOT c) \<rho> = simulate (NOT c) \<rho>"
by (cases c, auto)
lemma opt_CF_AND_is_sound: "simulate (opt_CF_AND c1 c2) \<rho> = simulate (AND c1 c2) \<rho>"
by (induct c1 c2 rule: opt_CF_AND.induct, auto)
lemma opt_CF_OR_is_sound: "simulate (opt_CF_OR c1 c2) \<rho> = simulate (OR c1 c2) \<rho>"
by (induct c1 c2 rule: opt_CF_OR.induct, auto)
theorem opt_CF_is_sound: "simulate (opt_CF c) \<rho> = simulate c \<rho>"
by (induct c rule: opt_CF.induct,
auto simp add: opt_CF_NOT_is_sound opt_CF_AND_is_sound opt_CF_OR_is_sound)
text \<open>To get an idea of whether the constant folder is complete, we can see whether it reduces a
circuit with only constant inputs into a single TRUE or FALSE constant. First, define what it
means for a circuit to have no inputs, and to be only a constant.\<close>
fun no_inputs where
"no_inputs (NOT c) = no_inputs c"
| "no_inputs (AND c1 c2) = (no_inputs c1 \<and> no_inputs c2)"
| "no_inputs (OR c1 c2) = (no_inputs c1 \<and> no_inputs c2)"
| "no_inputs (INPUT _) = False"
| "no_inputs _ = True"
fun is_constant where
"is_constant c = (c = TRUE \<or> c = FALSE)"
lemma opt_CF_NOT_reduce:
assumes "is_constant c"
shows "is_constant (opt_CF_NOT c)"
using assms
by (cases c, auto)
lemma opt_CF_AND_reduce:
assumes "is_constant c1" and "is_constant c2"
shows "is_constant (opt_CF_AND c1 c2)"
using assms
by (induct c1 c2 rule: opt_CF_AND.induct, auto)
lemma opt_CF_OR_reduce:
assumes "is_constant c1" and "is_constant c2"
shows "is_constant (opt_CF_OR c1 c2)"
using assms
by (induct c1 c2 rule: opt_CF_OR.induct, auto)
theorem opt_CF_reduce:
assumes "no_inputs c"
shows "is_constant (opt_CF c)"
using assms
by (induct c rule: opt_CF.induct,
auto simp add: opt_CF_NOT_reduce opt_CF_AND_reduce opt_CF_OR_reduce)
lemma opt_CF_NOT_doesnt_increase_area: "area (opt_CF_NOT c) \<le> area (NOT c)"
by (cases c, auto)
lemma opt_CF_AND_doesnt_increase_area: "area (opt_CF_AND c1 c2) \<le> area (AND c1 c2)"
by (induct c1 c2 rule: opt_CF_AND.induct, auto)
lemma opt_CF_OR_doesnt_increase_area: "area (opt_CF_OR c1 c2) \<le> area (OR c1 c2)"
by (induct c1 c2 rule: opt_CF_OR.induct, auto)
theorem opt_CF_doesnt_increase_area: "area (opt_CF c) \<le> area c"
proof (induct rule: opt_CF.induct)
case (1 c)
have "area (opt_CF (NOT c))
= area (opt_CF_NOT (opt_CF c))" by simp
also have "... \<le> area (NOT (opt_CF c))"
using opt_CF_NOT_doesnt_increase_area by assumption
also have "... \<le> area (NOT c)" using 1 by simp
finally show ?case by assumption
next
case (2 c1 c2)
have "area (opt_CF (AND c1 c2))
= area (opt_CF_AND (opt_CF c1) (opt_CF c2))" by simp
also have "... \<le> area (AND (opt_CF c1) (opt_CF c2))"
using opt_CF_AND_doesnt_increase_area by assumption
also have "... \<le> area (AND c1 c2)" using 2 by simp
finally show ?case by assumption
next
case (3 c1 c2)
have "area (opt_CF (OR c1 c2))
= area (opt_CF_OR (opt_CF c1) (opt_CF c2))" by simp
also have "... \<le> area (OR (opt_CF c1) (opt_CF c2))"
using opt_CF_OR_doesnt_increase_area by assumption
also have "... \<le> area (OR c1 c2)" using 3 by simp
finally show ?case by assumption
qed simp+
lemma opt_CF_NOT_doesnt_increase_delay: "delay (opt_CF_NOT c) \<le> delay (NOT c)"
by (cases c, auto)
lemma opt_CF_AND_doesnt_increase_delay: "delay (opt_CF_AND c1 c2) \<le> delay (AND c1 c2)"
by (induct c1 c2 rule: opt_CF_AND.induct, auto)
lemma opt_CF_OR_doesnt_increase_delay: "delay (opt_CF_OR c1 c2) \<le> delay (OR c1 c2)"
by (induct c1 c2 rule: opt_CF_OR.induct, auto)
theorem opt_CF_doesnt_increase_delay: "delay (opt_CF c) \<le> delay c"
proof (induct rule: opt_CF.induct)
case (1 c)
have "delay (opt_CF (NOT c))
= delay (opt_CF_NOT (opt_CF c))" by simp
also have "... \<le> delay (NOT (opt_CF c))"
using opt_CF_NOT_doesnt_increase_delay by assumption
also have "... \<le> delay (NOT c)" using 1 by simp
finally show ?case by assumption
next
case (2 c1 c2)
have "delay (opt_CF (AND c1 c2))
= delay (opt_CF_AND (opt_CF c1) (opt_CF c2))" by simp
also have "... \<le> delay (AND (opt_CF c1) (opt_CF c2))"
using opt_CF_AND_doesnt_increase_delay by assumption
also have "... \<le> delay (AND c1 c2)" using 2 by auto
finally show ?case by assumption
next
case (3 c1 c2)
have "delay (opt_CF (OR c1 c2))
= delay (opt_CF_OR (opt_CF c1) (opt_CF c2))" by simp
also have "... \<le> delay (OR (opt_CF c1) (opt_CF c2))"
using opt_CF_OR_doesnt_increase_delay by assumption
also have "... \<le> delay (OR c1 c2)" using 3 by auto
finally show ?case by assumption
qed simp+
section \<open>Task 11: Adding fan-out.\<close>
text \<open>Please see separate file.\<close>
end

204
isabelle/2019/HSV_tasks_2019_solutions_task11.thy Normal file
View file

@ -0,0 +1,204 @@
theory HSV_tasks_2019_solutions_task11 imports Main begin
section \<open>Representation of circuits.\<close>
text \<open>A wire is represented as an integer.\<close>
type_synonym wire = int
datatype gate =
NOT "wire" "wire"
| AND "wire" "wire" "wire"
| OR "wire" "wire" "wire"
| TRUE "wire"
| FALSE "wire"
text \<open>A circuit is represented as a list gates together with a list of output wires.\<close>
type_synonym circuit = "gate list \<times> wire list"
text \<open>Here are some examples of circuits.\<close>
definition "circuit1 == ([NOT 1 2], [2])"
definition "circuit2 == ([NOT 1 3, NOT 2 4, AND 3 4 5, NOT 5 6], [6])"
definition "circuit3 == ([NOT 1 3, NOT 2 4, NOT 1 7, AND 3 4 5, NOT 5 6], [6])"
definition "circuit4 == ([NOT 1 3, NOT 2 4, NOT 1 7, NOT 7 8, AND 3 4 5, NOT 5 6], [6])"
text \<open>Return the input wire(s) of a gate.\<close>
fun inputs_of where
"inputs_of (NOT wi _) = {wi}"
| "inputs_of (AND wi1 wi2 _) = {wi1, wi2}"
| "inputs_of (OR wi1 wi2 _) = {wi1, wi2}"
| "inputs_of (TRUE _) = {}"
| "inputs_of (FALSE _) = {}"
text \<open>Return the output wire of a gate.\<close>
fun output_of where
"output_of (NOT _ wo) = wo"
| "output_of (AND _ _ wo) = wo"
| "output_of (OR _ _ wo) = wo"
| "output_of (TRUE wo) = wo"
| "output_of (FALSE wo) = wo"
section \<open>Evaluating circuits.\<close>
text \<open>A valuation associates every wire with a truth-value.\<close>
type_synonym valuation = "wire \<Rightarrow> bool"
text \<open>A few examples of valuations.\<close>
definition "\<rho>0 == \<lambda>_. True"
definition "\<rho>1 == \<rho>0(1 := True, 2 := False, 3 := True)"
definition "\<rho>2 == \<rho>0(1 := True, 2 := True, 3 := True)"
text \<open>Calculate the output of a single gate, given a valuation.\<close>
fun sim_gate :: "valuation \<Rightarrow> gate \<Rightarrow> bool" where
"sim_gate \<rho> (NOT wi wo) = (\<not> \<rho> wi)"
| "sim_gate \<rho> (AND wi1 wi2 wo) = (\<rho> wi1 \<and> \<rho> wi2)"
| "sim_gate \<rho> (OR wi1 wi2 wo) = (\<rho> wi1 \<or> \<rho> wi2)"
| "sim_gate \<rho> (TRUE wo) = True"
| "sim_gate \<rho> (FALSE wo) = False"
text \<open>Simulates a list of gates, given an initial valuation. Produces a new valuation.\<close>
fun sim_gates :: "valuation \<Rightarrow> gate list \<Rightarrow> valuation" where
"sim_gates \<rho> [] = \<rho>"
| "sim_gates \<rho> (g # gs) = sim_gates (\<rho> (output_of g := sim_gate \<rho> g)) gs"
text \<open>Simulates a circuit, given an initial valuation. Produces a list of
truth-values, one truth-value per output.\<close>
fun sim :: "valuation \<Rightarrow> circuit \<Rightarrow> bool list" where
"sim \<rho> (gs, wos) = map (sim_gates \<rho> gs) wos"
text \<open>Testing the simulator.\<close>
value "sim \<rho>1 circuit1"
value "sim \<rho>2 circuit1"
value "sim \<rho>1 circuit2"
value "sim \<rho>2 circuit2"
value "sim \<rho>1 circuit3"
value "sim \<rho>2 circuit3"
section \<open>Optimising circuits by removing dead gates.\<close>
text \<open>Return the set of wires that lead to an output.\<close>
fun live_wires where
"live_wires ([], wos) = set wos"
| "live_wires (g # gs, wos) = (let ws = live_wires (gs, wos) in
(if output_of g \<in> ws then inputs_of g else {}) \<union> ws)"
value "live_wires ([NOT 1 3, NOT 2 4, NOT 1 7, AND 3 4 5, NOT 5 6], [6])"
value "live_wires ([NOT 1 3, NOT 2 4, NOT 1 7, NOT 7 8, AND 3 4 5, NOT 5 6], [6])"
value "live_wires ([NOT 1 3, NOT 2 4, NOT 1 7, NOT 7 8, AND 3 4 5, NOT 5 6], [6, 8])"
value "live_wires ([NOT 1 3, NOT 2 4, NOT 7 8, AND 3 4 5, NOT 5 6], [6])"
text \<open>This is a helper function for the next function .\<close>
fun remove_dead_inner where
"remove_dead_inner [] wos = []"
| "remove_dead_inner (g # gs) wos =
(let gs' = remove_dead_inner gs wos in
(if output_of g \<in> live_wires (gs', wos) then [g] else []) @ gs')"
text \<open>This function strips out gates that are not needed.\<close>
fun remove_dead where
"remove_dead (gs, wos) = (remove_dead_inner gs wos, wos)"
value "remove_dead circuit2"
value "remove_dead circuit3"
value "remove_dead circuit4"
section \<open>Proving that removing dead gates does not change a circuit's behaviour.\<close>
text \<open>This lemma is obviously false -- it wrongly claims that remove_dead
has no effect on a circuit.\<close>
lemma "remove_dead c = c" oops
text \<open>We shall say that two functions are 'congruent on X' if they coincide on all inputs in X.\<close>
fun cong_on where
"cong_on X f g = (\<forall>x \<in> X. f x = g x)"
text \<open>Congruency is transitive.\<close>
lemma cong_on_trans:
assumes "cong_on X g h"
assumes "cong_on X f g"
shows "cong_on X f h"
using assms by simp
text \<open>This is a rather technical lemma. It says that if two valuations \<rho> and \<rho>' are
congruent on all wires that are live in circuit (g # gs, wos), then the
respective valuations obtained after simulating g remain congruent on all wires
that are live in circuit (gs, wos). \<close>
lemma cong_on_live_wires:
assumes "cong_on (live_wires (g # gs, wos)) \<rho> \<rho>'"
shows "cong_on (live_wires (gs, wos)) (\<rho>(output_of g := sim_gate \<rho> g)) (\<rho>'(output_of g := sim_gate \<rho>' g))"
using assms
apply (cases "output_of g \<in> live_wires (gs, wos)", auto)
apply (cases g, auto)+
done
text \<open>If valuations \<rho> and \<rho>' are congruent on all wires that are live in circuit (gs, wos), then
the respective valuations obtained after simulating gs are congruent on all wires in wos.\<close>
lemma cong_sim_gates:
assumes "cong_on (live_wires (gs, wos)) \<rho> \<rho>'"
shows "cong_on (set wos) (sim_gates \<rho> gs) (sim_gates \<rho>' gs)"
using assms
proof (induct gs arbitrary: \<rho> \<rho>')
case Nil
thus ?case by auto
next
case (Cons g gs)
show ?case
apply (clarsimp simp del: cong_on.simps)
apply (rule Cons.hyps[OF cong_on_live_wires[OF Cons.prems]])
done
qed
text \<open>This is a slightly unwrapped version of the main theorem below.\<close>
lemma sim_remove_dead:
"cong_on (set wos) (sim_gates \<rho> (remove_dead_inner gs wos)) (sim_gates \<rho> gs)"
proof (induct gs arbitrary: \<rho>)
case Nil
thus ?case by simp
next
case (Cons g gs \<rho>)
show ?case
proof (cases "output_of g \<in> live_wires (remove_dead (gs, wos))")
case True
thus ?thesis using Cons.hyps by auto
next
case False
thus ?thesis
apply (simp del: cong_on.simps)
apply (rule cong_on_trans)
apply (rule Cons.hyps[of "\<rho>(output_of g := sim_gate \<rho> g)"])
apply (rule cong_sim_gates)
apply clarsimp
done
qed
qed
text \<open>We define a convenient shorthand for expressing that two circuits have the same behaviour.\<close>
fun sim_equiv (infix "\<sim>" 50) where
"c1 \<sim> c2 = (\<forall>\<rho>. sim \<rho> c1 = sim \<rho> c2)"
text \<open>Main theorem: removing the dead gates from a circuit does not change its behaviour.\<close>
theorem "remove_dead c \<sim> c"
using sim_remove_dead by (cases c, auto)
end

BIN
isabelle/2019/isabelle_exercises_2019.pdf Normal file
View file

Binary file not shown.

92
isabelle/2020/HSV_tasks_2020.thy Normal file
View file

@ -0,0 +1,92 @@
theory HSV_tasks_2020 imports Complex_Main begin
section \<open>Task 1: proving that "3 / sqrt 2" is irrational.\<close>
(* In case it is helpful, the following theorem is copied from Chapter 3 of the worksheet. *)
theorem sqrt2_irrational: "sqrt 2 \<notin> \<rat>"
proof auto
assume "sqrt 2 \<in> \<rat>"
then obtain m n where
"n \<noteq> 0" and "\<bar>sqrt 2\<bar> = real m / real n" and "coprime m n"
by (rule Rats_abs_nat_div_natE)
hence "\<bar>sqrt 2\<bar>^2 = (real m / real n)^2" by auto
hence "2 = (real m / real n)^2" by simp
hence "2 = (real m)^2 / (real n)^2" unfolding power_divide by auto
hence "2 * (real n)^2 = (real m)^2"
by (simp add: nonzero_eq_divide_eq `n \<noteq> 0`)
hence "real (2 * n^2) = (real m)^2" by auto
hence *: "2 * n^2 = m^2"
using of_nat_power_eq_of_nat_cancel_iff by blast
hence "even (m^2)" by presburger
hence "even m" by simp
then obtain m' where "m = 2 * m'" by auto
with * have "2 * n^2 = (2 * m')^2" by auto
hence "2 * n^2 = 4 * m'^2" by simp
hence "n^2 = 2 * m'^2" by simp
hence "even (n^2)" by presburger
hence "even n" by simp
with `even m` and `coprime m n` show False by auto
qed
theorem "3 / sqrt 2 \<notin> \<rat>"
sorry (* TODO: Complete this proof. *)
section \<open>Task 2: Centred pentagonal numbers.\<close>
fun pent :: "nat \<Rightarrow> nat" where
"pent n = (if n = 0 then 1 else 5 * n + pent (n - 1))"
value "pent 0" (* should be 1 *)
value "pent 1" (* should be 6 *)
value "pent 2" (* should be 16 *)
value "pent 3" (* should be 31 *)
theorem "pent n = (5 * n^2 + 5 * n + 2) div 2"
sorry (* TODO: Complete this proof. *)
section \<open>Task 3: Lucas numbers.\<close>
fun fib :: "nat \<Rightarrow> nat" where
"fib n = (if n = 0 then 0 else if n = 1 then 1 else fib (n - 1) + fib (n - 2))"
value "fib 0" (* should be 0 *)
value "fib 1" (* should be 1 *)
value "fib 2" (* should be 1 *)
value "fib 3" (* should be 2 *)
thm fib.induct (* rule induction theorem for fib *)
(* TODO: Complete this task. *)
section \<open>Task 4: Balancing circuits.\<close>
(* Here is a datatype for representing circuits, copied from the worksheet *)
datatype "circuit" =
NOT "circuit"
| AND "circuit" "circuit"
| OR "circuit" "circuit"
| TRUE
| FALSE
| INPUT "int"
text \<open>Delay (assuming all gates have a delay of 1)\<close>
(* The following "delay" function also appeared in the 2019 coursework exercises. *)
fun delay :: "circuit \<Rightarrow> nat" where
"delay (NOT c) = 1 + delay c"
| "delay (AND c1 c2) = 1 + max (delay c1) (delay c2)"
| "delay (OR c1 c2) = 1 + max (delay c1) (delay c2)"
| "delay _ = 0"
(* TODO: Complete this task. *)
section \<open>Task 5: Extending with NAND gates.\<close>
(* TODO: Complete this task. *)
end

BIN
isabelle/2020/isabelle_exercises_2020.pdf Normal file
View file

Binary file not shown.

59
isabelle/HSV_chapter3.thy Normal file
View file

@ -0,0 +1,59 @@
theory HSV_chapter3 imports Complex_Main begin
(* We use the following command to search Isabelle's library
for theorems that contain a particular pattern. *)
find_theorems "_ \<in> \<rat>"
thm Rats_abs_nat_div_natE
find_theorems "(_ / _)^_"
thm power_divide
(* A proof that the square root of 2 is irrational. *)
theorem sqrt2_irrational: "sqrt 2 \<notin> \<rat>"
proof auto
assume "sqrt 2 \<in> \<rat>"
then obtain m n where
"n \<noteq> 0" and "\<bar>sqrt 2\<bar> = real m / real n" and "coprime m n"
by (rule Rats_abs_nat_div_natE)
hence "\<bar>sqrt 2\<bar>^2 = (real m / real n)^2" by auto
hence "2 = (real m / real n)^2" by simp
hence "2 = (real m)^2 / (real n)^2" unfolding power_divide by auto
hence "2 * (real n)^2 = (real m)^2"
by (simp add: nonzero_eq_divide_eq `n \<noteq> 0`)
hence "real (2 * n^2) = (real m)^2" by auto
hence *: "2 * n^2 = m^2"
using of_nat_power_eq_of_nat_cancel_iff by blast
hence "even (m^2)" by presburger
hence "even m" by simp
then obtain m' where "m = 2 * m'" by auto
with * have "2 * n^2 = (2 * m')^2" by auto
hence "2 * n^2 = 4 * m'^2" by simp
hence "n^2 = 2 * m'^2" by simp
hence "even (n^2)" by presburger
hence "even n" by simp
with `even m` and `coprime m n` show False by auto
qed
(* A proof that there is no greatest even number. *)
theorem "\<forall>n::int. even n \<longrightarrow> (\<exists>m. even m \<and> m > n)"
proof clarify
fix n::int
assume "even n"
hence "even (n+2)" by simp
moreover
have "n < (n+2)" by simp
ultimately
show "\<exists>m. even m \<and> n < m" by blast
qed
(* The same proof in the procedural style. *)
theorem "\<forall>n::int. even n \<longrightarrow> (\<exists>m. even m \<and> m > n)"
apply clarify
apply (rule_tac x="n+2" in exI)
apply (rule conjI)
apply simp
apply (thin_tac "even n")
apply simp
done
end

83
isabelle/HSV_chapter4.thy Normal file
View file

@ -0,0 +1,83 @@
theory HSV_chapter4 imports Complex_Main begin
(* Triangle numbers *)
fun triangle :: "nat \<Rightarrow> nat" where
"triangle n = (if n = 0 then 0 else n + triangle (n-1))"
value "triangle 1"
value "triangle 2"
value "triangle 3"
theorem triangle_closed_form: "triangle n = (n+1) * n div 2"
apply (induct n)
apply simp+
done
(* Tetrahedral numbers *)
fun tet :: "nat \<Rightarrow> nat" where
"tet n = (if n = 0 then 0 else triangle n + tet (n-1))"
value "tet 1" (* 1 *)
value "tet 2" (* 4 *)
value "tet 3" (* 10 *)
value "tet 4" (* 20 *)
value "tet 5" (* 35 *)
value "tet 6" (* 56 *)
find_theorems "_ div ?x + _ div ?x"
thm div_add
(* Proving that closed form is equivalent to recursive definition *)
theorem "tet n = ((n + 2) * (n + 1) * n) div 6"
proof (induct n)
case 0
show ?case by simp
next
case (Suc k)
(* induction hypothesis *)
assume IH: "tet k = (k + 2) * (k + 1) * k div 6"
(* establish a useful fact and label it "*" *)
have "2 dvd (k + 2) * (k + 1)" by simp
hence *: "6 dvd (k + 2) * (k + 1) * 3" by presburger
(* establish another useful fact and label it "**" *)
have "2 dvd (k + 2) * (k + 1) * k" by simp
moreover have "3 dvd (k + 2) * (k + 1) * k"
proof -
{
assume "k mod 3 = 0"
hence "3 dvd k" by presburger
hence "3 dvd (k + 2) * (k + 1) * k" by fastforce
} moreover {
assume "k mod 3 = 1"
hence "3 dvd (k + 2)" by presburger
hence "3 dvd (k + 2) * (k + 1) * k" by fastforce
} moreover {
assume "k mod 3 = 2"
hence "3 dvd (k + 1)" by presburger
hence "3 dvd (k + 2) * (k + 1) * k" by fastforce
} ultimately
show "3 dvd (k + 2) * (k + 1) * k" by linarith
qed
ultimately have **: "6 dvd (k + 2) * (k + 1) * k" by presburger
(* the actual proof *)
have "tet (Suc k) = triangle (Suc k) + tet k"
by simp
also have "... = (k + 2) * (k + 1) div 2 + tet k"
using triangle_closed_form by simp
also have "... = (k + 2) * (k + 1) div 2 + (k + 2) * (k + 1) * k div 6"
using IH by simp
also have "... = ((k + 2) * (k + 1) * 3 + (k + 2) * (k + 1) * k) div 6"
using div_add[OF * **] by simp
also have "... = (k + 2) * (k + 1) * (k + 3) div 6"
by (simp add: distrib_left)
also have "... = (Suc k + 2) * (Suc k + 1) * Suc k div 6"
by (metis One_nat_def Suc_1 add.commute add_Suc_shift mult.assoc
mult.commute numeral_3_eq_3 plus_1_eq_Suc)
finally show ?case by assumption
qed
end

136
isabelle/HSV_chapter5.thy Normal file
View file

@ -0,0 +1,136 @@
theory HSV_chapter5 imports Main begin
section \<open>Representing circuits (cf. worksheet Section 5.1)\<close>
text \<open>Defining a data structure to represent fan-out-free circuits with numbered inputs\<close>
datatype "circuit" =
NOT "circuit"
| AND "circuit" "circuit"
| OR "circuit" "circuit"
| TRUE
| FALSE
| INPUT "int"
text \<open>A few example circuits\<close>
definition "circuit1 == AND (INPUT 1) (INPUT 2)"
definition "circuit2 == OR (NOT circuit1) FALSE"
definition "circuit3 == NOT (NOT circuit2)"
definition "circuit4 == AND circuit3 (INPUT 3)"
section \<open>Simulating circuits (cf. worksheet Section 5.2)\<close>
text \<open>Simulates a circuit given a valuation for each input wire\<close>
fun simulate where
"simulate (AND c1 c2) \<rho> = ((simulate c1 \<rho>) \<and> (simulate c2 \<rho>))"
| "simulate (OR c1 c2) \<rho> = ((simulate c1 \<rho>) \<or> (simulate c2 \<rho>))"
| "simulate (NOT c) \<rho> = (\<not> (simulate c \<rho>))"
| "simulate TRUE \<rho> = True"
| "simulate FALSE \<rho> = False"
| "simulate (INPUT i) \<rho> = \<rho> i"
text \<open>A few example valuations\<close>
definition "\<rho>0 == \<lambda>_. True"
definition "\<rho>1 == \<rho>0(1 := True, 2 := False, 3 := True)"
definition "\<rho>2 == \<rho>0(1 := True, 2 := True, 3 := True)"
text \<open>Trying out the simulator\<close>
value "simulate circuit1 \<rho>1"
value "simulate circuit2 \<rho>1"
value "simulate circuit3 \<rho>1"
value "simulate circuit4 \<rho>1"
value "simulate circuit1 \<rho>2"
value "simulate circuit2 \<rho>2"
value "simulate circuit3 \<rho>2"
value "simulate circuit4 \<rho>2"
section \<open>Structural induction on circuits (cf. worksheet Section 5.3)\<close>
text \<open>A function that switches each pair of wires entering an OR or AND gate\<close>
fun mirror where
"mirror (NOT c) = NOT (mirror c)"
| "mirror (AND c1 c2) = AND (mirror c2) (mirror c1)"
| "mirror (OR c1 c2) = OR (mirror c2) (mirror c1)"
| "mirror TRUE = TRUE"
| "mirror FALSE = FALSE"
| "mirror (INPUT i) = INPUT i"
value "circuit1"
value "mirror circuit1"
value "circuit2"
value "mirror circuit2"
text \<open>The following non-theorem is easily contradicted.\<close>
theorem "mirror c = c"
oops
text \<open>Proving that mirroring doesn't affect simulation behaviour.\<close>
theorem mirror_is_sound: "simulate (mirror c) \<rho> = simulate c \<rho>"
by (induct c, auto)
section \<open>A simple circuit optimiser (cf. worksheet Section 5.4)\<close>
text \<open>A function that optimises a circuit by removing pairs of consecutive NOT gates\<close>
fun opt_NOT where
"opt_NOT (NOT (NOT c)) = opt_NOT c"
| "opt_NOT (NOT c) = NOT (opt_NOT c)"
| "opt_NOT (AND c1 c2) = AND (opt_NOT c1) (opt_NOT c2)"
| "opt_NOT (OR c1 c2) = OR (opt_NOT c1) (opt_NOT c2)"
| "opt_NOT TRUE = TRUE"
| "opt_NOT FALSE = FALSE"
| "opt_NOT (INPUT i) = INPUT i"
text \<open>Trying out the optimiser\<close>
value "circuit1"
value "opt_NOT circuit1"
value "circuit2"
value "opt_NOT circuit2"
value "circuit3"
value "opt_NOT circuit3"
value "circuit4"
value "opt_NOT circuit4"
section \<open>Rule induction (cf. worksheet Section 5.5)\<close>
text \<open>A Fibonacci function that demonstrates complex recursion schemes\<close>
fun f :: "nat \<Rightarrow> nat" where
"f (Suc (Suc n)) = f n + f (Suc n)"
| "f (Suc 0) = 1"
| "f 0 = 1"
thm f.induct (* rule induction theorem for f *)
text \<open>We need to prove a stronger version of the theorem below
first, in order to make the inductive step work. Just like how
it often goes with loop invariants in Dafny!\<close>
lemma helper: "f n \<ge> n \<and> f n \<ge> 1"
by (rule f.induct[of "\<lambda>n. f n \<ge> n \<and> f n \<ge> 1"], auto)
text \<open>The nth Fibonacci number is greater than or equal to n\<close>
theorem "f n \<ge> n"
using helper by simp
section \<open>Verifying our optimiser (cf. worksheet Section 5.6)\<close>
text \<open>The following non-theorem is easily contradicted.\<close>
theorem "opt_NOT c = c"
oops
text \<open>The following theorem says that the optimiser is sound.\<close>
theorem opt_NOT_is_sound: "simulate (opt_NOT c) \<rho> = simulate c \<rho>"
by (induct rule:opt_NOT.induct, auto)
end

BIN
isabelle/isabelle.pdf Normal file
View file

Binary file not shown.

BIN
lectures/lecture10_solving.pdf Normal file
View file

Binary file not shown.

BIN
lectures/lecture1_intro_john.pdf Normal file
View file

Binary file not shown.

BIN
lectures/lecture3_dafny.pdf Normal file
View file

Binary file not shown.

BIN
lectures/lecture4_isabelle.pdf Normal file
View file

Binary file not shown.

BIN
lectures/lecture5_isabelle2.pdf Normal file
View file

Binary file not shown.