# HG changeset patch
# User nipkow
# Date 816973185 -3600
# Node ID 5fdd4da11d4908711d48965dbe8953fb80a24788
# Parent  90d615b599d958e9fc7eb1b3d7f70b540e2db426
Added lots of comments

diff -r 90d615b599d9 -r 5fdd4da11d49 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Tue Nov 21 15:10:12 1995 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Tue Nov 21 17:59:45 1995 +0100
@@ -9,6 +9,9 @@
 wrt the language accepted by the automaton.
 
 Main result: auto_chopper satisfies the is_auto_chopper specification.
+
+WARNING: auto_chopper is exponential(?)
+if the recursive calls in the penultimate argument are evaluated eagerly.
 *)
 
 AutoChopper = Auto + Chopper +
@@ -16,23 +19,73 @@
 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] \
-\	  => 'a list list * 'a list"
+  acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
+	  => 'a list list * 'a list"
 
 defs
-  is_auto_chopper_def "is_auto_chopper(chopperf) ==   \
-\		       !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
+  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_Nil  "acc [] st ys zs chopsr A =   \
-\	      (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
-  acc_Cons "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_Nil  "acc [] st ys zs chopsr A =
+	      (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
+  acc_Cons "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)"
 
 end
+
+(* The following definition of acc should also work:
+consts
+  acc :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list maybe]
+         => 'a list list * 'a list
+
+acc A [] s xss zs rec =
+  (case rec of
+     Yes(xs) => acc A zs (start A) (xss @ [xs]) [] No
+   | No => (xss, zs))
+acc A (y#ys) s xss zs rec =
+  let s' = next A s;
+      zs' = (if fin A s' then [] else zs@[y])
+      rec' = (if fin A s'
+              then Yes(case rec of
+                         Yes(xs) => xs@zs@[y]
+                       | No => zs@[y])
+              else rec)
+  in acc A ys s' xss zs' rec'
+
+Advantage: does not need lazy evaluation for reasonable (quadartic)
+performance.
+
+Termination measure:
+  size(A,ys,s,xss,zs,rec) =
+    case rec of
+      No => |ys|^2 + |ys|
+      Yes => (|ys|+|zs|)^2 + 2|ys| + |zs| + 1
+
+Termination proof:
+  
+  1. size(,[],,,zs,Yes(xs)) = z^2 + z + 1 > z^2 + z = size(,zs,,,[],No)
+
+  2. size(,y#ys,,,zs,No) = (y+1)^2 + y+1 = y^2 + 3y + 2
+  
+  2.1. fin A s' --> zs' = [] & rec' = Yes
+       size(,y#ys,,,zs,No) > y^2 + 2y + 1 = size(,ys,,,[],Yes)
+  
+  2.2. not(fin A s') --> rec' = rec = No
+       size(,y#ys,,,zs,No) > y^2 + y = size(,ys,,,,No)
+
+  3. size(,y#ys,,,zs,Yes) = (y+z+1)^2 + 2y + z + 3
+
+  3.1 fin A s' --> zs' = [] & rec' = Yes
+      size(,y#ys,,,zs,Yes) > y^2 + 2y + 1 = size(,ys,,,[],Yes)
+  3.2 not(fin A s') --> ze' = zs@[y] & rec' = rec = Yes
+      size(,y#ys,,,zs,Yes) > (y+z+1)^2 + 2y + z + 2 = size(,ys,,,zs@[y],Yes)
+
+where y := |ys| and z := |zs|
+*)