Cookies disclaimer

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.

Week 8 bonus 2

Week 8 bonus 2

Resources

Download Files

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

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