[isabelle] Polymorphic parameter in locales



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

--
- ------------------------------------------------------------------
Ewaryst Schulz                        office @ Universität Bremen:
Junior Researcher                     Cartesium 2.049
Safe and Secure Cognitive Systems     Enrique-Schmidt-Str. 5
DFKI-Lab Bremen                       FB3 Mathematik - Informatik
Robert-Hooke-Str. 5                   Universität Bremen
D-28359 Bremen                        P.O. Box 330 440
                                     D-28334 Bremen
phone: (+49) 421-218-64274            Fax:   (+49) 421-218-9864274
mail: Ewaryst.Schulz at dfki,de
www.dfki.de/sks/staff/ewschulz
------------------------------------------------------------------


-------------------------------------------------------------
Deutsches Forschungszentrum für Künstliche Intelligenz GmbH
Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern

Geschäftsführung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------







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