src/HOL/Subst/AList.thy
author berghofe
Mon May 15 17:32:39 2000 +0200 (2000-05-15)
changeset 8874 3242637f668c
parent 3842 b55686a7b22c
child 12406 c9775847ed66
permissions -rw-r--r--
alist_rec and assoc are now defined using primrec and thus no longer
refer to the recursion combinator list_rec, which should be considered
internal.
paulson@3268
     1
(*  Title:      Subst/AList.thy
paulson@3268
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
clasohm@968
     6
Association lists.
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
AList = List + 
clasohm@968
    10
clasohm@968
    11
consts
clasohm@968
    12
  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
clasohm@968
    13
  assoc      :: "['a,'b,('a*'b) list] => 'b"
clasohm@968
    14
berghofe@8874
    15
primrec
berghofe@8874
    16
  "alist_rec [] c d = c"
berghofe@8874
    17
  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
clasohm@968
    18
berghofe@8874
    19
primrec
berghofe@8874
    20
  "assoc v d [] = d"
berghofe@8874
    21
  "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
clasohm@968
    22
clasohm@968
    23
end