equal
deleted
inserted
replaced
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 thy [na2da_def] |
10 "!Q. DA.delta (na2da A) w Q = lift(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 |
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 thy [NAe.accepts_def,DA.accepts_def] |
38 "NAe.accepts A w = DA.accepts (nae2da 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"; |