Isabelle中带标记转移系统可达性引理证明求助

带标记转移系统（LTS）定义 #

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

节点间可达性函数LTS_is_reachable定义 #

归纳定义如下：

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒ ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" for Δ and Δ' where
  LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q [] q" |
  LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
  LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"

各规则说明：

• LTS_Empty：节点可通过空序列自达
• LTS_Step1：Δ'中节点间可无条件可达（不产生字母序列）
• LTS_Step2：节点可通过对应字母集的转移，生成字母序列

待证明引理 #

需要证明的引理如下：

lemma removeFromAtoEndTrans:"LTS_is_reachable Δ (insert (ini, end) Δ') ini l end ⟹ l ≠ [] ⟹ ∀(q, σ, p) ∈ Δ. q ≠ ini ∧ q ≠ end ⟹  ∀(end, p) ∈ Δ'. p = end ⟹  LTS_is_reachable Δ Δ' ini l end"

引理逻辑：当序列l非空时，可从Δ'中移除(ini, end)转移，该结论逻辑成立且nitpick未找到反例，但暂无证明思路。

证明思路与步骤 #

核心方法：对归纳谓词LTS_is_reachable做结构归纳 #

由于LTS_is_reachable是归纳定义的谓词，结构归纳是最直接的证明路径，具体步骤如下：

1. 基础情形（LTS_Empty规则）
   此时对应l = []，但前提明确l ≠ []，该情形与前提矛盾，直接用contradiction完成证明。

2. 归纳情形1（LTS_Step1规则）
   原推导依赖(q, q'') ∈ insert (ini, end) Δ'，分两种子情况讨论：

   • 子情况1：(q, q'') = (ini, end)
     此时原推导后续为LTS_is_reachable Δ (insert (ini, end) Δ') end l end。结合前提：
     • ∀(end, p) ∈ Δ'. p = end：Δ'中所有以end为起点的转移都是自环
     • ∀(q, σ, p) ∈ Δ. q ≠ end：Δ中没有以end为起点的转移
       要生成非空序列l，必须通过LTS_Step2产生字母，但end无法触发任何LTS_Step2转移；仅通过LTS_Step1的自环无法生成非空序列，因此该子情况与前提矛盾，直接排除。
   • 子情况2：(q, q'') ∈ Δ'
     对后续的LTS_is_reachable Δ (insert (ini, end) Δ') q'' l end应用归纳假设，得到LTS_is_reachable Δ Δ' q'' l end，再结合(q, q'') ∈ Δ'，通过LTS_Step1规则即可推导出目标结论。

3. 归纳情形2（LTS_Step2规则）
   根据前提∀(q, σ, p) ∈ Δ. q ≠ ini ∧ q ≠ end，该规则的转移起点q既不是ini也不是end，与(ini, end)转移完全无关。对后续的LTS_is_reachable Δ (insert (ini, end) Δ') q'' w end应用归纳假设，得到LTS_is_reachable Δ Δ' q'' w end，再结合a ∈ σ和(q, σ, q'') ∈ Δ，通过LTS_Step2规则即可推导出目标结论。

可选辅助引理（简化证明） #

为快速处理LTS_Step1子情况1，可先证明辅助引理：

lemma end_no_nonempty_path:
  assumes "∀(q, σ, p) ∈ Δ. q ≠ end" "∀(end, p) ∈ Δ'. p = end"
  shows "LTS_is_reachable Δ Δ' end l end ⟹ l = []"

该引理同样通过结构归纳证明，主引理中子情况1调用该引理后，结合l ≠ []即可直接得出矛盾。

内容的提问来源于stack exchange，提问作者Hongjian Jiang