title: Why is my simproc not activated on the prescribed pattern?
body: <p>I'm writing a simproc for sine simplifications. Here is an example rewriting sin(x+8pi+pi/2) to cos(x):</p>
  
  <pre><code>lemma rewrite_sine_1:
    fixes k' :: int and k :: real
    assumes "k  ≡ 2 * of_int k'" 
    shows "sin (x + k*pi + pi/2) ≡ cos (x)"
   sorry
  
  ML ‹
  fun rewrite_sine ctxt ct =
    let
      val sum = ct |&gt; Thm.term_of |&gt; dest_comb |&gt; snd 
      val x = sum |&gt; dest_comb |&gt; fst |&gt; dest_comb |&gt; snd 
              |&gt; dest_comb |&gt; fst |&gt; dest_comb |&gt; snd
      val k = sum |&gt; dest_comb |&gt; fst |&gt; dest_comb |&gt; snd 
              |&gt; dest_comb |&gt; snd |&gt; dest_comb |&gt; fst
              |&gt; dest_comb |&gt; snd |&gt; dest_comb |&gt; snd |&gt; HOLogic.dest_numeral
      val rk = SOME (Thm.cterm_of ctxt (HOLogic.mk_number HOLogic.realT k))
      val ik2 = SOME (Thm.cterm_of ctxt (HOLogic.mk_number HOLogic.intT (k div 2)))
      val cx = SOME( Thm.cterm_of ctxt x)
    in    
      SOME (Thm.instantiate' [] [rk,ik2,cx] @{thm rewrite_sine_1})    
    end
  ›
  
  ML ‹
  rewrite_sine @{context} @{cterm "sin(x+8*pi+pi/2)"}
  ›
  </code></pre>
  
  <p>Up to here everything works but once I set up my simproc:</p>
  
  <pre><code>simproc_setup sine1 ("sin (x + 8 * pi + pi / 2)") = ‹K rewrite_sine›
  
  (* this should be handled by sine1 only, but is not *)
  lemma "sin (x + 8 * pi + pi / 2) = cos(x)"
    apply simp
    sorry
  
  (* this should be handled by sine1 only, but is not *)
  lemma "sin(x+8*pi+pi/2) = cos(x)"
    apply(tactic ‹simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc sine1}]) 1›)
    sorry
  </code></pre>
  
  <p>I see that it is not really applying even with a basic simpset. Others simprocs is set-up did work, see <a href="https://github.com/rjraya/Tactics/blob/master/Tactics.thy" rel="nofollow noreferrer">here</a>.</p>