Search code examples
isabelleformal-verification

Isabelle/HOL using addition/subtraction associativity

I'm trying to prove something of the form

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

AFAIK the associativity theorems are part of the library but aren't marked as simplifications, so I need to to manually add them. What exactly are the names of the appropriate ones / which theory are they defined in?

Solution

  • Such goals are typically solved with the theorem collection algebra_simps. Just write by (simp add: algebra_simps).

    Note that the way you stated the theorem, you will not be able to prove it because you did not specify that b, c, and d are elements of a group. You will need to write something like

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

    or

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

    or something more special, like nat or int instead of 'a :: group_add.

    In fact, when you do that, the IDE will notify you that there is already such a lemma: Groups.group_add_class.add_diff_eq

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