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