Re: [isabelle] Implicit structure argument



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.

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.


	Makarius


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