Stream: Beginner Questions

Topic: local infix operator definition

Naso (Jul 21 2023 at 01:36):

Is this possible in Isabelle? Like in Haskell we can write (+) a b = myfun a b and use it as a + b within a local scope.

Lukas Stevens (Jul 21 2023 at 07:45):

You can introduce notation with the notation command

Lukas Stevens (Jul 21 2023 at 07:46):

notation myfun (infixl "+" 50)

Wolfgang Jeltsch (Jul 21 2023 at 15:58):

Unlike with Haskell, you even can introduce notation locally, using write.

Naso (Jul 22 2023 at 05:20):

I should clarify. I often have binary operators that take an additional parameter, e.g.
comb V a b

In the context of a proof, V is fixed, so I would like to write something (in haskell notation)

(+) a b = comb V a b

so that within the local context of the proof, I can use the infix operator + instead of comb V. Is this possible?

Wolfgang Jeltsch (Jul 22 2023 at 15:42):

I don’t know whether write can handle partial applications. Maybe you have to locally define a new constant that is equal to the partial application and give it the operator notation, something like the following:

define add (infixl …) where add = comb V

However, this means that you have to use the defining equation in proofs to tell Isabelle that add and comb V are the same thing. For proof methods involving the simplifier, this can be done once and for all by prefixing the defining equation with [simp]:.

Naso (Jul 23 2023 at 00:30):

Wolfgang Jeltsch said:

I don’t know whether write can handle partial applications. Maybe you have to locally define a new constant that is equal to the partial application and give it the operator notation, something like the following:

define add (infixl …) where add = comb V

However, this means that you have to use the defining equation in proofs to tell Isabelle that add and comb V are the same thing. For proof methods involving the simplifier, this can be done once and for all by prefixing the defining equation with [simp]:.

Thanks! I'm not completely sure what you mean though. I've tried this in a proof - context and I have an error:

image.png

Maybe I have misunderstood what was supposed to go in your ellipses?

Actually a more preferable place to make this definition would be in the statement of the lemma, in a defines. is that possible? Either way would be great though!

Mathias Fleury (Jul 23 2023 at 05:36):

You are not using the syntax correctly:

  define comb :: ‹nat ⇒ nat ⇒ nat ⇒ nat› where ‹comb = undefined›
  define V :: ‹nat› where ‹V = undefined›
  define "add" (infixl ‹combV› 55) where "a combV b = comb V a b" for a b
  have ‹a combV b = comb V b a› for a b
    sorry

Mathias Fleury (Jul 23 2023 at 05:38):

I would suggest using bold + (C-e rightarrow for bold) if you need a new operator instead of +

Last updated: Dec 21 2024 at 16:20 UTC