src/HOL/Lex/Chopper.thy

Half a lexical analyzer generator.

(*  Title: 	HOL/Lex/Chopper.thy
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1995 TUM

A 'chopper' is a function which returns
  1. a chopped up prefix of the input string
  2. together with the remaining suffix.

It is a longest_prefix_chopper if it
  1. chops up as much of the input as possible and
  2. chops it up into the longest substrings possible.

A chopper is parametrized by a language ('a list => bool),
i.e. a set of strings.
*)

Chopper = Prefix +

types   'a chopper = "'a list => 'a list list * 'a list"

consts
  is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool"

defs
  is_longest_prefix_chopper_def
    "is_longest_prefix_chopper L chopper == !xs.   \
\	 (!zs. chopper(xs) = ([],zs) --> \
\	       zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &  \
\ 	 (!ys yss zs. chopper(xs) = (ys#yss,zs) -->                \
\	    ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &   \
\           chopper(flat(yss)@zs) = (yss,zs) &     \
\           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
end