1 2\documentclass[a4paper,fleqn]{article} 3 4\usepackage{latexsym,graphicx} 5\usepackage[refpage]{nomencl} 6\usepackage{iman,extra,isar} 7\usepackage{isabelle,isabellesym} 8\usepackage{style} 9\usepackage{mathpartir} 10\usepackage{amsthm} 11\usepackage{pdfsetup} 12 13\newcommand{\cmd}[1]{\isacommand{#1}} 14 15\newcommand{\isasymINFIX}{\cmd{infix}} 16\newcommand{\isasymLOCALE}{\cmd{locale}} 17\newcommand{\isasymINCLUDES}{\cmd{includes}} 18\newcommand{\isasymDATATYPE}{\cmd{datatype}} 19\newcommand{\isasymDEFINES}{\cmd{defines}} 20\newcommand{\isasymNOTES}{\cmd{notes}} 21\newcommand{\isasymCLASS}{\cmd{class}} 22\newcommand{\isasymINSTANCE}{\cmd{instance}} 23\newcommand{\isasymLEMMA}{\cmd{lemma}} 24\newcommand{\isasymPROOF}{\cmd{proof}} 25\newcommand{\isasymQED}{\cmd{qed}} 26\newcommand{\isasymFIX}{\cmd{fix}} 27\newcommand{\isasymASSUME}{\cmd{assume}} 28\newcommand{\isasymSHOW}{\cmd{show}} 29\newcommand{\isasymNOTE}{\cmd{note}} 30\newcommand{\isasymCODEGEN}{\cmd{code\_gen}} 31\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}} 32\newcommand{\isasymFUN}{\cmd{fun}} 33\newcommand{\isasymFUNCTION}{\cmd{function}} 34\newcommand{\isasymPRIMREC}{\cmd{primrec}} 35\newcommand{\isasymRECDEF}{\cmd{recdef}} 36 37\newcommand{\qt}[1]{``#1''} 38\newcommand{\qtt}[1]{"{}{#1}"{}} 39\newcommand{\qn}[1]{\emph{#1}} 40\newcommand{\strong}[1]{{\bfseries #1}} 41\newcommand{\fixme}[1][!]{\strong{FIXME: #1}} 42 43\newtheorem{exercise}{Exercise}{\bf}{\itshape} 44%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape} 45 46\hyphenation{Isabelle} 47\hyphenation{Isar} 48 49\isadroptag{theory} 50\title{Defining Recursive Functions in Isabelle/HOL} 51\author{Alexander Krauss} 52 53\isabellestyle{tt} 54 55\begin{document} 56 57\date{\ \\} 58\maketitle 59 60\begin{abstract} 61 This tutorial describes the use of the \emph{function} package, 62 which provides general recursive function definitions for Isabelle/HOL. 63 We start with very simple examples and then gradually move on to more 64 advanced topics such as manual termination proofs, nested recursion, 65 partiality, tail recursion and congruence rules. 66\end{abstract} 67 68%\thispagestyle{empty}\clearpage 69 70%\pagenumbering{roman} 71%\clearfirst 72 73\input{intro.tex} 74\input{Functions.tex} 75%\input{conclusion.tex} 76 77\begingroup 78%\tocentry{\bibname} 79\bibliographystyle{plain} \small\raggedright\frenchspacing 80\bibliography{manual} 81\endgroup 82 83\end{document} 84 85 86%%% Local Variables: 87%%% mode: latex 88%%% TeX-master: t 89%%% End: 90