FDS week 2 homework

Definitions File

theory Defs
  imports Main
begin

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

end

Template File

theory Submission
  imports Defs
begin

text \<open>Homework 2.1\<close>

fun add ::"nat \<Rightarrow> nat \<Rightarrow> nat" where 
  "add _ _ = undefined"

lemma add_zero: "m = add m 0"
  sorry

lemma add_commute: "add n m = add m n"
  sorry

lemma add_assoc: "add l (add n m) = add (add l n) m"
  sorry

text \<open>Homework 2.2\<close>

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

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

lemma height_lt_leaves: "lheight t < num_leafs t"
  sorry

text \<open>Homework 2.3\<close>

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

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

lemma rlenc_dec_works: "rldec (rlenc a 0 l) = l"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma add_zero: "m = add m 0"
  by (rule Submission.add_zero)

lemma add_commute: "add n m = add m n"
  by (rule Submission.add_commute)

lemma add_assoc: "add l (add n m) = add (add l n) m"
  by (rule Submission.add_assoc)

text \<open>Homework 2.2\<close>

lemma height_lt_leaves: "lheight t < num_leafs t"
  by (rule Submission.height_lt_leaves)

text \<open>Homework 2.3\<close>

lemma rlenc_dec_works: "rldec (rlenc a 0 l) = l"
  by (rule Submission.rlenc_dec_works)

end