src/HOL/Subst/AList.thy
author wenzelm
Wed Oct 03 19:36:05 2007 +0200 (2007-10-03)
changeset 24823 bfb619994060
parent 15635 8408a06590a6
child 38140 05691ad74079
permissions -rw-r--r--
modernized specifications;
tuned proofs;
paulson@15635
     1
(*  ID:         $Id$
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
*)
clasohm@968
     6
paulson@15635
     7
header{*Association Lists*}
paulson@15635
     8
paulson@15635
     9
theory AList
paulson@15635
    10
imports Main
paulson@15635
    11
begin
clasohm@968
    12
wenzelm@24823
    13
consts alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
berghofe@8874
    14
primrec
berghofe@8874
    15
  "alist_rec [] c d = c"
berghofe@8874
    16
  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
clasohm@968
    17
wenzelm@24823
    18
consts assoc      :: "['a,'b,('a*'b) list] => 'b"
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
paulson@15635
    23
lemma alist_induct:
paulson@15635
    24
    "[| P([]);    
paulson@15635
    25
        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
wenzelm@24823
    26
  by (induct l) auto
paulson@15635
    27
clasohm@968
    28
end