[isabelle] Defines in locales in Isabelle 2009



Hi all,

I am currently converting my theories to Isabelle 2009 and stumbled across the following problem with locales:

In Isabelle 2008, things like the following worked very well:

locale foo =
  fixes x :: "'a => 'a => bool"
  and y :: "'a => 'a => bool"
  and P :: "'a => bool"
  and xs :: "'a => 'a => bool" ("_ ->* _")
  defines xs_def: "xs == (%a b. x a b & y a b)^**"
  assumes "a ->* b ==> P b"

interpretation f: foo["%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
                      "%a.True"]
apply(simp)
apply(unfold_locales)
apply(rule TrueI)
done


Here, I use the defines feature to introduce an abbreviation and notation for some complex term which can then be used to state the assumptions. Inside the locale, the defined parameter behaves like a definition whereas when interpreting these locales, these definitions are automatically unfolded.

If I try to do this to Isabelle 2009, everything seems to break. The locale definition works as before, but interpreting foo is terrible:

1st try:

interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
                      "%a.True"

This does not work because the defined parameter is not instantiated, but left as a free variable, which must be shown equal to the definition of xs in the locale.

2nd try:

interpretation f: foo "%a b. a > 0 & b <= Suc 0" "%a b. a < 10"
                      "%a. True"
                      "(%a b. a > 0 & b <= Suc 0 & a < 10)^**"

Now the explicit parameter is given, but unfold_locales nor intro_locales longer work any longer (empty result sequence). It seems that I have to prove the interpretation manually by (rule foo.intro, simp_all).


- Can I still do this trick of having parameters defined in a locale declaration that are unfolded automatically for all interpretations and that can be used in the assumptions (with additional syntax)? - How must interpretations be written such that such defined parameters need not be specified?
- Why do unfold_locales/intro_locales not work here? What else should I use?


Regards,
Andreas Lochbihler





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