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
```