src/HOL/Subst/AList.ML
author clasohm
Wed Mar 13 11:55:25 1996 +0100 (1996-03-13 ago)
changeset 1574 5a63ab90ee8a
parent 1465 5d7a7e439cec
child 3192 a75558a4ed37
permissions -rw-r--r--
modified primrec so it can be used in MiniML/Type.thy
clasohm@1465
     1
(*  Title:      Substitutions/AList.ML
clasohm@1465
     2
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@968
     3
    Copyright   1993  University of Cambridge
clasohm@968
     4
clasohm@968
     5
For AList.thy.
clasohm@968
     6
*)
clasohm@968
     7
clasohm@968
     8
open AList;
clasohm@968
     9
clasohm@968
    10
val al_rews = 
clasohm@968
    11
  let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
clasohm@1266
    12
                            (fn _ => [Simp_tac 1])
clasohm@968
    13
  in map mk_thm 
clasohm@968
    14
     ["alist_rec [] c d = c",
clasohm@972
    15
      "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
clasohm@968
    16
      "assoc v d [] = d",
clasohm@972
    17
      "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end;
clasohm@968
    18
clasohm@968
    19
val prems = goal AList.thy
clasohm@968
    20
    "[| P([]);   \
clasohm@972
    21
\       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
clasohm@968
    22
by (list.induct_tac "l" 1);
clasohm@968
    23
by (resolve_tac prems 1);
clasohm@968
    24
by (rtac PairE 1);
clasohm@968
    25
by (etac ssubst 1);
clasohm@968
    26
by (resolve_tac prems 1);
clasohm@968
    27
by (assume_tac 1);
clasohm@968
    28
qed "alist_induct";
clasohm@968
    29
clasohm@968
    30
(*Perform induction on xs. *)
clasohm@968
    31
fun alist_ind_tac a M = 
clasohm@968
    32
    EVERY [res_inst_tac [("l",a)] alist_induct M,
clasohm@1465
    33
           rename_last_tac a ["1"] (M+1)];