I agree 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.

Download Files
### Definitions File

### Template File

### Check 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" by (simp add: t) 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

theory Submission imports Defs begin lemma reconstruct_from_postorder: "distinct (preorder t) \<Longrightarrow> reconstruct (rev (postorder t)) (inorder t) = t" sorry end

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