Isabelle/HOL使用加法/减法结合

Question

我在试着证明某种形式

lemma assoc: "b + (c - d) = (b + c) - d"

AFAIK结合定理是库的一部分，但没有被标记为简化，所以我需要手动添加它们。适当的theory的确切名称是什么/它们是在哪一个中定义的？

Answer 1

这样的目标通常用定理集合algebra_simps来解决。写by (simp add: algebra_simps)就行了。

注意，按照您陈述定理的方式，您将无法证明它，因为您没有指定b、c和d是一个组的元素。你需要写些类似于

lemma assoc: "(b :: 'a :: group_add) + (c - d) = (b + c) - d"

或

lemma assoc: 
  fixes b c d :: "'a :: group_add"
  shows "b + (c - d) = (b + c) - d"

或者更特别的东西，比如nat或int，而不是'a :: group_add。

实际上，当您这样做时，IDE将通知您已经存在这样一个引理：Groups.group_add_class.add_diff_eq。

thm add_diff_eq
> ?a + (?b - ?c) = ?a + ?b - ?c