|
0
|
1 |
(* Title: Substitutions/alist.thy
|
|
|
2 |
Author: Martin Coen, Cambridge University Computer Laboratory
|
|
|
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
|
|
|
18 |
"alist_rec(al,b,c) == list_rec(al,b,%p xs g.split(p,%x y.c(x,y,xs,g)))"
|
|
|
19 |
|
|
|
20 |
assoc_def "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))"
|
|
|
21 |
|
|
|
22 |
end
|