1 (* Title: HOL/list |
1 (* Title: HOL/List.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Tobias Nipkow |
4 Copyright 1993 University of Cambridge |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 Definition of type 'a list by a least fixed point |
6 Definition of type 'a list as a datatype. This allows primrec to work. |
7 |
7 |
8 We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) |
|
9 and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) |
|
10 so that list can serve as a "functor" for defining other recursive types |
|
11 *) |
8 *) |
12 |
9 |
13 List = Sexp + |
10 List = Arith + |
14 |
11 |
15 types |
12 datatype 'a list = "[]" ("[]") | "#"('a,'a list) (infixr 65) |
16 'a list |
|
17 |
|
18 arities |
|
19 list :: (term) term |
|
20 |
|
21 |
13 |
22 consts |
14 consts |
23 |
15 |
24 list :: "'a item set => 'a item set" |
|
25 Rep_list :: "'a list => 'a item" |
|
26 Abs_list :: "'a item => 'a list" |
|
27 NIL :: "'a item" |
|
28 CONS :: "['a item, 'a item] => 'a item" |
|
29 Nil :: "'a list" |
|
30 "#" :: "['a, 'a list] => 'a list" (infixr 65) |
|
31 List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" |
|
32 List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" |
|
33 list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" |
|
34 list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" |
|
35 Rep_map :: "('b => 'a item) => ('b list => 'a item)" |
|
36 Abs_map :: "('a item => 'b) => 'a item => 'b list" |
|
37 null :: "'a list => bool" |
16 null :: "'a list => bool" |
38 hd :: "'a list => 'a" |
17 hd :: "'a list => 'a" |
39 tl,ttl :: "'a list => 'a list" |
18 tl,ttl :: "'a list => 'a list" |
40 mem :: "['a, 'a list] => bool" (infixl 55) |
19 mem :: "['a, 'a list] => bool" (infixl 55) |
41 list_all :: "('a => bool) => ('a list => bool)" |
20 list_all :: "('a => bool) => ('a list => bool)" |
42 map :: "('a=>'b) => ('a list => 'b list)" |
21 map :: "('a=>'b) => ('a list => 'b list)" |
43 "@" :: "['a list, 'a list] => 'a list" (infixr 65) |
22 "@" :: "['a list, 'a list] => 'a list" (infixr 65) |
44 filter :: "['a => bool, 'a list] => 'a list" |
23 filter :: "['a => bool, 'a list] => 'a list" |
|
24 foldl :: "[['b,'a] => 'b, 'b, 'a list] => 'b" |
|
25 length :: "'a list => nat" |
45 |
26 |
|
27 syntax |
46 (* list Enumeration *) |
28 (* list Enumeration *) |
47 |
29 "@list" :: "args => 'a list" ("[(_)]") |
48 "[]" :: "'a list" ("[]") |
|
49 "@list" :: "args => 'a list" ("[(_)]") |
|
50 |
30 |
51 (* Special syntax for list_all and filter *) |
31 (* Special syntax for list_all and filter *) |
52 "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) |
32 "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) |
53 "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])") |
33 "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])") |
54 |
34 |
55 translations |
35 translations |
56 "[x, xs]" == "x#[xs]" |
36 "[x, xs]" == "x#[xs]" |
57 "[x]" == "x#[]" |
37 "[x]" == "x#[]" |
58 "[]" == "Nil" |
|
59 |
|
60 "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys.b, xs)" |
|
61 |
38 |
62 "[x:xs . P]" == "filter(%x.P,xs)" |
39 "[x:xs . P]" == "filter(%x.P,xs)" |
63 "Alls x:xs.P" == "list_all(%x.P,xs)" |
40 "Alls x:xs.P" == "list_all(%x.P,xs)" |
64 |
41 |
65 defs |
42 primrec null list |
66 (* Defining the Concrete Constructors *) |
43 null_Nil "null([]) = True" |
67 NIL_def "NIL == In0(Numb(0))" |
44 null_Cons "null(x#xs) = False" |
68 CONS_def "CONS(M, N) == In1(M $ N)" |
45 primrec hd list |
69 |
46 hd_Nil "hd([]) = (@x.False)" |
70 inductive "list(A)" |
47 hd_Cons "hd(x#xs) = x" |
71 intrs |
48 primrec tl list |
72 NIL_I "NIL: list(A)" |
49 tl_Nil "tl([]) = (@x.False)" |
73 CONS_I "[| a: A; M: list(A) |] ==> CONS(a,M) : list(A)" |
50 tl_Cons "tl(x#xs) = xs" |
74 |
51 primrec ttl list |
75 rules |
52 (* a "total" version of tl: *) |
76 (* Faking a Type Definition ... *) |
53 ttl_Nil "ttl([]) = []" |
77 Rep_list "Rep_list(xs): list(range(Leaf))" |
54 ttl_Cons "ttl(x#xs) = xs" |
78 Rep_list_inverse "Abs_list(Rep_list(xs)) = xs" |
55 primrec "op mem" list |
79 Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M" |
56 mem_Nil "x mem [] = False" |
80 |
57 mem_Cons "x mem (y#ys) = if(y=x, True, x mem ys)" |
81 |
58 primrec list_all list |
82 defs |
59 list_all_Nil "list_all(P,[]) = True" |
83 (* Defining the Abstract Constructors *) |
60 list_all_Cons "list_all(P,x#xs) = (P(x) & list_all(P,xs))" |
84 Nil_def "Nil == Abs_list(NIL)" |
61 primrec map list |
85 Cons_def "x#xs == Abs_list(CONS(Leaf(x), Rep_list(xs)))" |
62 map_Nil "map(f,[]) = []" |
86 |
63 map_Cons "map(f,x#xs) = f(x)#map(f,xs)" |
87 List_case_def "List_case(c, d) == Case(%x.c, Split(d))" |
64 primrec "op @" list |
88 |
65 append_Nil "[] @ ys = ys" |
89 (* list Recursion -- the trancl is Essential; see list.ML *) |
66 append_Cons "(x#xs)@ys = x#(xs@ys)" |
90 |
67 primrec filter list |
91 List_rec_def |
68 filter_Nil "filter(P,[]) = []" |
92 "List_rec(M, c, d) == wfrec(trancl(pred_sexp), M, \ |
69 filter_Cons "filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs))" |
93 \ List_case(%g.c, %x y g. d(x, y, g(y))))" |
70 primrec foldl list |
94 |
71 foldl_Nil "foldl(f,a,[]) = a" |
95 list_rec_def |
72 foldl_Cons "foldl(f,a,x#xs) = foldl(f, f(a,x), xs)" |
96 "list_rec(l, c, d) == \ |
73 primrec length list |
97 \ List_rec(Rep_list(l), c, %x y r. d(Inv(Leaf, x), Abs_list(y), r))" |
74 length_Nil "length([]) = 0" |
98 |
75 length_Cons "length(x#xs) = Suc(length(xs))" |
99 (* Generalized Map Functionals *) |
|
100 |
|
101 Rep_map_def "Rep_map(f, xs) == list_rec(xs, NIL, %x l r. CONS(f(x), r))" |
|
102 Abs_map_def "Abs_map(g, M) == List_rec(M, Nil, %N L r. g(N)#r)" |
|
103 |
|
104 null_def "null(xs) == list_rec(xs, True, %x xs r.False)" |
|
105 hd_def "hd(xs) == list_rec(xs, @x.True, %x xs r.x)" |
|
106 tl_def "tl(xs) == list_rec(xs, @xs.True, %x xs r.xs)" |
|
107 (* a total version of tl: *) |
|
108 ttl_def "ttl(xs) == list_rec(xs, [], %x xs r.xs)" |
|
109 |
|
110 mem_def "x mem xs == \ |
|
111 \ list_rec(xs, False, %y ys r. if(y=x, True, r))" |
|
112 list_all_def "list_all(P, xs) == list_rec(xs, True, %x l r. P(x) & r)" |
|
113 map_def "map(f, xs) == list_rec(xs, [], %x l r. f(x)#r)" |
|
114 append_def "xs@ys == list_rec(xs, ys, %x l r. x#r)" |
|
115 filter_def "filter(P,xs) == \ |
|
116 \ list_rec(xs, [], %x xs r. if(P(x), x#r, r))" |
|
117 |
|
118 list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))" |
|
119 |
|
120 end |
76 end |