# HG changeset patch
# User nipkow
# Date 817131173 -3600
# Node ID 0defae128e43a0cc6736be335fbf4c899de9bb94
# Parent  8ea1a962ad721e762c3d4dc862c63cc42fdddab3
Updated comments

diff -r 8ea1a962ad72 -r 0defae128e43 src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Thu Nov 23 12:18:16 1995 +0100
+++ b/src/HOL/Lex/AutoChopper.thy	Thu Nov 23 13:52:53 1995 +0100
@@ -42,50 +42,29 @@
 
 (* 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
+  acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
+          => '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 =
+acc1 A [] s xss zs xs =
+  (if xs=[] then (xss, zs)
+   else acc1 A zs (start A) (xss @ [xs]) [] [])
+acc1 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'
+      xs' = (if fin A s' then xs@zs@[y] else xs)
+  in acc1 A ys s' xss zs' xs'
 
-Advantage: does not need lazy evaluation for reasonable (quadartic)
+Advantage: does not need lazy evaluation for reasonable (quadratic)
 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
+Disadavantage: not primrec.
   
-  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
+Termination measure:
+  size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
 
-  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)
+Termination proof: the first clause reduces the first component by |xs|,
+the second clause leaves the first component alone but reduces the second by 1.
 
-where y := |ys| and z := |zs|
+Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
+Generalization?
 *)