Isabelle 中的归纳证明：给定一个子目标，如何创建正确的辅助引理

Question

我已经定义了一个带标签的转换系统，以及接受该系统可以到达的列表的函数。为了方便起见，我定义了另一个用于收集可达状态的函数。我想证明这两个函数之间的关系。

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 {})

Answer 1

除了如何证明引理之外，您的示例还有一个问题：您对 LTS_is_reachable_set 的定义有问题。考虑这个定义的第二个等式：

"LTS_is_reachable_set Δ q (a # w) = ⋃ ((λ(q, σ, q''). ...

这里的问题是λ(q, σ, q'')中的变量q与[=31=中的参数q不相同] 边。因此，您应该将 right-hand 侧的 q 重命名为 q' 并明确检查 q 和 q' 是否相等，如下所示：

"LTS_is_reachable_set Δ q (a # w) = ⋃ ((λ(q', σ, q''). if a ∈ σ ∧ q' = q then ...

现在，您可以按照您的意愿在 w 上通过归纳来证明您的引理。但是，您需要通过使 q1 成为任意值来削弱归纳假设，以便您可以在证明中有效地应用它。这是一个如何证明引理的例子：

lemma "LTS_is_reachable Δ q1 w q2 ⟹ q2 ∈ LTS_is_reachable_set Δ q1 w"
proof (induction w arbitrary: q1)
  case Nil
  then show ?case
    by simp
next
  case (Cons a w)
  from `LTS_is_reachable Δ q1 (a # w) q2`
  obtain q'' and σ
  where "a ∈ σ" and "(q1, σ, q'') ∈ Δ" and "LTS_is_reachable Δ q'' w q2"
    by auto
  moreover from `LTS_is_reachable Δ q'' w q2` and Cons.IH
  have "q2 ∈ LTS_is_reachable_set Δ q'' w"
    by simp
  ultimately show ?case
    by fastforce
qed

Isabelle 中的归纳证明：给定一个子目标，如何创建正确的辅助引理

The induction proof in Isabelle: given a subgoal, how to create the right auxiliary lemma

isabelle