I would like to prove an equality by splitting it into a proof in each direction.
Is there a more elegant style to start such a proof than this way::
lemma eq_by_both_directions: shows "L = R" apply (unfold iff_conv_conj_imp; rule conjI; rule impI) proof (goal_cases) case 1 assume ?L show ?R by ... next case 2 assume ?R then show ?L by ... qed
Note: this is using the HOL theorem:
HOL.iff_conv_conj_imp: (?P = ?Q) = ((?P ⟶ ?Q) ∧ (?Q ⟶ ?P))
The proof is also bad style because of the 'apply' commands before starting the Isar proof.
(Strangely, if those apply commands are inserted into the proof startup just before 'goal_cases', then only one case is generated rather than two, so the 'next case 2' becomes incorrect. But this might be an unrelated to my question).
So, is there a nicer way of starting up a bi-directional equality proof? Thanks!