src/HOL/Subst/AList.thy
changeset 15635 8408a06590a6
parent 12406 c9775847ed66
child 24823 bfb619994060
     1.1 --- a/src/HOL/Subst/AList.thy	Mon Mar 28 16:19:56 2005 +0200
     1.2 +++ b/src/HOL/Subst/AList.thy	Tue Mar 29 12:30:48 2005 +0200
     1.3 @@ -1,12 +1,14 @@
     1.4 -(*  Title:      Subst/AList.thy
     1.5 -    ID:         $Id$
     1.6 +(*  ID:         $Id$
     1.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10 -Association lists.
    1.11  *)
    1.12  
    1.13 -AList = Main +
    1.14 +header{*Association Lists*}
    1.15 +
    1.16 +theory AList
    1.17 +imports Main
    1.18 +begin
    1.19  
    1.20  consts
    1.21    alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    1.22 @@ -20,4 +22,10 @@
    1.23    "assoc v d [] = d"
    1.24    "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    1.25  
    1.26 +
    1.27 +lemma alist_induct:
    1.28 +    "[| P([]);    
    1.29 +        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
    1.30 +by (induct_tac "l", auto)
    1.31 +
    1.32  end