--- a/src/HOL/Lex/AutoChopper.thy Mon Apr 27 16:45:27 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy Mon Apr 27 16:46:56 1998 +0200
@@ -16,28 +16,33 @@
A more efficient version is defined in AutoChopper1.
*)
-AutoChopper = Auto + Chopper +
+AutoChopper = Prefix + DA + Chopper +
+
+constdefs
+ is_auto_chopper :: (('a,'s)da => 'a chopper) => bool
+"is_auto_chopper(chopperf) ==
+ !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
consts
- is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
- auto_chopper :: ('a,'b)auto => 'a chopper
- acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
+ acc :: "['a list, 's, 'a list, 'a list, 'a list list*'a list, ('a,'s)da]
=> 'a list list * 'a list"
-
-defs
- is_auto_chopper_def "is_auto_chopper(chopperf) ==
- !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
-
- auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
-
primrec acc List.list
"acc [] st ys zs chopsr A =
(if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))"
- "acc(x#xs) st ys zs chopsr A =
- (let s0 = start(A); nxt = next(A); fin = fin(A)
- in if fin(nxt st x)
- then acc xs (nxt st x) (zs@[x]) (zs@[x])
- (acc xs s0 [] [] ([],xs) A) A
- else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
+ "acc(x#xs) s ys zs chopsr A =
+ (let t = next A x s
+ in if fin A t
+ then acc xs t (zs@[x]) (zs@[x])
+ (acc xs (start A) [] [] ([],xs) A) A
+ else acc xs t ys (zs@[x]) chopsr A)"
+
+constdefs
+ auto_chopper :: ('a,'s)da => 'a chopper
+"auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
+
+(* acc_prefix is an auxiliary notion for the proof *)
+constdefs
+ acc_prefix :: ('a,'s)da => 'a list => 's => bool
+"acc_prefix A xs s == ? us. us <= xs & us~=[] & fin A (delta A us s)"
end