theory Solution01 imports Main begin lemma "x + y = y + (x::nat)" apply auto done lemma "x + (y + z) = (x + y) + (z::nat)" apply auto done fun count :: "'a list \ 'a \ nat" where "count [] _ = 0" | "count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)" theorem "count xs x \ length xs" apply (induct xs) apply auto done 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" 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) fun repeat :: "nat \ 'a \ 'a list" where "repeat 0 a = []" | "repeat (Suc n) a = a # repeat n a" lemma "length (repeat n a) = n" by (induction n) auto lemma snoc_repeat: "snoc (repeat n a) a = a # repeat n a" by (induction n) auto lemma "reverse (repeat n a) = repeat n a" by (induction n) (auto simp add: snoc_repeat) end