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 8 bonus 2

Week 8 bonus 2

## Resources

### Definitions File

```theory Defs
imports Main  "~~/src/HOL/Library/Tree"
begin

definition lefts::"'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where "lefts y xs = takeWhile (\<lambda>x. x \<noteq> y) xs"

definition rights::"'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where "rights y xs = tl (dropWhile (\<lambda>x. x \<noteq> y) xs)"

fun reconstruct::"'a list \<Rightarrow> 'a list \<Rightarrow> 'a tree"
where
"reconstruct [] [] = \<langle>\<rangle>"
| "reconstruct (y#ys) zs =
(let
ls = lefts y zs;
rs = rights y zs
in \<langle>reconstruct (filter (\<lambda>y. y \<in> set ls) ys) ls, y,
reconstruct (filter (\<lambda>y. y \<in> set rs) ys) rs\<rangle>)"

value "reconstruct [3, 1, 6, 5, 8, 7, 9::int] [1, 3, 5, 6, 7, 8, 9]"
value "reconstruct [5, 3, 4, 1, 2] [1, 2, 3, 4, 5::int]"

lemma preorder_eq_Nil: "([] = preorder t) = (t = \<langle>\<rangle>)"
by (induct t) auto

lemma preorder_eq_Cons:
"x # xs = preorder n \<Longrightarrow> \<exists> l r. n = \<langle>l, x, r\<rangle>"
by (cases n) auto

lemma takeWhile_split: "x \<notin> set xs \<Longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) (xs @ x # ys) = xs"
by (induct xs) auto

lemma dropWhile_split: "x \<notin> set xs \<Longrightarrow> tl (dropWhile (\<lambda>z. z \<noteq> x) (xs @ x # ys)) = ys"
by (induct xs) auto

lemma
assumes disjoint: "x \<notin> set ls"
shows lefts_append: "lefts x (ls @ x # rs) = ls"
and rights_append: "rights x (ls @ x # rs) = rs"
using disjoint
by (auto simp: lefts_def rights_def dropWhile_split takeWhile_split)

lemma reconstruct_correct:
"distinct (preorder t) \<Longrightarrow> reconstruct (preorder t) (inorder t) = t"
proof (induction "preorder t" "inorder t" arbitrary: t rule: reconstruct.induct)
case (2 x xs)
then obtain l r where t: "t = \<langle>l, x, r\<rangle>"
by (meson preorder_eq_Cons)

from 2 have disjoint: "set_tree l \<inter> set_tree r = {}"
and [simp]: "x \<notin> set_tree l" "x \<notin> set_tree r"
by (auto simp: t)

have empties[simp]: "[y\<leftarrow>preorder r . y \<in> set_tree l] = []"
"[y\<leftarrow>preorder l . y \<in> set_tree r] = []"
using disjoint
by (auto intro!: filter_False)

have preorder: "preorder t = x # preorder l @ preorder r"

have l_eq: "lefts x (inorder t) = inorder l"
and r_eq: "rights x (inorder t) = inorder r"
by (auto simp: lefts_append rights_append t)

have "reconstruct (preorder t) (inorder t) =
\<langle>reconstruct (preorder l) (inorder l), x, reconstruct (preorder r) (inorder r)\<rangle>"
by (auto simp: r_eq l_eq preorder)
also have "reconstruct (preorder l) (inorder l) = l"
using 2(3-)
by (intro 2(1)) (auto simp: t lefts_append)
also have "reconstruct (preorder r) (inorder r) = r"
using 2(3-)
by (intro 2(2)) (auto simp: t rights_append)
finally show ?case unfolding t .
qed (auto simp: preorder_eq_Nil)

end```

### Template File

```theory Submission
imports Defs
begin

lemma reconstruct_from_postorder:
"distinct (preorder t) \<Longrightarrow> reconstruct (rev (postorder t)) (inorder t) = t"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma reconstruct_from_postorder:
"distinct (preorder t) \<Longrightarrow> reconstruct (rev (postorder t)) (inorder t) = t"
by(rule reconstruct_from_postorder)

end```

Terms and Conditions