Isabelle中LTS可达性拼接引理证明及primrec/fun战术咨询

问题背景 #

为实现特定需求，需证明两个关于标记迁移系统（LTS）路径可达性的引理：

1. concat_lemma：若路径qa可通过LTS迁移列表x可达，路径q可通过LTS迁移列表xa可达，则拼接路径qa@q可通过x@xa可达；
2. inverse_concat_lemma：若路径q可通过拼接迁移列表xa@y可达，则存在拆分路径qa、p，满足q=qa@p，且qa可通过xa可达、p可通过y可达。

相关定义代码 #

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

primrec LTS_is_reachable :: "('q, 'a) LTS ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" where
   "LTS_is_reachable Δ q [] q' = (q = q' ∨ (q, {}, q') ∈ Δ)"|
   "LTS_is_reachable Δ q (a # w) q' =
      (∃q'' sigma. a ∈ sigma ∧ (q, sigma, q'') ∈ Δ ∧ LTS_is_reachable Δ q'' w q')"

primrec single_LTS_reachable_by_path :: "'a list ⇒ (('q,'a) LTS * 'q * 'q) list ⇒ bool" where
"single_LTS_reachable_by_path w []= (w = [])"|
"single_LTS_reachable_by_path w (x# xs) = (∃p q. (w = p @ q ∧ LTS_is_reachable (fst x) (fst (snd x)) p (snd (snd x)) ∧ single_LTS_reachable_by_path q xs))"

核心问题 #

在Isabelle中，针对primrec和fun定义，可使用哪些证明战术？

常用证明战术 #

归纳类战术 #

• induction/induct_tac：针对primrec定义的递归结构（如列表、自然数）进行归纳证明。例如你的两个引理涉及列表拼接与递归可达性，可对迁移列表（x/xa/y）或路径列表做归纳，拆分基础情况（空列表）和归纳步骤（非空列表）逐一验证。
• case_tac：拆分定义中的分支情况（比如LTS_is_reachable的空列表/非空列表分支），对每种分支单独证明目标。

自动化推理战术 #

• auto：自动处理简单逻辑推导、等式替换、集合成员关系判断，适合快速解决引理的基础情况或简化复杂目标。例如空列表的可达性判断，auto可直接匹配定义完成证明。
• simp/simp_all：利用递归定义的化简规则，将复杂的递归调用展开为基础形式。比如展开LTS_is_reachable的非空列表定义，把目标拆解为存在性断言。
• blast：高效处理一阶逻辑中的量词（∃/∀）和逻辑连接词，适合inverse_concat_lemma这类存在性证明场景，自动寻找满足条件的拆分路径实例。

量词与等式处理战术 #

• exists_tac：当目标为∃x. P(x)时，手动指定x的具体实例（比如直接给出拆分路径qa和p的取值），再验证该实例满足条件。
• subgoal_tac：将复杂目标拆分为多个子目标分步证明，比如先证明路径拆分的等式q=qa@p，再分别验证两段路径的可达性。
• eq_tac：专注处理等式相关目标，比如验证拼接后的路径与迁移列表的对应关系。

递归定义专用战术 #

• primrec_induct：专门针对primrec定义生成的归纳规则，自动匹配递归结构生成归纳模板，比通用归纳战术更贴合primrec的递归逻辑。
• fun_induct：如果使用fun定义了更复杂的递归（如嵌套递归、非结构递归），用该战术调用其生成的归纳规则，适配非primrec支持的递归场景。

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