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 2

This is the task corresponding to homework 2.

## Resources

### Definitions File

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

datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree"

fun inorder :: "'a ltree \<Rightarrow> 'a list" where
"inorder (Leaf x) = [x]"
| "inorder (Node l r) = inorder l @ inorder r"

consts replace_tr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"

consts to_tree :: "'a tree => 'a ltree"

end```

### Template File

```theory Submission
imports Defs
begin

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

lemma replace_len: "length (replace a b xs) = length xs"
sorry

lemma replace_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace a b xs)"
sorry

lemma replace_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace a b xs)"
sorry

fun replace_tr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"replace_tr _ _ acc [] = rev acc" lemma replace_tr_len: "length (replace_tr a b [] xs) = length xs"
sorry

lemma replace_tr_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace_tr a b [] xs)"
sorry

lemma replace_tr_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace_tr a b [] xs)"
sorry

fun to_tree :: "'a tree => 'a ltree"  where
"to_tree _ = undefined"

lemma to_tree_inorder: "t \<noteq> \<langle>\<rangle> \<Longrightarrow> Tree.inorder t = inorder (to_tree t)"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma replace_len: "length (replace a b xs) = length xs"
by (rule Submission.replace_len)

lemma replace_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace a b xs)"
by (rule Submission.replace_set)

lemma replace_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace a b xs)"
by (rule Submission.replace_set2)

lemma replace_tr_len: "length (replace_tr a b [] xs) = length xs"
by (rule Submission.replace_tr_len)

lemma replace_tr_set: "a \<noteq> b \<Longrightarrow> a \<notin> set (replace_tr a b [] xs)"
by (rule Submission.replace_tr_set)

lemma replace_tr_set2: "b \<in> set xs \<Longrightarrow> b \<in> set (replace_tr a b [] xs)"
by (rule Submission.replace_tr_set2)

lemma to_tree_inorder: "t \<noteq> \<langle>\<rangle> \<Longrightarrow> Tree.inorder t = inorder (to_tree t)"
by (rule Submission.to_tree_inorder)

end```

Terms and Conditions