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