src/HOL/Lex/RegExp2NAe.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp2NAe.thy	Fri May 08 18:33:29 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      HOL/Lex/RegExp2NAe.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Conversion of regular expressions
+into nondeterministic automata with epsilon transitions
+*)
+
+RegExp2NAe = NAe + RegExp +
+
+types 'a bitsNAe = ('a,bool list)nae
+
+syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
+translations "x ## S" == "op # x `` S"
+
+constdefs
+ atom  :: 'a => 'a bitsNAe
+"atom a == ([True],
+            %b s. if s=[True] & b=Some a then {[False]} else {},
+            %s. s=[False])"
+
+ union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+"union == %(ql,dl,fl)(qr,dr,fr).
+   ([],
+    %a s. case s of
+            [] => if a=None then {True#ql,False#qr} else {}
+          | left#s => if left then True ## dl a s
+                              else False ## dr a s,
+    %s. case s of [] => False | left#s => if left then fl s else fr s)"
+
+ conc :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+"conc == %(ql,dl,fl)(qr,dr,fr).
+   (True#ql,
+    %a s. case s of
+            [] => {}
+          | left#s => if left then (True ## dl a s) Un
+                                   (if fl s & a=None then {False#qr} else {})
+                              else False ## dr a s,
+    %s. case s of [] => False | left#s => ~left & fr s)"
+
+ star :: 'a bitsNAe => 'a bitsNAe
+"star == %(q,d,f).
+   ([],
+    %a s. case s of
+            [] => if a=None then {True#q} else {}
+          | left#s => if left then (True ## d a s) Un
+                                   (if f s & a=None then {True#q} else {})
+                              else {},
+    %s. case s of [] => True | left#s => left & f s)"
+
+consts rexp2nae :: 'a rexp => 'a bitsNAe
+primrec rexp2nae rexp
+"rexp2nae Empty      = ([], %a s. {}, %s. False)"
+"rexp2nae(Atom a)    = atom a"
+"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Conc r s)  = conc  (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Star r)    = star  (rexp2nae r)"
+
+end