src/HOL/Lex/Chopper.thy
author nipkow
Wed Feb 12 18:54:39 1997 +0100 (1997-02-12)
changeset 2609 4370e5f0fa3f
parent 1559 9ba0906aa60d
child 10338 291ce4c4b50e
permissions -rw-r--r--
New class "order" and accompanying changes.
clasohm@1476
     1
(*  Title:      HOL/Lex/Chopper.thy
nipkow@1344
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@1344
     4
    Copyright   1995 TUM
nipkow@1344
     5
nipkow@1344
     6
A 'chopper' is a function which returns
nipkow@1344
     7
  1. a chopped up prefix of the input string
nipkow@1344
     8
  2. together with the remaining suffix.
nipkow@1344
     9
nipkow@1344
    10
It is a longest_prefix_chopper if it
nipkow@1344
    11
  1. chops up as much of the input as possible and
nipkow@1344
    12
  2. chops it up into the longest substrings possible.
nipkow@1344
    13
nipkow@1344
    14
A chopper is parametrized by a language ('a list => bool),
nipkow@1344
    15
i.e. a set of strings.
nipkow@1344
    16
*)
nipkow@1344
    17
nipkow@1344
    18
Chopper = Prefix +
nipkow@1344
    19
nipkow@1344
    20
types   'a chopper = "'a list => 'a list list * 'a list"
nipkow@1344
    21
clasohm@1559
    22
constdefs
clasohm@1374
    23
  is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
clasohm@1559
    24
  "is_longest_prefix_chopper L chopper == !xs.
clasohm@1559
    25
       (!zs. chopper(xs) = ([],zs) -->
clasohm@1559
    26
             zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
clasohm@1559
    27
       (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
nipkow@2609
    28
          ys ~= [] & L(ys) & xs=ys@concat(yss)@zs &
nipkow@2609
    29
          chopper(concat(yss)@zs) = (yss,zs) &
clasohm@1559
    30
          (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
nipkow@1344
    31
nipkow@1344
    32
end