equal
deleted
inserted
replaced
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 ***) |
|
8 |
|
9 Goalw [na2da_def] |
|
10 "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)"; |
|
11 by (induct_tac "w" 1); |
|
12 by Auto_tac; |
|
13 qed_spec_mp "DA_delta_is_lift_NA_delta"; |
|
14 |
|
15 Goalw [DA.accepts_def,NA.accepts_def] |
|
16 "NA.accepts A w = DA.accepts (na2da A) w"; |
|
17 by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1); |
|
18 by (simp_tac (simpset() addsimps [na2da_def]) 1); |
|
19 qed "NA_DA_equiv"; |
|
20 |
|
21 (*** Direct equivalence of NAe and DA ***) |
|
22 |
|
23 Goalw [nae2da_def] |
|
24 "!Q. (eps A)^* `` (DA.delta (nae2da A) w Q) = steps A w `` Q"; |
|
25 by (induct_tac "w" 1); |
|
26 by (Simp_tac 1); |
|
27 by (asm_full_simp_tac (simpset() addsimps [step_def]) 1); |
|
28 by (Blast_tac 1); |
|
29 qed_spec_mp "espclosure_DA_delta_is_steps"; |
|
30 |
|
31 Goalw [nae2da_def] |
|
32 "fin (nae2da A) Q = (? q : (eps A)^* `` Q. fin A q)"; |
|
33 by (Simp_tac 1); |
|
34 val lemma = result(); |
|
35 |
|
36 Goalw [NAe.accepts_def,DA.accepts_def] |
|
37 "DA.accepts (nae2da A) w = NAe.accepts A w"; |
|
38 by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1); |
|
39 by (simp_tac (simpset() addsimps [nae2da_def]) 1); |
|
40 by (Blast_tac 1); |
|
41 qed "NAe_DA_equiv"; |
|