isabelle: src/HOL/Lex/Automata.thy@bdd17e7b5bd9 (annotated)

4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	1	(* Title: HOL/Lex/Automata.thy
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	Conversions between different kinds of automata
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	7	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	8
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	9	Automata = DA + NAe +
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	10
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	11	constdefs
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	12	na2da :: ('a,'s)na => ('a,'s set)da
10834 a7897aebbffc * empty log message * nipkow parents: 10797 diff changeset	13	"na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)"
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	14
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	15	nae2da :: ('a,'s)nae => ('a,'s set)da
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	16	"nae2da A == ({start A},
10834 a7897aebbffc * empty log message * nipkow parents: 10797 diff changeset	17	%a Q. Union(next A (Some a) ` ((eps A)^* `` Q)),
a7897aebbffc * empty log message * nipkow parents: 10797 diff changeset	18	%Q. ? p: (eps A)^* `` Q. fin A p)"
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	20	end

author	wenzelm
	Tue, 15 Jan 2002 21:09:01 +0100
changeset 12770	bdd17e7b5bd9
parent 10834	a7897aebbffc
child 14428	bb2b0e10d9be
permissions	-rw-r--r--