author | wenzelm |
Tue, 21 Nov 2000 19:03:27 +0100 | |
changeset 10506 | 01333dbe1431 |
parent 6382 | 8b0c9205da75 |
child 11481 | c77e5401f2ff |
permissions | -rw-r--r-- |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/SList.thy |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
5 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
6 |
Definition of type 'a list (strict lists) by a least fixed point |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
7 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
8 |
We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
9 |
and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
10 |
so that list can serve as a "functor" for defining other recursive types |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
11 |
*) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
12 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
13 |
SList = Sexp + |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
14 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
15 |
consts |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
16 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
17 |
list :: 'a item set => 'a item set |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
18 |
NIL :: 'a item |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
19 |
CONS :: ['a item, 'a item] => 'a item |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
20 |
List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
21 |
List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
22 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
23 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
24 |
defs |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
25 |
(* Defining the Concrete Constructors *) |
5191
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3842
diff
changeset
|
26 |
NIL_def "NIL == In0 (Numb 0)" |
8ceaa19f7717
Renamed '$' to 'Scons' because of clashes with constants of the same
berghofe
parents:
3842
diff
changeset
|
27 |
CONS_def "CONS M N == In1 (Scons M N)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
28 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
29 |
inductive "list(A)" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
30 |
intrs |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
31 |
NIL_I "NIL: list(A)" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
32 |
CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
33 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
34 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
35 |
typedef (List) |
6382 | 36 |
'a list = "list(range Leaf) :: 'a item set" (list.NIL_I) |
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
37 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
38 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
39 |
(*Declaring the abstract list constructors*) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
40 |
consts |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
41 |
Nil :: 'a list |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
42 |
"#" :: ['a, 'a list] => 'a list (infixr 65) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
43 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
44 |
(* list Enumeration *) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
45 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
46 |
"[]" :: 'a list ("[]") |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
47 |
"@list" :: args => 'a list ("[(_)]") |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
48 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
49 |
(* Special syntax for filter *) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
50 |
"@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])") |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
51 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
52 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
53 |
translations |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
54 |
"[x, xs]" == "x#[xs]" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
55 |
"[x]" == "x#[]" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
56 |
"[]" == "Nil" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
57 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
58 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
59 |
defs |
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
60 |
Nil_def "Nil == Abs_List NIL" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
61 |
Cons_def "x#xs == Abs_List(CONS (Leaf x) (Rep_List xs))" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
62 |
|
3842 | 63 |
List_case_def "List_case c d == Case (%x. c) (Split d)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
64 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
65 |
(* list Recursion -- the trancl is Essential; see list.ML *) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
66 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
67 |
List_rec_def |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
68 |
"List_rec M c d == wfrec (trancl pred_sexp) |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
69 |
(%g. List_case c (%x y. d x y (g y))) M" |
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
70 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
71 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
72 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
73 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
74 |
constdefs |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
75 |
(* Generalized Map Functionals *) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
76 |
Rep_map :: ('b => 'a item) => ('b list => 'a item) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
77 |
"Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
78 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
79 |
Abs_map :: ('a item => 'b) => 'a item => 'b list |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
80 |
"Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
81 |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
82 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
83 |
list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
84 |
"list_rec l c d == |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
85 |
List_rec (Rep_List l) c (%x y r. d (inv Leaf x) (Abs_List y) r)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
86 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
87 |
null :: 'a list => bool |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
88 |
"null(xs) == list_rec xs True (%x xs r. False)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
89 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
90 |
hd :: 'a list => 'a |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
91 |
"hd(xs) == list_rec xs arbitrary (%x xs r. x)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
92 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
93 |
tl :: 'a list => 'a list |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
94 |
"tl(xs) == list_rec xs arbitrary (%x xs r. xs)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
95 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
96 |
(* a total version of tl *) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
97 |
ttl :: 'a list => 'a list |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
98 |
"ttl(xs) == list_rec xs [] (%x xs r. xs)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
99 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
100 |
set :: ('a list => 'a set) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
101 |
"set xs == list_rec xs {} (%x l r. insert x r)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
102 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
103 |
mem :: ['a, 'a list] => bool (infixl 55) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
104 |
"x mem xs == list_rec xs False (%y ys r. if y=x then True else r)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
105 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
106 |
map :: ('a=>'b) => ('a list => 'b list) |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
107 |
"map f xs == list_rec xs [] (%x l r. f(x)#r)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
108 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
109 |
filter :: ['a => bool, 'a list] => 'a list |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
110 |
"filter P xs == list_rec xs [] (%x xs r. if P(x) then x#r else r)" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
111 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
112 |
list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
113 |
"list_case a f xs == list_rec xs a (%x xs r. f x xs)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
114 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
115 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
116 |
consts |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
117 |
"@" :: ['a list, 'a list] => 'a list (infixr 65) |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
118 |
|
5977
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
119 |
defs |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
120 |
append_def "xs@ys == list_rec xs ys (%x l r. x#r)" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
121 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
122 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
123 |
translations |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
124 |
"case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs" |
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
125 |
|
9f0c8869cf71
tidied up list definitions, using type 'a option instead of
paulson
parents:
5191
diff
changeset
|
126 |
"[x:xs . P]" == "filter (%x. P) xs" |
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
127 |
|
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
128 |
end |