| author | kleing |
| Wed, 24 Dec 2003 08:54:30 +0100 | |
| changeset 14328 | fd063037fdf5 |
| parent 10834 | a7897aebbffc |
| 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 |