|
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);
|
|
|
27 |
by(safe_tac HOL_cs);
|
|
|
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);
|
|
|
32 |
by(fast_tac (HOL_cs addSEs [Cons_neq_Nil]) 1);
|
|
|
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);
|
|
|
37 |
by (fast_tac HOL_cs 1);
|
|
|
38 |
qed"acc_prefix_Cons";
|
|
|
39 |
Addsimps [acc_prefix_Cons];
|