如何解决如何让Isabelle“计算”归纳谓词的输出
我有一个归纳谓词P
,其行为类似于部分函数。换句话说,P x y = P x y' ⟹ y = y'
。在对一个具体值证明定理时,我想让Isabelle“计算”谓词的输出(例如)。
例如,假设我们有以下谓词div2
。
inductive div2 :: "nat ⇒ nat ⇒ bool" where
Zero: "div2 0 0" |
SS: "div2 n m ⟹ div2 (Suc (Suc n)) (Suc m)"
code_pred[show_modes] div2 .
如何在不提供输出m
的情况下证明以下引理(该术语太大而无法在实际情况下键入)?
lemma "(THE m. div2 8 m) ≠ 5"
sorry
解决方法
the
和some
上的属性几乎总是以相同的方式工作(大锤在它们上的效果不佳)。
- 证明证人的存在;
- 唯一:证明证人的独特性;
- 用
theI
或someI
推论该属性基于值; - 证明您真正想证明的定理。
在您的情况下,证明5不是证人:
inductive_cases div2E: ‹div2 m n›
lemma "(THE m. div2 8 m) ≠ 5"
proof -
have ex_div2: ‹div2 8 4› (*1: witness*)
by (auto simp: numeral_eq_Suc div2.intros)
moreover have ‹div2 8 m ⟹ m = 4› for m (*2: uniqueness*)
by (force simp: numeral_eq_Suc elim: div2E)
ultimately have ‹div2 8 (THE x. div2 8 x)› (*3: property holds*)
by (rule theI)
(*4 use the property*)
then show ?thesis
by (force simp: numeral_eq_Suc elim: div2E)
qed
如果您不需要the
,请改用some
,这样可以避免每次使用非常烦人的唯一性证明。
对于您的用例,我建议将定理写为div2 8 m ⟹ m ≠ 5
,这是等效的,但更易于使用和证明。
lemma "div2 8 m ⟹ m ≠ 5"
by (force simp: numeral_eq_Suc elim: div2E)
关于可重用性:
- 因子在单独引理中的第3步(如果存在一种有意义的方式来表达何时存在倒数)
- 通过引入定义来尽可能隐藏
the
谓词,并避免尽可能多地引用lambda定义。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。