I am tying to get a better understanding how Isabelle manages the chain proofs, specifically when associativity/commutativity is involved. Imagine I have a binary non-homogeneous operator op that is quite complex (and it involves some set operations). Its application looks like op(x, k), where k is some sort of index. Then I want to show it is associative in the sense that
op(op(x, k), l) = op(op(x, l), k).
The proof starts from the LH, unfold the definition of op, then use associativity/commutativity of set operators, to finally arrive at RH.
My (poor) way of doing this is:
lemma "op(op(x, k), l) = op(op(x, l), k)"
proof -
have a1: "op(op(x, k), l) = LHStep1" (some rewriting) <proof>
have a2: "LHStep1 = LHStep2" (some more rewriting) <proof>
...
have ai+1: "LHStepi = SOMETHING" <proof>
have ai: "SOMETHING = RHStepi" (here usually the terms are switched in the order of RH) <proof>
...
[the reverse steps to get to the actual RH]
...
have an: "RHStep1 = RH" <proof>
then show ?thesis using a1 a2... an by auto
qed
While this works, it pains me greatly to basically duplicate the proofs. Stopping in the middle so far proved to be unsuccessful. Also, most of the time using have... moreover... ultimately fails, hence the naming of the intermediary steps and using them all in the end, another ugly aspect.
I am not doing any calculations, this is a mathematical structure with a set of operators and axioms on which I need to prove some mathematical properties.
I am missing something and I don't know what. As usual, any help or pointing in the right direction would be greatly appreciated. Thank you!