Homework 7

Definitions File

theory Defs
  imports "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>)"



end

Template File

theory Submission
  imports Defs
begin

thm preorder.simps
thm inorder.simps

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

theorem reconstruct_correct:
  "distinct (preorder t) \<Longrightarrow> reconstruct (preorder t) (inorder t) = t"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem reconstruct_correct: "distinct (preorder t) \<Longrightarrow> reconstruct (preorder t) (inorder t) = t"
  by (rule Submission.reconstruct_correct)

end