(* * COMP4161 Assignment 3. *) theory s3 imports AutoCorres.AutoCorres "HOL-Library.Prefix_Order" begin section "Huffman Code" type_synonym 'a freq_list = "('a \ int) list" (* Q1 a): *) primrec add_one :: "'a \ 'a freq_list \ 'a freq_list" where "add_one c [] = [(c, 1)]" | "add_one c (x#as) = (case x of (a, n) \if c=a then (a, n+1)#as else (a, n)#(add_one c as))" fun freq_of :: "'a list \ 'a freq_list" where "freq_of [] = []" | "freq_of (a#as) = add_one a (freq_of as)" value "freq_of ''abcdaa''" lemma fst_set_add_one: "fst ` set (add_one x xs) = {x} \ fst ` set xs" by (induct xs; simp add: split_def) lemma distinct_add_one: "distinct (map fst xs) \ distinct (map fst (add_one a xs))" by (induct xs; clarsimp simp: fst_set_add_one) (* Q1 b): *) lemma distinct_freq[simp]: "distinct (map fst (freq_of cs))" by (induct cs; simp add: distinct_add_one) 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): *) definition encoder :: "('a \ code option) \ 'a list \ code" where "encoder mp xs = concat (map (the o mp) xs)" value "encoder (map_of (code_list (huffman_tree (freq_of ''abcdaa'')))) ''abcdaa''" lemma encoder_cons: "encoder mp (a#as) = (encoder mp [a])@(encoder mp as)" by (clarsimp simp: encoder_def) lemma encoder_single [simp]:"encoder mp [a] = the (mp a)" by (simp add: encoder_def) fun decoder :: "(code \ 'a option) \ code \ code \ 'a list" where "decoder mp acs [] = []" | "decoder mp acs (c#cs) = (if mp (acs@[c]) \ None then the (mp (acs@[c])) # 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'' = []" by (fastforce simp: unique_prefix_def dom_def less_list_def) lemma decoder_step: "\unique_prefix mp'; mp' ys' = None; mp' (ys' @ ys) = Some x\ \ decoder mp' ys' (ys @ zs) = x # decoder mp' [] zs" apply (induction ys arbitrary: ys' zs, simp) apply (rename_tac a ys ys' zs) apply (drule_tac x="ys'@[a]" in meta_spec, clarsimp) apply (drule_tac xs''=ys and xs'="ys'@[a]" in unique_prefixD; simp) done lemmas decoder_single = decoder_step[where zs="[]", simplified] lemma decoder_inductive: "\ is_inv mp mp'; unique_prefix mp'; set (x#xs) \ dom mp; [] \ dom mp'; mp' (ys'@ys) = Some x; mp' ys' = None; ys \ [] \ \ decoder mp' ys' (ys @ encoder mp xs) = x # xs" apply (induct xs arbitrary: ys, simp add: encoder_def decoder_single) apply (clarsimp simp add: decoder_step dom_def is_inv_def) apply (subst encoder_cons, simp) apply (rename_tac a xs ys y y') apply (drule_tac x=a and y=y' in spec2) apply clarsimp apply (simp add: decoder_step) done (* Q1 d): *) lemma decoder: "\ is_inv mp mp'; unique_prefix mp'; set xs \ dom mp; [] \ dom mp' \ \ decoder mp' [] (encoder mp xs) = xs" apply (induct xs, simp add: encoder_def) apply simp apply (subst encoder_cons) apply (clarsimp simp: dom_def is_inv_def) apply (rename_tac a xs y) apply (drule_tac x=a and y=y in spec2, clarsimp) apply (simp add: decoder_step) done (* 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))" apply (unfold is_inv_def) apply (induct xs, simp) apply (clarsimp simp: image_iff) by (smt (verit) fst_eqD map_of_eq_Some_iff map_upd_Some_unfold snd_eqD) (* Q1 f): *) primrec letters_of :: "'a htree \ 'a set" where "letters_of (Leaf c _) = {c}" | "letters_of (Branch t1 t2) = letters_of t1 \ letters_of t2" (* Q1 g): *) fun distinct_tree :: "'a htree \ bool" where "distinct_tree (Leaf _ _) = True" | "distinct_tree (Branch t1 t2) = (distinct_tree t1 \ distinct_tree t2 \ (letters_of t1 \ letters_of t2 = {}))" 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_add_bit: "fst o add_bit b = fst" by fastforce lemma fst_code_list: "fst ` set (code_list t) = letters_of t" by (induct t; simp add: image_Un fst_add_bit image_comp) (* Q1 h): *) lemma distinct_fst_code_list: "distinct_tree t \ distinct (map fst (code_list t))" by (induction t; clarsimp simp: fst_add_bit fst_code_list) 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)) = {})" apply (induct ts, simp) apply (clarsimp simp add: disjoint_iff_not_equal set_insort_key) by blast lemma distinct_build_tree: "distinct_forest ts \ distinct_tree (build_tree ts)" apply (induct ts rule: build_tree.induct, simp, simp) apply (fastforce simp add: distinct_forest_insort) done lemma distinct_insort_map: "distinct (map g (insort_key f x xs)) = (g x \ g ` set xs \ distinct (map g xs))" apply (rule; induction xs, simp) by (clarsimp split: if_splits simp: set_insort_key)+ lemma insort_map: "map g (insort_key (f o g) n ls) = (insort_key f (g n) (map g ls))" by (induction ls; simp) lemma sort_map: "map g (sort_key (f o g) ls) = (sort_key f (map g ls))" using insort_map[simp] by (induction ls; simp) lemma weight_eq: "snd = weight \ (\(x, y). htree.Leaf x y)" by fastforce lemma map_Leaf_sort: "map (\(x, y). htree.Leaf x y) (sort_key snd fs) = sort_key weight (map (\(x, y). htree.Leaf x y) fs)" by (simp add: weight_eq sort_map) (* Q1 i): *) lemma distinct_huffman: "distinct (map fst fs) \ distinct_tree (huffman_tree fs)" apply (simp add: huffman_tree_def map_Leaf_sort) apply (rule distinct_build_tree) apply (induct fs, simp) apply (clarsimp simp: distinct_forest_insort) apply (drule imageI[where f=fst], simp) done (* This is how one would complete correctness of the encoding scheme: *) lemma unique_prefix_add: "\unique_prefix m1; unique_prefix m2; \xs \ dom m1. \ys \ dom m2. \ xs < ys \ \ ys < xs \ \ unique_prefix (m1 ++ m2)" unfolding unique_prefix_def by blast lemma unique_prefix_code_map: "unique_prefix (map_of (code_map t))" apply(simp add: code_map_def unique_prefix_def dom_map_of_conv_image_fst) by (induct t; fastforce) lemma build_tree_Branch: "2 \ length ts \ \l r. build_tree ts = Branch l r" apply (induct ts rule: build_tree.induct; clarsimp) apply (case_tac cs; simp) done lemma inj_on_add_bit: "inj_on (snd \ add_bit b) (set (code_list t))" apply (induction t, simp) apply (simp add: inj_on_Un; auto intro!: inj_on_imageI) apply (clarsimp simp: inj_on_def, fastforce)+ done lemma distinct_snd_code_list: "distinct_tree t \ distinct (map snd (code_list t))" apply (induction t; clarsimp simp: image_comp[symmetric]; auto) apply (auto simp: distinct_map inj_on_add_bit) done lemma set_freq_of: "set (map fst (freq_of xs)) = set xs" apply (induct xs rule: freq_of.induct; simp) by (simp add: fst_set_add_one) lemma letters_of_build_tree: "ts\[] \ letters_of (build_tree ts) = \ (set (map letters_of ts))" by (induct rule: build_tree.induct; auto simp: set_insort_key) 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" apply (simp add: code_map_def) apply (rule decoder) apply (simp add: is_inv_map_of distinct_snd_code_list distinct_huffman distinct_fst_code_list) apply (rule unique_prefix_code_map[simplified code_map_def]) apply (simp add: dom_map_of_conv_image_fst fst_code_list huffman_tree_def comp_def) apply (subst letters_of_build_tree) apply (metis Nil_is_map_conv length_sort list.size(3) not_numeral_le_zero) apply (fastforce simp: split_def comp_def image_iff[symmetric] set_freq_of[simplified]) apply (clarsimp simp add: dom_map_of_conv_image_fst huffman_tree_def) apply (drule ord_le_eq_trans[of 2]) defer apply (drule_tac ts="(map (\(x, y). htree.Leaf x y) (sort_key snd (freq_of ys)))" in build_tree_Branch) apply fastforce+ done (* ------------------------------------------------------------------------------------ *) 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 begin 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" lemma is_stack_Nil_top[simp]: "is_stack [] s = (top_'' s = -1)" by (simp add: is_empty'_def is_stack_def) lemma is_stack_Nil_is_empty: "is_stack [] s = (is_empty' s = 1)" by (simp add: is_empty'_def) lemma stack_from_neg[simp]: "stack_from xs (- 1) s = (xs = [])" by (cases xs; simp) lemma is_stack_single: "is_stack [x] s = (top_'' s = 0 \ content_'' s.[0] = x)" by (auto simp: is_stack_def) 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)" by (auto simp: is_stack_def) lemma stack_from_top_upd[simp]: "stack_from xs n (s\top_'' := t\) = stack_from xs n s" by (induct xs arbitrary: n; simp) 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" apply (induct xs arbitrary: n; simp) apply (drule_tac x="n - 1" in meta_spec) apply (case_tac "n = 0", simp) apply (clarsimp simp: unat_minus_one) done 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" apply (cases "n = -1", simp) apply (simp add: unat_Suc2) apply (rule stack_from_top_and_array_upd') apply clarsimp done lemma pop_correct_partial: "\ \s. is_stack (x#xs) s \ pop' \ \rv s. rv = x \ is_stack xs s \" unfolding pop'_def by (wpsimp simp: is_stack_def) lemma pop_correct_total: "\ \s. is_stack (x#xs) s \ pop' \ \rv s. rv = x \ is_stack xs s \!" unfolding pop'_def by (wpsimp simp: is_stack_def) lemma push_correct_partial: "\ \s. is_stack xs s \ push' x \ \_ s. is_stack (x#xs) s \" supply word_less_nat_alt[simp] unfolding push'_def by (wpsimp simp: is_stack_def) lemma push_correct_total: "\ \s. is_stack xs s \ has_capacity' s = 1 \ push' x \ \_ s. is_stack (x#xs) s \!" supply word_less_nat_alt[simp] unfolding push'_def apply (wpsimp simp: is_stack_def has_capacity'_def split: if_split_asm) apply (subgoal_tac "unat (top_'' s + 1) < LEN", simp) apply (clarsimp simp: unat_word_ariths) done 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="\result s. \ys. is_stack ys s \ sum_list xs = result + sum_list ys"]) apply wp apply (simp add: pop'_def) apply wpsimp apply (clarsimp simp: is_stack_def) apply (case_tac ys, simp) apply fastforce apply (fastforce simp: is_stack_def) apply fastforce done end end