Week 9 homework 1

Definitions File

theory Defs
  imports Main "HOL-Data_Structures.Balance" "HOL-Data_Structures.RBT_Set"
begin

fun mk_rbt :: "'a Tree.tree \<Rightarrow> 'a rbt" where
  "mk_rbt Tree.Leaf = Tree2.Leaf"
| "mk_rbt (Tree.Node l a r) = (let
    l'=mk_rbt l;
    r'=mk_rbt r
  in
    if min_height l > min_height r then
      B (paint Red l') a r'
    else if min_height l < min_height r then
      B l' a (paint Red r')
    else
      B l' a r'
  )"

end

Template File

theory Submission
  imports Defs
begin

fun list_to_rbt :: "'a list \<Rightarrow> 'a rbt" where
  "list_to_rbt _ = undefined"

lemma balanced_alt:
  "balanced t \<longleftrightarrow> Tree.height t = min_height t \<or> Tree.height t = min_height t + 1"
  sorry

lemma mk_rbt_inorder: "Tree2.inorder (list_to_rbt xs) = xs"
  sorry

lemma mk_rbt_color: "color (list_to_rbt xs) = Black"
  sorry

lemma mk_rbt_invh: "invh (list_to_rbt xs)"
  sorry

lemma mk_rbt_invc: "invc (list_to_rbt t)"
  sorry


end

Check File

theory Check
  imports Submission
begin

lemma balanced_alt:
  "balanced t \<longleftrightarrow> Tree.height t = min_height t \<or> Tree.height t = min_height t + 1"
  by(rule balanced_alt)

lemma mk_rbt_inorder: "Tree2.inorder (list_to_rbt xs) = xs"
  by(rule mk_rbt_inorder)

lemma mk_rbt_color: "color (list_to_rbt xs) = Black"
  by(rule mk_rbt_color)

lemma mk_rbt_invh: "invh (list_to_rbt xs)"
  by(rule mk_rbt_invh)

lemma mk_rbt_invc: "invc (list_to_rbt t)"
  by(rule mk_rbt_invc)

end