src/HOL/Subst/AList.thy
author paulson
Tue Mar 29 12:30:48 2005 +0200 (2005-03-29)
changeset 15635 8408a06590a6
parent 12406 c9775847ed66
child 24823 bfb619994060
permissions -rw-r--r--
converted HOL-Subst to tactic scripts
     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
    14   alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    15   assoc      :: "['a,'b,('a*'b) list] => 'b"
    16 
    17 primrec
    18   "alist_rec [] c d = c"
    19   "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    20 
    21 primrec
    22   "assoc v d [] = d"
    23   "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    24 
    25 
    26 lemma alist_induct:
    27     "[| P([]);    
    28         !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
    29 by (induct_tac "l", auto)
    30 
    31 end