Isabelle/HOL 使用 addition/subtraction 关联性

Question

我正在尝试证明某种形式

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

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

Answer 1

此类目标通常使用定理集 algebra_simps 来解决。直接写 by (simp add: algebra_simps).

请注意，您陈述定理的方式将无法证明它，因为您没有指定 b、c 和 d 是 a 的元素团体。你需要写类似

的东西

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

Isabelle/HOL using addition/subtraction associativity