# [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.*