title: Universal Quantification in Isabelle/HOL
body: <p>It has come to my attention that there are several ways to deal with universal quantification when working with Isabelle/HOL Isar. I am trying to write some proofs in a style that is suitable for undergraduate students to understand and reproduce (that's why I'm using Isar!) and I am confused about how to express universal quantification in a nice way.</p>
  
  <p>In Coq for example, I can write <code>forall x, P(x)</code> and then I may say "induction x" and that will automatically generate goals according to the corresponding induction principle. However, in Isabelle/HOL Isar, if I want to directly apply an induction principle I must state the theorem without any quantification, like this:</p>
  
  <pre><code>lemma foo: P(x)
  proof (induct x)
  </code></pre>
  
  <p>And this works fine as x is then treated as a schematic variable, as if it was universally quantified. However, it lacks the universal quantification in the statement which is not very educational. Another way I have fund is by using <code>\&lt;And&gt;</code> and <code>\&lt;forall&gt;</code>. However, I can not directly apply the induction principle if I state the lemma in this way, I have to first fix the universally quantified variables... which again seems inconvenient from an educational point of view:</p>
  
  <pre><code>lemma foo: \&lt;And&gt;x. P(x)
  proof -
  fix x
  show "P(x)"
  proof (induct x)
  </code></pre>
  
  <p>What is a nice proof pattern for expressing universal quantification that does not require me to explicitly fix variables before induction?</p>