COMP4161 Isabelle a3

* COMP4161 Assignment 3.

AutoCorres.AutoCorres
“HOL-Library.Prefix_Order”

section “Huffman Code”

(* The template for this question contains hints in the form of lemmas
that are not one of the direct questions a)-j). They are marked with
“oops”. You can, but do not have to prove these lemma. There is more
than one way to arrive at a correct proof.

The lemmas marked with sorry and TODO are the ones you should prove
unchanged for Q1. In Q2 you are allowed to tune the lemma statements.

type_synonym ‘a freq_list = “(‘a \ int) list”

(* Q1 a): TODO *)
primrec add_one :: “‘a \ ‘a freq_list \ ‘a freq_list” where
“add_one c [] = undefined” (* TODO *)

primrec freq_of :: “‘a list \ ‘a freq_list” where
“freq_of [] = undefined” (* TODO *)

value “freq_of ”abcdaa””

lemma fst_set_add_one:
“fst ` set (add_one x xs) = {x} \ fst ` set xs”

(* Q1 b): *)
lemma distinct_freq[simp]:
“distinct (map fst (freq_of cs))”
sorry (* TODO *)

datatype ‘a htree = Leaf ‘a int | Branch “‘a htree” “‘a htree”

primrec weight :: “‘a htree \ int” where
“weight (Leaf _ w) = w” |
“weight (Branch l r) = weight l + weight r”

fun build_tree :: “‘a htree list \ ‘a htree” where
“build_tree [] = Leaf undefined 0” |
“build_tree [t] = t” |
“build_tree (t1 # t2 # cs) = build_tree (insort_key weight (Branch t1 t2) cs)”

definition huffman_tree :: “‘a freq_list \ ‘a htree” where
“huffman_tree = build_tree o map (\(c,w). Leaf c w) o sort_key snd”

definition
“some_tree = huffman_tree (freq_of ”abcdaa”)”

value some_tree

type_synonym code = “bool list”

fun add_bit :: “bool \ ‘a \ code \ ‘a \ code” where
“add_bit b (c, code) = (c, b # code)”

primrec code_list :: “‘a htree \ (‘a \ code) list” where
“code_list (Leaf c _) = [(c,[])]” |
“code_list (Branch l r) = map (add_bit False) (code_list l) @ map (add_bit True) (code_list r)”

definition code_map :: “‘a htree \ (code \ ‘a) list” where
“code_map tree = map (\(a,b). (b,a)) (code_list tree)”

value “code_list some_tree”
value “code_map some_tree”

(* Q1 c): TODO *)

definition encoder :: “(‘a \ code option) \ ‘a list \ code” where
“encoder mp xs = undefined” (* TODO *)

fun decoder :: “(code \ ‘a option) \ code \ code \ ‘a list” where
“decoder mp acs [] = []” |
“decoder mp acs (c#cs) = (if mp \ None
then the (mp # decoder mp [] cs
else decoder mp (acs @ [c]) cs)”

definition unique_prefix :: “(code \ ‘a option) \ bool” where
“unique_prefix cm = (\xs\dom cm. \ys\dom cm. \ ys < xs)" definition is_inv :: "('a \ ‘b option) \ (‘b \ ‘a option) \ bool” where
“is_inv mp mp’ = (\x y. mp x = Some y \ mp’ y = Some x)”

lemma unique_prefixD:
“\ unique_prefix m; m xs = Some y; m xs’ = Some y’; xs = xs’ @ xs” \ \ xs” = []”

lemma decoder_step:
“\unique_prefix mp’; mp’ ys’ = None; mp’ (ys’ @ ys) = Some x\
\ decoder mp’ ys’ (ys @ zs) = x # decoder mp’ [] zs”

(* Q1 d): *)
lemma decoder:
“\ is_inv mp mp’; unique_prefix mp’; set xs \ dom mp; [] \ dom mp’ \
\ decoder mp’ [] (encoder mp xs) = xs”
sorry (* TODO *)

(* Q1 e): *)
lemma is_inv_map_of:
“\ distinct (map snd xs); distinct (map fst xs) \ \
is_inv (map_of xs) (map_of (map (\(a,b). (b,a)) xs))”
sorry (* TODO *)

(* Q1 f): *)
primrec letters_of :: “‘a htree \ ‘a set” where
“letters_of (Leaf c _) = undefined” (* TODO: complete *)

(* Q1 g): *)
fun distinct_tree :: “‘a htree \ bool” where
“distinct_tree (Leaf _ _) = undefined” (* TODO: complete *)

