969
|
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 |
mem :: "['a, 'a list] => bool" (infixl 55)
|
|
41 |
list_all :: "('a => bool) => ('a list => bool)"
|
|
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 list_all and filter *)
|
|
52 |
"@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10)
|
|
53 |
"@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
|
|
54 |
|
|
55 |
translations
|
|
56 |
"[x, xs]" == "x#[xs]"
|
|
57 |
"[x]" == "x#[]"
|
|
58 |
"[]" == "Nil"
|
|
59 |
|
|
60 |
"case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
|
|
61 |
|
|
62 |
"[x:xs . P]" == "filter (%x.P) xs"
|
|
63 |
"Alls x:xs.P" == "list_all (%x.P) xs"
|
|
64 |
|
|
65 |
defs
|
|
66 |
(* Defining the Concrete Constructors *)
|
|
67 |
NIL_def "NIL == In0(Numb(0))"
|
|
68 |
CONS_def "CONS M N == In1(M $ N)"
|
|
69 |
|
|
70 |
inductive "list(A)"
|
|
71 |
intrs
|
|
72 |
NIL_I "NIL: list(A)"
|
|
73 |
CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)"
|
|
74 |
|
|
75 |
rules
|
|
76 |
(* Faking a Type Definition ... *)
|
|
77 |
Rep_list "Rep_list(xs): list(range(Leaf))"
|
|
78 |
Rep_list_inverse "Abs_list(Rep_list(xs)) = xs"
|
|
79 |
Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
|
|
80 |
|
|
81 |
|
|
82 |
defs
|
|
83 |
(* Defining the Abstract Constructors *)
|
|
84 |
Nil_def "Nil == Abs_list(NIL)"
|
|
85 |
Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
|
|
86 |
|
|
87 |
List_case_def "List_case c d == Case (%x.c) (Split d)"
|
|
88 |
|
|
89 |
(* list Recursion -- the trancl is Essential; see list.ML *)
|
|
90 |
|
|
91 |
List_rec_def
|
1151
|
92 |
"List_rec M c d == wfrec (trancl pred_sexp) M
|
|
93 |
(List_case (%g.c) (%x y g. d x y (g y)))"
|
969
|
94 |
|
|
95 |
list_rec_def
|
1151
|
96 |
"list_rec l c d ==
|
|
97 |
List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
|
969
|
98 |
|
|
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 |
|
1151
|
110 |
mem_def "x mem xs ==
|
|
111 |
list_rec xs False (%y ys r. if y=x then True else r)"
|
969
|
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)"
|
1151
|
115 |
filter_def "filter P xs ==
|
|
116 |
list_rec xs [] (%x xs r. if P(x) then x#r else r)"
|
969
|
117 |
|
|
118 |
list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
|
|
119 |
|
|
120 |
end
|