2570
|
1 |
(* Title: HOLCF/Dlist.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Franz Regensburger
|
|
4 |
Copyright 1993 Technische Universitaet Muenchen
|
|
5 |
|
|
6 |
Theory for finite lists 'a dlist = one ++ ('a ** 'a dlist)
|
|
7 |
*)
|
|
8 |
|
|
9 |
Dlist = Classlib +
|
|
10 |
|
|
11 |
domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
|
|
12 |
|
|
13 |
ops curried
|
|
14 |
|
|
15 |
lmap :: "('a -> 'b) -> 'a dlist -> 'b dlist"
|
|
16 |
lmem :: "('a::eq) -> 'a dlist -> tr" (cinfixl 50)
|
|
17 |
|
|
18 |
defs
|
|
19 |
|
|
20 |
lmap_def " lmap Ú fix`(LAM h f s. case s of dnil => dnil
|
|
21 |
| x ## xs => f`x ## h`f`xs)"
|
|
22 |
|
|
23 |
lmem_def "op lmem Ú fix`(LAM h e l. case l of dnil => FF
|
|
24 |
| x ## xs => If e Ù x then TT else h`e`xs fi)"
|
|
25 |
|
|
26 |
end
|
|
27 |
|