Re: [isabelle] Locale import



Hi Andreas,

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"
  assume "f"

locale B = A "g b"
  for g :: "'b => 'a"
  assumes ...

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)"
  and ...

sublocale B < A "g b"
  for b
by(rule A)

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.)

Best regards,

Clemens







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