1\documentclass[11pt,a4paper]{report} 2 3\input{prelude} 4 5\begin{document} 6 7\title{How to Prove it in Isabelle/HOL} 8%\subtitle{\includegraphics[scale=.7]{isabelle_hol}} 9\author{Tobias Nipkow} 10\maketitle 11 12 13\begin{abstract} 14 How does one perform induction on the length of a list? How are numerals 15 converted into \isa{Suc} terms? How does one prove equalities in rings 16 and other algebraic structures? 17 18 This document is a collection of practical hints and techniques for dealing 19 with specific frequently occurring situations in proofs in Isabelle/HOL. 20 Not arbitrary proofs but proofs that refer to material that is part of 21 \isa{Main} or \isa{Complex\_Main}. 22 23 This is \emph{not} an introduction to 24\begin{itemize} 25\item proofs in general; for that see mathematics or logic books. 26\item Isabelle/HOL and its proof language; for that see the tutorial 27 \cite{ProgProve} or the reference manual~\cite{IsarRef}. 28\item the contents of theory \isa{Main}; for that see the overview 29 \cite{Main}. 30\end{itemize} 31\end{abstract} 32 33\setcounter{tocdepth}{1} 34\tableofcontents 35 36\input{How_to_Prove_it.tex} 37 38\bibliographystyle{plain} 39\bibliography{root} 40 41%\printindex 42 43\end{document} 44