author | wenzelm |
Thu, 12 Feb 1998 17:53:05 +0100 | |
changeset 4628 | 0c7e97836e3c |
parent 4137 | 2ce2e659c2b1 |
child 4832 | bc11b5b06f87 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: HOL/Lex/AutoChopper.thy |
1344 | 2 |
ID: $Id$ |
1476 | 3 |
Author: Tobias Nipkow |
1344 | 4 |
Copyright 1995 TUM |
5 |
||
6 |
auto_chopper turns an automaton into a chopper. Tricky, because primrec. |
|
7 |
||
8 |
is_auto_chopper requires its argument to produce longest_prefix_choppers |
|
9 |
wrt the language accepted by the automaton. |
|
10 |
||
11 |
Main result: auto_chopper satisfies the is_auto_chopper specification. |
|
1362 | 12 |
|
13 |
WARNING: auto_chopper is exponential(?) |
|
14 |
if the recursive calls in the penultimate argument are evaluated eagerly. |
|
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
1900
diff
changeset
|
15 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
1900
diff
changeset
|
16 |
A more efficient version is defined in AutoChopper1. |
1344 | 17 |
*) |
18 |
||
19 |
AutoChopper = Auto + Chopper + |
|
20 |
||
21 |
consts |
|
1374 | 22 |
is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool |
23 |
auto_chopper :: ('a,'b)auto => 'a chopper |
|
1362 | 24 |
acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto] |
1476 | 25 |
=> 'a list list * 'a list" |
1344 | 26 |
|
27 |
defs |
|
1362 | 28 |
is_auto_chopper_def "is_auto_chopper(chopperf) == |
1476 | 29 |
!A. is_longest_prefix_chopper(accepts A)(chopperf A)" |
1344 | 30 |
|
31 |
auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A" |
|
32 |
||
33 |
primrec acc List.list |
|
1900 | 34 |
"acc [] st ys zs chopsr A = |
1476 | 35 |
(if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" |
1900 | 36 |
"acc(x#xs) st ys zs chopsr A = |
1476 | 37 |
(let s0 = start(A); nxt = next(A); fin = fin(A) |
1362 | 38 |
in if fin(nxt st x) |
39 |
then acc xs (nxt st x) (zs@[x]) (zs@[x]) |
|
40 |
(acc xs s0 [] [] ([],xs) A) A |
|
41 |
else acc xs (nxt st x) ys (zs@[x]) chopsr A)" |
|
1344 | 42 |
|
43 |
end |