Exercise 3

Definitions File

theory Defs
  (* Improve loading time, do not import those*)
  imports (* "HOL-Data_Structures.AA_Set" *) (* "HOL-Data_Structures.RBT_Set" *)
    "HOL-Data_Structures.RBT"
begin

(* Copied from HOL-Data_Structures.RBT_Set, to improve loading time *)
fun color :: "'a rbt \<Rightarrow> color" where
"color Leaf = Black" |
"color (Node _ (_, c) _) = c"

fun bheight :: "'a rbt \<Rightarrow> nat" where
"bheight Leaf = 0" |
"bheight (Node l (x, c) r) = (if c = Black then bheight l + 1 else bheight l)"

fun invc :: "'a rbt \<Rightarrow> bool" where
"invc Leaf = True" |
"invc (Node l (a,c) r) =
  ((c = Red \<longrightarrow> color l = Black \<and> color r = Black) \<and> invc l \<and> invc r)"

fun invh :: "'a rbt \<Rightarrow> bool" where
"invh Leaf = True" |
"invh (Node l (x, c) r) = (bheight l = bheight r \<and> invh l \<and> invh r)"

(* Copied from HOL-Data_Structures.AA_Set, to improve loading time *)
type_synonym 'a aa_tree = "('a*nat) tree"

definition empty :: "'a aa_tree" where
"empty = Leaf"

fun lvl :: "'a aa_tree \<Rightarrow> nat" where
"lvl Leaf = 0" |
"lvl (Node _ (_, lv) _) = lv"

fun invar :: "'a aa_tree \<Rightarrow> bool" where
"invar Leaf = True" |
"invar (Node l (a, h) r) =
 (invar l \<and> invar r \<and>
  h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (\<exists>lr b rr. r = Node lr (b,h) rr \<and> h = lvl rr + 1)))"

(* New stuff for exercise *)

fun invc' :: "'a rbt \<Rightarrow> bool"  where
 "invc' Leaf = True" 
| "invc' (Node l (a,c) r) =
  ((c = Red \<longrightarrow> color r = Black) \<and> color l = Black \<and> invc' l \<and> invc' r)"

consts rbt_to_aa :: "'a rbt \<Rightarrow> 'a aa_tree"
consts aa_to_rbt :: "'a aa_tree \<Rightarrow> 'a rbt"


(* Ignore everything below here, just here to make quickcheck work *)

fun invar' where "invar' Leaf = True"
|  "invar' (Node l (a,h) r) =  (invar' l \<and> invar' r \<and>
  h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (case r of Node lr (b,h') rr \<Rightarrow> h = h' \<and> h = lvl rr + 1 | _ \<Rightarrow> False)))"

lemma problem_point: "(\<exists>lr b rr. r = \<langle>lr, (b, h), rr\<rangle> \<and> h = lvl rr + 1)
   \<longleftrightarrow> (case r of Node lr (b,h') rr \<Rightarrow> h = h' \<and> h = lvl rr + 1 | _ \<Rightarrow> False)"
  by (cases r)auto
lemma replacement[code]: "invar t = invar' t"
  by (induction t) (auto simp add: problem_point split: tree.splits) 

end

Template File

theory Submission
  imports Defs
begin

fun rbt_to_aa :: "'a rbt \<Rightarrow> 'a aa_tree"  where
  "rbt_to_aa _ = undefined"

(*Should all be True*)
value "rbt_to_aa \<langle>\<rangle> = (\<langle>\<rangle>::nat aa_tree)"
value "rbt_to_aa (B \<langle>\<rangle> (1::nat) (R \<langle>\<rangle> 2 \<langle>\<rangle>)) = \<langle>\<langle>\<rangle>, (1,1), \<langle>\<langle>\<rangle>, (2,1), \<langle>\<rangle>\<rangle>\<rangle>"
value "rbt_to_aa (B (B \<langle>\<rangle> 2 \<langle>\<rangle>) (5::nat) (R (B \<langle>\<rangle> 7 \<langle>\<rangle>) 10 (B \<langle>\<rangle> 15 \<langle>\<rangle>))) 
  = \<langle>\<langle>\<langle>\<rangle>, (2, 1), \<langle>\<rangle>\<rangle>, (5, 2), \<langle>\<langle>\<langle>\<rangle>, (7, 1), \<langle>\<rangle>\<rangle>, (10, 2), \<langle>\<langle>\<rangle>, (15, 1), \<langle>\<rangle>\<rangle>\<rangle>\<rangle>"

fun aa_to_rbt :: "'a aa_tree \<Rightarrow> 'a rbt" where
  "aa_to_rbt _ = undefined"

(* Should all be True *)
value "aa_to_rbt (\<langle>\<rangle>::nat aa_tree) = \<langle>\<rangle>"
value "aa_to_rbt \<langle>\<langle>\<rangle>, (1,1), \<langle>\<langle>\<rangle>, (2,1), \<langle>\<rangle>\<rangle>\<rangle> = (B \<langle>\<rangle> (1::nat) (R \<langle>\<rangle> 2 \<langle>\<rangle>))"
value "aa_to_rbt \<langle>\<langle>\<langle>\<rangle>, (2, 1), \<langle>\<rangle>\<rangle>, (5, 2), \<langle>\<langle>\<langle>\<rangle>, (7, 1), \<langle>\<rangle>\<rangle>, (10, 2), \<langle>\<langle>\<rangle>, (15, 1), \<langle>\<rangle>\<rangle>\<rangle>\<rangle>
  = (B (B \<langle>\<rangle> 2 \<langle>\<rangle>) (5::nat) (R (B \<langle>\<rangle> 7 \<langle>\<rangle>) 10 (B \<langle>\<rangle> 15 \<langle>\<rangle>)))"


(* Do not prove *)
lemma rbt_to_aa: "invc' t \<Longrightarrow> invh t \<Longrightarrow> color t = Black \<Longrightarrow> invar (rbt_to_aa t)" oops
lemma inorder_rbt_to_aa: "invc' t \<Longrightarrow> invh t \<Longrightarrow> color t = Black \<Longrightarrow> inorder (rbt_to_aa t) = inorder t" oops
lemma aa_to_rbt: "invar t \<Longrightarrow> invc' (aa_to_rbt t) \<and> invh (aa_to_rbt t)" oops
lemma inorder_aa_to_rbt: "invar t \<Longrightarrow> inorder (aa_to_rbt t) = inorder t" oops
lemma aa_to_rbt_rbt_to_aa: "invc' t \<Longrightarrow> invh t \<Longrightarrow> color t = Black \<Longrightarrow> aa_to_rbt (rbt_to_aa t) = t" oops
lemma rbt_to_aa_aa_to_rbt: "invar t \<Longrightarrow> rbt_to_aa (aa_to_rbt t) = t" oops

end

Check File

theory Check
  imports Submission
begin

(* Nothing to prove *)

end