Re: [isabelle] Implicit structure argument



Anyone an idea?

I now introduced an auxiliary locale:

locale Bar' = Bar +
  fixes G (structure)
  defines "G == s_G"

and will do all the work then in context Bar'.

But this looks hacky.

- René

Am 14.03.2013 14:21, schrieb René Neumann:
> Hi,
> 
> 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.
> 
> Thanks,
> 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.