# 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"
begin
typedecl tm

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

` "TM_rep = (SOME f. inj_on f (explode TM) \<and> (UNIV :: tm set) =
``image f (explode TM))"
`
lemma "inj_on TM_rep (explode TM)"
sorry
lemma "(UNIV :: tm set) = image TM_rep (explode TM)"
sorry
datatype kind = Star | F kind kind
fun rel :: "kind \<Rightarrow> ZF"
where
"rel Star = CartProd TM TM"
| "rel (F a b) = Fun (rel a) (rel b)"
end
------------------------------------------------------------------------------

`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.
`
Steven

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