isabelle: src/HOL/Lex/Automata.ML@24f992a25adc (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)";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	11	by (induct_tac "w" 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	12	by (ALLGOALS Asm_simp_tac);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	13	by (ALLGOALS Blast_tac);
4832 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";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	18	by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	19	by (simp_tac (simpset() addsimps [na2da_def]) 1);
4832 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";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 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);
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	28	by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 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)";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	34	by (Simp_tac 1);
4832 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";
5132 24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	39	by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	40	by (simp_tac (simpset() addsimps [nae2da_def]) 1);
24f992a25adc isatool expandshort; wenzelm parents: 5069 diff changeset	41	by (Blast_tac 1);
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	42	qed "NAe_DA_equiv";

author	wenzelm
	Sun, 12 Jul 1998 11:49:17 +0200
changeset 5132	24f992a25adc
parent 5069	3ea049f7979d
child 5323	028e00595280
permissions	-rw-r--r--