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"

lemma reverse_snoc: "reverse (snoc xs y) = y # reverse xs"
  by (induct xs) auto

theorem "reverse (reverse xs) = xs"
  by (induct xs) (auto simp add: reverse_snoc)


consts fold_right :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"


end

Template File

theory Submission
  imports Defs
begin

fun fold_right :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"  where
  "fold_right _ = undefined"

value "fold_right (+) [1,2,3] (4 :: nat) = 10"
value "fold_right (#) [a,b,c] [] = [a,b,c]"

lemma fold_map: "fold_right f (map g xs) a = fold_right (f o g) xs a"
  sorry

lemma fold_append: "fold_right f (xs @ ys) a = fold_right f xs (fold_right f ys a)"
  sorry

lemma fold_append_plus:
  "fold_right (+) (xs @ ys) (0 :: nat) = fold_right (+) xs 0 + fold_right (+) ys 0"
  sorry

theorem fold_add_reverse:
  "fold_right (+) (reverse xs) (x :: nat) = fold_right (+) xs x"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma fold_map: "fold_right f (map g xs) a = fold_right (f o g) xs a"
  by (rule Submission.fold_map)

lemma fold_append: "fold_right f (xs @ ys) a = fold_right f xs (fold_right f ys a)"
  by (rule Submission.fold_append)

lemma fold_append_plus: "fold_right (+) (xs @ ys) (0 :: nat) = fold_right (+) xs 0 + fold_right (+) ys 0"
  by (rule Submission.fold_append_plus)

theorem fold_add_reverse: "fold_right (+) (reverse xs) (x :: nat) = fold_right (+) xs x"
  by (rule Submission.fold_add_reverse)

end