(*
 * COMP4161 Assignment 3.
 *)

theory s3
  imports
    AutoCorres.AutoCorres
    "HOL-Library.Prefix_Order"
begin


section "Huffman Code"

type_synonym 'a freq_list = "('a \<times> int) list"

(* Q1 a): *)
primrec add_one :: "'a \<Rightarrow> 'a freq_list \<Rightarrow> 'a freq_list" where
  "add_one c [] = [(c, 1)]"
| "add_one c (x#as) = (case x of (a, n) \<Rightarrow>if c=a then (a, n+1)#as
                            else (a, n)#(add_one c as))"

fun freq_of :: "'a list \<Rightarrow> '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} \<union> fst ` set xs"
  by (induct xs; simp add: split_def)

lemma distinct_add_one: "distinct (map fst xs) \<Longrightarrow> 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 \<Rightarrow> int" where
  "weight (Leaf _ w) = w" |
  "weight (Branch l r) = weight l + weight r"

fun build_tree :: "'a htree list \<Rightarrow> '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 \<Rightarrow> 'a htree" where
  "huffman_tree = build_tree o map (\<lambda>(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 \<Rightarrow> 'a \<times> code \<Rightarrow> 'a \<times> code" where
  "add_bit b (c, code) = (c, b # code)"

primrec code_list :: "'a htree \<Rightarrow> ('a \<times> 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 \<Rightarrow> (code \<times> 'a) list" where
  "code_map tree = map (\<lambda>(a,b). (b,a)) (code_list tree)"

value "code_list some_tree"
value "code_map some_tree"


(* Q1 c): *)
definition encoder :: "('a \<Rightarrow> code option) \<Rightarrow> 'a list \<Rightarrow> 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 \<Rightarrow> 'a option) \<Rightarrow> code \<Rightarrow> code \<Rightarrow> 'a list" where
  "decoder mp acs [] = []" |
  "decoder mp acs (c#cs) = (if mp (acs@[c]) \<noteq> None
                            then the (mp (acs@[c])) # decoder mp [] cs
                            else decoder mp (acs @ [c]) cs)"


definition unique_prefix :: "(code \<Rightarrow> 'a option) \<Rightarrow> bool" where
  "unique_prefix cm = (\<forall>xs\<in>dom cm. \<forall>ys\<in>dom cm. \<not> ys < xs)"

definition is_inv :: "('a \<Rightarrow> 'b option) \<Rightarrow> ('b \<Rightarrow> 'a option) \<Rightarrow> bool" where
  "is_inv mp mp' = (\<forall>x y. mp x = Some y \<longleftrightarrow> mp' y = Some x)"


lemma unique_prefixD:
  "\<lbrakk> unique_prefix m; m xs = Some y; m xs' = Some y'; xs = xs' @ xs'' \<rbrakk> \<Longrightarrow> xs'' = []"
  by (fastforce simp: unique_prefix_def dom_def less_list_def)

