isabelle: src/HOL/Lex/Automata.ML@3ea049f7979d (annotated)

4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	1	(* Title: HOL/Lex/Automata.ML
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	2	ID: $Id$
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	3	Author: Tobias Nipkow
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	4	Copyright 1998 TUM
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	5	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	6
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	7	(* Equivalence of NA and DA --- redundant *)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	8
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	9	Goalw [na2da_def]
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4900 diff changeset	10	"!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	11	by(induct_tac "w" 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	12	by(ALLGOALS Asm_simp_tac);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	13	by(ALLGOALS Blast_tac);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	14	qed_spec_mp "DA_delta_is_lift_NA_delta";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	15
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	16	Goalw [DA.accepts_def,NA.accepts_def]
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	17	"NA.accepts A w = DA.accepts (na2da A) w";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	18	by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19	by(simp_tac (simpset() addsimps [na2da_def]) 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	20	qed "NA_DA_equiv";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	21
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	22	(* Direct equivalence of NAe and DA *)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	23
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	24	Goalw [nae2da_def]
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	25	"!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	26	by(induct_tac "w" 1);
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	27	by (Simp_tac 1);
a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	28	by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	29	by(Blast_tac 1);
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	30	qed_spec_mp "espclosure_DA_delta_is_steps";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	31
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	32	Goalw [nae2da_def]
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	33	"fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	34	by(Simp_tac 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	35	val lemma = result();
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	36
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	37	Goalw [NAe.accepts_def,DA.accepts_def]
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4900 diff changeset	38	"DA.accepts (nae2da A) w = NAe.accepts A w";
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	39	by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	40	by(simp_tac (simpset() addsimps [nae2da_def]) 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	41	by(Blast_tac 1);
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	42	qed "NAe_DA_equiv";

author	wenzelm
	Mon, 22 Jun 1998 17:26:46 +0200
changeset 5069	3ea049f7979d
parent 4907	0eb6730de30f
child 5132	24f992a25adc
permissions	-rw-r--r--