Search code examples
isabelle

Rewriting sine using simprocs in Isabelle

I want to implement a simproc capable of rewriting the argument of sin into a linear combination x + k * pi + k' * pi / 2 (where ideally k' = 0 or k' = 1) and then apply existing lemmas about additions of arguments in sines.

The steps could be as follows:

  1. Pattern match the goal to extract the argument of sin(expr):
fun dest_sine t =
      case t of
        (@{term "(sin):: real ⇒ real"} $ t') => t'
      | _ => raise TERM ("dest_sine", [t]) ;

  1. Prove that for some x, k, k': expr = x + k*pi + k' * pi/2.

  2. Use existing lemmas to rewrite to a simpler trigonometric function:

fun rewriter x k k' =
 if (k mod 2 = 0 andalso k' = 0) then @{term "sin"} $ x
 else if (k mod 2 = 0 andalso k' = 1) then @{term "cos"} $ x
 else if (k mod 2 = 1 andalso k' = 0) then @{term "-sin"} $ x
 else @{term "-cos"} $ x

I'm stuck at step two. The idea is to use algebra simplifications to obtain the x,k,k' where the theorem holds. I believe schematic goals should do this but I haven't ever used them.

My thoughts

Could I rather assume that the expression is of this form and let the simplifier find it so that the simproc can be triggered?

If I first start assuming the linear form x + k*pi + k' * pi/2 then:

  1. Extract x,k,k' from this combination.
  2. Apply rewriter and obtain the corresponding term to be rewritten two.
  3. Apply in a sequence: rules dealing with + pi/2, rules dealing with + 2 pi
Solution

  • I would start easy and ignore the pi / 2 part for now.

    You probably want to build a simproc that matches on anything of the form sin x. Then you want to write a conversion that takes that term x (which is assumed to be a sum of several terms) and brings it into the form a + of_int b * p.

    A conversion is essentially a function of type cterm → thm which takes a cterm ct and returns a theorem of the form ct ≡ …, i.e. it's a form of deterministic rewriting (a conversion can also fail by throwing a CTERM exception, by convention). There are a lot of combinators for building and using these in Pure/conv.ML.

    This is probably a bit fiddly. You essentially have to descend through the term and, for each atom (i.e. anything not of the form _ + _) you have to figure out whether it can be brought into the form of_int … * pi (e.g. again by writing a conversion that does this transformation – to make it easy you can omit this part so that your procedure only works if the terms are already in that form) and then group all the terms of the form of_int … * pi to the right and all the terms not of that form to the left using associativity and commutativity.

    I would suggest this:

    • Define a function SIN_SIMPROC_ATOM x n = x + of_int n * pi
    • Write a conversion sin_atom_conv that rewrites of_int n * pi to SIN_SIMPROC_ATOM 0 n and everything else into SIN_SIMPROC_ATOM x 0
    • Write a conversion that descends through +, applies sin_atom_conv to every atom, and then applies some kind of combination rule like SIN_SIMPROC_ATOM x1 n1 + SIN_SIMPROC_ATOM x2 n2 = SIN_SIMPROC_ATOM (x1 + x2) (n1 + n2)
    • In the end, you have rewritten your entire form to the form sin (SIN_SIMPROC_ATOM x n), and then you can apply some suitable rule to that.

    It's not quite clear to me how to best handle the parity of n. You could rewrite sin (SIN_SIMPROC_ATOM x n) = (-1) ^ nat ¦n¦ * sin x but I'm not sure if that's what the user really wants in most cases. It might make more sense to only do that if you can deduce the parity of n statically (e.g. by using the simplifier) and then directly simplify to sin x or -sin x.

    The situation becomes even more complicated if you want to include halves of π. You can of course extend SIN_SIMPROC_ATOM by a second term for halves of π (and one for doubles of π as well to make it more uniform). Or you could ad all of them together so that you just have a single integer n that describes your multiples of π/2, and k multiples of π simply contribute 2k to that term. And then you have to figure out what n mod 4 is – possibly again with the simplifier or with some clever static method.