lemma decoder_step:
  "\<lbrakk>unique_prefix mp'; mp' ys' = None; mp' (ys' @ ys) = Some x\<rbrakk>
   \<Longrightarrow> 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:
  "\<lbrakk> is_inv mp mp'; unique_prefix mp'; set (x#xs) \<subseteq> dom mp; [] \<notin> dom mp';
     mp' (ys'@ys) = Some x; mp' ys' = None; ys \<noteq> [] \<rbrakk>
   \<Longrightarrow> 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:
  "\<lbrakk> is_inv mp mp'; unique_prefix mp'; set xs \<subseteq> dom mp; [] \<notin> dom mp' \<rbrakk>
   \<Longrightarrow> 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:
  "\<lbrakk> distinct (map snd xs); distinct (map fst xs) \<rbrakk> \<Longrightarrow>
  is_inv (map_of xs) (map_of (map (\<lambda>(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 \<Rightarrow> 'a set" where
  "letters_of (Leaf c _) = {c}"
| "letters_of (Branch t1 t2) = letters_of t1 \<union> letters_of t2"

(* Q1 g): *)
fun distinct_tree :: "'a htree \<Rightarrow> bool"  where
  "distinct_tree (Leaf _ _) = True"
| "distinct_tree (Branch t1 t2) = (distinct_tree t1 \<and> distinct_tree t2
                                   \<and> (letters_of t1 \<inter> letters_of t2 = {}))"


fun distinct_forest :: "'a htree list \<Rightarrow> bool" where
  "distinct_forest [] = True" |
  "distinct_forest (t#ts) = (distinct_tree t \<and> distinct_forest ts \<and>
                             letters_of t \<inter> \<Union> (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 \<Longrightarrow> 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 \<and> distinct_forest ts \<and> letters_of t \<inter> \<Union> (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 \<Longrightarrow> 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 \<notin> g ` set xs \<and> 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 \<circ> (\<lambda>(x, y). htree.Leaf x y)"
  by fastforce

lemma map_Leaf_sort:
   "map (\<lambda>(x, y). htree.Leaf x y) (sort_key snd fs)
    = sort_key weight (map (\<lambda>(x, y). htree.Leaf x y) fs)"
   by (simp add: weight_eq sort_map)

(* Q1 i): *)
lemma distinct_huffman:
  "distinct (map fst fs) \<Longrightarrow> 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:
  "\<lbrakk>unique_prefix m1; unique_prefix m2; \<forall>xs \<in> dom m1. \<forall>ys \<in> dom m2. \<not> xs < ys \<and> \<not> ys < xs \<rbrakk>
    \<Longrightarrow> 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 \<le> length ts \<Longrightarrow> \<exists>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 \<circ> 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 \<Longrightarrow> 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\<noteq>[] \<Longrightarrow> letters_of (build_tree ts) = \<Union> (set (map letters_of ts))"
  by (induct rule: build_tree.induct; auto simp: set_insort_key)

theorem huffman_decoder:
  "\<lbrakk>set xs \<subseteq> set ys; tree = huffman_tree (freq_of ys); 2 \<le> length (freq_of ys) \<rbrakk> \<Longrightarrow>
   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 (\<lambda>(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 \<Rightarrow> machine_word \<Rightarrow> lifted_globals \<Rightarrow> bool" where
  "stack_from [] n s = (n = -1 )" |
  "stack_from (x # xs) n s = (n < LEN \<and> content_'' s.[unat n] = x \<and> stack_from xs (n - 1) s)"

definition is_stack where
  "is_stack xs s \<equiv> 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 \<and> content_'' s.[0] = x)"
  by (auto simp: is_stack_def)

lemma is_stack_Cons[simp]:
  "is_stack (x # xs) s =
   (top_'' s < LEN \<and> content_'' s.[unat (top_'' s)] = x \<and> stack_from xs (top_'' s - 1) s)"
  by (auto simp: is_stack_def)

lemma stack_from_top_upd[simp]:
  "stack_from xs n (s\<lparr>top_'' := t\<rparr>) = stack_from xs n s"
  by (induct xs arbitrary: n; simp)

lemma stack_from_top_and_array_upd':
  "\<lbrakk> \<forall>i \<le> unat n. a.[i] = content_'' s.[i] \<rbrakk> \<Longrightarrow>
   stack_from xs n (s\<lparr>top_'' := t, content_'' := a\<rparr>) = 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 \<Longrightarrow>
   stack_from xs n (s\<lparr>top_'' := n+1, content_'' := Arrays.update (content_'' s) (unat (n+1)) x\<rparr>) = 
   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:
  "\<lbrace> \<lambda>s. is_stack (x#xs) s \<rbrace> pop' \<lbrace> \<lambda>rv s. rv = x \<and> is_stack xs s \<rbrace>"
  unfolding pop'_def
  by (wpsimp simp: is_stack_def)

lemma pop_correct_total:
  "\<lbrace> \<lambda>s. is_stack (x#xs) s \<rbrace> pop' \<lbrace> \<lambda>rv s. rv = x \<and> is_stack xs s \<rbrace>!"
  unfolding pop'_def
  by (wpsimp simp: is_stack_def)

lemma push_correct_partial:
  "\<lbrace> \<lambda>s. is_stack xs s \<rbrace> push' x \<lbrace> \<lambda>_ s. is_stack (x#xs) s \<rbrace>"
  supply word_less_nat_alt[simp]
  unfolding push'_def
  by (wpsimp simp: is_stack_def)

lemma push_correct_total:
  "\<lbrace> \<lambda>s. is_stack xs s \<and> has_capacity' s = 1 \<rbrace> push' x \<lbrace> \<lambda>_ s. is_stack (x#xs) s \<rbrace>!"
  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:
  "\<lbrace> \<lambda>s. is_stack xs s \<rbrace> sum' \<lbrace> \<lambda>rv s. is_stack [] s \<and> rv = sum_list xs \<rbrace>"
  unfolding sum'_def
  apply (subst whileLoop_add_inv[where
                 I="\<lambda>result s. \<exists>ys. is_stack ys s \<and> 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
