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



Dear all,
I have come accross the following situation. I have a formalization of
parametricity for an extension of System F in Isabelle/HOL, where types
are interpreted as relations between terms. We have:

types rel  = "(tm×tm) set"
consts Interpret :: "ty => substitution => rel"

And Interpret takes a type (ty) and an environment (substitution) and
returns a relation (rel). Its definition is just a recdef.

[Please excuse my dependent types notation below but that's the way I
started thinking about it.] What I want to do is the following.
Given a type for kinds:

datatype kind = Star | Fun kind kind

I want to define a *type* that I call rel(k) so that:
  rel(Star)      = rel
  rel(Fun k1 k2) = rel(k1) => rel(k2)

That is, I want "rel(Fun k1 k2)" to mean the set of all HOL functions
from "rel(k1)" to "rel(k2)". And finally I want Interpret to have
the pseudo-type:

Interpret :: (k:kind) => ty => substitution => rel(k)

So, modulo dependent types notation, what I really really want
is temporarily go to some common type that I can give to the
"rel(k)" above, call it  GeneralizedRel, so that Interpret returns one
of these. So the real type of Interpret would be:
   kind => ty => substitution => GeneralizedRel
and I would hopefully be able to prove the extra dependencies with
the help of some lemmas.

Is is known how can one do something like that in Isabelle/HOL? I am not
particularly attached to the style of definitions (recursive functions
vs. inductive relations) so any suggestions and ideas are very
welcome.

Thanks!
--dimitris





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