Re: [isabelle] Defines in locales in Isabelle 2009



On Wed, Apr 22, 2009 at 10:07 AM, Clemens Ballarin <ballarin at in.tum.de>wrote:

> Quoting Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>:
>
>  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"]
>>
>
> The feature that defined parameters may be omitted in interpretation has
> been withdrawn in an attempt to make defines more similar to assumes.


So what (if any) is the difference between "defines" and "assumes" now? It
seems that with the current locale package, locale "foo" might as well be
defined as below, with "assumes xs_def". Am I missing something?

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

- Brian




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