Re: [isabelle] Implicit structure argument



Am 02.04.2013 16:55, schrieb Makarius:
> On Thu, 14 Mar 2013, René Neumann wrote:
> 
>> I have problems declaring something as "(structure)", when it is not a
>> locale parameter (Isabelle2012 is used). Take the following example:
>>
>> definition adj :: "'a set ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40)
>> where "
>>  adj G v w ≡ v ∈ G ∧ v = w"
>>
>> locale Foo =
>>  fixes G :: "'a set" (structure)
>>
>> locale Bar =
>>  fixes s :: "'a"
>> begin
>> definition "s_G = {s}"
>> end
>>
>> sublocale Bar ⊆ Foo s_G by unfold_locales
>>
>>
>>
>> In the context 'Bar' I'd like to use "v → w", but I can't as s_G is not
>> marked as an implicit structure. I then tried (in context Bar)
>>
>> notation s_G (structure)
>>
>> From reading the documentation, this should be legal, but it yields:
>>
>> *** Bad mixfix declaration for "local.s_G"
>>
>> I appreciate any useful hints to make s_G the implicit structure
>> argument.
> 
> The implicit structure notation is only available for locale parameters.
> 
> Can you point to the place in the documentation where it is suggested
> otherwise?  The only place I see in Isabelle2012 isar-ref is section
> 5.6.2 about the 'fixes' of locale declarations.

Section 7.3: notation goes with a 'struct_mixfix'. (Ironically, the
nonterminal 'fixes' (p. 82) does not support "(structure)" according to
the diagram given).

> I can't say on the spot if it is feasible to make implicit structures
> more general -- they have been a bit on retreat in recent years, and are
> now a bit old-fashioned anyway.

But there is no replacement, is there?

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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