Isabelle 简化器为 if 语句引入了大小写区分（为什么？什么时候？）

Question

如果我将 simp 方法应用于包含 if 表达式的目标，简化器会自动引入大小写区分：

lemma "undefined (if x then True else False)"
  apply simp

这给出了目标：

(x ⟶ undefined True) ∧ (¬ x ⟶ undefined False)

我的问题是：如何让简化器执行此操作？我可以找到一个简化规则来判断是否可能导致这种行为，也不是 simproc。我怎样才能为其他类似 if 的常量获得类似的行为？

Answer 1

该功能由 拆分器 启用。简化器本身是一个大循环，不仅执行重写，而且在它再次开始重写之前还会执行各种其他操作。

对于 if，相关的 split 规则是 if_splits:

?P (if ?Q then ?x else ?y) = ((?Q ⟶ ?P ?x) ∧ (¬ ?Q ⟶ ?P ?y))
?P (if ?Q then ?x else ?y) = (¬ (?Q ∧ ¬ ?P ?x ∨ ¬ ?Q ∧ ¬ ?P ?y))

第一个 split 规则适用于结论中出现的 if _ then _ else _，后者适用于前提中的出现。（这两个规则分别作为 if_split 和 if_split_asm 提供。）

case 数据类型的常量有类似的规则，例如bool.splits:

?P (case ?bool of True ⇒ ?f1.0 | False ⇒ ?f2.0) =
  ((?bool = True ⟶ ?P ?f1.0) ∧ (?bool = False ⟶ ?P ?f2.0))
?P (case ?bool of True ⇒ ?f1.0 | False ⇒ ?f2.0) =
  (¬ (?bool = True ∧ ¬ ?P ?f1.0 ∨ ?bool = False ∧ ¬ ?P ?f2.0))

规则可以通过用 [split].

注释来声明为 split 规则

可以在 reference manual 的 §9.3.1 中找到更多信息。整个第 9.3 小节更详细地解释了简化器（尽管公认的关于简化器的很多知识基本上是 "ancient wisdom"）。

Isabelle 简化器为 if 语句引入了大小写区分（为什么？什么时候？）

Isabelle simplifier introduces case distinction for if-statement (why? when?)

isabelle