|
1344
|
1 |
(* Title: HOL/Lex/Auto.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1995 TUM
|
|
|
5 |
|
|
|
6 |
Automata expressed as triples of
|
|
|
7 |
1. a start state,
|
|
|
8 |
2. a transition function and
|
|
|
9 |
3. a test for final states.
|
|
|
10 |
|
|
|
11 |
NOTE: this functional representation is suitable for all kinds of automata,
|
|
|
12 |
not just finite ones!
|
|
|
13 |
*)
|
|
|
14 |
|
|
|
15 |
Auto = Prefix +
|
|
|
16 |
|
|
|
17 |
types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
|
|
|
18 |
|
|
|
19 |
consts
|
|
1374
|
20 |
start :: ('a, 'b)auto => 'b
|
|
|
21 |
next :: ('a, 'b)auto => ('b => 'a => 'b)
|
|
|
22 |
fin :: ('a, 'b)auto => ('b => bool)
|
|
|
23 |
nexts :: ('a, 'b)auto => 'b => 'a list => 'b
|
|
|
24 |
accepts :: ('a,'b) auto => 'a list => bool
|
|
|
25 |
acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
|
|
1344
|
26 |
|
|
|
27 |
defs
|
|
|
28 |
start_def "start(A) == fst(A)"
|
|
|
29 |
next_def "next(A) == fst(snd(A))"
|
|
|
30 |
fin_def "fin(A) == snd(snd(A))"
|
|
|
31 |
nexts_def "nexts(A) == foldl(next(A))"
|
|
|
32 |
|
|
|
33 |
accepts_def "accepts A xs == fin A (nexts A (start A) xs)"
|
|
|
34 |
|
|
|
35 |
acc_prefix_def
|
|
|
36 |
"acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
|
|
|
37 |
|
|
|
38 |
end
|