src/HOL/Subst/AList.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 24823 bfb619994060
child 38140 05691ad74079
permissions -rw-r--r--
simplified method setup;
     1 (*  ID:         $Id$
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 *)
     6 
     7 header{*Association Lists*}
     8 
     9 theory AList
    10 imports Main
    11 begin
    12 
    13 consts alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    14 primrec
    15   "alist_rec [] c d = c"
    16   "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    17 
    18 consts assoc      :: "['a,'b,('a*'b) list] => 'b"
    19 primrec
    20   "assoc v d [] = d"
    21   "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    22 
    23 lemma alist_induct:
    24     "[| P([]);    
    25         !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
    26   by (induct l) auto
    27 
    28 end