Exercise 1

Definitions File

theory Defs
  imports "HOL-Library.Tree"
begin

fun join :: "'a list list \<Rightarrow> 'a list list \<Rightarrow> 'a list list" where
  "join xss [] = xss" |
  "join [] yss = yss" |
  "join (xs#xss) (ys#yss) = (xs @ ys) # join xss yss"

fun levels :: "'a tree \<Rightarrow> 'a list list" where
  "levels Leaf = []" |
  "levels (Node l a r) = [a] # join (levels l) (levels r)"

definition set2 :: "'a list list \<Rightarrow> 'a set" where
  "set2 xss \<equiv> \<Union>(set (map set xss))"

end

Template File

theory Submission
  imports Defs
begin

lemma levels_height: "length(levels t) = height t"
  sorry


lemma levels_set: "set2 (levels t) = set_tree t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma levels_height: "length(levels t) = height t"
  by (rule Submission.levels_height)


lemma levels_set: "set2 (levels t) = set_tree t"
  by (rule Submission.levels_set)

end