src/HOL/Lex/AutoMaxChop.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/AutoMaxChop.thy	Tue Mar 10 13:27:13 1998 +0100
@@ -0,0 +1,20 @@
+(*  Title:      HOL/Lex/AutoMaxChop.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+AutoMaxChop = Auto + MaxChop +
+
+consts
+ auto_split :: "('a,'s)auto => 's => 'a list => 'a list => 'a list * 'a list
+                => 'a list * 'a list"
+primrec auto_split list
+"auto_split A q ps []     res = (if fin A q then (ps,[]) else res)"
+"auto_split A q ps (x#xs) res = auto_split A (next A q x) (ps@[x]) xs
+                                     (if fin A q then (ps,x#xs) else res)"
+
+constdefs
+ auto_chop :: "('a,'s)auto => 'a chopper"
+"auto_chop A == chop (%xs. auto_split A (start A) [] xs ([],xs))"
+end