Re: [isabelle] "defines" in a locale



Thanks Andreas. I ended up doing this.

cheers,
peter

> 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"
> 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
>> 

-- 
http://peteg.org/





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