Isar无法检索字面事实：原因分析及更优替代方案咨询

问题场景 #

我编写了如下Isar代码：

assume H: "x ≠ xa ∧ x ∈ elems xs" (is "?H1 ∧ ?H2")
hence "?H1" and "?H2" by auto
from Cons.IH[OF `?H2` ] have 1: "∃ys zs. xs = ys @ x # zs ∧ x ∉ elems ys" by simp
then obtain ys zs where 2: "xs = ys @ x # zs ∧ x ∉ elems ys" (is "?C1 ∧ ?C2") by blast
hence "?C1" and "?C2" by auto
from `?C1` have R1: "xa # xs = (xa # ys) @ x # zs" by simp
from `x ≠ xa` and `x ∉ elems ys` have R2: "x ∉ elems (xa#ys)" by auto
from R1 R2 show ?case by blast

若移除hence "?H1" and "?H2" by auto和hence "?C1" and "?C2" by auto这两行，无法引用字面事实?H2和?C1，甚至无法引用这些元变量展开后的具体事实，会报错“Failed to retrieve literal fact⌂: x ∈ elems xs”，但错误信息中已展开元变量，说明它们应在作用域内。

问题解答 #

1. 问题原因
   Isar的事实引用机制要求：只有被显式声明为独立事实的命题才能被直接引用。assume H: "P ∧ Q" (is "?H1 ∧ ?H2")只是给复合命题绑定了元变量别名，并没有将?H1、?H2作为单独的事实加入证明上下文。同理，obtain ... where 2: "C1 ∧ C2" (is "?C1 ∧ ?C2")也只是给复合命题加了元变量，?C1、?C2并未成为独立事实。错误信息里展开元变量只是语法层面的提示，不代表这些子命题已经在上下文里可用。

2. 更优解决方法
   不需要用hence ... by auto拆分事实，有两种更简洁的方式：

• 直接在引用时拆分复合事实：利用Isar的事实访问语法，通过H[THEN conjunct1]或H[THEN conjunct2]直接提取合取式的两个分支。比如把from Cons.IH[OF ?H2 ]改成from Cons.IH[OF H[THEN conjunct2]]，就能直接用H的第二个合取支，无需提前拆分。
• 在assume/obtain时直接绑定子事实：声明合取命题时，同时拆分并绑定子事实，比如：

  assume "x ≠ xa" and "x ∈ elems xs"
  

  或者对于obtain的情况：

  then obtain ys zs where "xs = ys @ x # zs" and "x ∉ elems ys" by blast
  

  这种方式直接将子命题作为独立事实加入上下文，后续可以直接引用，无需额外拆分步骤。

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