title: How can we force Isabelle to reveal to us what rule it's applying in the background in Isar when a proof starts?
body: <p>I was trying to prove:</p>
  
  <pre><code>lemma
    shows "¬ ev (Suc 0)"
  </code></pre>
  
  <p>I did:</p>
  
  <pre><code>lemma
    shows "¬ ev (Suc 0)"
  proof (rule notI)
    assume "ev (Suc 0)"
    then show False 
    proof
  </code></pre>
  
  <p>and it gave me really pretty goals:</p>
  
  <pre><code>proof (state)
  goal (2 subgoals):
   1. Suc 0 = 0 ⟹ False
   2. ⋀n. ⟦Suc 0 = Suc (Suc n); ev n⟧ ⟹ False
  </code></pre>
  
  <p>that could probably make my proof readable.</p>
  
  <p>It seems it applied some sort of cases in the background. But when I wrote cases the proof finished immediately instead of showing the above rule inversion cases explicitly. See:</p>
  
  <pre><code>lemma
    shows "¬ ev (Suc 0)"
  proof (rule notI)
    assume "ev (Suc 0)"
    then show False 
    proof (cases)
  </code></pre>
  
  <p>which shows:</p>
  
  <pre><code>proof (state)
  goal:
  No subgoals!
  </code></pre>
  
  <p>which means I can just place a <code>qed</code>. </p>
  
  <p>How can I figure out exactly what (introduction?) rules Isar is doing automatically in Isabelle?</p>