Homework 1

Definitions File

theory Defs
  imports Main
begin

text \<open>Definitions and lemmas from the tutorial\<close>

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"

lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs"
  by (induction xs) simp_all

theorem reverse_reverse: "reverse (reverse xs) = xs"
  by (induction xs) (simp_all add: reverse_snoc)


consts list_product :: "nat list \<Rightarrow> nat"

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


end

Template File

theory Submission
  imports Defs
begin

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

value "list_product [1, 2, 3, 4] = 24"
value "list_product [0, 5, 6, 7] = 0"

lemma list_product_filter_neq_1:
  "list_product (filter (\<lambda>x. x \<noteq> 1) xs) = list_product xs"
  sorry

lemma list_product_rev: "list_product (rev xs) = list_product 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 list_product_flatten: "list_product (flatten xss) = list_product (map list_product xss)"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma list_product_filter_neq_1: "list_product (filter (\<lambda>x. x \<noteq> 1) xs) = list_product xs"
  by (rule Submission.list_product_filter_neq_1)

lemma list_product_rev: "list_product (rev xs) = list_product xs"
  by (rule Submission.list_product_rev)

lemma list_product_flatten: "list_product (flatten xss) = list_product (map list_product xss)"
  by (rule Submission.list_product_flatten)

end