author | nipkow |
Wed, 20 Nov 1996 10:32:58 +0100 | |
changeset 2212 | bd705e9de196 |
parent 1476 | 608483c2122a |
child 3192 | a75558a4ed37 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: Substitutions/alist.thy |
2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
|
968 | 3 |
Copyright 1993 University of Cambridge |
4 |
||
5 |
Association lists. |
|
6 |
*) |
|
7 |
||
8 |
AList = List + |
|
9 |
||
10 |
consts |
|
11 |
||
12 |
alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" |
|
13 |
assoc :: "['a,'b,('a*'b) list] => 'b" |
|
14 |
||
15 |
rules |
|
16 |
||
17 |
alist_rec_def "alist_rec al b c == list_rec b (split c) al" |
|
18 |
||
19 |
assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)" |
|
20 |
||
21 |
end |