finite sequences as useful as introductory example;

--- a/src/HOL/IsaMakefile	Sun Sep 18 12:48:45 2011 +0200
+++ b/src/HOL/IsaMakefile	Sun Sep 18 13:39:33 2011 +0200
@@ -1041,18 +1041,19 @@
   ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
   ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
   ex/Iff_Oracle.thy ex/Induction_Schema.thy				\
-  ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy	\
-  ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy		\
-  ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy	\
-  ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
-  ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
-  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
+  ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy			\
+  ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy		\
+  ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\
+  ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy			\
+  ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy		\
+  ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
+  ex/Quickcheck_Lattice_Examples.thy					\
   ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML	\
   ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
   ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy			\
   ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML	\
-  ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy		\
-  ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy			\
+  ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
+  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
   ex/Unification.thy ex/While_Combinator_Example.thy			\
   ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML		\
   ex/svc_test.thy ../Tools/interpretation_with_defs.ML

--- a/src/HOL/ex/ROOT.ML	Sun Sep 18 12:48:45 2011 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Sep 18 13:39:33 2011 +0200
@@ -71,7 +71,8 @@
   "Quicksort",
   "Birthday_Paradox",
   "List_to_Set_Comprehension_Examples",
-  "Set_Algebras"
+  "Set_Algebras",
+  "Seq"
 ];
 
 if getenv "ISABELLE_GHC" = "" then ()

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Seq.thy	Sun Sep 18 13:39:33 2011 +0200
@@ -0,0 +1,35 @@
+(*  Title:      HOL/ex/Seq.thy
+    Author:     Makarius
+*)
+
+header {* Finite sequences *}
+
+theory Seq
+imports Main
+begin
+
+datatype 'a seq = Empty | Seq 'a "'a seq"
+
+fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
+where
+  "conc Empty ys = ys"
+| "conc (Seq x xs) ys = Seq x (conc xs ys)"
+
+fun reverse :: "'a seq \<Rightarrow> 'a seq"
+where
+  "reverse Empty = Empty"
+| "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)"
+
+lemma conc_empty: "conc xs Empty = xs"
+  by (induct xs) simp_all
+
+lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)"
+  by (induct xs) simp_all
+
+lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)"
+  by (induct xs) (simp_all add: conc_empty conc_assoc)
+
+lemma reverse_reverse: "reverse (reverse xs) = xs"
+  by (induct xs) (simp_all add: reverse_conc)
+
+end