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 3

This is the task corresponding to homework 3.

## 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)"

lemma set_tree_isin: "bst t \<Longrightarrow> isin t x = (x \<in> set_tree t)"
apply(induction t)
apply auto
done

lemma set_tree_ins: "set_tree (ins x t) = {x} \<union> set_tree t"
apply(induction t)
apply auto
done

lemma bst_ins: "bst t \<Longrightarrow> bst (ins x t)"
apply(induction t)
apply (auto simp: set_tree_ins)
done

datatype direction = L | R
type_synonym path = "direction list"

declare [[names_short]]

consts bst_remdups_aux :: "'a::linorder tree \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"

consts get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"

consts put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"

consts valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"

consts find :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> path set"

end```

### Template File

```theory Submission
imports Defs
begin

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

definition "bst_remdups xs \<equiv> bst_remdups_aux Leaf xs"

theorem remdups_set: "set (bst_remdups xs) = set xs"
sorry

theorem remdups_distinct: "distinct (bst_remdups xs)"
sorry

fun sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  where
"sublist _ = undefined"

theorem remdups_sub: "sublist (bst_remdups xs) xs"
sorry

fun get :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree"  where
"get _ = undefined"

fun put :: "'a tree \<Rightarrow> path \<Rightarrow> 'a tree \<Rightarrow> 'a tree"  where
"put _ = undefined"

fun valid :: "'a tree \<Rightarrow> path \<Rightarrow> bool"  where
"valid _ = undefined"

fun find :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> path set"  where
"find _ = undefined"

lemma get_put: "valid t p \<Longrightarrow> put t p (get t p) = t"
sorry

lemma put_get: "valid t p \<Longrightarrow> get (put t p s) p = s"
sorry

lemma find_get: "p \<in> find t s \<Longrightarrow> get t p = s"
sorry

lemma put_find: "valid t p \<Longrightarrow> p \<in> find (put t p s) s"
sorry

end```

### Check File

```theory Check
imports Submission
begin

theorem remdups_set: "set (bst_remdups xs) = set xs"
by (rule Submission.remdups_set)

theorem remdups_distinct: "distinct (bst_remdups xs)"
by (rule Submission.remdups_distinct)

theorem remdups_sub: "sublist (bst_remdups xs) xs"
by (rule Submission.remdups_sub)

lemma get_put: "valid t p \<Longrightarrow> put t p (get t p) = t"
by (rule Submission.get_put)

lemma put_get: "valid t p \<Longrightarrow> get (put t p s) p = s"
by (rule Submission.put_get)

lemma find_get: "p \<in> find t s \<Longrightarrow> get t p = s"
by (rule Submission.find_get)

lemma put_find: "valid t p \<Longrightarrow> p \<in> find (put t p s) s"
by (rule Submission.put_find)

end```

Terms and Conditions