Solving equations with an associative and commutative operator

Question

Consider a goal like this in Isabelle (and don’t worry about ccProd and ccFromList):

ccProd {x} (set xs) ⊔ (ccProd {x} (set ys) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ ccProd (set xs) (set ys)))) =
ccProd {x} (set xs) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ (ccProd {x} (set ys) ⊔ ccProd (set xs) (set ys))))

This is true, since ⊔ is associative and commutative. My usual approach to this is to use

apply (metis join_assoc join_comm)

and it works, but already takes a noticeable time to finish.

Similarly, I have a goal like

ccProd {x} (set xs) ⊔ (ccProd {x} (set ys) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ ccProd (set xs) (set ys)))) =
ccFromList xs ⊔ (ccProd {x} (set ys) ⊔ (ccFromList ys ⊔ (ccProd (set xs) {x} ⊔ ccProd (set xs) (set ys))))

where I also need to apply the commutativity of ccProd in one instance. Again

apply (metis join_assoc join_comm ccProd_comm)

does the job, but takes even longer.

Are there better ways to solve equations involving a commutative and associative operator?

Maybe a tactic or simpproc that, given the theorems join_assoc join_comm, would solve the first goal and reduce the second goal to

ccProd {x} (set xs) = ccProd (set xs) {x} 

Answer 1

Reasoning upto associativity and commutativity is usually done in Isabelle with the simplifier and ordered rewriting. In your example, you provide the simplifier with the associativity rule (oriented from left to right), the commutativity rule, and the left-commutativity rule. The details are explained in the Tutorial on Isabelle/HOL (Section 9.1, Permutative rewrite rules).

Then, the simplifier will reorder both sides of the equations into a normal form which is determined by the implicit term order in Isabelle. Hence, you get equal terms on both sides, which are shown to be equal by reflexivity. Unless your operator also satisfies cancellation laws, this approach does not reduce the second example to the differing parts. If you are lucky and the simplifier rotates both of these terms at the same position. you could use a bunch of introduction rules of the form a = b ==> a ⊔ c = b ⊔ c. However, this is rather fragile. If you rename your variables, the order can change and thus break the proof. However, ccProd seems to be commutative as well, so just add the commutativity law to the simplifier as well. Then, it will normalise these subterms first and solve everything.

Answer 2

If you have an instance of ab_semigroup_mult or ab_semigroup_add than adding ac_simps to the simpset often does the trick.

For example, if I replace your above goal by the following (since I get a syntax error with ⊔):

lemma
  fixes ccProd :: "_ ⇒ _ ⇒ 'a::ab_semigroup_add"
  shows "ccProd {x} (set xs) + (ccProd {x} (set ys) + (ccFromList xs + (ccFromList ys + ccProd (set xs) (set ys)))) =
    ccProd {x} (set xs) + (ccFromList xs + (ccFromList ys + (ccProd {x} (set ys) + ccProd (set xs) (set ys))))"

Then by (simp add: ac_simps) succeeds.

Update: There's also the corresponding locale abel_semigroup that is again "registered" with ac_simps. So your second lemma could work along the following lines

interpretation abel_semigroup ccProd
sorry

That is you show that ccProd is AC (in addition to the already established ab_semigroup_add instance above).

lemma
  "ccProd {x} (set xs) + (ccProd {x} (set ys) + (ccFromList xs + (ccFromList ys + ccProd (set xs) (set ys)))) =
  ccFromList xs + (ccProd {x} (set ys) + (ccFromList ys + (ccProd (set xs) {x} + ccProd (set xs) (set ys))))"
by (simp add: ac_simps)