Search code examples
isabelle

Power with integer exponents in Isabelle

Here is my definition of power for integer exponents following this mailing-list post:

definition 
 "ipow x n = (if n < 0 then (1 / x) ^ n else x ^ n)" 

notation ipow (infixr "^⇩i" 80)
  1. Is there a better way to define it?
  2. Is there an existing theory in Isabelle that already includes it so that I can reuse its results?

Context

I am dealing with complex exponentials, for instance consider this theorem:

enter image description here

after I proved it I realized I need to work with integers n not just naturals and this involves using powers to take out the n from the exponential.

Solution

  • I don't think something like this exists in the library. However, you have a typo in your definition. I believe you want something like

    definition 
 "ipow x n = (if n < 0 then (1 / x) ^ nat (-n) else x ^ nat n)"

    Apart from that, it is fine. You could write inverse x ^ nat (-n), but it should make little difference in practice. I would suggest the name int_power since the corresponding operation with natural exponents is called power.

    Personally, I would avoid introducting a new constant like this because in order to actually use it productively, you also need an extensive collection of theorems around it. This means quite a bit of (tedious) work. Do you really need to talk about integers here? I find that one can often get around it in practice (in particular, note that the exponentials in question are periodic anyway).

    It may be useful to introduce such a power operator nevertheless; all I'm saying is you should be aware of the trade-off.

    Side note: An often overlooked function in Isabelle that is useful when talking about exponentials like this is cis (as in ‘cosine + i · sine‘). cis x is equivalent to ‘exp(ix)’ where x is real.