src/HOL/Lex/Auto.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1559 9ba0906aa60d
child 4670 f309259fa828
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Lex/Auto.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TUM
     5 
     6 Automata expressed as triples of
     7   1. a start state,
     8   2. a transition function and
     9   3. a test for final states.
    10 
    11 NOTE: this functional representation is suitable for all kinds of automata,
    12       not just finite ones!
    13 *)
    14 
    15 Auto = Prefix +
    16 
    17 types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
    18 
    19 constdefs
    20 
    21   start :: ('a, 'b)auto => 'b
    22   "start(A) == fst(A)"
    23 
    24   next  :: ('a, 'b)auto => ('b => 'a => 'b)
    25   "next(A) == fst(snd(A))"
    26 
    27   fin   :: ('a, 'b)auto => ('b => bool)
    28   "fin(A) == snd(snd(A))"
    29 
    30   nexts :: ('a, 'b)auto => 'b => 'a list => 'b
    31   "nexts(A) == foldl(next(A))"
    32 
    33   accepts :: ('a,'b) auto => 'a list => bool
    34   "accepts A xs == fin A (nexts A (start A) xs)"
    35 
    36   acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
    37   "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
    38 
    39 end