1\section{Introduction} 2 3Starting from Isabelle 2007, new facilities for recursive 4function definitions~\cite{krauss2006} are available. They provide 5better support for general recursive definitions than previous 6packages. But despite all tool support, function definitions can 7sometimes be a difficult thing. 8 9This tutorial is an example-guided introduction to the practical use 10of the package and related tools. It should help you get started with 11defining functions quickly. For the more difficult definitions we will 12discuss what problems can arise, and how they can be solved. 13 14We assume that you have mastered the fundamentals of Isabelle/HOL 15and are able to write basic specifications and proofs. To start out 16with Isabelle in general, consult the Isabelle/HOL tutorial 17\cite{isa-tutorial}. 18 19 20 21\paragraph{Structure of this tutorial.} 22Section 2 introduces the syntax and basic operation of the \cmd{fun} 23command, which provides full automation with reasonable default 24behavior. The impatient reader can stop after that 25section, and consult the remaining sections only when needed. 26Section 3 introduces the more verbose \cmd{function} command which 27gives fine-grained control. This form should be used 28whenever the short form fails. 29After that we discuss more specialized issues: 30termination, mutual, nested and higher-order recursion, partiality, pattern matching 31and others. 32 33 34\paragraph{Some background.} 35Following the LCF tradition, the package is realized as a definitional 36extension: Recursive definitions are internally transformed into a 37non-recursive form, such that the function can be defined using 38standard definition facilities. Then the recursive specification is 39derived from the primitive definition. This is a complex task, but it 40is fully automated and mostly transparent to the user. Definitional 41extensions are valuable because they are conservative by construction: 42The \qt{new} concept of general wellfounded recursion is completely reduced 43to existing principles. 44 45 46 47 48The new \cmd{function} command, and its short form \cmd{fun} have mostly 49replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve 50a few of technical issues around \cmd{recdef}, and allow definitions 51which were not previously possible. 52 53In addition there is also the \cmd{partial\_function} command 54(see \cite{isabelle-isar-ref}) that supports the definition of partial 55and tail recursive functions. 56 57 58