| author | paulson |
| Thu, 13 Aug 1998 17:44:50 +0200 | |
| changeset 5312 | b380921982b9 |
| 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 |