Email Gateway (Aug 22 2022 at 13:55): Email Gateway (Aug 22 2022 at 13:55):From: Lars Hupel <hupel@in.tum.de>
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_localesalthough 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_localesand 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
Email Gateway (Aug 22 2022 at 13:57):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:59):From: "J.V. Paiva-Miranda-De-Siqueira" <jvp27@cam.ac.uk>
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
Last updated: Nov 21 2024 at 12:39 UTC