J.V. Paiva-Miranda-De-Siqueira

2016-08-01 09:47:17 UTC

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

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