src/HOL/Lex/AutoChopper.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1900 c7a869229091
child 4137 2ce2e659c2b1
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Lex/AutoChopper.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 
     6 auto_chopper turns an automaton into a chopper. Tricky, because primrec.
     7 
     8 is_auto_chopper requires its argument to produce longest_prefix_choppers
     9 wrt the language accepted by the automaton.
    10 
    11 Main result: auto_chopper satisfies the is_auto_chopper specification.
    12 
    13 WARNING: auto_chopper is exponential(?)
    14 if the recursive calls in the penultimate argument are evaluated eagerly.
    15 *)
    16 
    17 AutoChopper = Auto + Chopper +
    18 
    19 consts
    20   is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
    21   auto_chopper :: ('a,'b)auto => 'a chopper
    22   acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
    23           => 'a list list * 'a list"
    24 
    25 defs
    26   is_auto_chopper_def "is_auto_chopper(chopperf) ==
    27                        !A. is_longest_prefix_chopper(accepts A)(chopperf A)"
    28 
    29   auto_chopper_def "auto_chopper A xs == acc xs (start A) [] [] ([],xs) A"
    30 
    31 primrec acc List.list
    32   "acc [] st ys zs chopsr A =
    33               (if ys=[] then chopsr else (ys#fst(chopsr),snd(chopsr)))" 
    34   "acc(x#xs) st ys zs chopsr A =
    35             (let s0 = start(A); nxt = next(A); fin = fin(A)
    36              in if fin(nxt st x)
    37                 then acc xs (nxt st x) (zs@[x]) (zs@[x])
    38                          (acc xs s0 [] [] ([],xs) A) A
    39                 else acc xs (nxt st x) ys (zs@[x]) chopsr A)"
    40 
    41 end
    42 
    43 (* The following definition of acc should also work:
    44 consts
    45   acc1 :: [('a,'b)auto, 'a list, 'b, 'a list list, 'a list, 'a list]
    46           => 'a list list * 'a list
    47 
    48 acc1 A [] s xss zs xs =
    49   (if xs=[] then (xss, zs)
    50    else acc1 A zs (start A) (xss @ [xs]) [] [])
    51 acc1 A (y#ys) s xss zs rec =
    52   let s' = next A s;
    53       zs' = (if fin A s' then [] else zs@[y])
    54       xs' = (if fin A s' then xs@zs@[y] else xs)
    55   in acc1 A ys s' xss zs' xs'
    56 
    57 Advantage: does not need lazy evaluation for reasonable (quadratic)
    58 performance.
    59 
    60 Disadavantage: not primrec.
    61   
    62 Termination measure:
    63   size(A,ys,s,xss,zs,rec) = (|xs| + |ys| + |zs|, |ys|)
    64 
    65 Termination proof: the first clause reduces the first component by |xs|,
    66 the second clause leaves the first component alone but reduces the second by 1.
    67 
    68 Claim: acc1 A xs s [] [] [] = acc xs s [] [] ([],xs) A
    69 Generalization?
    70 *)