为什么我的 simproc 没有按照规定的模式激活？

Question

我正在为正弦简化写一个 simproc。这是一个将 sin(x+8pi+pi/2) 重写为 cos(x):

的示例

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 |> Thm.term_of |> dest_comb |> snd 
    val x = sum |> dest_comb |> fst |> dest_comb |> snd 
            |> dest_comb |> fst |> dest_comb |> snd
    val k = sum |> dest_comb |> fst |> dest_comb |> snd 
            |> dest_comb |> snd |> dest_comb |> fst
            |> dest_comb |> snd |> dest_comb |> snd |> 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)"}
›

到目前为止一切正常，但是一旦我设置了 simproc：

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

我发现即使使用基本的简单集也没有真正应用。其他 simprocs 设置确实有效，请参阅 here。

Answer 1

在第一个示例中，您的 simproc 没有被调用，因为 simprocs（如果我没记错的话）仅在用尽所有“正常”重写后才被调用，并且您的目标立即被重写为 sin (17 * pi / 2 + x) = cos x。由于您的 simproc 不再符合该目标，因此不会调用它。

在第二个例子中，你的 simproc 被调用 （你可以通过插入例如 val _ = @{print} "foo" 到你的 let 块来验证这一点）并且它确实产生重写规则。不幸的是，这个重写规则仍然有前提条件 8 ≡ 2 * real_of_int 4，simp 不能用你正在使用的非常基本的简化器设置来解决，所以它无法应用规则。

您可以使用简化器跟踪找出那里发生了什么：

lemma "sin(x+8*pi+pi/2) = cos(x)"
  using [[simp_trace, simp_trace_depth_limit = 100]]
  apply(tactic ‹simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [@{simproc sine1}]) 1›)

输出：

[0]Adding simplification procedure "Scratch.sine1" for
sin (?x + 8 * pi + pi / 2) 
[0]Adding simplification procedure "Scratch.sine1" for
sin (?x + 8 * pi + pi / 2) 
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
sin (x + 8 * pi + pi / 2) = cos x 
[1]Procedure "Scratch.sine1" produced rewrite rule:
8 ≡ 2 * real_of_int 4 ⟹
sin (x + 8 * pi + pi / 2) ≡ cos x 
[1]Applying instance of rewrite rule
8 ≡ 2 * real_of_int 4 ⟹
sin (x + 8 * pi + pi / 2) ≡ cos x 
[1]Trying to rewrite:
8 ≡ 2 * real_of_int 4 ⟹
sin (x + 8 * pi + pi / 2) ≡ cos x 
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
8 ≡ 2 * real_of_int 4 
[1]FAILED
8 ≡ 2 * real_of_int 4 ⟹
sin (x + 8 * pi + pi / 2) ≡ cos x 
[1]IGNORED result of simproc "Scratch.sine1" -- does not match
sin (x + 8 * pi + pi / 2)

如果您将规则 2 * real_of_int 4 ≡ 8 添加到您的简单集，它将按预期工作。

为什么我的 simproc 没有按照规定的模式激活？

Why is my simproc not activated on the prescribed pattern?

isabelle