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