title: How to show that 2 formula sare semantically equivalent in Isabelle
body: <p>I want to (miss-)use Isabelle to show that two given formulas are syntactically equivalent. For example <code>A ∧ B = B ∧ A</code>.</p>
  
  <p>I don't want to go into any detail with regards towards the logic behind the formulas. I don't want to care that <code>A ∧ B</code> is true when both A and B are true. I just want to compare the two formulas on a structural level and say that they are equivalent because of the commutative property. </p>
  
  <p>Basicly i want to be abled to write lemmas comparing 2 formulas with some equality function and use the given, however they are to be specified, axioms.</p>
  
  <p>So far i thought that this could and should be done using <code>axiomatization</code>, but everyone here tells me <code>axiomatzation</code> is bad.</p>
  
  <p>This leads me to my question how should this task be done. How can 2, say propositional, formulas be compared in Isabelle with regards towards their syntactical equivalence. To give a concrete example:</p>
  
  <pre><code>formula ∧ formula | formula ∨ formula
  </code></pre>
  
  <p>are given as operators, if possible as datatype</p>
  
  <p>and <code>distributive and commutative property</code> are given as rules.
  <code>A ∧ B = B ∧ A</code>, if stated in a theorem should be provable.</p>
  
  <p>That's what i want to do, i hope the idea is clear and someone can explain to me how to pursue this properly in Isabelle. Thanks in advance.</p>