| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 07 Aug 2012 16:55:17 +0100 | |
| changeset 3195 | deef21dc972f |
| parent 3084 | faeac3ae43e5 |
| permissions | -rw-r--r-- |
|
3084
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Sigma |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
imports Nominal2 |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
nominal_datatype obj = |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
Var name |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
| Obj smlst |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
| Inv obj string |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
| Upd obj string method |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
and smlst = |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
SMNil |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
| SMCons string method smlst |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
and method = |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
Sig n::name o::obj binds n in o |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
|
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
end |
|
faeac3ae43e5
Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |