*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Defining an operation on a particular set and arguments of the definition command*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 24 Jul 2016 18:03:37 +0200*In-reply-to*: <99dc87e67607bfd483ae2ee2671a634b@cam.ac.uk>*References*: <99dc87e67607bfd483ae2ee2671a634b@cam.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

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**

**References**:**[isabelle] Defining an operation on a particular set and arguments of the definition command***From:*J.V. Paiva-Miranda-De-Siqueira

- Previous by Date: Re: [isabelle] Printing full ML output in Isabelle/jEdit
- Next by Date: Re: [isabelle] Eisbach match drule
- Previous by Thread: [isabelle] Defining an operation on a particular set and arguments of the definition command
- Next by Thread: [isabelle] Plugin error with Isabelle-2016
- Cl-isabelle-users July 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list