title: How to use obtain to make forward elimination proofs easier to read?
body: <p>I'm trying to do basic natural deduction proofs in Isabelle, following <a href="https://isabelle.in.tum.de/Isar/Isar-ND.pdf" rel="nofollow noreferrer">this document</a> (particularly slide 23).</p>
  
  <p>I know I can do things like</p>
  
  <pre><code>theorem ‹(A ⟶ B) ⟶ A ⟶ B›
  proof -
    {
      assume ‹A ⟶ B›
      {
        assume ‹A›
        with ‹A ⟶ B› have ‹B› ..
      }
      hence ‹A ⟶ B› ..
    }
    thus ‹(A ⟶ B) ⟶ A ⟶ B› ..
  qed
  </code></pre>
  
  <p>But also</p>
  
  <pre><code>theorem ‹(A ⟶ B) ⟶ A ⟶ B›
  proof
    assume ‹A ⟶ B› and ‹A›
    then obtain ‹B› ..
  qed
  </code></pre>
  
  <p>achieves the same goal.</p>
  
  <p>So when I try to write the proof</p>
  
  <pre><code>theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
  proof -
    {
      assume ‹A ⟶ A ⟶ B›
      {
        assume ‹A›
        with ‹A ⟶ A ⟶ B› have ‹A ⟶ B› ..
        hence ‹B› using ‹A› ..
      }
      hence ‹A ⟶ B› ..
    }
    thus ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B› ..
  qed
  </code></pre>
  
  <p>like</p>
  
  <pre><code>theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
  proof
    assume ‹A ⟶ A ⟶ B› and ‹A›
    hence ‹A ⟶ B› ..
    then obtain ‹B› using ‹A› ..
  qed
  </code></pre>
  
  <p>why does Isabelle complain that</p>
  
  <pre><code>Failed to finish proof:
  goal (1 subgoal):
   1. A ⟶ A ⟶ B ⟹ A ⟶ B
  </code></pre>
  
  <p>I'm aware that these are very simple things that Isabelle can prove in one step: the goal here is to produce a concise proof which is human readable (to the extent that Natural Deduction is), without having to consult Isabelle.</p>