如何解决扩展Isabelle引理中的所有定义
请问我如何告诉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
)。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。