| author | wenzelm |
| Mon, 03 Nov 1997 12:13:18 +0100 | |
| changeset 4089 | 96fba19bcbe2 |
| parent 2056 | 93c093620c28 |
| child 4162 | 4c2da701b801 |
| permissions | -rw-r--r-- |
| 1465 | 1 |
(* Title: HOL/Lex/Auto.ML |
| 1344 | 2 |
ID: $Id$ |
| 1465 | 3 |
Author: Richard Mayr & Tobias Nipkow |
| 1344 | 4 |
Copyright 1995 TUM |
5 |
*) |
|
6 |
||
7 |
open Auto; |
|
8 |
||
9 |
goalw Auto.thy [nexts_def] "nexts A st [] = st"; |
|
10 |
by(Simp_tac 1); |
|
11 |
qed"nexts_Nil"; |
|
12 |
||
13 |
goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs"; |
|
14 |
by(Simp_tac 1); |
|
15 |
qed"nexts_Cons"; |
|
16 |
||
17 |
Addsimps [nexts_Nil,nexts_Cons]; |
|
18 |
||
19 |
goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []"; |
|
20 |
by(Simp_tac 1); |
|
21 |
qed"acc_prefix_Nil"; |
|
22 |
Addsimps [acc_prefix_Nil]; |
|
23 |
||
24 |
goalw Auto.thy [acc_prefix_def] |
|
25 |
"acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)"; |
|
| 4089 | 26 |
by(simp_tac (simpset() addsimps [prefix_Cons]) 1); |
27 |
by(safe_tac (claset())); |
|
| 1344 | 28 |
by(Asm_full_simp_tac 1); |
29 |
by (case_tac "zs=[]" 1); |
|
30 |
by(hyp_subst_tac 1); |
|
31 |
by(Asm_full_simp_tac 1); |
|
|
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
1894
diff
changeset
|
32 |
by(Fast_tac 1); |
| 1344 | 33 |
by(res_inst_tac [("x","[x]")] exI 1);
|
| 4089 | 34 |
by(asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
| 1344 | 35 |
by(res_inst_tac [("x","x#us")] exI 1);
|
36 |
by(Asm_simp_tac 1); |
|
37 |
qed"acc_prefix_Cons"; |
|
38 |
Addsimps [acc_prefix_Cons]; |