Re: [isabelle] "defines" in a locale



Hi Peter,

"defines" used to work like this until around 2008. Since then, it does not really make sense to use "defines" in a locale because you still have to provide the defined parameter in the instantiations. Normally, sublocales work much better.

consts P :: "'a â bool"
consts Q :: "'a â bool"
consts f :: "'a â 'a"

locale l =
  fixes a
  assumes "P a"

locale m =
  fixes b
  assumes "Q b"
begin

sublocale l "f b" apply(unfold_locales) sorry

end

Hope this helps,
Andreas

On 25/01/16 05:41, Peter Gammie wrote:
Hi,

Is this supposed to work? Iâm guessing not. The error that arises is not very good (for recent repository versions and 2016-RC2).

In my actual use-case I assume âQ bâ where Q implies P, and the definition is non-trivial. As a syntactic nicety I donât want to have to provide âaâ when I instantiate locale m. I can make this work for now by saying: assumes âa = bâ but it is ugly.

cheers,
peter

theory l
imports Main
begin

locale l =
   fixes a
   assumes "P a"

locale m = l +
   fixes b
   (* assumes âP bâ *)
   defines "a == b"

end





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