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


Download Files

Definitions File

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

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"
  "reconstruct [] [] = \<langle>\<rangle>"
| "reconstruct (y#ys) zs =
      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

  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)


Template File

theory Submission
  imports Defs

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


Check File

theory Check
  imports Submission

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


Terms and Conditions