# [isabelle] Proving something is an instance of a locale

Dear Isabelle Users,

`I seem to be missing something while trying to show a certain
``construction is a Ring (a locale in an imported theory).
`
I defined all the necessary operations and this
definition stalk_ring :: "'a â ('a set Ã 'a) set Ring" where
"stalk_ring x =
âcarrier = stalk x,
pop = stalk_pop x,
mop = stalk_mop x,
zero = stalk_zero x,
tp = stalk_tp x,
un = stalk_un xâ"

`which should give me a Ring stalk_ring x for each x. I then tried to
``show it's a ring, but have been unable to show any of the subgoals after
``writing
`
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
`
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? 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. 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.
`

`I'm a mathematician recently introduced to Isabelle, so I'd appreciate
``any orientation on the matter.
`
Sincerely,
JosÃ Siqueira

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