Re: [isabelle] Why do some abbreviations become "abbreviatees" inside locales?



On Sun, 23 Aug 2009, Andrei Popescu wrote:

I do not understand the following behavior of abbreviations inside locales:

locale dummy = fixes F::'a

context dummy begin
  abbreviation G :: 'a where "G == id F"
  term "id F" term G  (* OK  *)
  (*   *)
  definition F1::nat where "F1 == 7"
  abbreviation G1 :: nat where "G1 == F1"
  term F1 term G1  (* OK *)
  (*   *)
  definition F2::nat where "F2 == 7"
  abbreviation G2 :: nat where "G2 == id F2"
  term "id F2" term G2  (* ? *)
end

Why doesn't "G2" abbreviate "id F2" inside "dummy"?  It appears that, to the contrary, "id F2" abbreviates "G2". (This is not the case of "G" and "G1",  however, which do behave as I would expect. )   

The abbreviation "G2 == id F2" expands correctly, but printing produces an unexpected result. The reason for this is an extra indirection in F2, which is also associated with an internal abbreviation, because it is a constant inside a locale target (even though it does not depend on any locale parameters).

You can inspect the internals like this:

  ML {* set long_names *}
  print_abbrevs

The print mechanism folds "local.F2 == Scratch.dummy.F2" first, so "Scratch.dummy.G2 == Fun.id Scratch.dummy.F2" cannot be folded anymore.

Folding abbreviations that depend on each other is a bit unpredictable in general. The abbreviation mechanism could be a bit smarter in its strategy, but some uncertainty would always remain.


	Makarius


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