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
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
clasohm@968
    13
consts
clasohm@968
    14
  alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
clasohm@968
    15
  assoc      :: "['a,'b,('a*'b) list] => 'b"
clasohm@968
    16
berghofe@8874
    17
primrec
berghofe@8874
    18
  "alist_rec [] c d = c"
berghofe@8874
    19
  "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
clasohm@968
    20
berghofe@8874
    21
primrec
berghofe@8874
    22
  "assoc v d [] = d"
berghofe@8874
    23
  "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
clasohm@968
    24
paulson@15635
    25
paulson@15635
    26
lemma alist_induct:
paulson@15635
    27
    "[| P([]);    
paulson@15635
    28
        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
paulson@15635
    29
by (induct_tac "l", auto)
paulson@15635
    30
clasohm@968
    31
end