author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 10797 | 028d22926a41 |
child 14428 | bb2b0e10d9be |
permissions | -rw-r--r-- |
4832 | 1 |
(* Title: HOL/Lex/Automata.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TUM |
|
5 |
||
6 |
Conversions between different kinds of automata |
|
7 |
*) |
|
8 |
||
9 |
Automata = DA + NAe + |
|
10 |
||
11 |
constdefs |
|
12 |
na2da :: ('a,'s)na => ('a,'s set)da |
|
10834 | 13 |
"na2da A == ({start A}, %a Q. Union(next A a ` Q), %Q. ? q:Q. fin A q)" |
4832 | 14 |
|
15 |
nae2da :: ('a,'s)nae => ('a,'s set)da |
|
16 |
"nae2da A == ({start A}, |
|
10834 | 17 |
%a Q. Union(next A (Some a) ` ((eps A)^* `` Q)), |
18 |
%Q. ? p: (eps A)^* `` Q. fin A p)" |
|
4832 | 19 |
|
20 |
end |