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
wenzelm@38140
     1
(*  Title:      HOL/Subst/AList.thy
clasohm@1476
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
*)
clasohm@968
     5
wenzelm@38140
     6
header {* Association Lists *}
paulson@15635
     7
paulson@15635
     8
theory AList
paulson@15635
     9
imports Main
paulson@15635
    10
begin
clasohm@968
    11
wenzelm@38140
    12
primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
wenzelm@38140
    13
where
berghofe@8874
    14
  "alist_rec [] c d = c"
wenzelm@38140
    15
| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
clasohm@968
    16
wenzelm@38140
    17
primrec assoc :: "['a,'b,('a*'b) list] => 'b"
wenzelm@38140
    18
where
berghofe@8874
    19
  "assoc v d [] = d"
wenzelm@38140
    20
| "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
clasohm@968
    21
paulson@15635
    22
lemma alist_induct:
wenzelm@38140
    23
    "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
wenzelm@24823
    24
  by (induct l) auto
paulson@15635
    25
clasohm@968
    26
end