isabelle: src/HOL/Lex/Automata.ML@bc084e1b4d8d (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
5323 028e00595280 Direct translation RegExp -> NA! nipkow parents: 5132 diff changeset	7	(* Equivalence of NA and DA *)
4832 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)";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	11	by (induct_tac "w" 1);
6294 bc084e1b4d8d tidied paulson parents: 5323 diff changeset	12	by Auto_tac;
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	13	qed_spec_mp "DA_delta_is_lift_NA_delta";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	14
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	15	Goalw [DA.accepts_def,NA.accepts_def]
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	16	"NA.accepts A w = DA.accepts (na2da A) w";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	17	by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	18	by (simp_tac (simpset() addsimps [na2da_def]) 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19	qed "NA_DA_equiv";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	20
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	21	(* Direct equivalence of NAe and DA *)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	22
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	23	Goalw [nae2da_def]
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	24	"!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	25	by (induct_tac "w" 1);
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	26	by (Simp_tac 1);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	27	by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	28	by (Blast_tac 1);
4900 a4301a63bf5c Got rid of NAe.delta nipkow parents: 4832 diff changeset	29	qed_spec_mp "espclosure_DA_delta_is_steps";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	30
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	31	Goalw [nae2da_def]
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	32	"fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	33	by (Simp_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	34	val lemma = result();
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	35
5069 3ea049f7979d isatool fixgoal; wenzelm parents: 4907 diff changeset	36	Goalw [NAe.accepts_def,DA.accepts_def]
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4900 diff changeset	37	"DA.accepts (nae2da A) w = NAe.accepts A w";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	38	by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	39	by (simp_tac (simpset() addsimps [nae2da_def]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	40	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	41	qed "NAe_DA_equiv";

author	paulson
	Mon, 01 Mar 1999 18:37:52 +0100
changeset 6294	bc084e1b4d8d
parent 5323	028e00595280
child 10797	028d22926a41
permissions	-rw-r--r--