时间戳

首页 > 解决方案 > 在 Isabelle 中使用 simprocs 重写正弦

isabelle - 在 Isabelle 中使用 simprocs 重写正弦

问题描述

我想实现一个能够将 sin 的参数重写为线性组合 x + k * pi + k' * pi / 2 的 simproc （理想情况下 k' = 0 或 k' = 1），然后应用现有的关于添加的引理正弦参数。

步骤如下：

  1. 模式匹配目标以提取 sin(expr) 的参数：
fun dest_sine t =
      case t of
        (@{term "(sin):: real ⇒ real"} $ t') => t'
      | _ => raise TERM ("dest_sine", [t]) ;

  1. 证明对于某些 x、k、k'：expr = x + k*pi + k' * pi/2。

  2. 使用现有的引理重写为更简单的三角函数：

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

我被困在第二步。这个想法是使用代数简化来获得定理成立的 x,k,k'。我相信原理图目标应该这样做，但我从未使用过它们。

我的想法

我是否可以假设表达式是这种形式并让简化器找到它以便可以触发 simproc？

如果我首先开始假设线性形式 x + k*pi + k' * pi/2 那么：

  1. 从此组合中提取 x,k,k'。
  2. 应用重写器，得到对应的要重写的词条两个。
  3. 依次应用：规则处理+ pi/2，规则处理+ 2 pi

标签： isabelle

解决方案

推荐阅读