[isabelle] splicing out part of HOL function space and non-uniform definitions
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and