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