Re: [isabelle] Locale import
I want to import a locale A into a locale B such that one of A's
parameters is replaced by a fixed parameter of B applied to an
arbitrary value. Here's a short example what I would like to write:
locale A =
fixes f :: "'a"
locale B = A "g b"
for g :: "'b => 'a"
I am not sure what your ultimate goal is, and I don't see what
semantics of b should be here. Locale parameters are "arbitrary but
fixed". I don't know what "arbitrary and not fixed" should mean when
it comes to applying the module in another context.
However, Isabelle complains at B's declaration that b is an illegal
free variable. Adding b to the for clause is no solution to my problem,
because this fixes b. I am currently doing the following:
locale B = fixes g :: "'b => 'a"
assumes A: "A (g b)"
sublocale B < A "g b"
Although this works for the moment, I am not happy with this solution:
I can only use definitions from A in the other assumptions of B via
their full name with all parameters explicitly provided.
The declaration of B is still strange and should probably be rejected.
Don't rely on this in future version of Isabelle.
What is the best way to import A in B?
Since both declarations of B are "strange" this question is not well-defined.
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and