|
4832
|
1 |
(* Title: HOL/Lex/Automata.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
(*** Equivalence of NA and DA --- redundant ***)
|
|
|
8 |
|
|
|
9 |
goalw thy [na2da_def]
|
|
|
10 |
"!Q. DA.delta (na2da A) w Q = lift(NA.delta A w) Q";
|
|
|
11 |
by(induct_tac "w" 1);
|
|
|
12 |
by(ALLGOALS Asm_simp_tac);
|
|
|
13 |
by(ALLGOALS Blast_tac);
|
|
|
14 |
qed_spec_mp "DA_delta_is_lift_NA_delta";
|
|
|
15 |
|
|
|
16 |
goalw thy [DA.accepts_def,NA.accepts_def]
|
|
|
17 |
"NA.accepts A w = DA.accepts (na2da A) w";
|
|
|
18 |
by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
|
|
|
19 |
by(simp_tac (simpset() addsimps [na2da_def]) 1);
|
|
|
20 |
qed "NA_DA_equiv";
|
|
|
21 |
|
|
|
22 |
(*** Direct equivalence of NAe and DA ***)
|
|
|
23 |
|
|
|
24 |
goalw thy [nae2da_def]
|
|
4900
|
25 |
"!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
|
|
4832
|
26 |
by(induct_tac "w" 1);
|
|
4900
|
27 |
by (Simp_tac 1);
|
|
|
28 |
by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
|
|
4832
|
29 |
by(Blast_tac 1);
|
|
4900
|
30 |
qed_spec_mp "espclosure_DA_delta_is_steps";
|
|
4832
|
31 |
|
|
|
32 |
goalw thy [nae2da_def]
|
|
|
33 |
"fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
|
|
|
34 |
by(Simp_tac 1);
|
|
|
35 |
val lemma = result();
|
|
|
36 |
|
|
|
37 |
goalw thy [NAe.accepts_def,DA.accepts_def]
|
|
|
38 |
"NAe.accepts A w = DA.accepts (nae2da A) w";
|
|
4900
|
39 |
by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
|
|
4832
|
40 |
by(simp_tac (simpset() addsimps [nae2da_def]) 1);
|
|
|
41 |
by(Blast_tac 1);
|
|
|
42 |
qed "NAe_DA_equiv";
|