Re: [isabelle] splicing out part of HOL function space and non-uniform definitions

I don't think what you want is possible in Isabelle/HOL.

Nevertheless, a workaround could be to take the type GeneralizedRel as the type of all Zermelo-Fraenkel sets,
which is available in Isabelle/HOL in the theory HOL/ZF/MainZF:

theory recty
imports "~~/src/HOL/ZF/MainZF"

typedecl tm

axioms tm_representable: "\<exists> f z. (UNIV :: tm set) = image f (explode z)"

 "TM = (SOME z. (\<exists> f. (UNIV :: tm set) = image f (explode z)))"

"TM_rep = (SOME f. inj_on f (explode TM) \<and> (UNIV :: tm set) = image f (explode TM))"

lemma "inj_on TM_rep (explode TM)"

lemma "(UNIV :: tm set) = image TM_rep (explode TM)"

datatype kind = Star | F kind kind

fun rel :: "kind \<Rightarrow> ZF"
 "rel Star = CartProd TM TM"
| "rel (F a b) = Fun (rel a) (rel b)"


Here the axiom tm_representable is something which you could probably show for your terms (your terms should be countable?)

Of course, you would not exactly be working in pure type theory anymore :-)

The above is just a rough scetch, should you consider this option don't hesitate to contact me with any further comments/questions.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.