src/HOL/Lex/RegExp2NAe.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
nipkow@4907
     1
(*  Title:      HOL/Lex/RegExp2NAe.thy
nipkow@4907
     2
    ID:         $Id$
nipkow@4907
     3
    Author:     Tobias Nipkow
nipkow@4907
     4
    Copyright   1998 TUM
nipkow@4907
     5
nipkow@4907
     6
Conversion of regular expressions
nipkow@4907
     7
into nondeterministic automata with epsilon transitions
nipkow@4907
     8
*)
nipkow@4907
     9
wenzelm@8732
    10
RegExp2NAe = RegExp + NAe +
nipkow@4907
    11
nipkow@4907
    12
types 'a bitsNAe = ('a,bool list)nae
nipkow@4907
    13
nipkow@4907
    14
syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
nipkow@10834
    15
translations "x ## S" == "Cons x ` S"
nipkow@4907
    16
nipkow@4907
    17
constdefs
nipkow@4907
    18
 atom  :: 'a => 'a bitsNAe
nipkow@4907
    19
"atom a == ([True],
nipkow@4907
    20
            %b s. if s=[True] & b=Some a then {[False]} else {},
nipkow@4907
    21
            %s. s=[False])"
nipkow@4907
    22
nipkow@12792
    23
 or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
nipkow@12792
    24
"or == %(ql,dl,fl)(qr,dr,fr).
nipkow@4907
    25
   ([],
nipkow@4907
    26
    %a s. case s of
nipkow@4907
    27
            [] => if a=None then {True#ql,False#qr} else {}
nipkow@4907
    28
          | left#s => if left then True ## dl a s
nipkow@4907
    29
                              else False ## dr a s,
nipkow@4907
    30
    %s. case s of [] => False | left#s => if left then fl s else fr s)"
nipkow@4907
    31
nipkow@4907
    32
 conc :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
nipkow@4907
    33
"conc == %(ql,dl,fl)(qr,dr,fr).
nipkow@4907
    34
   (True#ql,
nipkow@4907
    35
    %a s. case s of
nipkow@4907
    36
            [] => {}
nipkow@4907
    37
          | left#s => if left then (True ## dl a s) Un
nipkow@4907
    38
                                   (if fl s & a=None then {False#qr} else {})
nipkow@4907
    39
                              else False ## dr a s,
nipkow@4907
    40
    %s. case s of [] => False | left#s => ~left & fr s)"
nipkow@4907
    41
nipkow@4907
    42
 star :: 'a bitsNAe => 'a bitsNAe
nipkow@4907
    43
"star == %(q,d,f).
nipkow@4907
    44
   ([],
nipkow@4907
    45
    %a s. case s of
nipkow@4907
    46
            [] => if a=None then {True#q} else {}
nipkow@4907
    47
          | left#s => if left then (True ## d a s) Un
nipkow@4907
    48
                                   (if f s & a=None then {True#q} else {})
nipkow@4907
    49
                              else {},
nipkow@4907
    50
    %s. case s of [] => True | left#s => left & f s)"
nipkow@4907
    51
nipkow@4907
    52
consts rexp2nae :: 'a rexp => 'a bitsNAe
berghofe@5184
    53
primrec
nipkow@4907
    54
"rexp2nae Empty      = ([], %a s. {}, %s. False)"
nipkow@4907
    55
"rexp2nae(Atom a)    = atom a"
nipkow@12792
    56
"rexp2nae(Or r s)    = or   (rexp2nae r) (rexp2nae s)"
nipkow@12792
    57
"rexp2nae(Conc r s)  = conc (rexp2nae r) (rexp2nae s)"
nipkow@12792
    58
"rexp2nae(Star r)    = star (rexp2nae r)"
nipkow@4907
    59
nipkow@4907
    60
end