title: Why won't Isabelle simplify the body of my "if _ then _ else" construct?
body: <p>I have the following Isabelle goal:</p>
  
  <pre><code>lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"
  </code></pre>
  
  <p>None of the tactics <code>simp</code>, <code>fast</code>, <code>clarsimp</code>, <code>blast</code>, <code>fastforce</code>, etc. make any progress on the goal, despite it being quite simple.</p>
  
  <p>Why doesn't Isabelle just simplify the body of the <code>if</code> construct so that both "a ≠ a" and "b ≠ b" become <code>False</code>, and hence solve the goal?</p>