src/HOL/Lex/RegExp2NAe.thy
author nipkow
Fri, 08 May 1998 18:33:29 +0200
changeset 4907 0eb6730de30f
child 5184 9b8547a9496a
permissions -rw-r--r--
Reshuffeling, renaming and a few simple corollaries.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4907
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Lex/RegExp2NAe.thy
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     4
    Copyright   1998 TUM
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     5
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     6
Conversion of regular expressions
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     7
into nondeterministic automata with epsilon transitions
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     8
*)
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
     9
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    10
RegExp2NAe = NAe + RegExp +
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    11
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    12
types 'a bitsNAe = ('a,bool list)nae
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    13
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    14
syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    15
translations "x ## S" == "op # x `` S"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    16
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    17
constdefs
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    18
 atom  :: 'a => 'a bitsNAe
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    19
"atom a == ([True],
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    20
            %b s. if s=[True] & b=Some a then {[False]} else {},
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    21
            %s. s=[False])"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    22
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    23
 union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    24
"union == %(ql,dl,fl)(qr,dr,fr).
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    25
   ([],
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    26
    %a s. case s of
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    27
            [] => if a=None then {True#ql,False#qr} else {}
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    28
          | left#s => if left then True ## dl a s
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    29
                              else False ## dr a s,
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    30
    %s. case s of [] => False | left#s => if left then fl s else fr s)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    31
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    32
 conc :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    33
"conc == %(ql,dl,fl)(qr,dr,fr).
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    34
   (True#ql,
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    35
    %a s. case s of
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    36
            [] => {}
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    37
          | left#s => if left then (True ## dl a s) Un
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    38
                                   (if fl s & a=None then {False#qr} else {})
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    39
                              else False ## dr a s,
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    40
    %s. case s of [] => False | left#s => ~left & fr s)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    41
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    42
 star :: 'a bitsNAe => 'a bitsNAe
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    43
"star == %(q,d,f).
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    44
   ([],
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    45
    %a s. case s of
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    46
            [] => if a=None then {True#q} else {}
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    47
          | left#s => if left then (True ## d a s) Un
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    48
                                   (if f s & a=None then {True#q} else {})
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    49
                              else {},
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    50
    %s. case s of [] => True | left#s => left & f s)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    51
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    52
consts rexp2nae :: 'a rexp => 'a bitsNAe
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    53
primrec rexp2nae rexp
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    54
"rexp2nae Empty      = ([], %a s. {}, %s. False)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    55
"rexp2nae(Atom a)    = atom a"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    56
"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    57
"rexp2nae(Conc r s)  = conc  (rexp2nae r) (rexp2nae s)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    58
"rexp2nae(Star r)    = star  (rexp2nae r)"
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    59
0eb6730de30f Reshuffeling, renaming and a few simple corollaries.
nipkow
parents:
diff changeset
    60
end