(*
 * COMP4161 Assignment 3.
 *)
theory a3
imports AutoCorres "~~/src/HOL/Number_Theory/Number_Theory"
begin

  
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 \<times> int) list"

(* Q1 a): TODO *)
primrec add_one :: "'a \<Rightarrow> 'a freq_list \<Rightarrow> 'a freq_list" where
  "add_one c [] = undefined" (* TODO *)
  
primrec freq_of :: "'a list \<Rightarrow> 'a freq_list" where
  "freq_of [] = undefined" (* TODO *)

value "freq_of ''abcdaa''"


lemma fst_set_add_one:
  "fst ` set (add_one x xs) = {x} \<union> fst ` set xs"
  oops
      
(* 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 \<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): TODO *)
  
definition encoder :: "('a \<Rightarrow> code option) \<Rightarrow> 'a list \<Rightarrow> code" where
  "encoder mp xs = undefined" (* TODO *)


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'' = []"
  oops


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"
  oops

    
(* 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"
  sorry (* TODO *)

    
    
(* 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))"
  sorry (* TODO *)


  
(* Q1 f): *)
primrec letters_of :: "'a htree \<Rightarrow> 'a set" where
  "letters_of (Leaf c _) = undefined" (* TODO: complete *)

(* Q1 g): *)
fun distinct_tree :: "'a htree \<Rightarrow> bool"  where
  "distinct_tree (Leaf _ _) = undefined" (* TODO: complete *)
  
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_code_list:
  "fst ` set (code_list t) = letters_of t"
  oops

(* Q1 h): *)
lemma distinct_fst_code_list[simp]:
  "distinct_tree t \<Longrightarrow> distinct (map fst (code_list t))"
  sorry (* TODO *)
  
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) = {})"
  oops


lemma distinct_build_tree:
  "distinct_forest ts \<Longrightarrow> distinct_tree (build_tree ts)"
  oops
  
lemma distinct_insort_map:
  "distinct (map g (insort_key f x xs)) = (g x \<notin> g ` set xs \<and> distinct (map g xs))"
  oops

(* Q1 i): *)    
lemma distinct_huffman[simp]:
  "distinct (map fst fs) \<Longrightarrow> distinct_tree (huffman_tree fs)"
  sorry (* TODO *)
    

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)"
  oops
    
      
lemma unique_prefix_code_map[simp]:
  "unique_prefix (map_of (code_map t))"
  oops
    

lemma build_tree_Branch:
  "2 \<le> length ts \<Longrightarrow> \<exists>l r. build_tree ts = Branch l r"
  oops



(* Q1 j): *)    
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"
  sorry (* TODO *)


    
(*******************************************************************)
(* C Verification                                                  *)
(*******************************************************************)

  
(* Parse the C file into SIMPL. *)
install_C_file "prime2.c"

(* Convert the SIMPL into monadic representation. *)

autocorres [unsigned_word_abs=is_prime_2, ts_force nondet=is_prime_2] "prime2.c"


(*******************************************************************)

section "Primality modulo 2"

context prime2 begin

thm is_prime_2'_def

(* Q2 a): Loop invariant for "is_prime_2". *)
definition
  is_prime_inv :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
  "is_prime_inv i n \<equiv>
	True (*TODO*)"


(* Q2 b): Measure function for "is_prime_2". Must be strictly decreasing
 * for each loop iteration. *)
definition
  is_prime_measure :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "is_prime_measure i n \<equiv> undefined" (*TODO*)


(* Q2 c1): A prime is either 2 or an odd number *)
lemma prime_2_or_odd: "prime n \<Longrightarrow> n = 2 \<or> n mod 2 = Suc 0"
  sorry (* TODO *)


(* Q2 c2): The loop invariant holds coming into the loop. *)
lemma is_prime_precond_implies_inv: 
  "True"
  sorry (*TODO*)


(* Q2 c3): The loop invariant holds for each loop iteration. *)
lemma is_prime_body_obeys_inv:
  "True"
  sorry (*TODO*)


(* Q2 c4): The loop measure decrements each loop iteration. *)
lemma is_prime_body_obeys_measure:
  "\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0 \<rbrakk>
      \<Longrightarrow> is_prime_measure i n > is_prime_measure (i + 2) n"
  sorry (*TODO*)


(* Q2 c5): The loop invariant implies there is no overflow. *)
lemma is_prime_body_implies_no_overflow:
  "\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0\<rbrakk> \<Longrightarrow> i + 2 \<le> UINT_MAX"
  sorry


(* Q2 c6): The loop invariant implies the post-condition. *)
lemma is_prime_inv_implies_postcondition:
  "True"
  sorry (*TODO*)


(*
 * Q2 d): Show that "is_prime' n" is correct.
 *
 * AutoCorres has applied "word abstraction" to this function,
 * meaning that you are able to reason using "nats" instead of
 * "word32" data types, at the price of having to reason that
 * your values don't overflow UINT_MAX.
 *)
lemma is_prime_correct:
  "\<lbrace>\<lambda>s. n \<le> UINT_MAX \<rbrace> is_prime_2' n \<lbrace>\<lambda>r s. r = (if prime n then 1 else 0) \<rbrace>!"
  (* Unfold the program body. *)
  apply (unfold is_prime_2'_def)
  (* Annotate the loop with an invariant and measure. *)
  apply (subst whileLoop_add_inv [where
     I="\<lambda>i s. is_prime_inv i n" and
     M="\<lambda>(i, s). is_prime_measure i n" ])

  (*
   * Run "wp" to generate verification conditions.
   *
   * The resulting subgoals are:
   *    1. The loop body obeys the invariant, causes the measure to decrease, and
            does not lead to overflow;
   *    2. The invariant implies the post-condition of the function; and
   *    3. The pre-condition of the function implies the invariant.
   *
   * You will need to run "apply wp" more times to convert Hoare-triples
   * into standard Isabelle goals.
   *)
  apply wp
  sorry (*TODO*)

end


end