Homework 9

Definitions File

theory Defs
  imports "HOL-Data_Structures.RBT_Set"
begin

fun min_height :: "'a tree \<Rightarrow> nat" where
"min_height Leaf = 0" |
"min_height (Node l _ r) = min (min_height l) (min_height r) + 1"

definition "balanced t \<equiv> height t - min_height t \<le> 1"

fun mk_rbt :: "'a tree \<Rightarrow> 'a rbt" where
  "mk_rbt Leaf = Leaf"
| "mk_rbt (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'
  )"


consts mk_rbt' :: "'a tree \<Rightarrow> 'a rbt \<times> nat"


end

Template File

theory Submission
  imports Defs
begin

lemma balanced_subt: "balanced (Node l a r) \<Longrightarrow> balanced l \<and> balanced r"
  sorry

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

lemma mk_rbt_inorder: "inorder (mk_rbt t) = Tree.inorder t"
  sorry

lemma mk_rbt_color: "color (mk_rbt t) = Black"
  sorry

lemma mk_rbt_bheight: "balanced t \<Longrightarrow> bheight (mk_rbt t) = min_height t"
  sorry

lemma mk_rbt_invh: "balanced t \<Longrightarrow> invh (mk_rbt t)"
  sorry

lemma mk_rbt_invc: "balanced t \<Longrightarrow> invc (mk_rbt t)"
  sorry

fun mk_rbt' :: "'a tree \<Rightarrow> 'a rbt \<times> nat"
 where
  "mk_rbt' _ = undefined"

lemma mk_rbt'_refine: "fst (mk_rbt' t) = mk_rbt t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma balanced_subt: "balanced (Node l a r) \<Longrightarrow> balanced l \<and> balanced r"
  by (rule Submission.balanced_subt)

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

lemma mk_rbt_inorder: "inorder (mk_rbt t) = Tree.inorder t"
  by (rule Submission.mk_rbt_inorder)

lemma mk_rbt_color: "color (mk_rbt t) = Black"
  by (rule Submission.mk_rbt_color)

lemma mk_rbt_bheight: "balanced t \<Longrightarrow> bheight (mk_rbt t) = min_height t"
  by (rule Submission.mk_rbt_bheight)

lemma mk_rbt_invh: "balanced t \<Longrightarrow> invh (mk_rbt t)"
  by (rule Submission.mk_rbt_invh)

lemma mk_rbt_invc: "balanced t \<Longrightarrow> invc (mk_rbt t)"
  by (rule Submission.mk_rbt_invc)

lemma mk_rbt'_refine: "fst (mk_rbt' t) = mk_rbt t"
  by (rule Submission.mk_rbt'_refine)

end