问题描述
请问我如何告诉Isabelle扩展我所有的deFinition，因为那样的证明是微不足道的？不幸的是，没有默认的扩展或简化操作，基本上我把原始表达式作为子目标。
示例：
theory Test
imports Main
begin
deFinition b0 :: "nat⇒nat"
where "b0 n ≡ (n mod 2)"
deFinition b1 :: "nat⇒nat"
where "b1 n ≡ (n div 2)"
lemma "(a::nat)≤3 ∧ (b::nat)≤3 ⟶
2*(b1 a)+(b0 a)+2*(b1 b)+(b0 b) = a+b"
apply auto
oops
end
在oops之前居住：
proof (prove)
goal (1 subgoal):
1. a ≤ 3 ⟹
b ≤ 3 ⟹ 2 * b1 a + b0 a + 2 * b1 b + b0 b = a + b
解决方法
我的推荐：unfolding
在证明开始时，有一个特殊的关键字unfolding用于解开定义。对于您的示例，其内容为：
unfolding b0_def b1_def by simp
我认为unfolding是最优雅的方式。在编写证明时也有帮助。在内部，这（主要是？）等同于使用unfold方法：
apply (unfold b0_def b1_def) by simp
这将递归地（！）使用您提供的等式集重写证明目标。 （由于递归，您宁可不要提供可能会产生循环的一组等式...）
替代：使用简化器
在可能存在循环的情况下，简化程序可能能够顺利展开而不会陷入这些循环，这可能是通过与其他简化程序进行交错来实现的。在这种情况下，正如您所建议的，by (simp add: b0_def b1_def)很棒！
替代定义：也许只是abbreviation（而不是definition）？
如果发现自己在每个实例中都展开了定义，则可以考虑使用abbreviation而不是definition。然后，伊莎贝尔（Isabelle）的一些魔术师将为您打包/拆包，而无需进一步的提示。 abbeviation仅影响用户与Isabelle的通信方式。它不会在对象级别引入新符号，因此，将不会有b1_def事实等。
abbreviation b0 :: "nat⇒nat"
where "b0 n ≡ (n mod 2)"
通常不建议：使用简化器来构建类似缩写的内容
如果（出于某种原因）您想要在对象级别拥有一个已定义的名称，但几乎在每个实例中都将其展开，则还可以将定义的等式直接输入到简化器中。
definition b0 :: "nat⇒nat"
where [simp]: "b0 n ≡ (n mod 2)"
（通常没有什么理由选择最后一个选项。）
,是的，我一直忘记默认情况下，简化中不使用定义。
将定义显式添加到简化规则可以解决此问题：
class SubscriberDevice extends Model
{
protected $table = 'subscriber_devices';
public function _status($token,$reason)
{
self::where('token',$token)->update([
'reason' => $reason,'status' => 'inactive',]);
}
}
通过这种方式可以正确使用定义（lemma "(a::nat)≤3 ∧ (b::nat)≤3 ⟶
2*(b1 a)+(b0 a)+2*(b1 b)+(b0 b) = a+b"
by (simp add: b0_def b1_def)
，b0）。