4907
|
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 |
|
8732
|
10 |
RegExp2NAe = RegExp + NAe +
|
4907
|
11 |
|
|
12 |
types 'a bitsNAe = ('a,bool list)nae
|
|
13 |
|
|
14 |
syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
|
10834
|
15 |
translations "x ## S" == "Cons x ` S"
|
4907
|
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
|
5184
|
53 |
primrec
|
4907
|
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
|