theory List_Demo imports Main begin datatype 'a lst = N | C "'a" "'a lst" fun app :: "'a lst \ 'a lst \ 'a lst" where "app N ys = ys" | "app (C x xs) ys = C x (app xs ys)" fun rvs :: "'a lst \ 'a lst" where "rvs N = N" | "rvs (C x xs) = app (rvs xs) (C x N)" value "rvs(C True (C False N))" value "rvs(C a (C b N))" lemma app_Nil2[simp]: "app xs N = xs" apply (induct xs) apply auto done lemma app_assoc[simp]: "app (app xs ys) zs = app xs (app ys zs)" apply (induct xs) apply auto done lemma rvs_app[simp]: "rvs (app xs ys) = app (rvs ys) (rvs xs)" apply (induct xs) apply auto done theorem rvs_rvs[simp]: "rvs (rvs xs) = xs" apply (induct xs) apply auto done (* Hint for demo: do the proof top down, discovering the lemmas one by one, *) end