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