|
2113
|
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 |
|
|
|
20 |
val prems = goal AList.thy
|
|
|
21 |
"[| P([]); \
|
|
|
22 |
\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)";
|
|
|
23 |
by (list.induct_tac "l" 1);
|
|
|
24 |
by (resolve_tac prems 1);
|
|
|
25 |
by (rtac PairE 1);
|
|
|
26 |
by (etac ssubst 1);
|
|
|
27 |
by (resolve_tac prems 1);
|
|
|
28 |
by (assume_tac 1);
|
|
|
29 |
qed "alist_induct";
|
|
|
30 |
|
|
|
31 |
(*Perform induction on xs. *)
|
|
|
32 |
fun alist_ind_tac a M =
|
|
|
33 |
EVERY [res_inst_tac [("l",a)] alist_induct M,
|
|
|
34 |
rename_last_tac a ["1"] (M+1)];
|