mirror of
https://github.com/supleed2/ELEC70056-HSV-CW1.git
synced 2024-09-19 20:46:16 +00:00
137 lines
4.1 KiB
Plaintext
137 lines
4.1 KiB
Plaintext
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
|