# HG changeset patch
# User nipkow
# Date 1671210663 -3600
# Node ID 9a6cb5ecc183d35c0cd2aaaa2f06422689bc6530
# Parent  f8826fc8c4191cafa8cc8100596bddba7bafc62e
Added section about code generation for partial functions

diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Codegen/Introduction.thy
--- a/src/Doc/Codegen/Introduction.thy	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Fri Dec 16 18:11:03 2022 +0100
@@ -222,6 +222,9 @@
       dramatically by applying refinement techniques, which are
       introduced in \secref{sec:refinement}.
 
+    \item How to define partial functions such that code can be generated
+      is explained in \secref{sec:partial}.
+
     \item Inductive predicates can be turned executable using an
       extension of the code generator \secref{sec:inductive}.
 
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Codegen/document/root.tex
--- a/src/Doc/Codegen/document/root.tex	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Codegen/document/root.tex	Fri Dec 16 18:11:03 2022 +0100
@@ -15,7 +15,7 @@
 
 \title{\includegraphics[scale=0.5]{isabelle_logo}
   \\[4ex] Code generation from Isabelle/HOL theories}
-\author{\emph{Florian Haftmann with contributions from Lukas Bulwahn}}
+\author{\emph{Florian Haftmann}\\ with contributions by Lukas Bulwahn and Tobias Nipkow}
 
 \begin{document}
 
@@ -35,6 +35,7 @@
 \input{Introduction.tex}
 \input{Foundations.tex}
 \input{Refinement.tex}
+\input{Partial_Functions.tex}
 \input{Inductive_Predicate.tex}
 \input{Evaluation.tex}
 \input{Computations.tex}
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Functions/Functions.thy	Fri Dec 16 18:11:03 2022 +0100
@@ -750,7 +750,7 @@
 termination by (relation "{}") simp
 
 
-section \<open>Partiality\<close>
+section \<open>Partiality \label{sec:partiality}\<close>
 
 text \<open>
   In HOL, all functions are total. A function \<^term>\<open>f\<close> applied to
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/Functions/document/intro.tex
--- a/src/Doc/Functions/document/intro.tex	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/Functions/document/intro.tex	Fri Dec 16 18:11:03 2022 +0100
@@ -43,8 +43,6 @@
 to existing principles.
 
 
-
-
 The new \cmd{function} command, and its short form \cmd{fun} have mostly
 replaced the traditional \cmd{recdef} command \cite{slind-tfl}. They solve
 a few of technical issues around \cmd{recdef}, and allow definitions
@@ -52,6 +50,10 @@
 
 In addition there is also the \cmd{partial\_function} command
 (see \cite{isabelle-isar-ref}) that supports the definition of partial
-and tail recursive functions.
+and tail recursive functions. This command is particulary relevant if one wants to
+generate executable code. This is covered in detail in the Code Generation
+tutorial~\cite{Haftmann-codegen}.
+The approach to partial function presented in Section~\ref{sec:partiality}
+of this tutorial does not support code generation.
 
 
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/ROOT	Fri Dec 16 18:11:03 2022 +0100
@@ -26,6 +26,7 @@
     Introduction
     Foundations
     Refinement
+    Partial_Functions
     Inductive_Predicate
     Evaluation
     Computations
diff -r f8826fc8c419 -r 9a6cb5ecc183 src/Doc/manual.bib
--- a/src/Doc/manual.bib	Fri Dec 16 09:55:22 2022 +0100
+++ b/src/Doc/manual.bib	Fri Dec 16 18:11:03 2022 +0100
@@ -827,6 +827,10 @@
 
 %H
 
+@manual{Haftmann-codegen,author={Florian Haftmann},
+title={Code generation from {Isabelle/HOL} theories},
+note={\url{http://isabelle.in.tum.de/doc/codegen.pdf}}}
+
 @inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
   author =      {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
   title =       {Data Refinement in {Isabelle/HOL}},