170
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
2 |
Copyright 1998 TUM
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
3 |
*)
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
4 |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
5 |
header "Regular expressions"
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
6 |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
7 |
theory Regular_Exp
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
8 |
imports Regular_Set
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
9 |
begin
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
10 |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
11 |
datatype 'a rexp =
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
12 |
Zero |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
13 |
One |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
14 |
Atom 'a |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
15 |
Plus "('a rexp)" "('a rexp)" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
16 |
Times "('a rexp)" "('a rexp)" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
17 |
Star "('a rexp)"
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
18 |
|
203
|
19 |
primrec lang :: "'a rexp => 'a lang" where
|
170
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
20 |
"lang Zero = {}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
21 |
"lang One = {[]}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
22 |
"lang (Atom a) = {[a]}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
23 |
"lang (Plus r s) = (lang r) Un (lang s)" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
24 |
"lang (Times r s) = conc (lang r) (lang s)" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
25 |
"lang (Star r) = star(lang r)"
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
26 |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
27 |
primrec atoms :: "'a rexp \<Rightarrow> 'a set"
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
28 |
where
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
29 |
"atoms Zero = {}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
30 |
"atoms One = {}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
31 |
"atoms (Atom a) = {a}" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
32 |
"atoms (Plus r s) = atoms r \<union> atoms s" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
33 |
"atoms (Times r s) = atoms r \<union> atoms s" |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
34 |
"atoms (Star r) = atoms r"
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
35 |
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
36 |
end
|