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.Tree23" "HOL-Data_Structures.RBT_Set"
begin

fun bhs :: "'a rbt \<Rightarrow> nat set" where
"bhs Tree.Leaf = {0}" |
"bhs (Tree.Node l (_,c) r) = (let H = bhs l \<union> bhs r in if c=Black then Suc ` H else H)"

consts mk_rbt :: "'a tree23 \<Rightarrow> 'a rbt"

end```

### Template File

```theory Submission
imports Defs
begin

fun mk_rbt :: "'a tree23 \<Rightarrow> 'a rbt"  where
"mk_rbt _ = undefined"

lemma mk_rbt_inorder_btree: "Tree2.inorder (mk_rbt t) = Tree23.inorder t"
sorry

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

lemma mk_rbt_invh_btree: "Tree23.complete t \<Longrightarrow> invh (mk_rbt t)"
sorry

lemma mk_rbt_invc_btree: "invc (mk_rbt t)"
sorry

theorem invh_iff_bhs: "invh t \<longleftrightarrow> bhs t = {bheight t}"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma mk_rbt_inorder_btree: "Tree2.inorder (mk_rbt t) = Tree23.inorder t"
by (rule Submission.mk_rbt_inorder_btree)

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

lemma mk_rbt_invh_btree: "Tree23.complete t \<Longrightarrow> invh (mk_rbt t)"
by (rule Submission.mk_rbt_invh_btree)

lemma mk_rbt_invc_btree: "invc (mk_rbt t)"
by (rule Submission.mk_rbt_invc_btree)

theorem invh_iff_bhs: "invh t \<longleftrightarrow> bhs t = {bheight t}"
by (rule Submission.invh_iff_bhs)

end```

Terms and Conditions