Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 9

This is the task corresponding to homework 9.

## Resources

### 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```

Terms and Conditions