# 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? *)