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
```     1 (*  Title:      Substitutions/AList.ML
```
```     2     Author:     Martin Coen, Cambridge University Computer Laboratory
```
```     3     Copyright   1993  University of Cambridge
```
```     4
```
```     5 For AList.thy.
```
```     6 *)
```
```     7
```
```     8 open AList;
```
```     9
```
```    10 val al_rews =
```
```    11   let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s
```
```    12                             (fn _ => [Simp_tac 1])
```
```    13   in map mk_thm
```
```    14      ["alist_rec [] c d = c",
```
```    15       "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)",
```
```    16       "assoc v d [] = d",
```
```    17       "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end;
```
```    18
```
```    19 val prems = goal AList.thy
```
```    20     "[| P([]);   \
```
```    21 \       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
```
```    22 by (list.induct_tac "l" 1);
```
```    23 by (resolve_tac prems 1);
```
```    24 by (rtac PairE 1);
```
```    25 by (etac ssubst 1);
```
```    26 by (resolve_tac prems 1);
```
```    27 by (assume_tac 1);
```
```    28 qed "alist_induct";
```
```    29
```
```    30 (*Perform induction on xs. *)
```
```    31 fun alist_ind_tac a M =
```
```    32     EVERY [res_inst_tac [("l",a)] alist_induct M,
```
```    33            rename_last_tac a ["1"] (M+1)];
```