author | berghofe |
Fri, 16 Jul 1999 14:06:13 +0200 | |
changeset 7020 | 75ff179df7b7 |
parent 3268 | 012c43174664 |
child 8874 | 3242637f668c |
permissions | -rw-r--r-- |
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
1 |
(* Title: Subst/AList.ML |
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
2 |
ID: $Id$ |
1465 | 3 |
Author: Martin Coen, Cambridge University Computer Laboratory |
968 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
3268
012c43174664
Mostly cosmetic changes: updated headers, ID lines, etc.
paulson
parents:
3192
diff
changeset
|
6 |
Association lists. |
968 | 7 |
*) |
8 |
||
9 |
open AList; |
|
10 |
||
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
11 |
let fun prove s = prove_goalw AList.thy [alist_rec_def,assoc_def] s |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
12 |
(fn _ => [Simp_tac 1]) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
13 |
in |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
14 |
Addsimps |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
15 |
( |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
16 |
map prove |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
17 |
["alist_rec [] c d = c", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
18 |
"alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
19 |
"assoc v d [] = d", |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
20 |
"assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
21 |
) |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
22 |
end; |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
23 |
|
968 | 24 |
|
25 |
val prems = goal AList.thy |
|
26 |
"[| P([]); \ |
|
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
968
diff
changeset
|
27 |
\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; |
3192
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
28 |
by (induct_tac "l" 1); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
29 |
by (split_all_tac 2); |
a75558a4ed37
New version, modified by Konrad Slind and LCP for TFL
paulson
parents:
1465
diff
changeset
|
30 |
by (REPEAT (ares_tac prems 1)); |
968 | 31 |
qed "alist_induct"; |
32 |
||
33 |
(*Perform induction on xs. *) |
|
34 |
fun alist_ind_tac a M = |
|
35 |
EVERY [res_inst_tac [("l",a)] alist_induct M, |
|
1465 | 36 |
rename_last_tac a ["1"] (M+1)]; |