equal
deleted
inserted
replaced
|
1 (* Title: HOL/Lex/MaxChop.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 *) |
|
6 |
|
7 MaxChop = MaxPrefix + |
|
8 |
|
9 types 'a chopper = "'a list => 'a list list * 'a list" |
|
10 |
|
11 constdefs |
|
12 is_maxchopper :: ('a list => bool) => 'a chopper => bool |
|
13 "is_maxchopper P chopper == |
|
14 !xs zs yss. |
|
15 (chopper(xs) = (yss,zs)) = |
|
16 (xs = concat yss @ zs & (!ys : set yss. ys ~= []) & |
|
17 (case yss of |
|
18 [] => is_maxpref P [] xs |
|
19 | us#uss => is_maxpref P us xs & chopper(concat(uss)@zs) = (uss,zs)))" |
|
20 |
|
21 constdefs |
|
22 reducing :: "'a splitter => bool" |
|
23 "reducing splitf == |
|
24 !xs ys zs. splitf xs = (ys,zs) & ys ~= [] --> length zs < length xs" |
|
25 |
|
26 consts |
|
27 chopr :: "'a splitter * 'a list => 'a list list * 'a list" |
|
28 recdef chopr "measure (length o snd)" |
|
29 "chopr (splitf,xs) = (if reducing splitf |
|
30 then let pp = splitf xs |
|
31 in if fst(pp)=[] then ([],xs) |
|
32 else let qq = chopr (splitf,snd pp) |
|
33 in (fst pp # fst qq,snd qq) |
|
34 else arbitrary)" |
|
35 constdefs |
|
36 chop :: 'a splitter => 'a chopper |
|
37 "chop splitf xs == chopr(splitf,xs)" |
|
38 |
|
39 end |