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.