Email Gateway (Aug 22 2022 at 13:50): Email Gateway (Aug 22 2022 at 13:50):From: "J.V. Paiva-Miranda-De-Siqueira" <jvp27@cam.ac.uk>
Dear Isabelle Users,
I'm a mathematician recently introduced to Isabelle, and am working on a
certain theory
requiring the usage of locales. I ran into a problem while trying to
define operations on
a certain set, which I want to be recognized as an instance of a locale
"Ring" of an imported
theory.
This set is named "stalk x", where x is a parameter, i.e, I have stalk::
"'a ⇒( ('a set × 'a) set) set"
where "stalk x = {germ x U s |U s. (U,s) ∈ prestalk x}" (here prestalk
is of type "'a ⇒('a set × 'a) set"
and germ is of type "'a ⇒ 'a set ⇒ 'a ⇒ ('a set × 'a) set").
I'm trying to have stalk x as the carrier of a ring, so I need to define
operations and thus
attempted the following:
definition stalk_pop :: "'a ⇒ [('a set × 'a) set , ('a set × 'a) set]
⇒ ('a set × 'a) set " where
"stalk_pop x (germ x U s) (germ x V t) = germ x (U∩V)
( (restrictionsmap (U, U∩V) s)±⇘objectsmap (U∩V)⇙
(restrictionsmap (V, U∩V) t)) "
The RHS seems to be correct, but the definition command complains about
the arguments on the LHS
(the germs, namely). I can't define this operation for everything of
type [('a set × 'a) set , ('a set × 'a) set]
in a way it reduces to what I want (the RHS) over stalk x and nothing
here is recursively defined.
Is there a good way to define this operation strictly over ('a set × 'a)
sets of the form germ x U s?
Thanks for your time and pardon the potentially silly question.
Sincerely,
José Siqueira
Email Gateway (Aug 22 2022 at 13:51):From: Tobias Nipkow <nipkow@in.tum.de>
The "definition" command allows only variables on the lhs. You can use the
"function" command instead. But there is no free lunch. This will generate two
kinds of subgoals:
that all cases have been covered; in your case you haven't. HOL functions are
total; in the worst case you can return the value "undefined" in all other cases.
that cases involving non-patterns make sense; in your case: are independent of
the choices of x U s, x V t.
For details see "Defining Recursive Functions in Isabelle/HOL".
Tobias
smime.p7s
Last updated: Apr 25 2024 at 16:19 UTC