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



Dear JosÃ,

> I seem to be missing something while trying to show a certain
> construction is a Ring (a locale in an imported theory).

could you maybe point us to the theory file where this is defined? It
would make helping you solve your problem much easier. (The answers
below are speculations because I don't know the details.)

> lemma stalk_set_is_ring:
> assumes P: "x ââT"
> shows "Ring (stalk_ring x)"
> proof unfold_locales
> 
> although at least most of them must be trivial (I built this ring out of
> an existing one). There must be a gap in my understanding of this
> process, since I tried to prove this apparently trivial

Where exactly did you get stuck? This looks at least like the correct
lemma statement.

> lemma (in presheaf) objecstmapringvalued:
> assumes L: "(U:: 'a set) â T"
> shows "Ring (objectsmap U)"
> proof unfold_locales
> 
> and failed. This should show for each U that objectsmap U is a Ring, and
> here objectsmap :: "'a set â ('a, 'm) Ring_scheme" is one of the
> parameters of the locale presheaf, so wouldn't that be immediate since
> the last type is ('a,'m) Ring_schemes?

Again, this is hard to say without seeing the "Ring" locale. There could
be additional assumptions you have to show.

> I also noticed that although I
> can invoke presheaf_axioms and presheaf_def, I can't directly use
> something like the definition of objectsmap itself in a proof.

How so? There should be a theorem called "objectsmap_def" if
"objectsmap" is a regular "definition". You can unfold that using "apply
(subst objectsmap_def)" or "unfolding objectsmap_def".

> I'm still not sure about how to tell Isabelle to use an instance of the ring
> axioms or theorems for a particular ring during a proof -- in my
> situation, for example, all the new ring operations are built out of
> those of rings objectsmap U, so it would be great to invoke facts for such.

You can use the command "interpret" in a proof to obtain the facts for
an existing structure, like so:

  interpret xyz: Ring "other_structure"

... then, if there's an assumption "abc" in the "Ring" locale, you can
access that via "xyz.abc". See the locale manual for more details on
this process.

Cheers
Lars




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