Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 2

This is the task corresponding to homework 2.

Resources

Download Files

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

Terms and Conditions