Homework 1

Definitions File

theory Defs
  imports Main
begin

fun snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" (*<*) where
  "snoc [] x = [x]" |
  "snoc (y # ys) x = y # (snoc ys x)" (*>*)

fun reverse :: "'a list \<Rightarrow> 'a list" where
  "reverse [] = []" |
  "reverse (x # xs) = snoc (reverse xs) x"


consts listsum :: "int list \<Rightarrow> int"

consts flatten :: "'a list list \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

fun listsum :: "int list \<Rightarrow> int"  where
  "listsum _ = undefined"

value "listsum [1,2,3] = 6"
value "listsum [] = 0"
value "listsum [1,-2,3] = 2"


lemma listsum_filter_z: "listsum (filter (\<lambda>x. x\<noteq>0) l) = listsum l"
  sorry

lemma listsum_rev: "listsum (rev xs) = listsum xs"
  sorry

fun flatten :: "'a list list \<Rightarrow> 'a list"  where
  "flatten _ = undefined"

value "flatten [[1,2,3],[2]] = [1,2,3,2::int]"
value "flatten [[1,2,3],[],[2]] = [1,2,3,2::int]"


lemma sum_flatten: "listsum (flatten xs) = listsum (map listsum xs)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma listsum_filter_z: "listsum (filter (\<lambda>x. x\<noteq>0) l) = listsum l"
  by (rule Submission.listsum_filter_z)

lemma listsum_rev: "listsum (rev xs) = listsum xs"
  by (rule Submission.listsum_rev)

lemma sum_flatten: "listsum (flatten xs) = listsum (map listsum xs)"
  by (rule Submission.sum_flatten)

end