|
4832
|
1 |
(* Title: HOL/Lex/RegExp.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
|
|
|
6 |
Regular expressions
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
RegExp = RegSet +
|
|
|
10 |
|
|
|
11 |
datatype 'a rexp = Empty
|
|
|
12 |
| Atom 'a
|
|
|
13 |
| Union ('a rexp) ('a rexp)
|
|
|
14 |
| Conc ('a rexp) ('a rexp)
|
|
|
15 |
| Star ('a rexp)
|
|
|
16 |
|
|
|
17 |
consts lang :: 'a rexp => 'a list set
|
|
5184
|
18 |
primrec
|
|
4832
|
19 |
lang_Emp "lang Empty = {}"
|
|
|
20 |
lang_Atom "lang (Atom a) = {[a]}"
|
|
|
21 |
lang_Un "lang (Union el er) = (lang el) Un (lang er)"
|
|
|
22 |
lang_Conc "lang (Conc el er) = RegSet.conc (lang el) (lang er)"
|
|
|
23 |
lang_Star "lang (Star e) = RegSet.star(lang e)"
|
|
|
24 |
|
|
|
25 |
end
|