1476
|
1 |
(* Title: HOL/Lex/Chopper.thy
|
1344
|
2 |
ID: $Id$
|
1476
|
3 |
Author: Tobias Nipkow
|
1344
|
4 |
Copyright 1995 TUM
|
|
5 |
|
|
6 |
A 'chopper' is a function which returns
|
|
7 |
1. a chopped up prefix of the input string
|
|
8 |
2. together with the remaining suffix.
|
|
9 |
|
|
10 |
It is a longest_prefix_chopper if it
|
|
11 |
1. chops up as much of the input as possible and
|
|
12 |
2. chops it up into the longest substrings possible.
|
|
13 |
|
|
14 |
A chopper is parametrized by a language ('a list => bool),
|
|
15 |
i.e. a set of strings.
|
|
16 |
*)
|
|
17 |
|
|
18 |
Chopper = Prefix +
|
|
19 |
|
|
20 |
types 'a chopper = "'a list => 'a list list * 'a list"
|
|
21 |
|
|
22 |
consts
|
1374
|
23 |
is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
|
1344
|
24 |
|
|
25 |
defs
|
|
26 |
is_longest_prefix_chopper_def
|
|
27 |
"is_longest_prefix_chopper L chopper == !xs. \
|
1476
|
28 |
\ (!zs. chopper(xs) = ([],zs) --> \
|
|
29 |
\ zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) & \
|
|
30 |
\ (!ys yss zs. chopper(xs) = (ys#yss,zs) --> \
|
|
31 |
\ ys ~= [] & L(ys) & xs=ys@flat(yss)@zs & \
|
1344
|
32 |
\ chopper(flat(yss)@zs) = (yss,zs) & \
|
|
33 |
\ (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
|
|
34 |
end
|