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.

# FDS Week 3 Homework

Week 3 homework.

## Resources

### Definitions File

```theory Defs
imports "HOL-Library.Tree"
begin

fun isin :: "('a::linorder) tree \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node l a r) x =
(if x < a then isin l x else
if x > a then isin r x
else True)"

fun ins :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"ins x Leaf = Node Leaf x Leaf" |
"ins x (Node l a r) =
(if x < a then Node (ins x l) a r else
if x > a then Node l a (ins x r)
else Node l a r)"

end
```

### Template File

```theory Template
imports Defs
begin

abbreviation bst_eq :: "('a::linorder) tree \<Rightarrow> bool" where
"bst_eq \<equiv> undefined"

lemma isin_bst_eq: "bst_eq t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
sorry

lemma bst_eq_ins: "bst_eq t \<Longrightarrow> bst_eq (ins x t)"
sorry

fun ins_eq :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
where
"ins_eq _ _= undefined"

lemma bst_eq_ins_eq: "bst_eq t \<Longrightarrow> bst_eq (ins_eq x t)"
sorry

fun count_tree :: "'a \<Rightarrow> 'a tree \<Rightarrow> nat"
where
"count_tree _ _ = undefined"

lemma count_tree_ins_eq: "count_tree x (ins_eq x t) = Suc (count_tree x t)"
sorry

lemma count_tree_ins_eq_diff: "x\<noteq>y \<Longrightarrow> count_tree y (ins_eq x t) = count_tree y t"
sorry

end
```

### Check File

```theory Check
imports Submission
begin

lemma isin_bst_eq: "bst_eq t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
by (rule isin_bst_eq)

lemma bst_eq_ins: "bst_eq t \<Longrightarrow> bst_eq (ins x t)"
by(rule bst_eq_ins)

lemma bst_eq_ins_eq: "bst_eq t \<Longrightarrow> bst_eq (ins_eq x t)"
by(rule bst_eq_ins_eq)

lemma count_tree_ins_eq: "count_tree x (ins_eq x t) = Suc (count_tree x t)"
by (rule count_tree_ins_eq)

lemma "x\<noteq>y \<Longrightarrow> count_tree y (ins_eq x t) = count_tree y t"
by (rule count_tree_ins_eq_diff)

end
```

Terms and Conditions