src/HOL/Lex/Chopper.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2609 4370e5f0fa3f
child 10338 291ce4c4b50e
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Lex/Chopper.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     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 constdefs
    23   is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
    24   "is_longest_prefix_chopper L chopper == !xs.
    25        (!zs. chopper(xs) = ([],zs) -->
    26              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
    27        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
    28           ys ~= [] & L(ys) & xs=ys@concat(yss)@zs &
    29           chopper(concat(yss)@zs) = (yss,zs) &
    30           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
    31 
    32 end