Re: [isabelle] Locale import



Andreas,

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"
begin

definition "h = f o g"

lemma HX: "h x = f (g x)" ...

end

Could the locale mechanism produce extra definitions of the form:

record 'c A_fixes =
 f :: "'c => 'c"
g :: "'c => 'c"
(* captures "fixes" *)

definition
  A_pred :: "'c A_fixes => bool"
(* captures the two "assumes" *)

definition
 "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.

cheers
peter

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 ...
> begin
> definition foo where "foo = ... f ..."
> lemma bar: "P foo" sorry -- "P is some property"
> end
> 
> 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,
> Andreas
> 
> -- 
> 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
> http://pp.info.uni-karlsruhe.de
> KIT - Universität des Landes Baden-Württemberg und nationales Großforschungszentrum in der Helmholtz-Gemeinschaft
> 

-- 
http://peteg.org/






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