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