2 回答
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.