Re: [isabelle] Locale import
I think this is similar to what I wanted to do. (You can try reading my earlier email to this list but it is nowhere as clear as yours is.)
I have a question for you and a suggestion for the locale implementors. Please excuse my top posting: your context is important.
How do you expect to later instantiate 'c'?
I overcame my parameterisation problem by rewriting the locale as a record (of variables that were 'fixes' in the locale) and a predicate (capturing the locale assumptions). I suggest the locale mechanism be extended to do this, in addition to whatever it now does. Concretely, imagine:
locale A =
fixes f :: "''c => 'c"
fixes g :: "'c => 'c"
assumes "P f"
assumes "Q g"
definition "h = f o g"
lemma HX: "h x = f (g x)" ...
Could the locale mechanism produce extra definitions of the form:
record 'c A_fixes =
f :: "'c => 'c"
g :: "'c => 'c"
(* captures "fixes" *)
A_pred :: "'c A_fixes => bool"
(* captures the two "assumes" *)
"A_h :: 'c A_fixes => 'c => 'c"
lemma A_HX: "A_pred A ==> h x = f (g x)"
The idea is to shift from the curried form where external definitions capture only the locale-fixed variables used in the expression to an uncurried form where the record aggregates all locale-fixed variables. I intend this to be a purely syntactic matter.
This idea is essentially the same as using records to simulate type classes in Haskell, sometimes termed an evidence-passing translation. This implies it might have typing implications (viz require higher-ranked polymorphism) but I'm yet to run into any.
In my case I would get the benefit of being able to state things in the locale conveniently and later uniformly abstract at the term level using the record-based external definitions.
I admit I have no deep understanding of locales, so there is a good chance this proposal stumbles on some key matter.
On 17/02/2010, at 6:26 PM, Andreas Lochbihler wrote:
> probably my example was too reduced to convey my problem, so I try again with a (hopefully better) example.
> Suppose we have two locales A and B that are independent of each other:
> locale A =
> fixes f :: "'a => 'b"
> assumes ...
> definition foo where "foo = ... f ..."
> lemma bar: "P foo" sorry -- "P is some property"
> locale B =
> fixes g :: "'c => 'a => 'b"
> assumes ...
> Now, I want to combine both A and B in a new locale C such that A's parameter f is instantiated with B's parameter g applied to any value.
> locale C = B +
> assumes A: "A (g c)"
> and Q: "Q g c (A.foo (g c))" -- "Q is some predicate"
> sublocale C < A "g c" for c by(rule A)
> In context C, the sublocale introduces an abbreviation foo for
> "%c. A.foo (g c)"
> and the inherited lemma bar from locale A is now
> "P (foo c)" where c is a free variable.
> This is what I want to achieve. Two things are unsatisfactory here:
> 1. I mention a locale predicate as an assumption of a locale instead of properly importing it. The first step after the locale declaration is to change the locale graph to include this import.
> 2. The assumption Q in locale C involves a constant defined in A. Since I do not know how to add A to the import list, I must resort to the global constant A.foo. In my real case, A (and B) have a lot more fixed parameters and writing all of them makes the assumptions hard to read.
> I hope that this illustrates better what I am trying to achieve: In locale C, I want to use everything from locale A with f instantiated by "g c", where I can use a different c each time.
> Is there a better way to achieve something like this?
> I do not want to change locale A because I need to interpret it elsewhere with parameters that only take one argument.
>> Possibly you want to redeclare syntax for definitions that was disabled since inherited through a non-identical morphism (cf. Section 6 of the tutorial, immediately before Section 6.1 starts.)
> No, this has nothing to do with syntax declarations for constants, but with the abbreviations introduced by the locales.
> Best regards,
> Karlsruher Institut für Technologie
> IPD Snelting
> Andreas Lochbihler
> wissenschaftlicher Mitarbeiter
> Adenauerring 20a, Gebäude 50.41, Raum 023
> 76131 Karlsruhe
> Telefon: +49 721 608-8352
> Fax: +49 721 608-8457
> E-Mail: andreas.lochbihler at kit.edu
> KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft
This archive was generated by a fusion of
Pipermail (Mailman edition) and