Email Gateway (Aug 18 2022 at 10:38): Email Gateway (Aug 18 2022 at 10:38):From: Dimitrios Vytiniotis <dimitriv@cis.upenn.edu>
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
Email Gateway (Aug 18 2022 at 10:38):From: Steven Obua <obua@in.tum.de>
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
Last updated: May 03 2024 at 12:27 UTC