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 (induct xs) auto

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


consts repeat :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list"


end

Template File

theory Submission
  imports Defs
begin

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

value "repeat 5 (0::nat) = [0, 0, 0, 0, 0]"
value "repeat 3 (1::nat) = [1, 1, 1]"

theorem rep_len: "length (repeat n a) = n"
  sorry

theorem rep_rev: "reverse (repeat n a) = repeat n a"
  sorry

end

Check File

theory Check
  imports Submission
begin

theorem rep_len: "length (repeat n a) = n"
  by (rule Submission.rep_len)

theorem rep_rev: "reverse (repeat n a) = repeat n a"
  by (rule Submission.rep_rev)

end