equal
deleted
inserted
replaced
1 (* Title: HOL/Subst/AList.thy |
|
2 Author: Martin Coen, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 *) |
|
5 |
|
6 header {* Association Lists *} |
|
7 |
|
8 theory AList |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" |
|
13 where |
|
14 "alist_rec [] c d = c" |
|
15 | "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)" |
|
16 |
|
17 primrec assoc :: "['a,'b,('a*'b) list] => 'b" |
|
18 where |
|
19 "assoc v d [] = d" |
|
20 | "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)" |
|
21 |
|
22 lemma alist_induct: |
|
23 "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l" |
|
24 by (induct l) auto |
|
25 |
|
26 |
|
27 |
|
28 end |
|