--- a/src/Doc/Codegen/Foundations.thy Sat Dec 17 10:18:12 2022 +0100
+++ b/src/Doc/Codegen/Foundations.thy Sat Dec 17 21:26:24 2022 +0100
@@ -263,8 +263,9 @@
subsection \<open>Explicit partiality \label{sec:partiality}\<close>
text \<open>
- Partiality usually enters the game by partial patterns, as
- in the following example, again for amortised queues:
+ Explicit partiality is caused by missing patterns
+ (in contrast to partiality caused by nontermination, which is covered in Section~\ref{sec:partial}).
+ Here is an example, again for amortised queues:
\<close>
definition %quote strict_dequeue :: "'a queue \<Rightarrow> 'a \<times> 'a queue" where
--- a/src/Doc/Codegen/Partial_Functions.thy Sat Dec 17 10:18:12 2022 +0100
+++ b/src/Doc/Codegen/Partial_Functions.thy Sat Dec 17 21:26:24 2022 +0100
@@ -1,10 +1,11 @@
theory Partial_Functions
-imports Main "HOL-Library.Monad_Syntax"
+imports Setup "HOL-Library.Monad_Syntax"
begin
section \<open>Partial Functions \label{sec:partial}\<close>
-text \<open>We demonstrate three approaches to defining executable partial recursive functions.
+text \<open>We demonstrate three approaches to defining executable partial recursive functions,
+i.e.\ functions that do not terminate for all inputs.
The main points are the definitions of the functions and the inductive proofs about them.
Our concrete example represents a typical termination problem: following a data structure that
@@ -23,7 +24,7 @@
lemma finite_rel[simp]: "finite(rel ns)"
(*<*)by(simp add: rel_def)(*>*)
-text \<open>This relation should be acyclic
+text \<open>\noindent This relation should be acyclic
to guarantee termination of the partial functions defined below.\<close>
@@ -83,7 +84,7 @@
"count ns n
= (if n < length ns then do {k \<leftarrow> count ns (ns!n); Some (k+1)} else Some 0)"
-text \<open>We use a Haskell-like \<open>do\<close> notation (import @{theory "HOL-Library.Monad_Syntax"})
+text \<open>\noindent We use a Haskell-like \<open>do\<close> notation (import @{theory "HOL-Library.Monad_Syntax"})
to abbreviate the clumsy explicit
\noindent
@@ -123,8 +124,13 @@
morphisms rep_acyc abs_acyc
using acyclic_rel_Nil by auto
-text \<open>This defines two functions \<open>rep_acyc :: acyc \<Rightarrow> nat list\<close> and \<open>abs_acyc :: nat list \<Rightarrow> acyc\<close>.
-Function @{const abs_acyc} is only defined on acyclic lists and not executable for that reason.\<close>
+text \<open>\noindent This defines two functions @{term [source] "rep_acyc :: acyc \<Rightarrow> nat list"}
+and @{const abs_acyc} \<open>::\<close> \mbox{@{typ "nat list \<Rightarrow> acyc"}}.
+Function @{const abs_acyc} is only defined on acyclic lists and not executable for that reason.
+Type \<open>dlist\<close> in Section~\ref{sec:partiality} is defined in the same manner.
+
+The following command sets up infrastructure for lifting functions on @{typ "nat list"}
+to @{typ acyc} (used by @{command_def lift_definition} below) \cite{isabelle-isar-ref}.\<close>
setup_lifting type_definition_acyc
@@ -135,7 +141,7 @@
= (let ns = rep_acyc ac in if n < length ns then follow2 ac (ns!n) else n)"
by pat_completeness auto
-text \<open>Now we prepare for termination proof.
+text \<open>Now we prepare for the termination proof.
Relation \<open>rel_follow2\<close> is almost identical to @{const rel_follow}.\<close>
definition "rel_follow2 = same_fst (acyclic o rel o rep_acyc) (rel o rep_acyc)"
@@ -188,7 +194,7 @@
"\<lambda>ns. if acyclic(rel ns) then ns else []"
(*<*)by (auto simp: acyclic_rel_Nil)(*>*)
-text \<open>This works because we can easily prove that for any \<open>ns\<close>,
+text \<open>\noindent This works because we can easily prove that for any \<open>ns\<close>,
the \<open>\<lambda>\<close>-term produces an acyclic list.
But it requires the possibly expensive check @{prop "acyclic(rel ns)"}.\<close>