Homework 2

Definitions File

theory Defs
  imports Main
begin

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

fun inorder :: "'a ltree \<Rightarrow> 'a list" where
  "inorder (Leaf x) = [x]"
| "inorder (Node l r) = inorder l @ inorder r"  
  
fun fold_ltree :: "('a \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> 'a ltree \<Rightarrow> 's \<Rightarrow> 's" where
  "fold_ltree f (Leaf x) s = f x s"
| "fold_ltree f (Node l r) s = fold_ltree f r (fold_ltree f l s)"

lemma "fold f (inorder t) s = fold_ltree f t s"  
  by (induction t arbitrary: s) auto

fun mirror where
  "mirror (Node l r) = Node (mirror r) (mirror l)"
| "mirror (Leaf x) = Leaf x"  

fun shuffles :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
  "shuffles xs [] = [xs]"
| "shuffles [] ys = [ys]"  
| "shuffles (x#xs) (y#ys) = map (\<lambda>xs. x # xs) (shuffles xs (y#ys)) @ map (\<lambda>ys. y # ys) (shuffles (x#xs) ys)"  


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 perfect :: "'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 _ _ = []"

definition ctest :: "(int * int) list" where "ctest \<equiv> [
    (2,3),(2,5),(2,7),(2,9), 
    (3,2),(3,4),(3,5),(3,7),(3,8),
    (4,3),(4,5),(4,7),(4,9),
    (5,2),(5,3),(5,4),(5,6),(5,7),(5,8),(5,9),
    (6,5),(6,7),
    (7,2),(7,3),(7,4),(7,5),(7,6),(7,8),(7,9),
    (8,3),(8,5),(8,7),(8,9),
    (9,2),(9,4),(9,5),(9,7),(9,8)
  ]"

value "collect 3 ctest = [2,4,5,7,8]"
value "collect 1 ctest = []"


lemma collect_alt: "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 _ _ _ = []"

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

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

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

fun perfect :: "'a ltree \<Rightarrow> bool"  where
  "perfect _ = True"

lemma perfect_num_leafs_height: "perfect t \<Longrightarrow> num_leafs t = 2^lheight t"
  sorry

lemma set_shuffles: "zs \<in> set (shuffles xs ys) \<Longrightarrow> set zs = set xs \<union> set ys"
  sorry

end

Check File

theory Check
  imports Submission
begin

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

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

lemma perfect_num_leafs_height: "perfect t \<Longrightarrow> num_leafs t = 2^lheight t"
  by (rule Submission.perfect_num_leafs_height)

lemma set_shuffles: "zs \<in> set (shuffles xs ys) \<Longrightarrow> set zs = set xs \<union> set ys"
  by (rule Submission.set_shuffles)

end