|
4832
|
1 |
(* Title: HOL/Lex/DA.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
|
|
|
6 |
Deterministic automata
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
DA = List + AutoProj +
|
|
|
10 |
|
|
|
11 |
types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
|
|
|
12 |
|
|
|
13 |
constdefs
|
|
|
14 |
foldl2 :: ('a => 'b => 'b) => 'a list => 'b => 'b
|
|
|
15 |
"foldl2 f xs a == foldl (%a b. f b a) a xs"
|
|
|
16 |
|
|
|
17 |
delta :: ('a,'s)da => 'a list => 's => 's
|
|
|
18 |
"delta A == foldl2 (next A)"
|
|
|
19 |
|
|
|
20 |
accepts :: ('a,'s)da => 'a list => bool
|
|
|
21 |
"accepts A == %w. fin A (delta A w (start A))"
|
|
|
22 |
|
|
|
23 |
end
|