author | clasohm |
Wed, 04 Oct 1995 13:12:14 +0100 | |
changeset 1266 | 3ae9fe3c0f68 |
parent 972 | e61b058d58d2 |
child 1465 | 5d7a7e439cec |
permissions | -rw-r--r-- |
968 | 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 |
|
1266 | 12 |
(fn _ => [Simp_tac 1]) |
968 | 13 |
in map mk_thm |
14 |
["alist_rec [] c d = c", |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
15 |
"alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)", |
968 | 16 |
"assoc v d [] = d", |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
17 |
"assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end; |
968 | 18 |
|
19 |
val prems = goal AList.thy |
|
20 |
"[| P([]); \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
21 |
\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; |
968 | 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)]; |