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.
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
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
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