author | paulson |
Thu, 12 Sep 1996 10:40:05 +0200 | |
changeset 1985 | 84cf16192e03 |
parent 1894 | c2c8279d40f0 |
child 2056 | 93c093620c28 |
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)"; |
|
26 |
by(simp_tac (!simpset addsimps [prefix_Cons]) 1); |
|
1894 | 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); |
34 |
by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1); |
|
35 |
by(res_inst_tac [("x","x#us")] exI 1); |
|
36 |
by(Asm_simp_tac 1); |
|
1894 | 37 |
by (Fast_tac 1); |
1344 | 38 |
qed"acc_prefix_Cons"; |
39 |
Addsimps [acc_prefix_Cons]; |