|
1 (* Title: HOL/List.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Definition of type 'a list as a datatype. This allows primrec to work. |
|
7 |
|
8 *) |
|
9 |
|
10 List = Arith + |
|
11 |
|
12 datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65) |
|
13 |
|
14 consts |
|
15 |
|
16 null :: "'a list => bool" |
|
17 hd :: "'a list => 'a" |
|
18 tl,ttl :: "'a list => 'a list" |
|
19 mem :: "['a, 'a list] => bool" (infixl 55) |
|
20 list_all :: "('a => bool) => ('a list => bool)" |
|
21 map :: "('a=>'b) => ('a list => 'b list)" |
|
22 "@" :: "['a list, 'a list] => 'a list" (infixr 65) |
|
23 filter :: "['a => bool, 'a list] => 'a list" |
|
24 foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" |
|
25 length :: "'a list => nat" |
|
26 flat :: "'a list list => 'a list" |
|
27 nth :: "[nat, 'a list] => 'a" |
|
28 |
|
29 syntax |
|
30 (* list Enumeration *) |
|
31 "@list" :: "args => 'a list" ("[(_)]") |
|
32 |
|
33 (* Special syntax for list_all and filter *) |
|
34 "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) |
|
35 "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])") |
|
36 |
|
37 translations |
|
38 "[x, xs]" == "x#[xs]" |
|
39 "[x]" == "x#[]" |
|
40 |
|
41 "[x:xs . P]" == "filter (%x.P) xs" |
|
42 "Alls x:xs.P" == "list_all (%x.P) xs" |
|
43 |
|
44 primrec null list |
|
45 null_Nil "null([]) = True" |
|
46 null_Cons "null(x#xs) = False" |
|
47 primrec hd list |
|
48 hd_Nil "hd([]) = (@x.False)" |
|
49 hd_Cons "hd(x#xs) = x" |
|
50 primrec tl list |
|
51 tl_Nil "tl([]) = (@x.False)" |
|
52 tl_Cons "tl(x#xs) = xs" |
|
53 primrec ttl list |
|
54 (* a "total" version of tl: *) |
|
55 ttl_Nil "ttl([]) = []" |
|
56 ttl_Cons "ttl(x#xs) = xs" |
|
57 primrec "op mem" list |
|
58 mem_Nil "x mem [] = False" |
|
59 mem_Cons "x mem (y#ys) = if (y=x) True (x mem ys)" |
|
60 primrec list_all list |
|
61 list_all_Nil "list_all P [] = True" |
|
62 list_all_Cons "list_all P (x#xs) = (P(x) & list_all P xs)" |
|
63 primrec map list |
|
64 map_Nil "map f [] = []" |
|
65 map_Cons "map f (x#xs) = f(x)#map f xs" |
|
66 primrec "op @" list |
|
67 append_Nil "[] @ ys = ys" |
|
68 append_Cons "(x#xs)@ys = x#(xs@ys)" |
|
69 primrec filter list |
|
70 filter_Nil "filter P [] = []" |
|
71 filter_Cons "filter P (x#xs) = if (P x) (x#filter P xs) (filter P xs)" |
|
72 primrec foldl list |
|
73 foldl_Nil "foldl f a [] = a" |
|
74 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
|
75 primrec length list |
|
76 length_Nil "length([]) = 0" |
|
77 length_Cons "length(x#xs) = Suc(length(xs))" |
|
78 primrec flat list |
|
79 flat_Nil "flat([]) = []" |
|
80 flat_Cons "flat(x#xs) = x @ flat(xs)" |
|
81 defs |
|
82 nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))" |
|
83 end |