FDS Week 7 homework

Definitions File

theory Defs
  imports Main  "HOL-Data_Structures.Sorting" "~~/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>)"

end

Template File

theory Submission
  imports Defs
begin

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

end

Check File

theory Check
  imports Submission
begin

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

end