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 4

This is the task corresponding to homework 4.

## Resources

### Definitions File

```theory Defs
imports Main
begin

datatype 'a rtree = Leaf | Node "'a rtree" nat 'a "'a rtree"

definition "at_index i l x \<equiv> i<length l \<and> l!i=x"

declare Let_def [simp]
declare [[names_short]]

consts num_nodes :: "'a rtree \<Rightarrow> nat"

consts rbst :: "'a::linorder rtree \<Rightarrow> bool"

consts rins :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree"

consts risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool"

consts inorder :: "'a rtree \<Rightarrow> 'a list"

consts rank :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> nat"

consts select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a"

end```

### Template File

```theory Submission
imports Defs
begin

fun num_nodes :: "'a rtree \<Rightarrow> nat"  where
"num_nodes _ = undefined"

fun rbst :: "'a::linorder rtree \<Rightarrow> bool"  where
"rbst _ = undefined"

fun rins :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> 'a rtree"  where
"rins _ = undefined"

lemma rins_set: "set_rtree (rins x t) = insert x (set_rtree t)"
sorry

lemma rins_invar: "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
sorry

fun risin :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> bool"  where
"risin _ = undefined"

lemma risin_set: "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
sorry

fun inorder :: "'a rtree \<Rightarrow> 'a list"  where
"inorder _ = undefined"

fun rank :: "'a::linorder \<Rightarrow> 'a rtree \<Rightarrow> nat"  where
"rank _ = undefined"

lemma inorder_index: "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
sorry

fun select :: "nat \<Rightarrow> 'a::linorder rtree \<Rightarrow> 'a"  where
"select _ = undefined"

lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma rins_set: "set_rtree (rins x t) = insert x (set_rtree t)"
by (rule Submission.rins_set)

lemma rins_invar: "x\<notin>set_rtree t \<Longrightarrow> rbst t \<Longrightarrow> rbst (rins x t)"
by (rule Submission.rins_invar)

lemma risin_set: "rbst t \<Longrightarrow> risin x t \<longleftrightarrow> x\<in>set_rtree t"
by (rule Submission.risin_set)

lemma inorder_index: "rbst t \<Longrightarrow> x\<in>set_rtree t \<Longrightarrow> at_index (rank x t) (inorder t) x"
by (rule Submission.inorder_index)

lemma select_correct: "rbst t \<Longrightarrow> i<length (inorder t) \<Longrightarrow> select i t = inorder t ! i"
by (rule Submission.select_correct)

end```

Terms and Conditions