Homework 2

Definitions File

theory Defs
  imports Main
begin

datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree"


consts collect :: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b list"

consts collect_tr :: "'a list \<Rightarrow> 'b \<Rightarrow> ('b \<times> 'a) list \<Rightarrow> 'a list"

consts lheight :: "'a ltree \<Rightarrow> nat"

consts num_leafs :: "'a ltree \<Rightarrow> nat"

consts complete :: "'a ltree \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

fun collect :: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b list"  where
  "collect _ = undefined"

value "collect (2::nat) [(2,3::int),(4,4),(2,5),(2,7),(3,0)] = [3,5,7]"
value "collect (1::nat) [(2,3::int),(4,4),(2,5),(2,7),(3,0)] = []"


lemma collect_functional: "collect x ys = map snd (filter (\<lambda>kv. fst kv = x) ys)"
  sorry

fun collect_tr :: "'a list \<Rightarrow> 'b \<Rightarrow> ('b \<times> 'a) list \<Rightarrow> 'a list"  where
  "collect_tr acc x [] = rev acc"
| "collect_tr _ = undefined"

lemma collect_tr_correct: "collect_tr [] x ys = collect x ys"
  sorry

fun lheight :: "'a ltree \<Rightarrow> nat"  where
  "lheight _ = undefined"

fun num_leafs :: "'a ltree \<Rightarrow> nat"  where
  "num_leafs _ = undefined"

fun complete :: "'a ltree \<Rightarrow> bool"  where
  "complete _ = undefined"

theorem complete_size: "complete t \<Longrightarrow> num_leafs t = 2^lheight t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma collect_functional: "collect x ys = map snd (filter (\<lambda>kv. fst kv = x) ys)"
  by (rule Submission.collect_functional)

lemma collect_tr_correct: "collect_tr [] x ys = collect x ys"
  by (rule Submission.collect_tr_correct)

theorem complete_size: "complete t \<Longrightarrow> num_leafs t = 2^lheight t"
  by (rule Submission.complete_size)

end