[isabelle] Abbreviations in locales



Hi all,

I have a problem/question how abbreviations in locales are handled.
Regard the following toy example:

locale foo =
  fixes a :: 'a
begin
  abbreviation "f == (a,a,a)"
end

locale bar1 = s1!: foo a for a
begin
  term "s1.f" -- printed as s1.f
end


locale bar2 = s1!: foo b for b
begin
  term "s1.f" -- printed as (b,b,b)
end


Why is the abbreviation in the second case valid input syntax, but not
pretty-printed in output? And how can I change this behaviour, towards
also using the abbreviation in the output?

A similar problem arises when interpreting the locales. 
After interpretation bar2 c (for constant c), the abbreviation "s1.f"
only works as input.


The current behaviour is somewhat strange, as it depends on the
conincidence of the parameter name in the locale expression 
"s1!: foo a for a" and the fixed variable name "a" that was used when
declaring the locale.


In my concrete example, I use quite a lot of abbreviations, and one gets
easily confused if one always sees them expanded in the output. Concrete
example: "s1.lookup" vs. "map_op_lookup ops1"


Thanks in advance for any help/hints 
  Peter








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