isabelle - 如何使用 Isar 证明消除规则?
问题描述
这是一个简单的理论:
datatype t1 = A | B | C
datatype t2 = D | E t1 | F | G
inductive R where
"R A B"
| "R B C"
inductive_cases [elim]: "R x B" "R x A" "R x C"
inductive S where
"S D (E _)"
| "R x y ⟹ S (E x) (E y)"
inductive_cases [elim]: "S x D" "S x (E y)"
elim
我可以使用两个辅助引理来证明引理:
lemma tranclp_S_x_E:
"S⇧+⇧+ x (E y) ⟹ x = D ∨ (∃z. x = E z)"
by (induct rule: converse_tranclp_induct; auto)
(* Let's assume that it's proven *)
lemma reflect_tranclp_E:
"S⇧+⇧+ (E x) (E y) ⟹ R⇧+⇧+ x y"
sorry
lemma elim:
"S⇧+⇧+ x (E y) ⟹
(x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
using reflect_tranclp_E tranclp_S_x_E by blast
我需要证明elim
使用 Isar:
lemma elim:
assumes "S⇧+⇧+ x (E y)"
shows "(x = D ⟹ P) ⟹ (⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P) ⟹ P"
proof -
assume "S⇧+⇧+ x (E y)"
then obtain z where "x = D ∨ x = E z"
by (induct rule: converse_tranclp_induct; auto)
also have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
sorry
finally show ?thesis
但我收到以下错误:
No matching trans rules for calculation:
x = D ∨ x = E z
S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(S⇧+⇧+ x (E y)) ⟹ P
如何修复它们?
我想这个引理可以有一个更简单的证明。但我需要分两步证明:
- 显示可能的值
x
E
反映传递闭包的显示
我还认为这个引理可以通过案例来证明x
。但是我的真实数据类型有太多的案例。因此,这不是首选解决方案。
解决方案
此变体似乎有效:
lemma elim:
assumes "S⇧+⇧+ x (E y)"
and "x = D ⟹ P"
and "⋀z. x = E z ⟹ R⇧+⇧+ z y ⟹ P"
shows "P"
proof -
have "S⇧+⇧+ x (E y)" by (simp add: assms(1))
then obtain z where "x = D ∨ x = E z"
by (induct rule: converse_tranclp_induct; auto)
moreover
have "S⇧+⇧+ (E z) (E y) ⟹ R⇧+⇧+ z y"
sorry
ultimately show ?thesis
using assms by auto
qed
- 假设应该与目标分开。
- 作为第一个声明,我应该使用
have
而不是assume
. 这不是一个新的假设,只是现有的假设。 - 而不是
finally
我应该使用ultimately
. 似乎后者的应用逻辑更简单。
推荐阅读
- python - 我想在具有特定条件的 jinja2 模板中使用 for 循环
- google-cloud-platform - 用于 Json 消息的 Apache Beam Kafka IO - org.apache.kafka.common.errors.SerializationException
- java - 从 swagger hub 导出 spring 存根导致编译错误
- c# - 如何从其他函数 C++ 访问参数?
- python - 从裁剪后的图像 yolov3 中获取原始颜色
- c# - 在 MySQL.Data.EntityFrameworkCore 中找不到 Extensions 命名空间
- typescript - 在 TypeScript 中给定泛型类型或参数时,如何缩小函数响应的类型
- javascript - 带有脚本的 PHP 表单不执行 POST
- python - 向前矢量化 PyTorch 操作
- python - 如何将用户可配置的 dict 传递给类实例