Re: [isabelle] "defines" in a locale
Thanks Andreas. I ended up doing this.
> On 25 Jan 2016, at 16:53, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
> 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"
> sublocale l "f b" apply(unfold_locales) sorry
> Hope this helps,
> On 25/01/16 05:41, Peter Gammie wrote:
>> 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.
>> theory l
>> imports Main
>> locale l =
>> fixes a
>> assumes "P a"
>> locale m = l +
>> fixes b
>> (* assumes âP bâ *)
>> defines "a == b"
This archive was generated by a fusion of
Pipermail (Mailman edition) and