src/HOL/Subst/AList.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 9747 043098ba5098
permissions -rw-r--r--
import -> imports
paulson@3268
     1
(*  Title:      Subst/AList.ML
paulson@3268
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     4
    Copyright   1993  University of Cambridge
clasohm@968
     5
paulson@3268
     6
Association lists.
clasohm@968
     7
*)
clasohm@968
     8
clasohm@968
     9
open AList;
clasohm@968
    10
clasohm@968
    11
val prems = goal AList.thy
clasohm@968
    12
    "[| P([]);   \
clasohm@972
    13
\       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
paulson@3192
    14
by (induct_tac "l" 1);
paulson@3192
    15
by (split_all_tac 2);
paulson@3192
    16
by (REPEAT (ares_tac prems 1));
clasohm@968
    17
qed "alist_induct";
clasohm@968
    18
clasohm@968
    19
(*Perform induction on xs. *)
clasohm@968
    20
fun alist_ind_tac a M = 
nipkow@9747
    21
    EVERY [induct_thm_tac alist_induct a M,
clasohm@1465
    22
           rename_last_tac a ["1"] (M+1)];