# A Practical Introduction to Theorem Proving with Isabelle/HOL

### 21-23 August 2015 in Nanjing, preceding ITP 2015

You would like to learn how to use the proof assistant Isabelle/HOL? This
intensive 3-day tutorial is aimed both at theorem proving novices and at
people already familiar with another proof assistant who want to learn about
Isabelle. The tutorial consists of a mixture of interactive lectures and
hands-on lab sessions where the participants solve theorem proving problems
with Isabelle. The following material is covered:
- A Functional Programming introduction to theorem proving:
Data types, recursive functions and proof by induction
- Beyond equality: logic and set theory
- Inductive definitions
- Isabelle's automatic proof toolbox
- Isar: a language for writing structured and readable proofs

The tutorial (given by Tobias Nipkow)
will be based on Part I of the book Concrete Semantics that is
freely availble online (and is also available as this separate
document). Participants should bring their own laptops with Isabelle already installed on it (or
share with a fellow student - the latter is encouraged for the practical
exercises.)
This tutorial can also serve as a pre-ITP introduction to the field of
interactive theorem proving for novices.