Re: [isabelle] Proving something is an instance of a locale



Hi JosÃ,

> Sorry for the delay, it seems I was missing a hypothesis in my locale
> declaration (presheaf) and after adding
> that I spent some time trying to make it work using your suggestion, to
> no avail (although it's certainly progress).

did you mean to reply to the list instead of privately?

> I've attached all the relevant theories. The one I'm building is
> "Sheaves.thy", while the locale "Ring"
> is declared in "Algebra4.thy". It still says "objectsmap_def" is an
> undefined fact, by the way.

The reason is that "objectsmap" is not a definition.

If you use a definitional package in Isabelle, for example, "fun",
"inductive", or plain old "definition", you will get a constant (e.g.
"x") and an accompanying theorem "x_def".

If you however introduce a parameter in a locale (as you did in the
"presheaf" locale), there is no such theorem. You can only use the
assumptions of the locale.

Cheers
Lars




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