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