| author | urbanc |
| Thu, 28 Jul 2011 17:52:36 +0000 | |
| changeset 180 | b755090d0f3d |
| parent 170 | b1258b7d2789 |
| child 203 | 5d724fe0e096 |
| permissions | -rw-r--r-- |
|
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 |
|
|
b1258b7d2789
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
urbanc
parents:
diff
changeset
|
19 |
primrec lang :: "'a rexp => 'a list set" where |
|
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 |