author | haftmann |
Tue, 10 Jul 2007 17:30:50 +0200 | |
changeset 23709 | fd31da8f752a |
parent 15635 | 8408a06590a6 |
child 24823 | bfb619994060 |
permissions | -rw-r--r-- |
15635 | 1 |
(* ID: $Id$ |
1476 | 2 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 3 |
Copyright 1993 University of Cambridge |
4 |
||
5 |
*) |
|
6 |
||
15635 | 7 |
header{*Association Lists*} |
8 |
||
9 |
theory AList |
|
10 |
imports Main |
|
11 |
begin |
|
968 | 12 |
|
13 |
consts |
|
14 |
alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" |
|
15 |
assoc :: "['a,'b,('a*'b) list] => 'b" |
|
16 |
||
8874
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
17 |
primrec |
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
18 |
"alist_rec [] c d = c" |
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
19 |
"alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)" |
968 | 20 |
|
8874
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
21 |
primrec |
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
22 |
"assoc v d [] = d" |
3242637f668c
alist_rec and assoc are now defined using primrec and thus no longer
berghofe
parents:
3842
diff
changeset
|
23 |
"assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)" |
968 | 24 |
|
15635 | 25 |
|
26 |
lemma alist_induct: |
|
27 |
"[| P([]); |
|
28 |
!!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)" |
|
29 |
by (induct_tac "l", auto) |
|
30 |
||
968 | 31 |
end |