theory Demo
imports PreList
begin

text {*
 Note: to avoid name clashes with the existing type of lists we build
 on top of PreList rather than Main. This is an exception!
*}

datatype 'a list = Nil | Cons 'a "'a list"

consts
  app :: "'a list => 'a list => 'a list"
  rev :: "'a list => 'a list"

primrec
  "app Nil ys = ys"
  "app (Cons x xs) ys = Cons x (app xs ys)"

primrec
  "rev Nil = Nil"
  "rev (Cons x xs) = app (rev xs) (Cons x Nil)"


text {*
  Simple proofs:

  Command 'lemma' / 'theorem': state a proposition
  Attribute 'simp': use this theorem as a simplification rule in future proofs
  Method 'induct': structural induction
  Method 'auto':  automatic proof (mostly by simplification)
  Command 'done':  end of proof
*}

lemma [simp]: "app xs Nil = xs"
  apply (induct xs)
  apply auto
  done

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

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

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

(* Hint for demo:
   do the proof top down, discovering the lemmas one by one,
   as described in LNCS2283.
*)

end