From d33337a7a6dbd3c6817194128b861de34863107a Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Fri, 21 Jan 2022 21:58:27 +0000 Subject: [PATCH] uploading 2021 solutions --- dafny/2021/solutions_2021.dfy | 227 +++++++ isabelle/2021/HSV_tasks_2021_solutions.thy | 689 +++++++++++++++++++++ 2 files changed, 916 insertions(+) create mode 100644 dafny/2021/solutions_2021.dfy create mode 100644 isabelle/2021/HSV_tasks_2021_solutions.thy diff --git a/dafny/2021/solutions_2021.dfy b/dafny/2021/solutions_2021.dfy new file mode 100644 index 0000000..da0a0d6 --- /dev/null +++ b/dafny/2021/solutions_2021.dfy @@ -0,0 +1,227 @@ +// Dafny coursework solutions +// Autumn term, 2021 +// +// Authors: John Wickerson + + +predicate sorted_between(A:array, lo:int, hi:int) + reads A +{ + forall m,n :: 0 <= lo <= m < n < hi <= A.Length ==> A[m] <= A[n] +} +predicate sorted(A:array) + reads A +{ + sorted_between(A,0,A.Length) +} + +// Task 1. Difficulty: * +method create_multiples_of_two(A:array) +ensures forall n :: 0 <= n < A.Length ==> A[n] == 2*n +modifies A +{ + var i := 0; + while i < A.Length + invariant 0 <= i <= A.Length + invariant forall n :: 0 <= n < i ==> A[n] == 2*n + { + A[i] := 2 * i; + i := i + 1; + } +} + +// Task 2. Difficulty: ** +predicate partitioned(A:array, index:int) + reads A + requires 0 <= index <= A.Length +{ + forall i,j :: 0 <= i < index <= j < A.Length ==> A[i] <= A[j] +} + +method exchange_sort (A:array) +ensures sorted(A) +modifies A +{ + var i := 0; + while i < A.Length - 1 + invariant 0 < A.Length ==> 0 <= i < A.Length + invariant 0 < A.Length ==> partitioned(A, i) + invariant sorted_between(A,0,i+1); + { + var j := i + 1; + while j < A.Length + invariant i < j <= A.Length + invariant partitioned(A, i) + invariant sorted_between(A,0,i+1); + invariant forall k :: i <= k < j ==> A[i] <= A[k] + { + 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) +ensures sorted(A) +modifies A +{ + var i := 0; + while i < A.Length + invariant i <= A.Length + invariant sorted_between (A, 0, i) + { + var j := 0; + while j < A.Length + invariant j <= A.Length + invariant sorted_between (A, 0, i) + invariant 0 < j ==> A[j-1] <= A[i] + invariant i <= j ==> sorted_between (A, 0, i+1) + { + 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, 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) + ensures sorted(A) + modifies A + decreases * +{ + var is_sorted := false; + while !is_sorted + invariant is_sorted ==> sorted(A) + decreases * + { + is_sorted := true; + var i := 0; + while 2*i+2 < A.Length + invariant 0 < A.Length ==> 0 <= 2*i < A.Length + invariant odd_sorted (A, 2*i+1) + { + 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 + invariant 0 <= 2*i <= A.Length + invariant is_sorted ==> odd_sorted (A, A.Length) + invariant is_sorted ==> 2*i+1 < A.Length ==> sorted_between(A, 0, 2*i+1); + invariant is_sorted ==> 2*i+1 >= A.Length ==> sorted_between(A, 0, 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) + ensures sorted(A) + modifies A + decreases * +{ + var stable := false; + while !stable + invariant stable ==> sorted(A) + decreases * + //decreases entropy(A) + { + stable := true; + var j := 0; + while 2*j+2 <= A.Length + invariant stable ==> sorted_between(A, 0, 2*j+1) + invariant stable ==> 2*j+2 == A.Length + 2 ==> sorted_between(A, 0, A.Length) + invariant 2*j+2 <= A.Length + 2 + decreases A.Length - j + { + 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 5, bonus +function method entropy_elem(A:array, i:int, j:int) : int +reads A +requires 0 <= i < j <= A.Length +ensures entropy_elem(A, i, j) >= 0 +decreases A.Length - j +{ + if j == A.Length then 0 else + entropy_elem(A, i, j+1) + (if A[i] > A[j] then 1 else 0) +} + +function method entropy_from(A:array, i:int) : int +reads A +requires 0 <= i <= A.Length +ensures entropy_from(A, i) >= 0 +decreases A.Length - i +{ + if i == A.Length then 0 else + entropy_elem(A, i, i+1) + entropy_from(A, i + 1) +} + +function method entropy(A:array) : int +reads A +ensures entropy(A) >= 0 +{ + entropy_from(A, 0) +} + +method print_array(A:array) +{ + var i := 0; + while i < A.Length { + print A[i]; + i := i + 1; + } +} + +method Main() +decreases * +{ + var A:array := 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"; +} \ No newline at end of file diff --git a/isabelle/2021/HSV_tasks_2021_solutions.thy b/isabelle/2021/HSV_tasks_2021_solutions.thy new file mode 100644 index 0000000..c222f3a --- /dev/null +++ b/isabelle/2021/HSV_tasks_2021_solutions.thy @@ -0,0 +1,689 @@ +theory HSV_tasks_2021_solutions imports Complex_Main begin + +section \Task 1: Factorising circuits.\ + +(* Datatype for representing simple circuits. *) +datatype "circuit" = + NOT "circuit" +| AND "circuit" "circuit" +| OR "circuit" "circuit" +| TRUE +| FALSE +| INPUT "int" + +(* Simulates a circuit given a valuation for each input wire. *) +fun simulate where + "simulate (AND c1 c2) \ = ((simulate c1 \) \ (simulate c2 \))" +| "simulate (OR c1 c2) \ = ((simulate c1 \) \ (simulate c2 \))" +| "simulate (NOT c) \ = (\ (simulate c \))" +| "simulate TRUE \ = True" +| "simulate FALSE \ = False" +| "simulate (INPUT i) \ = \ i" + +(* Equivalence between circuits. *) +fun circuits_equiv (infix "\" 50) (* the "50" indicates the operator precedence *) where + "c1 \ c2 = (\\. simulate c1 \ = simulate c2 \)" + +(* An optimisation that exploits the following Boolean identities: + `(a | b) & (a | c) = a | (b & c)` + `(a | b) & (c | a) = a | (b & c)` + `(a | b) & (b | c) = b | (a & c)` + `(a | b) & (c | b) = b | (a & c)` + *) +fun factorise where + "factorise (NOT c) = NOT (factorise c)" +| "factorise (AND (OR c1 c2) (OR c3 c4)) = ( + let c1' = factorise c1; c2' = factorise c2; c3' = factorise c3; c4' = factorise c4 in + if c1' = c3' then OR c1' (AND c2' c4') + else if c1' = c4' then OR c1' (AND c2' c3') + else if c2' = c3' then OR c2' (AND c1' c4') + else if c2' = c4' then OR c2' (AND c1' c3') + else AND (OR c1' c2') (OR c3' c4'))" +| "factorise (AND c1 c2) = AND (factorise c1) (factorise c2)" +| "factorise (OR c1 c2) = OR (factorise c1) (factorise c2)" +| "factorise TRUE = TRUE" +| "factorise FALSE = FALSE" +| "factorise (INPUT i) = INPUT i" + +lemma (* test case *) + "factorise (AND TRUE TRUE) = AND TRUE TRUE" + by eval +lemma (* test case *) + "factorise (AND (OR (INPUT 1) FALSE) (OR TRUE (INPUT 1))) = + OR (INPUT 1) (AND FALSE TRUE)" + by eval +lemma (* test case *) + "factorise (NOT (AND (OR FALSE (INPUT 2)) (OR TRUE (INPUT 2)))) = + NOT (OR (INPUT 2) (AND FALSE TRUE))" + by eval + +theorem factorise_is_sound: "factorise c \ c" +proof (induct rule: factorise.induct) + case (2 c1 c2 c3 c4) + let ?c1' = "factorise c1" + let ?c2' = "factorise c2" + let ?c3' = "factorise c3" + let ?c4' = "factorise c4" + from 2 have IH: "?c1' \ c1" "?c2' \ c2" "?c3' \ c3" "?c4' \ c4" by auto + have "factorise (AND (OR c1 c2) (OR c3 c4)) = ( + if ?c1' = ?c3' then OR ?c1' (AND ?c2' ?c4') + else if ?c1' = ?c4' then OR ?c1' (AND ?c2' ?c3') + else if ?c2' = ?c3' then OR ?c2' (AND ?c1' ?c4') + else if ?c2' = ?c4' then OR ?c2' (AND ?c1' ?c3') + else AND (OR ?c1' ?c2') (OR ?c3' ?c4'))" + by auto + also have "... \ AND (OR c1 c2) (OR c3 c4)" using IH by auto + finally show ?case by auto +qed(simp_all) + +fun factorise2 where + "factorise2 (NOT c) = NOT (factorise2 c)" +| "factorise2 (AND (OR c1 c2) (OR c3 c4)) = ( + let c1' = factorise2 c1; c2' = factorise2 c2; c3' = factorise2 c3; c4' = factorise2 c4 in + if c1' = c3' then OR c1' (AND c2' c4') + else if c1' = c4' then OR c1' (AND c2' c3') + else if c2' = c3' then OR c2' (AND c1' c4') + else if c2' = c4' then OR c2' (AND c1' c3') + else AND (OR c1' c2') (OR c3' c4'))" +| "factorise2 (OR (AND c1 c2) (AND c3 c4)) = ( + let c1' = factorise2 c1; c2' = factorise2 c2; c3' = factorise2 c3; c4' = factorise2 c4 in + if c1' = c3' then AND c1' (OR c2' c4') + else if c1' = c4' then AND c1' (OR c2' c3') + else if c2' = c3' then AND c2' (OR c1' c4') + else if c2' = c4' then AND c2' (OR c1' c3') + else OR (AND c1' c2') (AND c3' c4'))" +| "factorise2 (AND c1 c2) = AND (factorise2 c1) (factorise2 c2)" +| "factorise2 (OR c1 c2) = OR (factorise2 c1) (factorise2 c2)" +| "factorise2 TRUE = TRUE" +| "factorise2 FALSE = FALSE" +| "factorise2 (INPUT i) = INPUT i" + +lemma (* test case *) + "factorise2 (OR (AND (INPUT 1) (INPUT 2)) (AND TRUE (INPUT 1))) = + AND (INPUT 1) (OR (INPUT 2) TRUE)" + by eval + +theorem factorise2_is_sound: "factorise2 c \ c" +proof (induct rule: factorise2.induct) + case (2 c1 c2 c3 c4) + let ?c1' = "factorise2 c1" + let ?c2' = "factorise2 c2" + let ?c3' = "factorise2 c3" + let ?c4' = "factorise2 c4" + from 2 have IH: "?c1' \ c1" "?c2' \ c2" "?c3' \ c3" "?c4' \ c4" by auto + have "factorise2 (AND (OR c1 c2) (OR c3 c4)) = ( + if ?c1' = ?c3' then OR ?c1' (AND ?c2' ?c4') + else if ?c1' = ?c4' then OR ?c1' (AND ?c2' ?c3') + else if ?c2' = ?c3' then OR ?c2' (AND ?c1' ?c4') + else if ?c2' = ?c4' then OR ?c2' (AND ?c1' ?c3') + else AND (OR ?c1' ?c2') (OR ?c3' ?c4'))" + by auto + also have "... \ AND (OR c1 c2) (OR c3 c4)" using IH by auto + finally show ?case by auto +next + case (3 c1 c2 c3 c4) + let ?c1' = "factorise2 c1" + let ?c2' = "factorise2 c2" + let ?c3' = "factorise2 c3" + let ?c4' = "factorise2 c4" + from 3 have IH: "?c1' \ c1" "?c2' \ c2" "?c3' \ c3" "?c4' \ c4" by auto + have "factorise2 (OR (AND c1 c2) (AND c3 c4)) = ( + if ?c1' = ?c3' then AND ?c1' (OR ?c2' ?c4') + else if ?c1' = ?c4' then AND ?c1' (OR ?c2' ?c3') + else if ?c2' = ?c3' then AND ?c2' (OR ?c1' ?c4') + else if ?c2' = ?c4' then AND ?c2' (OR ?c1' ?c3') + else OR (AND ?c1' ?c2') (AND ?c3' ?c4'))" + by auto + also have "... \ OR (AND c1 c2) (AND c3 c4)" using IH by auto + finally show ?case by auto +qed(simp_all) + +section \Task 2: A theorem about divisibility.\ + +theorem plus_dvd_odd_power: + "(a::int) + b dvd a ^ (2 * n + 1) + b ^ (2 * n + 1)" +proof (induct n) + case 0 + thus ?case by auto +next + case (Suc n) + then obtain k::int where "a ^ (2 * n + 1) + b ^ (2 * n + 1) = (a + b) * k" + unfolding dvd_class.dvd_def by auto + hence IH: "a ^ (2 * n + 1) = (a + b) * k - b ^ (2 * n + 1)" by auto + + have "a ^ (2 * Suc n + 1) + b ^ (2 * Suc n + 1) = a ^ (2 * n + 2 + 1) + b ^ (2 * n + 2 + 1)" + by simp + also have "... = a\<^sup>2 * a ^ (2 * n + 1) + b\<^sup>2 * b ^ (2 * n + 1)" + by (metis (no_types, lifting) add.commute add_Suc_right plus_1_eq_Suc power_add) + also have "... = a\<^sup>2 * ((a + b) * k - b ^ (2 * n + 1)) + b\<^sup>2 * b ^ (2 * n + 1)" + unfolding IH by auto + also have "... = a\<^sup>2 * (a + b) * k - a\<^sup>2 * b ^ (2 * n + 1) + b\<^sup>2 * b ^ (2 * n + 1)" + by algebra + also have "... = a\<^sup>2 * (a + b) * k - ((a\<^sup>2 - b\<^sup>2) * b ^ (2 * n + 1))" + by algebra + also have "... = a\<^sup>2 * (a + b) * k - ((a + b) * (a - b) * b ^ (2 * n + 1))" + by algebra + also have "... = (a + b) * (a\<^sup>2 * k - ((a - b) * b ^ (2 * n + 1)))" + by algebra + finally have "a ^ (2 * Suc n + 1) + b ^ (2 * Suc n + 1) = + (a + b) * (a ^ 2 * k - ((a - b) * b ^ (2 * n + 1)))" . + thus ?case by simp +qed + +theorem plus_dvd_power: + "(a::int) + b dvd a ^ (2 * n + 2) + b ^ (2 * n + 2)" + oops + +section \Task 3: Proving that the shift-and-add-3 algorithm is correct.\ + +subsection \Binary and its conversion to nat\ + +type_synonym bit = "bool" + +abbreviation B0 where "B0 == False" +abbreviation B1 where "B1 == True" + +(* The following lemma says that if I want to prove a property of +all 5-bit binary numbers, it suffices to just consider all 32 bit patterns. *) +lemma cases_b5: + fixes v w x y z :: "bit" + assumes "(v, w, x, y, z) = (B0, B0, B0, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B0, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B0, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B0, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B1, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B1, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B1, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B0, B1, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B0, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B0, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B0, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B0, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B1, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B1, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B1, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B0, B1, B1, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B0, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B0, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B0, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B0, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B1, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B1, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B1, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B0, B1, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B0, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B0, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B0, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B0, B1, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B1, B0, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B1, B0, B1) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B1, B1, B0) \ P v w x y z" + assumes "(v, w, x, y, z) = (B1, B1, B1, B1, B1) \ P v w x y z" + shows "P v w x y z" + using assms + apply (cases v) + apply (cases w) + apply (cases x) + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases x) + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases w) + apply (cases x) + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases x) + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + apply (cases y) + apply (cases z) + apply auto[2] + apply (cases z) + apply auto[2] + done + +fun binary_to_nat :: "bit list \ nat" +where + "binary_to_nat [] = 0" +| "binary_to_nat (b # bs) = (if b then 2 ^ length bs else 0) + binary_to_nat bs" + + +lemma (* test case *) "binary_to_nat [B0, B1, B0, B1] = 5" by eval +lemma (* test case *) "binary_to_nat [B0, B0, B1, B0, B1] = 5" by eval +lemma (* test case *) "binary_to_nat [B1] = 1" by eval +lemma (* test case *) "binary_to_nat [B0] = 0" by eval + +subsection \BCD and its conversion to nat\ + +type_synonym nibble = "bit * bit * bit * bit" + +fun nibble_to_nat :: "nibble \ nat" +where + "nibble_to_nat (B0,B0,B0,B0) = 0" +| "nibble_to_nat (B0,B0,B0,B1) = 1" +| "nibble_to_nat (B0,B0,B1,B0) = 2" +| "nibble_to_nat (B0,B0,B1,B1) = 3" +| "nibble_to_nat (B0,B1,B0,B0) = 4" +| "nibble_to_nat (B0,B1,B0,B1) = 5" +| "nibble_to_nat (B0,B1,B1,B0) = 6" +| "nibble_to_nat (B0,B1,B1,B1) = 7" +| "nibble_to_nat (B1,B0,B0,B0) = 8" +| "nibble_to_nat (B1,B0,B0,B1) = 9" +| "nibble_to_nat (B1,B0,B1,B0) = 10" +| "nibble_to_nat (B1,B0,B1,B1) = 11" +| "nibble_to_nat (B1,B1,B0,B0) = 12" +| "nibble_to_nat (B1,B1,B0,B1) = 13" +| "nibble_to_nat (B1,B1,B1,B0) = 14" +| "nibble_to_nat (B1,B1,B1,B1) = 15" + +fun bcd_to_nat :: "nibble list \ nat" +where + "bcd_to_nat [] = 0" +| "bcd_to_nat (n # ns) = bcd_to_nat ns + nibble_to_nat n * 10 ^ length ns" + +lemma (* test case *) "bcd_to_nat [(B0,B1,B1,B0)] = 6" by eval +lemma (* test case *) "bcd_to_nat [(B0,B1,B1,B0),(B1,B0,B0,B1)] = 69" by eval +lemma (* test case *) "bcd_to_nat [(B0,B0,B0,B0),(B1,B0,B0,B1)] = 9" by eval +lemma (* test case *) "bcd_to_nat [(B0,B0,B1,B1),(B0,B0,B0,B0)] = 30" by eval + + +subsection \Left-shifting BCD numbers\ + +(* +"Add-three-and-shift" + bcd_part bin_part combined + ([ ], [1,0,1,0,1,0,1]) 0 85 0 + 85 = 85 +\ ([ (0,0,0,1)], [0,1,0,1,0,1]) 1 21 1*64 + 21 = 85 +\ ([ (0,0,1,0)], [1,0,1,0,1]) 2 21 2*32 + 21 = 85 +\ ([ (0,1,0,1)], [0,1,0,1]) 5 5 5*16 + 5 = 85 +\ ([(0,0,0,1),(0,0,0,0)], [1,0,1]) 10 5 10*8 + 5 = 85 +\ ([(0,0,1,0),(0,0,0,1)], [0,1]) 21 1 21*4 + 1 = 85 +\ ([(0,1,0,0),(0,0,1,0)], [1]) 42 1 42*2 + 1 = 85 +\ ([(1,0,0,0),(0,1,0,1)], []) 85 0 85 + 0 = 85 +\ done +*) + +fun shift_helper :: "nibble list \ bit \ (bit * nibble list)" + where + "shift_helper [] b = (b, [])" +| "shift_helper ((b1, b2, b3, b4) # ns) b = ( + let (c, ns') = shift_helper ns b in + (b1, (b2,b3,b4,c) # ns'))" + +fun shift :: "nibble list \ bit \ nibble list" +where + "shift ns b = (let (c,ns') = shift_helper ns b in + if c = B1 then (B0,B0,B0,c) # ns' else ns')" + +lemma (* test case *) + "shift [(B0, B1, B0, B1), (B1, B0, B1, B0)] B0 + = [(B1, B0, B1, B1), (B0, B1, B0, B0)]" +by eval + +lemma (* test case *) + "shift [(B1, B1, B0, B1), (B1, B0, B1, B0)] B0 + = [(B0, B0, B0, B1), (B1, B0, B1, B1), (B0, B1, B0, B0)]" +by eval + +lemma (* test case *) + "shift [] B1 + = [(B0, B0, B0, B1)]" +by eval + +subsection \Functions for adding 3 to BCD digits\ + +(* Even though this function is only used on nibbles 0 to 9, I've + defined it as a total, bijective function so that it is invertible; + this seems to make the proof easier later on. *) +fun maybe_add3 :: "nibble \ nibble" +where + "maybe_add3 (B0,B0,B0,B0) = (B0,B0,B0,B0)" (* 0 \ 0 *) +| "maybe_add3 (B0,B0,B0,B1) = (B0,B0,B0,B1)" (* 1 \ 1 *) +| "maybe_add3 (B0,B0,B1,B0) = (B0,B0,B1,B0)" (* 2 \ 2 *) +| "maybe_add3 (B0,B0,B1,B1) = (B0,B0,B1,B1)" (* 3 \ 3 *) +| "maybe_add3 (B0,B1,B0,B0) = (B0,B1,B0,B0)" (* 4 \ 4 *) +| "maybe_add3 (B0,B1,B0,B1) = (B1,B0,B0,B0)" (* 5 \ 8 *) +| "maybe_add3 (B0,B1,B1,B0) = (B1,B0,B0,B1)" (* 6 \ 9 *) +| "maybe_add3 (B0,B1,B1,B1) = (B1,B0,B1,B0)" (* 7 \ 10 *) +| "maybe_add3 (B1,B0,B0,B0) = (B1,B0,B1,B1)" (* 8 \ 11 *) +| "maybe_add3 (B1,B0,B0,B1) = (B1,B1,B0,B0)" (* 9 \ 12 *) +| "maybe_add3 (B1,B0,B1,B0) = (B1,B1,B0,B1)" (* 10 \ 13 *) +| "maybe_add3 (B1,B0,B1,B1) = (B1,B1,B1,B0)" (* 11 \ 14 *) +| "maybe_add3 (B1,B1,B0,B0) = (B1,B1,B1,B1)" (* 12 \ 15 *) +| "maybe_add3 (B1,B1,B0,B1) = (B0,B1,B0,B1)" (* 13 \ 5 *) +| "maybe_add3 (B1,B1,B1,B0) = (B0,B1,B1,B0)" (* 14 \ 6 *) +| "maybe_add3 (B1,B1,B1,B1) = (B0,B1,B1,B1)" (* 15 \ 7 *) + +fun maybe_add3_inv :: "nibble \ nibble" +(* It's sometimes handy to be able to run the `maybe_add3` function backwards *) +where + "maybe_add3_inv (B0,B0,B0,B0) = (B0,B0,B0,B0)" +| "maybe_add3_inv (B0,B0,B0,B1) = (B0,B0,B0,B1)" +| "maybe_add3_inv (B0,B0,B1,B0) = (B0,B0,B1,B0)" +| "maybe_add3_inv (B0,B0,B1,B1) = (B0,B0,B1,B1)" +| "maybe_add3_inv (B0,B1,B0,B0) = (B0,B1,B0,B0)" +| "maybe_add3_inv (B1,B0,B0,B0) = (B0,B1,B0,B1)" +| "maybe_add3_inv (B1,B0,B0,B1) = (B0,B1,B1,B0)" +| "maybe_add3_inv (B1,B0,B1,B0) = (B0,B1,B1,B1)" +| "maybe_add3_inv (B1,B0,B1,B1) = (B1,B0,B0,B0)" +| "maybe_add3_inv (B1,B1,B0,B0) = (B1,B0,B0,B1)" +| "maybe_add3_inv (B1,B1,B0,B1) = (B1,B0,B1,B0)" +| "maybe_add3_inv (B1,B1,B1,B0) = (B1,B0,B1,B1)" +| "maybe_add3_inv (B1,B1,B1,B1) = (B1,B1,B0,B0)" +| "maybe_add3_inv (B0,B1,B0,B1) = (B1,B1,B0,B1)" +| "maybe_add3_inv (B0,B1,B1,B0) = (B1,B1,B1,B0)" +| "maybe_add3_inv (B0,B1,B1,B1) = (B1,B1,B1,B1)" + +lemma maybe_add3_inv1: + "maybe_add3_inv (maybe_add3 n) = n" +by (cases n, metis (full_types) maybe_add3.simps maybe_add3_inv.simps) + +lemma maybe_add3_inv2: + "maybe_add3 (maybe_add3_inv n) = n" +by (cases n, metis (full_types) maybe_add3.simps maybe_add3_inv.simps) + + +subsection \Converting binary to BCD\ + +fun binary_to_bcd_helper :: "nibble list \ bit list \ nibble list" +where + "binary_to_bcd_helper ns [] = ns" +| "binary_to_bcd_helper ns (b # bs) = binary_to_bcd_helper (shift (map maybe_add3 ns) b) bs" + +fun binary_to_bcd :: "bit list \ nibble list" +where + "binary_to_bcd bs = binary_to_bcd_helper [] bs" + +lemma (* test case *) + "binary_to_bcd [B1,B0,B1,B0,B1,B0,B1] = [(B1,B0,B0,B0), (B0,B1,B0,B1)]" + by eval + +(* more test cases *) +lemma "binary_to_bcd [B1,B1,B1] = [(B0,B1,B1,B1)]" by eval +lemma "binary_to_bcd [B1,B0,B0,B0,B0,B0,B0,B0] = [(B0,B0,B0,B1),(B0,B0,B1,B0),(B1,B0,B0,B0)]" by eval +lemma "binary_to_bcd [B0,B0,B0,B0,B0,B1] = [(B0,B0,B0,B1)]" by eval +lemma "binary_to_bcd [B1,B1,B0,B0,B0,B0,B0] = [(B1,B0,B0,B1),(B0,B1,B1,B0)]" by eval + +subsection \Checking that nibbles correspond to valid BCD digits\ + +fun valid_nibble :: "nibble \ bool" +where + "valid_nibble (B0,B0,B0,B0) = True" +| "valid_nibble (B0,B0,B0,B1) = True" +| "valid_nibble (B0,B0,B1,B0) = True" +| "valid_nibble (B0,B0,B1,B1) = True" +| "valid_nibble (B0,B1,B0,B0) = True" +| "valid_nibble (B0,B1,B0,B1) = True" +| "valid_nibble (B0,B1,B1,B0) = True" +| "valid_nibble (B0,B1,B1,B1) = True" +| "valid_nibble (B1,B0,B0,B0) = True" +| "valid_nibble (B1,B0,B0,B1) = True" +| "valid_nibble (B1,B0,B1,B0) = False" +| "valid_nibble (B1,B0,B1,B1) = False" +| "valid_nibble (B1,B1,B0,B0) = False" +| "valid_nibble (B1,B1,B0,B1) = False" +| "valid_nibble (B1,B1,B1,B0) = False" +| "valid_nibble (B1,B1,B1,B1) = False" + +lemma shift_helper_valid: + "list_all valid_nibble ns \ + list_all valid_nibble (snd (shift_helper (map maybe_add3 ns) b))" +proof (induct ns) + case Nil + thus ?case by simp +next + case (Cons n ns) + thus ?case + apply auto + apply (cases "maybe_add3 n") + apply auto + apply (split prod.split) + apply auto + apply (cases n) + apply (smt (z3) maybe_add3.simps valid_nibble.simps prod.inject) + done +qed + +lemma binary_to_bcd_helper_step_valid: + assumes "list_all valid_nibble ns" + shows "list_all valid_nibble (shift (map maybe_add3 ns) b)" +using assms +apply auto +apply (split prod.split) +apply (smt (z3) list_all_simps(1) shift_helper_valid snd_conv valid_nibble.simps(2)) +done + +lemma binary_to_bcd_helper_valid: + "list_all valid_nibble ns \ + list_all valid_nibble (binary_to_bcd_helper ns bs)" +proof (induct bs arbitrary: ns) + case Nil + thus ?case by auto +next + case (Cons b bs) + thus ?case using binary_to_bcd_helper_step_valid by auto +qed + +theorem binary_to_bcd_valid: + "list_all valid_nibble (binary_to_bcd bs)" +using binary_to_bcd_helper_valid by auto + +subsection \Proof that the binary_to_bcd translation is correct.\ + +(* `shift_helper` doesn't change the length of its list *) +lemma length_shift_helper: + "length ns = length (snd (shift_helper ns b))" +proof (induct ns) + case Nil + thus ?case by auto +next + case (Cons a ns) + show ?case + apply auto + apply (cases a) + apply auto + apply (cases "shift_helper ns b") + apply (auto simp add: Cons) + done +qed + +lemma shift_helper: + "list_all valid_nibble ns \ + shift_helper (map maybe_add3 ns) b = (c, ns') \ + bcd_to_nat ((B0,B0,B0,c) # ns') = bcd_to_nat ns * 2 + (if b then 1 else 0)" +proof (induct ns arbitrary: c ns') + case Nil + thus ?case by simp +next + case (Cons n ns) + + obtain c' ns'' where *: "shift_helper (map maybe_add3 ns) b = (c', ns'')" by fastforce + with Cons have IH: + "bcd_to_nat ((B0, B0, B0, c') # ns'') = bcd_to_nat ns * 2 + (if b then 1 else 0)" by simp + + obtain b1 b2 b3 b4 where maybe_add3_n: "maybe_add3 n = (b1, b2, b3, b4)" + by (cases rule: prod_cases4) + hence "maybe_add3_inv (maybe_add3 n) = maybe_add3_inv (b1, b2, b3, b4)" by auto + with maybe_add3_inv1 have n_def: "n = maybe_add3_inv (b1, b2, b3, b4)" by auto + + have "c = b1" and ns'_def: "ns' = (b2, b3, b4, c') # ns''" using maybe_add3_n * Cons by auto + + have "length ns'' = length ns" + by (metis * length_map length_shift_helper snd_conv) + + have "nibble_to_nat (b2, b3, b4, c') * 10 ^ length ns + + nibble_to_nat (B0, B0, B0, b1) * 10 * 10 ^ length ns = + nibble_to_nat (B0, B0, B0, c') * 10 ^ length ns + + nibble_to_nat n * 10 ^ length ns * 2" + apply (rule cases_b5[of b1 b2 b3 b4 c']) + using Cons apply (auto simp add: n_def) + done + thus ?case using ns'_def IH `length ns'' = length ns` `c = b1` by auto +qed + +(* Determines the "current state" of a translation-in-progress. See examples below. *) +fun bcd_binary_to_nat :: "nibble list \ bit list \ nat" +where + "bcd_binary_to_nat ns bs = bcd_to_nat ns * 2 ^ length bs + binary_to_nat bs" + +lemma "bcd_binary_to_nat [] [B1,B0,B1,B0,B1,B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B0,B0,B1)] [B0,B1,B0,B1,B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B0,B1,B0)] [B1,B0,B1,B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B1,B0,B1)] [B0,B1,B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B0,B0,B1), (B0,B0,B0,B0)] [B1,B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B0,B1,B0), (B0,B0,B0,B1)] [B0,B1] = 85" by eval +lemma "bcd_binary_to_nat [(B0,B1,B0,B0), (B0,B0,B1,B0)] [B1] = 85" by eval +lemma "bcd_binary_to_nat [(B1,B0,B0,B0), (B0,B1,B0,B1)] [] = 85" by eval + +lemma binary_to_bcd_helper_step_correct: + assumes "list_all valid_nibble ns" + shows "bcd_binary_to_nat ns (b # bs) = + bcd_binary_to_nat (shift (map maybe_add3 ns) b) bs" +proof - + have "bcd_to_nat (shift (map maybe_add3 ns) B0) = bcd_to_nat ns * 2" + apply (auto simp del: bcd_to_nat.simps) + apply (split prod.split) + apply (auto simp del: bcd_to_nat.simps) + using assms shift_helper apply presburger + apply (smt (z3) assms shift_helper add.right_neutral bcd_to_nat.simps(2) + mult_zero_left nibble_to_nat.simps(1)) + done + moreover + have "bcd_to_nat (shift (map maybe_add3 ns) B1) = bcd_to_nat ns * 2 + 1" + apply (auto simp del: bcd_to_nat.simps) + apply (split prod.split) + apply (auto simp del: bcd_to_nat.simps) + using assms shift_helper apply presburger + apply (smt (z3) One_nat_def add_Suc_shift add_right_imp_eq assms bcd_to_nat.simps(2) + mult_zero_left nibble_to_nat.simps(1) shift_helper) + done + ultimately show ?thesis using assms by auto +qed + +lemma binary_to_bcd_helper_correct: + "list_all valid_nibble ns \ + bcd_to_nat (binary_to_bcd_helper ns bs) = bcd_binary_to_nat ns bs" +proof (induct bs arbitrary: ns) + case Nil + thus ?case by simp +next + case Cons + thus ?case + using binary_to_bcd_helper_step_correct and binary_to_bcd_helper_step_valid + by auto +qed + +theorem binary_to_bcd_correct: + "bcd_to_nat (binary_to_bcd bs) = binary_to_nat bs" +using binary_to_bcd_helper_correct by auto + +section \ Alternative implementation of binary_to_bcd that converts to nat and then to bcd \ + +lemma mod10_induct [case_names 0 1 2 3 4 5 6 7 8 9]: + fixes n :: nat + assumes "P 0" "P 1" "P 2" "P 3" "P 4" "P 5" "P 6" "P 7" "P 8" "P 9" + shows "P (n mod 10)" +proof - + have "n mod 10 \ {..<10}" + by simp + also have "{..<10} = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9 :: nat}" + by (simp add: lessThan_nat_numeral lessThan_Suc insert_commute) + finally show ?thesis using assms + by fastforce +qed + +fun nat_to_nibble :: "nat \ nibble" +where + "nat_to_nibble n = ( + if n = 0 then (B0,B0,B0,B0) else + if n = 1 then (B0,B0,B0,B1) else + if n = 2 then (B0,B0,B1,B0) else + if n = 3 then (B0,B0,B1,B1) else + if n = 4 then (B0,B1,B0,B0) else + if n = 5 then (B0,B1,B0,B1) else + if n = 6 then (B0,B1,B1,B0) else + if n = 7 then (B0,B1,B1,B1) else + if n = 8 then (B1,B0,B0,B0) else + if n = 9 then (B1,B0,B0,B1) else + (B1,B1,B1,B1))" (* unreachable *) + +fun nat_to_bcd :: "nat \ nibble list" +where + "nat_to_bcd n = (if n = 0 then [] else + nat_to_bcd (n div 10) @ [nat_to_nibble (n mod 10)])" + +value "nat_to_bcd 420" +value "nat_to_bcd 42" +value "nat_to_bcd 4" +value "nat_to_bcd 0" + +fun binary_to_bcd2 :: "bit list \ nibble list" +where + "binary_to_bcd2 bs = nat_to_bcd (binary_to_nat bs)" + +lemma nat_to_nibble_valid: + "valid_nibble (nat_to_nibble (n mod 10))" +by (induct rule: mod10_induct, auto) + +lemma nat_to_bcd_valid: + "list_all valid_nibble (nat_to_bcd n)" + using nat_to_nibble_valid + by (induct rule: nat_to_bcd.induct, simp) + +theorem binary_to_bcd2_valid: + "list_all valid_nibble (binary_to_bcd2 bs)" +using nat_to_bcd_valid by auto + +lemma bcd_to_nat_snoc: + "bcd_to_nat (ns @ [n]) = bcd_to_nat ns * 10 + bcd_to_nat [n]" + by (induct ns, auto) + +lemma bcd_to_nat_nibble: + "bcd_to_nat [nat_to_nibble (n mod 10)] = n mod 10" + by (induct rule: mod10_induct, auto) + +lemma bcd_to_nat_inv: + "bcd_to_nat (nat_to_bcd n) = n" + apply (induct rule: nat_to_bcd.induct) + apply (subst nat_to_bcd.simps) + apply (case_tac "n=0") + apply simp + apply (simp del: nat_to_bcd.simps nat_to_nibble.simps) + apply (subst bcd_to_nat_snoc) + apply (subst bcd_to_nat_nibble) + apply simp + done + +theorem binary_to_bcd2_correct: + "bcd_to_nat (binary_to_bcd2 bs) = binary_to_nat bs" + using bcd_to_nat_inv by auto + +end \ No newline at end of file