author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 4907 | 0eb6730de30f |
child 10797 | 028d22926a41 |
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 |
|
4907
0eb6730de30f
Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
4832
diff
changeset
|
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}, |
|
4907
0eb6730de30f
Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
4832
diff
changeset
|
17 |
%a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)), |
4832 | 18 |
%Q. ? p: (eps A)^* ^^ Q. fin A p)" |
19 |
||
20 |
end |