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.

# Week 9 homework 1

Week 9 homework 1

## Resources

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

Terms and Conditions