Homework 9

Definitions File

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

fun mk_rbt :: "'a tree \<Rightarrow> 'a rbt" where
  "mk_rbt \<langle>\<rangle> = \<langle>\<rangle>"
| "mk_rbt \<langle>l, a, r\<rangle> = (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 list_to_rbt :: "'a list \<Rightarrow> 'a rbt"


end

Template File

theory Submission
  imports Defs
begin

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

lemma acomplete_alt:
  "acomplete t \<longleftrightarrow> height t = min_height t \<or> 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 acomplete_alt: "acomplete t \<longleftrightarrow> height t = min_height t \<or> height t = min_height t + 1"
  by (rule Submission.acomplete_alt)

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

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

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

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

end