theory Exercise01 imports Main begin (* definitions from the tutorial *) fun snoc :: "'a list \ 'a \ 'a list" where "snoc [] x = [x]" | "snoc (y # ys) x = y # (snoc ys x)" fun reverse :: "'a list \ 'a list" where "reverse [] = []" | "reverse (x # xs) = snoc (reverse xs) x" (* proofs from the tutorial that may be used in the proofs below *) 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) (* define repeat here *) consts repeat :: "nat \ 'a \ 'a list" (* prove properties below *) lemma "length (repeat n a) = n" sorry lemma "reverse (repeat n a) = repeat n a" sorry end