Isabelle中的诱导证明：给定子目标，如何创建正确的辅助引理
我已经定义了一个标记的过渡系统，以及可以访问该系统可以到达的列表的功能。令人信服的是，我定义了另一种用于收集可及状态的功能。我想证明这两个功能之间的关系。
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
primrec LTS_is_reachable :: "('q, 'a) LTS \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
"LTS_is_reachable \<Delta> q [] q' = (q = q')"|
"LTS_is_reachable \<Delta> q (a # w) q' =
(\<exists>q'' \<sigma>. a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q')"
primrec LTS_is_reachable_set :: "('q, 'a) LTS ⇒ 'q ⇒ 'a list ⇒ 'q set" where
"LTS_is_reachable_set Δ q [] = {q}"|
"LTS_is_reachable_set Δ q (a # w) = \<Union> ((λ(q, σ, q''). if a \<in> σ then LTS_is_reachable_set Δ q'' w else {}) ` Δ)"
lemma "LTS_is_reachable Δ q1 w q2 \<Longrightarrow> q2\<in>(LTS_is_reachable_set Δ q1 w)"
apply (induct w)
apply simp
有这样的引理，我不知道如何证明这一点。
子目标在这里：
⋀a w. (LTS_is_reachable Δ q1 w q2 ⟹ q2 ∈ LTS_is_reachable_set Δ q1 w) ⟹
∃q'' σ. a ∈ σ ∧ (q1, σ, q'') ∈ Δ ∧ LTS_is_reachable Δ q'' w q2 ⟹
∃x∈Δ. q2 ∈ (case x of (q, σ, q'') ⇒ if a ∈ σ then LTS_is_reachable_set Δ q'' w else {})
I have defined a labeled transition system, and the function which accpets the list that system could reach. For convinence, I defined another funtion used for collecting reachable states. And I want to prove the relation between these two functions.
type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"
primrec LTS_is_reachable :: "('q, 'a) LTS \<Rightarrow> 'q \<Rightarrow> 'a list \<Rightarrow> 'q \<Rightarrow> bool" where
"LTS_is_reachable \<Delta> q [] q' = (q = q')"|
"LTS_is_reachable \<Delta> q (a # w) q' =
(\<exists>q'' \<sigma>. a \<in> \<sigma> \<and> (q, \<sigma>, q'') \<in> \<Delta> \<and> LTS_is_reachable \<Delta> q'' w q')"
primrec LTS_is_reachable_set :: "('q, 'a) LTS ⇒ 'q ⇒ 'a list ⇒ 'q set" where
"LTS_is_reachable_set Δ q [] = {q}"|
"LTS_is_reachable_set Δ q (a # w) = \<Union> ((λ(q, σ, q''). if a \<in> σ then LTS_is_reachable_set Δ q'' w else {}) ` Δ)"
lemma "LTS_is_reachable Δ q1 w q2 \<Longrightarrow> q2\<in>(LTS_is_reachable_set Δ q1 w)"
apply (induct w)
apply simp
Have such a lemma, I don't know how to prove it.
The subgoal is here:
⋀a w. (LTS_is_reachable Δ q1 w q2 ⟹ q2 ∈ LTS_is_reachable_set Δ q1 w) ⟹
∃q'' σ. a ∈ σ ∧ (q1, σ, q'') ∈ Δ ∧ LTS_is_reachable Δ q'' w q2 ⟹
∃x∈Δ. q2 ∈ (case x of (q, σ, q'') ⇒ if a ∈ σ then LTS_is_reachable_set Δ q'' w else {})
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您的示例有一个问题，除了如何证明引理：您对
lts_is_reachable_set的定义是错误的。考虑此定义的第二个方程：这里的问题是
Qinλ（q，σ，q''）is not 与左侧的参数q相同。因此，您应该在右侧重命名q，例如q'，并明确检查q和q '相等如下：现在，您可以按照您的意愿来通过
w来证明您的引理。但是，您需要通过制作Q1任意值来削弱归纳假设，以便您可以有效地将其应用于证明。这是您如何证明自己的引理的一个示例：There is a problem with your example beyond how to prove the lemma: Your definition of
LTS_is_reachable_setis buggy. Consider the second equation of this definition:The issue here is that variable
qinλ(q, σ, q'')is not the same as the parameterqin the left-hand side. Therefore, you should renameqin the right-hand side to, for example,q'and explicitly check thatqandq'are equal as follows:Now, you can prove your lemma by induction on
was you intended to do it. However, you need to weaken the induction hypotheses by makingq1an arbitrary value so you can effectively apply it in your proof. Here's an example of how you can prove your lemma: