1(* Title: ZF/Coind/Language.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4*) 5 6theory Language imports ZF begin 7 8 9text\<open>these really can't be definitions without losing the abstraction\<close> 10 11axiomatization 12 Const :: i and (* Abstract type of constants *) 13 c_app :: "[i,i] => i" (* Abstract constructor for fun application*) 14where 15 constNEE: "c \<in> Const ==> c \<noteq> 0" and 16 c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const" 17 18 19consts 20 Exp :: i (* Datatype of expressions *) 21 ExVar :: i (* Abstract type of variables *) 22 23datatype 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") 29 30end 31