Toylist

theory Toylist
imports Main
begin
declare [[names_short]]
no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)

fun app::"'a list ⇒ 'a list ⇒ 'a list" (infixr "@" 65)
where
"[] @ ys = ys"|"(x # xs) @ ys = x # (xs @ ys)"

fun rev::"'a list ⇒ 'a list"
where
"rev [] = []"|"rev (x # xs) = rev xs @ x # []"

lemma rev1[simp]:"xs @ [] = xs"
apply(induct xs)
apply(auto)
done

lemma rev2[simp]:"xs @ ys @ zs = (xs @ ys) @ zs"
apply(induct xs)
apply(auto)
done

lemma rev3[simp]:"rev(xs @ ys) = rev ys @ rev xs"
apply(induct xs)
apply(auto)
done

theorem rev_twice:"rev(rev xs) = xs"
apply(induct xs)
apply(auto)
done
end