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 2

Week 9 homework 2

## Resources

### Definitions File

```theory Defs
imports "HOL-Data_Structures.Tree2"
"HOL-Data_Structures.Cmp"
"HOL-Data_Structures.List_Ins_Del"
begin

datatype color = Red | Black

type_synonym 'a rbt = "('a,color * nat)tree"

text \<open>

Define a function for accessing the new field:
\<close>

fun bh :: "'a rbt \<Rightarrow> nat" where
"bh Leaf = 0" |
"bh (Node l a (c,h) r) = h"

abbreviation R where "R l a h r \<equiv> Node l a (Red,h) r"
abbreviation B where "B l a h r \<equiv> Node l a (Black,h) r"

abbreviation rd where "rd l a r \<equiv> Node l a (Red,bh l) r"
abbreviation bk where "bk l a r \<equiv> Node l a (Black,Suc(bh l)) r"

end```

### Template File

```theory Submission
imports Defs
begin

definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"insert _ = undefined"

fun invh2 :: "'a rbt \<Rightarrow> bool" where
"invh2 _ = undefined"

definition rbt :: "'a rbt \<Rightarrow> bool" where
"rbt _ = undefined"

lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
sorry

theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
by(rule inorder_insert)

theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
by(rule rbt_insert)

end```

Terms and Conditions