src/HOL/Lex/RegExp2NA.thy
author nipkow
Thu Jan 17 19:32:22 2002 +0100 (2002-01-17)
changeset 12792 b344226f924c
parent 10834 a7897aebbffc
child 14440 3d6ed7eedfc8
permissions -rw-r--r--
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
     1 (*  Title:      HOL/Lex/RegExp2NA.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TUM
     5 
     6 Conversion of regular expressions *directly*
     7 into nondeterministic automata *without* epsilon transitions
     8 *)
     9 
    10 RegExp2NA = RegExp + NA +
    11 
    12 types 'a bitsNA = ('a,bool list)na
    13 
    14 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
    15 translations "x ## S" == "Cons x ` S"
    16 
    17 constdefs
    18  atom  :: 'a => 'a bitsNA
    19 "atom a == ([True],
    20             %b s. if s=[True] & b=a then {[False]} else {},
    21             %s. s=[False])"
    22 
    23  or :: 'a bitsNA => 'a bitsNA => 'a bitsNA
    24 "or == %(ql,dl,fl)(qr,dr,fr).
    25    ([],
    26     %a s. case s of
    27             [] => (True ## dl a ql) Un (False ## dr a qr)
    28           | left#s => if left then True ## dl a s
    29                               else False ## dr a s,
    30     %s. case s of [] => (fl ql | fr qr)
    31                 | left#s => if left then fl s else fr s)"
    32 
    33  conc :: 'a bitsNA => 'a bitsNA => 'a bitsNA
    34 "conc == %(ql,dl,fl)(qr,dr,fr).
    35    (True#ql,
    36     %a s. case s of
    37             [] => {}
    38           | left#s => if left then (True ## dl a s) Un
    39                                    (if fl s then False ## dr a qr else {})
    40                               else False ## dr a s,
    41     %s. case s of [] => False | left#s => left & fl s & fr qr | ~left & fr s)"
    42 
    43  epsilon :: 'a bitsNA
    44 "epsilon == ([],%a s. {}, %s. s=[])"
    45 
    46  plus :: 'a bitsNA => 'a bitsNA
    47 "plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
    48 
    49  star :: 'a bitsNA => 'a bitsNA
    50 "star A == or epsilon (plus A)"
    51 
    52 consts rexp2na :: 'a rexp => 'a bitsNA
    53 primrec
    54 "rexp2na Empty      = ([], %a s. {}, %s. False)"
    55 "rexp2na(Atom a)    = atom a"
    56 "rexp2na(Or r s)    = or   (rexp2na r) (rexp2na s)"
    57 "rexp2na(Conc r s)  = conc (rexp2na r) (rexp2na s)"
    58 "rexp2na(Star r)    = star (rexp2na r)"
    59 
    60 end