|
5323
|
1 |
(* Title: HOL/Lex/NA.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Goal
|
|
|
8 |
"steps A (v@w) = steps A w O steps A v";
|
|
|
9 |
by (induct_tac "v" 1);
|
|
|
10 |
by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
|
|
|
11 |
qed "steps_append";
|
|
|
12 |
Addsimps [steps_append];
|
|
|
13 |
|
|
|
14 |
Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
|
|
|
15 |
by(rtac (steps_append RS equalityE) 1);
|
|
|
16 |
by(Blast_tac 1);
|
|
|
17 |
qed "in_steps_append";
|
|
|
18 |
AddIffs [in_steps_append];
|
|
|
19 |
|
|
|
20 |
Goal
|
|
|
21 |
"!p. delta A w p = {q. (p,q) : steps A w}";
|
|
|
22 |
by(induct_tac "w" 1);
|
|
|
23 |
by(auto_tac (claset(), simpset() addsimps [step_def]));
|
|
|
24 |
qed_spec_mp "delta_conv_steps";
|
|
|
25 |
|
|
|
26 |
Goalw [accepts_def]
|
|
|
27 |
"accepts A w = (? q. (start A,q) : steps A w & fin A q)";
|
|
|
28 |
by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
|
|
|
29 |
qed "accepts_conv_steps";
|