src/HOL/ex/Seq.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 58889 5b7a9633cfa8
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Seq.thy
     2     Author:     Makarius
     3 *)
     4 
     5 section \<open>Finite sequences\<close>
     6 
     7 theory Seq
     8 imports Main
     9 begin
    10 
    11 datatype 'a seq = Empty | Seq 'a "'a seq"
    12 
    13 fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
    14 where
    15   "conc Empty ys = ys"
    16 | "conc (Seq x xs) ys = Seq x (conc xs ys)"
    17 
    18 fun reverse :: "'a seq \<Rightarrow> 'a seq"
    19 where
    20   "reverse Empty = Empty"
    21 | "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)"
    22 
    23 lemma conc_empty: "conc xs Empty = xs"
    24   by (induct xs) simp_all
    25 
    26 lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)"
    27   by (induct xs) simp_all
    28 
    29 lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)"
    30   by (induct xs) (simp_all add: conc_empty conc_assoc)
    31 
    32 lemma reverse_reverse: "reverse (reverse xs) = xs"
    33   by (induct xs) (simp_all add: reverse_conc)
    34 
    35 end