Re: [isabelle] Defining an operation on a particular set and arguments of the definition command



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

On 24/07/2016 11:28, J.V. Paiva-Miranda-De-Siqueira wrote:
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




Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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