Isabelle 简化器引入了 if 语句的大小写区分(为什么？何时？)

Question

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

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

这给出了目标:

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

我的问题是:如何告诉简化器这样做？我可以找到一个简化规则来判断是否会导致这种行为，也可以找到一个简化规则。如何为其他类似 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 小节更详细地解释了简化器(尽管不可否认，有关简化器的许多知识基本上都是“古老的智慧”)。