Email Gateway (Aug 18 2022 at 14:07): Email Gateway (Aug 18 2022 at 14:07):From: Ewaryst Schulz <ewaryst.schulz@dfki.de>
Hi,
is it possible in Isabelle 2009 to define local theories which can
handle polymorphic function-parameters whose type-variables aren't fixed
in the body of the local theory?
As what I understood reading the paper local theory specifications in
Isabelle/Isar it is not possible to do that, because Isabelle doesn't
support type quantification.
But perhaps there is another way to solve my problem, I don't know. All
what I want is to be able to outsource some part of my theory which will
be reused in many other theories (it's just a modularization/reuse issue).
Consider the following theory:
theory T
...
consts
my_subt :: "'a => 'b => bool"
... other consts ...
axioms
type_transitive:
"ALL (x :: 'a).
ALL (y :: 'b).
ALL (z :: 'c). (my_subt x y) & (my_subt y z) --> (my_subt x z)"
... other axioms ...
lemma my_type_lemma1: "... my_subt x y ..."
...
lemma my_type_lemmaN: "..."
... other lemmas ...
I would like to move the type lemmas into a locale and interpret the
locale in theory T with the my_subt const:
theory L
locale subtype =
fixes
subt :: "'a => 'b => bool"
assumes
trans :
"ALL (x :: 'a) (y :: 'b) (z :: 'c). subt x y & subt y z --> subt x z"
begin
lemma type_lemma1: "... subt x y ..."
...
lemma type_lemmaN: "..."
...
theory T
imports L ...
...
consts
my_subt :: "'a => 'b => bool"
... other consts ...
axioms
type_transitive:
"ALL (x :: 'a).
ALL (y :: 'b).
ALL (z :: 'c). (my_subt x y) & (my_subt y z) --> (my_subt x z)"
... other axioms ...
interpretation of locale subtype by my_subt
now I want type_lemma1 until type_lemmaN to be accessible for subt
substituted by my_subt
... other lemmas ...
The main problem is that in the locale subtype the signature of the
parameter subt is fixed, i.e., I get an typing error in
the assumption trans, because subt is used there with the 3 type-signatures:
subt :: "'a => 'b => bool"
subt :: "'b => 'c => bool"
subt :: "'a => 'c => bool"
Isabelle tries to match 'a with 'b and 'b with 'c and gets a clash.
Any suggestions or workarounds?
I have in addition the constraint that I can't remove the const
declaration of my_subt and its axioms from theory T because it's
auto-generated in my scenario. Otherwise I wouldn't have to use an
interpretation, but just the usual import mechanism.
Thank you in advance,
cheers,
Ewaryst
Email Gateway (Aug 18 2022 at 14:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Ewaryst,
perhaps theory interpretation is something suitable for your problem;
see http://www.informatik.uni-bremen.de/~cxl/awe/.
Hope this helps
Florian
signature.asc
Last updated: Apr 19 2024 at 20:15 UTC