src/HOL/Subst/AList.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 12406 c9775847ed66
child 15635 8408a06590a6
permissions -rw-r--r--
import -> imports
     1 (*  Title:      Subst/AList.thy
     2     ID:         $Id$
     3     Author:     Martin Coen, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Association lists.
     7 *)
     8 
     9 AList = Main +
    10 
    11 consts
    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 primrec
    16   "alist_rec [] c d = c"
    17   "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    18 
    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 end