1 (* Title: HOL/ex/SList.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Definition of type 'a list (strict lists) by a least fixed point |
|
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 *) |
|
12 |
|
13 SList = Sexp + |
|
14 |
|
15 types |
|
16 'a list |
|
17 |
|
18 arities |
|
19 list :: (term) term |
|
20 |
|
21 |
|
22 consts |
|
23 |
|
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 |
|
38 hd :: 'a list => 'a |
|
39 tl,ttl :: 'a list => 'a list |
|
40 set_of_list :: ('a list => 'a set) |
|
41 mem :: ['a, 'a list] => bool (infixl 55) |
|
42 map :: ('a=>'b) => ('a list => 'b list) |
|
43 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
|
44 filter :: ['a => bool, 'a list] => 'a list |
|
45 |
|
46 (* list Enumeration *) |
|
47 |
|
48 "[]" :: 'a list ("[]") |
|
49 "@list" :: args => 'a list ("[(_)]") |
|
50 |
|
51 (* Special syntax for filter *) |
|
52 "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])") |
|
53 |
|
54 translations |
|
55 "[x, xs]" == "x#[xs]" |
|
56 "[x]" == "x#[]" |
|
57 "[]" == "Nil" |
|
58 |
|
59 "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs" |
|
60 |
|
61 "[x:xs . P]" == "filter (%x.P) xs" |
|
62 |
|
63 defs |
|
64 (* Defining the Concrete Constructors *) |
|
65 NIL_def "NIL == In0(Numb(0))" |
|
66 CONS_def "CONS M N == In1(M $ N)" |
|
67 |
|
68 inductive "list(A)" |
|
69 intrs |
|
70 NIL_I "NIL: list(A)" |
|
71 CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)" |
|
72 |
|
73 rules |
|
74 (* Faking a Type Definition ... *) |
|
75 Rep_list "Rep_list(xs): list(range(Leaf))" |
|
76 Rep_list_inverse "Abs_list(Rep_list(xs)) = xs" |
|
77 Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M" |
|
78 |
|
79 |
|
80 defs |
|
81 (* Defining the Abstract Constructors *) |
|
82 Nil_def "Nil == Abs_list(NIL)" |
|
83 Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))" |
|
84 |
|
85 List_case_def "List_case c d == Case (%x.c) (Split d)" |
|
86 |
|
87 (* list Recursion -- the trancl is Essential; see list.ML *) |
|
88 |
|
89 List_rec_def |
|
90 "List_rec M c d == wfrec (trancl pred_sexp) |
|
91 (%g. List_case c (%x y. d x y (g y))) M" |
|
92 |
|
93 list_rec_def |
|
94 "list_rec l c d == |
|
95 List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)" |
|
96 |
|
97 (* Generalized Map Functionals *) |
|
98 |
|
99 Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" |
|
100 Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" |
|
101 |
|
102 null_def "null(xs) == list_rec xs True (%x xs r.False)" |
|
103 hd_def "hd(xs) == list_rec xs (@x.True) (%x xs r.x)" |
|
104 tl_def "tl(xs) == list_rec xs (@xs.True) (%x xs r.xs)" |
|
105 (* a total version of tl: *) |
|
106 ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)" |
|
107 |
|
108 set_of_list_def "set_of_list xs == list_rec xs {} (%x l r. insert x r)" |
|
109 |
|
110 mem_def "x mem xs == |
|
111 list_rec xs False (%y ys r. if y=x then True else r)" |
|
112 map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" |
|
113 append_def "xs@ys == list_rec xs ys (%x l r. x#r)" |
|
114 filter_def "filter P xs == |
|
115 list_rec xs [] (%x xs r. if P(x) then x#r else r)" |
|
116 |
|
117 list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)" |
|
118 |
|
119 end |
|