将简化器应用于任意项
Apply simplifier to arbitrary term
我想到了一个术语，比如 "foo 1 2 a b"，我想知道 Isabelle 是否可以为我简化它。我想写点像
simplify "foo 1 2 a b"
并在输出缓冲区中打印简化术语。这可能吗？
我目前的'workaround'是：
lemma "foo 1 2 a b = blah"
apply simp
效果不错，但看起来有点老套。
不起作用的（在我的例子中）是：
value "foo 1 2 a b"
因为 a 和 b 是未绑定的变量，并且因为我的 foo 涉及无限集和其他花哨的东西，代码生成器对此感到窒息。
当使用value命令时，参数的评估是由注册的评估者进行的（参见Isabelle2013-2的Reference Manual）。
在以前的 Isabelle 版本（例如 Isabelle2013-2）中，过去可以通过给 value 命令一个额外的参数来明确选择一个评估器。例如，
value [simp] "foo 1 2 a b"
似乎在 Isabelle2014 中删除了此参数，根据 Isabelle2014 的 Reference Manual，该策略现在固定为首先使用 ML 代码生成，如果失败，则通过评估进行归一化。
从 Isabelle 开发版本 (e82c72f3b227) 中的 NEWS 文件来看，似乎在即将发布的 Isabelle 版本中将再次启用此参数。
更新： 正如 Andreas 指出的那样，value [simp] 没有使用与 apply simp 相同的一组简化规则。因此，即使可用，我上面描述的解决方案也很可能不会产生您想要的结果。
没有内置功能 AFAIK，但有几种方法可以实现。你已经发现了其中之一，即把这个术语说成引理，然后调用简化器。缺点是这不能在所有上下文中使用，例如，不能在应用证明脚本中使用。
或者，您可以通过属性 [simplified] 调用简化器。这通过 thm 命令在所有上下文中都有效，并在输出缓冲区中产生输出。首先，必须将项注入定理，然后可以将 simplify 应用于定理并用 thm 显示结果。这是可以进入您的杂项理论的准备工作。
definition simp :: "'a ⇒ bool" where "simp _ = True"
notation (output) simp ("_")
lemma simp: "simp x" by(simp add: simp_def)
然后，你可以这样写
thm simp[of "foo 1 2 a b", simplified]
并查看输出中的简化项 window。
评估机制可能不是您想要的，因为评估使用的重写规则集（即代码方程）与简化器通常使用的（简单集）不同。因此，这可能会评估为与应用简化器不同的术语。要查看差异，请在使用 lemma "foo 1 2 a b = blah" 的方法中应用 code_simp 而不是 simp。证明方法 code_simp 使用代码方程式，就像 value [simp] 曾经使用过的那样。
我想到了一个术语，比如 "foo 1 2 a b"，我想知道 Isabelle 是否可以为我简化它。我想写点像
simplify "foo 1 2 a b"
并在输出缓冲区中打印简化术语。这可能吗？
我目前的'workaround'是：
lemma "foo 1 2 a b = blah"
apply simp
效果不错，但看起来有点老套。
不起作用的（在我的例子中）是：
value "foo 1 2 a b"
因为 a 和 b 是未绑定的变量，并且因为我的 foo 涉及无限集和其他花哨的东西，代码生成器对此感到窒息。
当使用value命令时，参数的评估是由注册的评估者进行的（参见Isabelle2013-2的Reference Manual）。
在以前的 Isabelle 版本（例如 Isabelle2013-2）中，过去可以通过给 value 命令一个额外的参数来明确选择一个评估器。例如，
value [simp] "foo 1 2 a b"
似乎在 Isabelle2014 中删除了此参数，根据 Isabelle2014 的 Reference Manual，该策略现在固定为首先使用 ML 代码生成，如果失败，则通过评估进行归一化。
从 Isabelle 开发版本 (e82c72f3b227) 中的 NEWS 文件来看，似乎在即将发布的 Isabelle 版本中将再次启用此参数。
更新： 正如 Andreas 指出的那样，value [simp] 没有使用与 apply simp 相同的一组简化规则。因此，即使可用，我上面描述的解决方案也很可能不会产生您想要的结果。
没有内置功能 AFAIK，但有几种方法可以实现。你已经发现了其中之一，即把这个术语说成引理，然后调用简化器。缺点是这不能在所有上下文中使用，例如，不能在应用证明脚本中使用。
或者，您可以通过属性 [simplified] 调用简化器。这通过 thm 命令在所有上下文中都有效，并在输出缓冲区中产生输出。首先，必须将项注入定理，然后可以将 simplify 应用于定理并用 thm 显示结果。这是可以进入您的杂项理论的准备工作。
definition simp :: "'a ⇒ bool" where "simp _ = True"
notation (output) simp ("_")
lemma simp: "simp x" by(simp add: simp_def)
然后，你可以这样写
thm simp[of "foo 1 2 a b", simplified]
并查看输出中的简化项 window。
评估机制可能不是您想要的，因为评估使用的重写规则集（即代码方程）与简化器通常使用的（简单集）不同。因此，这可能会评估为与应用简化器不同的术语。要查看差异，请在使用 lemma "foo 1 2 a b = blah" 的方法中应用 code_simp 而不是 simp。证明方法 code_simp 使用代码方程式，就像 value [simp] 曾经使用过的那样。