author | immler |
Sun, 03 Nov 2019 21:46:46 -0500 | |
changeset 71034 | e0755162093f |
parent 65449 | c82e63b11b8b |
child 76213 | e44d86131648 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Coind/Language.thy |
2 |
Author: Jacob Frost, Cambridge University Computer Laboratory |
|
915 | 3 |
Copyright 1995 University of Cambridge |
4 |
*) |
|
5 |
||
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
60770
diff
changeset
|
6 |
theory Language imports ZF begin |
915 | 7 |
|
8 |
||
60770 | 9 |
text\<open>these really can't be definitions without losing the abstraction\<close> |
41779 | 10 |
|
11 |
axiomatization |
|
12 |
Const :: i and (* Abstract type of constants *) |
|
13 |
c_app :: "[i,i] => i" (* Abstract constructor for fun application*) |
|
14 |
where |
|
15 |
constNEE: "c \<in> Const ==> c \<noteq> 0" and |
|
12595 | 16 |
c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const" |
915 | 17 |
|
18 |
||
19 |
consts |
|
1478 | 20 |
Exp :: i (* Datatype of expressions *) |
21 |
ExVar :: i (* Abstract type of variables *) |
|
6112 | 22 |
|
23 |
datatype |
|
12595 | 24 |
"Exp" = e_const ("c \<in> Const") |
25 |
| e_var ("x \<in> ExVar") |
|
26 |
| e_fn ("x \<in> ExVar","e \<in> Exp") |
|
27 |
| e_fix ("x1 \<in> ExVar","x2 \<in> ExVar","e \<in> Exp") |
|
28 |
| e_app ("e1 \<in> Exp","e2 \<in> Exp") |
|
915 | 29 |
|
30 |
end |