fun distinct_forest :: “‘a htree list \ bool” where
“distinct_forest [] = True” |
“distinct_forest (t#ts) = (distinct_tree t \ distinct_forest ts \
letters_of t \ \ (set (map letters_of ts)) = {})”

lemma fst_code_list:
“fst ` set (code_list t) = letters_of t”

(* Q1 h): *)
lemma distinct_fst_code_list[simp]:
“distinct_tree t \ distinct (map fst (code_list t))”
sorry (* TODO *)

lemma distinct_forest_insort:
“distinct_forest (insort_key f t ts) =
(distinct_tree t \ distinct_forest ts \ letters_of t \ \ (set (map letters_of ts)) = {})”

lemma distinct_build_tree:
“distinct_forest ts \ distinct_tree (build_tree ts)”

lemma distinct_insort_map:
“distinct (map g (insort_key f x xs)) = (g x \ g ` set xs \ distinct (map g xs))”

(* Q1 i): *)
lemma distinct_huffman[simp]:
“distinct (map fst fs) \ distinct_tree (huffman_tree fs)”
sorry (* TODO *)

(* If you’re curious, this would be the overall correctness statement.
You do not need to prove this one.
theorem huffman_decoder:
“\set xs \ set ys; tree = huffman_tree (freq_of ys); 2 \ length (freq_of ys) \ \
decoder (map_of (code_map tree)) [] (encoder (map_of (code_list tree)) xs) = xs”

(* ———————————————————————————— *)

declare [[syntax_ambiguity_warning = false]]

definition “LEN = 1000”
declare LEN_def[simp]

external_file “stack.c”
install_C_file “stack.c”

autocorres “stack.c”

context stack

thm is_empty’_def
thm has_capacity’_def
thm push’_def
thm pop’_def
thm sum’_def

primrec stack_from :: “machine_word list \ machine_word \ lifted_globals \ bool” where
“stack_from [] n s = (n = -1 )” |
“stack_from (x # xs) n s = (n < LEN \ content_” s.[unat n] = x \ stack_from xs (n – 1) s)”

definition is_stack where
“is_stack xs s \ stack_from xs (top_” s) s”

(* Q2 a) *)
lemma is_stack_Nil_top[simp]:
“is_stack [] s = (top_” s = -1)”
sorry (* TODO *)

(* Q2 b) *)
lemma is_stack_Nil_is_empty:
“is_stack [] s = (is_empty’ s = 1)”
sorry (* TODO *)

(* Q2 c) *)
lemma stack_from_neg[simp]:
“stack_from xs (- 1) s = (xs = [])”
sorry (* TODO *)

(* Q2 d) *)
lemma is_stack_single:
“is_stack [x] s = (top_” s = 0 \ content_” s.[0] = x)”
sorry (* TODO *)

(* Q2 e) *)
lemma is_stack_Cons[simp]:
“is_stack (x # xs) s =
(top_” s < LEN \ content_” s.[unat (top_” s)] = x \ stack_from xs (top_” s – 1) s)”
sorry (* TODO *)

(* Q2 f) *)
lemma stack_from_top_upd[simp]:
“stack_from xs n (s\top_” := t\) = stack_from xs n s”
sorry (* TODO *)

(* Helper lemma — you can prove this one or state your own *)
lemma stack_from_top_and_array_upd’:
“\ \i \ unat n. a.[i] = content_” s.[i] \ \
stack_from xs n (s\top_” := t, content_” := a\) = stack_from xs n s”

(* Q2 g) *)
lemma stack_from_top_and_array_upd[simp]:
“unat (n + 1) < LEN \
stack_from xs n (s\top_” := n+1, content_” := Arrays.update (content_” s) (unat (n+1)) x\) =
stack_from xs n s”
sorry (* TODO *)

(* Q2 h) *)
lemma pop_correct_partial:
“\ \s. is_stack (x#xs) s \ pop’ \ \rv s. rv = x \ TODO \”
sorry (* TODO *)

(* Q2 i) *)
lemma pop_correct_total:
“\ \s. TODO \ pop’ \ \rv s. TODO \!”
sorry (* TODO *)

(* Q2 j) *)
lemma push_correct_total:
“\ \s. TODO \ push’ x \ \_ s. TODO \!”
supply word_less_nat_alt[simp]
sorry (* TODO *)

(* Q2 k) *)
lemma sum_correct_partial:
“\ \s. is_stack xs s \ sum’ \ \rv s. is_stack [] s \ rv = sum_list xs \”
unfolding sum’_def
apply (subst whileLoop_add_inv[where
I=”TODO”])
sorry (* TODO *)