theory ToyList
imports PreList
begin

  datatype 'a list = Nil                         ("[]")
                   | Cons 'a "'a list"           (infixr "#" 65)

  consts app :: "'a list => 'a list => 'a list"  (infixr "@" 65)
         rev :: "'a list => 'a list"
         revH :: "'a list => 'a list => 'a list"

  primrec
  "[] @ xs = xs"
  "(x # xs) @ ys = x # (xs @ ys)"

  primrec
  "rev [] = []"
  "rev (x # xs) = (rev xs) @ (x # [])"

  primrec
  "revH [] ys = ys"
  "revH (x # xs) ys = revH xs (x # ys)"

lemma app_Nil2 [simp]: "xs @ [] = xs"
apply(induct_tac xs)
apply(auto)
done

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

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

lemma rev_rev [simp]: "rev (rev xs) = xs"
apply(induct_tac xs)
apply(auto)
done

lemma rev_revH: "ALL ys. revH xs ys = rev xs @ ys"
apply(induct_tac xs)
apply(auto)
done

lemma rev_rev2: "rev xs = revH xs []"
apply(simp add: rev_revH)
done