|
4714
|
1 |
(* Title: HOL/Lex/AutoMaxChop.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
4832
|
7 |
AutoMaxChop = DA + MaxChop +
|
|
4714
|
8 |
|
|
|
9 |
consts
|
|
4910
|
10 |
auto_split :: "('a,'s)da => 's => 'a list * 'a list => 'a list => 'a splitter"
|
|
5184
|
11 |
primrec
|
|
4910
|
12 |
"auto_split A q res ps [] = (if fin A q then (ps,[]) else res)"
|
|
|
13 |
"auto_split A q res ps (x#xs) =
|
|
|
14 |
auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
|
|
4714
|
15 |
|
|
|
16 |
constdefs
|
|
4832
|
17 |
auto_chop :: "('a,'s)da => 'a chopper"
|
|
4910
|
18 |
"auto_chop A == chop (%xs. auto_split A (start A) ([],xs) [] xs)"
|
|
4714
|
19 |
end
|