src/HOL/Subst/AList.thy
author hoelzl
Tue Jan 18 21:37:23 2011 +0100 (2011-01-18)
changeset 41654 32fe42892983
parent 38140 05691ad74079
child 44367 74c08021ab2e
permissions -rw-r--r--
Gauge measure removed
     1 (*  Title:      HOL/Subst/AList.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 *)
     5 
     6 header {* Association Lists *}
     7 
     8 theory AList
     9 imports Main
    10 begin
    11 
    12 primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    13 where
    14   "alist_rec [] c d = c"
    15 | "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
    16 
    17 primrec assoc :: "['a,'b,('a*'b) list] => 'b"
    18 where
    19   "assoc v d [] = d"
    20 | "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    21 
    22 lemma alist_induct:
    23     "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
    24   by (induct l) auto
    25 
    26 end