1344
|
1 |
(* Title: HOL/Lex/AutoChopper.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
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.
|
1344
|
15 |
*)
|
|
16 |
|
|
17 |
AutoChopper = Auto + Chopper +
|
|
18 |
|
|
19 |
consts
|
1374
|
20 |
is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
|
|
21 |
auto_chopper :: ('a,'b)auto => 'a chopper
|
1362
|
22 |
acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
|
|
23 |
=> 'a list list * 'a list"
|
1344
|
24 |
|
|
25 |
defs
|
1362
|
26 |
is_auto_chopper_def "is_auto_chopper(chopperf) ==
|
|
27 |
!A. is_longest_prefix_chopper(accepts A)(chopperf A)"
|
1344
|
28 |
|
|
29 |
auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
|
|
30 |
|
|
31 |
primrec acc List.list
|
1362
|
32 |
acc_Nil "acc [] st ys zs chopsr A =
|
|
33 |
(if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))"
|
|
34 |
acc_Cons "acc(x#xs) st ys zs chopsr A =
|
|
35 |
(let s0 = start(A); nxt = next(A); fin = fin(A)
|
|
36 |
in if fin(nxt st x)
|
|
37 |
then acc xs (nxt st x) (zs@[x]) (zs@[x])
|
|
38 |
(acc xs s0 [] [] ([],xs) A) A
|
|
39 |
else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
|
1344
|
40 |
|
|
41 |
end
|
1362
|
42 |
|
|
43 |
(* The following definition of acc should also work:
|
|
44 |
consts
|
1365
|
45 |
acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
|
|
46 |
=> 'a list list * 'a list
|
1362
|
47 |
|
1365
|
48 |
acc1 A [] s xss zs xs =
|
|
49 |
(if xs=[] then (xss, zs)
|
|
50 |
else acc1 A zs (start A) (xss @ [xs]) [] [])
|
|
51 |
acc1 A (y#ys) s xss zs rec =
|
1362
|
52 |
let s' = next A s;
|
|
53 |
zs' = (if fin A s' then [] else zs@[y])
|
1365
|
54 |
xs' = (if fin A s' then xs@zs@[y] else xs)
|
|
55 |
in acc1 A ys s' xss zs' xs'
|
1362
|
56 |
|
1365
|
57 |
Advantage: does not need lazy evaluation for reasonable (quadratic)
|
1362
|
58 |
performance.
|
|
59 |
|
1365
|
60 |
Disadavantage: not primrec.
|
1362
|
61 |
|
1365
|
62 |
Termination measure:
|
|
63 |
size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
|
1362
|
64 |
|
1365
|
65 |
Termination proof: the first clause reduces the first component by |xs|,
|
|
66 |
the second clause leaves the first component alone but reduces the second by 1.
|
1362
|
67 |
|
1365
|
68 |
Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
|
|
69 |
Generalization?
|
1362
|
70 |
*)
|