src/HOL/ex/Seq.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
permissions -rw-r--r--
prefer symbols;
     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