Introduction to the Isabelle Proof Assistant

Clemens Ballarin

Time and Location: 20 July 2016, Bielefeld, Germany.  Part of the FOMUS Workshop on Foundation of Mathematics.

Overview
This tutorial is a short introduction to the proof assistant Isabelle and its use.

• Part I
  Interacting with Isabelle, step-by-step natural deduction proofs and some automation.
  Slides [pdf]  [Demo1.thy]  [Demo2.thy]  [Exercise1.thy]  [Solution1.pdf] 


• Part II
  Isar, Isabelle’s declarative proof language, support for inductive definitions and induction.
  Slides [pdf]  [Demo3.thy]  [Demo4.thy]  [Exercise2.thy]  [Solution2.pdf]