equal
deleted
inserted
replaced
|
1 (* Title: HOL/Lex/NAe.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 |
|
6 Nondeterministic automata with epsilon transitions |
|
7 *) |
|
8 |
|
9 NAe = List + Option + NA + |
|
10 |
|
11 types ('a,'s)nae = ('a option,'s)na |
|
12 |
|
13 constdefs |
|
14 step :: "('a,'s)nae => 'a option => ('s * 's)set" |
|
15 "step A a == {(p,q) . q : next A a p}" |
|
16 |
|
17 syntax eps :: "('a,'s)nae => ('s * 's)set" |
|
18 translations "eps A" == "step A None" |
|
19 |
|
20 consts steps :: "('a,'s)nae => 'a list => ('s * 's)set" |
|
21 primrec steps list |
|
22 "steps A [] = (eps A)^*" |
|
23 "steps A (a#w) = steps A w O step A (Some a) O (eps A)^*" |
|
24 |
|
25 consts delta :: "('a,'s)nae => 'a list => 's => 's set" |
|
26 primrec delta list |
|
27 "delta A [] s = (eps A)^* ^^ {s}" |
|
28 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))" |
|
29 |
|
30 constdefs |
|
31 accepts :: ('a,'s)nae => 'a list => bool |
|
32 "accepts A w == ? q. (start A,q) : steps A w & fin A q" |
|
33 |
|
34 end |