removed advanced recdef section and replaced it by citation of Alex's tutorial.
authornipkow
Mon Nov 05 15:37:41 2007 +0100 (2007-11-05)
changeset 252818d309beb66d6
parent 25280 c7686ac6c240
child 25282 1cc04c8e1253
removed advanced recdef section and replaced it by citation of Alex's tutorial.
doc-src/TutorialI/Advanced/ROOT.ML
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/fp.tex
     1.1 --- a/doc-src/TutorialI/Advanced/ROOT.ML	Mon Nov 05 15:04:19 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/ROOT.ML	Mon Nov 05 15:37:41 2007 +0100
     1.3 @@ -1,5 +1,2 @@
     1.4  use "../settings.ML";
     1.5 -no_document use_thy "While_Combinator";
     1.6  use_thy "simp";
     1.7 -use_thy "WFrec";
     1.8 -use_thy "Partial";
     2.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Nov 05 15:04:19 2007 +0100
     2.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Mon Nov 05 15:37:41 2007 +0100
     2.3 @@ -1,51 +1,49 @@
     2.4 -\chapter{Advanced Simplification, Recursion and Induction}
     2.5 +\chapter{Advanced Simplification and Induction}
     2.6  
     2.7 -Although we have already learned a lot about simplification, recursion and
     2.8 +Although we have already learned a lot about simplification and
     2.9  induction, there are some advanced proof techniques that we have not covered
    2.10 -yet and which are worth learning. The three sections of this chapter are almost
    2.11 -independent of each other and can be read in any order. Only the notion of
    2.12 -\emph{congruence rules}, introduced in the section on simplification, is
    2.13 -required for parts of the section on recursion.
    2.14 +yet and which are worth learning. The sections of this chapter are
    2.15 +independent of each other and can be read in any order.
    2.16  
    2.17  \input{Advanced/document/simp.tex}
    2.18  
    2.19 -\section{Advanced Forms of Recursion}
    2.20 -\index{recdef@\isacommand {recdef} (command)|(}
    2.21 -
    2.22 -This section introduces advanced forms of
    2.23 -\isacommand{recdef}: how to establish termination by means other than measure
    2.24 -functions, how to define recursive functions over nested recursive datatypes
    2.25 -and how to deal with partial functions.
    2.26 -
    2.27 -If, after reading this section, you feel that the definition of recursive
    2.28 -functions is overly complicated by the requirement of
    2.29 -totality, you should ponder the alternatives.  In a logic of partial functions,
    2.30 -recursive definitions are always accepted.  But there are many
    2.31 -such logics, and no clear winner has emerged. And in all of these logics you
    2.32 -are (more or less frequently) required to reason about the definedness of
    2.33 -terms explicitly. Thus one shifts definedness arguments from definition time to
    2.34 -proof time. In HOL you may have to work hard to define a function, but proofs
    2.35 -can then proceed unencumbered by worries about undefinedness.
    2.36 -
    2.37 -\subsection{Beyond Measure}
    2.38 -\label{sec:beyond-measure}
    2.39 -\input{Advanced/document/WFrec.tex}
    2.40 -
    2.41 -\subsection{Recursion Over Nested Datatypes}
    2.42 -\label{sec:nested-recdef}
    2.43 -\input{Recdef/document/Nested0.tex}
    2.44 -\input{Recdef/document/Nested1.tex}
    2.45 -\input{Recdef/document/Nested2.tex}
    2.46 -
    2.47 -\subsection{Partial Functions}
    2.48 -\index{functions!partial}
    2.49 -\input{Advanced/document/Partial.tex}
    2.50 -
    2.51 -\index{recdef@\isacommand {recdef} (command)|)}
    2.52 -
    2.53  \section{Advanced Induction Techniques}
    2.54  \label{sec:advanced-ind}
    2.55  \index{induction|(}
    2.56  \input{Misc/document/AdvancedInd.tex}
    2.57  \input{CTL/document/CTLind.tex}
    2.58  \index{induction|)}
    2.59 +
    2.60 +%\section{Advanced Forms of Recursion}
    2.61 +%\index{recdef@\isacommand {recdef} (command)|(}
    2.62 +
    2.63 +%This section introduces advanced forms of
    2.64 +%\isacommand{recdef}: how to establish termination by means other than measure
    2.65 +%functions, how to define recursive functions over nested recursive datatypes
    2.66 +%and how to deal with partial functions.
    2.67 +%
    2.68 +%If, after reading this section, you feel that the definition of recursive
    2.69 +%functions is overly complicated by the requirement of
    2.70 +%totality, you should ponder the alternatives.  In a logic of partial functions,
    2.71 +%recursive definitions are always accepted.  But there are many
    2.72 +%such logics, and no clear winner has emerged. And in all of these logics you
    2.73 +%are (more or less frequently) required to reason about the definedness of
    2.74 +%terms explicitly. Thus one shifts definedness arguments from definition time to
    2.75 +%proof time. In HOL you may have to work hard to define a function, but proofs
    2.76 +%can then proceed unencumbered by worries about undefinedness.
    2.77 +
    2.78 +%\subsection{Beyond Measure}
    2.79 +%\label{sec:beyond-measure}
    2.80 +%\input{Advanced/document/WFrec.tex}
    2.81 +%
    2.82 +%\subsection{Recursion Over Nested Datatypes}
    2.83 +%\label{sec:nested-recdef}
    2.84 +%\input{Recdef/document/Nested0.tex}
    2.85 +%\input{Recdef/document/Nested1.tex}
    2.86 +%\input{Recdef/document/Nested2.tex}
    2.87 +%
    2.88 +%\subsection{Partial Functions}
    2.89 +%\index{functions!partial}
    2.90 +%\input{Advanced/document/Partial.tex}
    2.91 +%
    2.92 +%\index{recdef@\isacommand {recdef} (command)|)}
     3.1 --- a/doc-src/TutorialI/Datatype/Nested.thy	Mon Nov 05 15:04:19 2007 +0100
     3.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Mon Nov 05 15:37:41 2007 +0100
     3.3 @@ -142,17 +142,17 @@
     3.4  
     3.5  declare subst_App [simp del]
     3.6  
     3.7 -text{*\noindent
     3.8 -The advantage is that now we have replaced @{const substs} by
     3.9 -@{term map}, we can profit from the large number of pre-proved lemmas
    3.10 -about @{term map}.  Unfortunately inductive proofs about type
    3.11 -@{text term} are still awkward because they expect a conjunction. One
    3.12 -could derive a new induction principle as well (see
    3.13 -\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
    3.14 -and to define functions with \isacommand{fun} instead.
    3.15 -Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
    3.16 -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can 
    3.17 -handle nested recursion.
    3.18 +text{*\noindent The advantage is that now we have replaced @{const
    3.19 +substs} by @{const map}, we can profit from the large number of
    3.20 +pre-proved lemmas about @{const map}.  Unfortunately, inductive proofs
    3.21 +about type @{text term} are still awkward because they expect a
    3.22 +conjunction. One could derive a new induction principle as well (see
    3.23 +\S\ref{sec:derive-ind}), but simpler is to stop using
    3.24 +\isacommand{primrec} and to define functions with \isacommand{fun}
    3.25 +instead.  Simple uses of \isacommand{fun} are described in
    3.26 +\S\ref{sec:fun} below.  Advanced applications, including functions
    3.27 +over nested datatypes like @{text term}, are discussed in a
    3.28 +separate tutorial~\cite{isabelle-function}.
    3.29  
    3.30  Of course, you may also combine mutual and nested recursion of datatypes. For example,
    3.31  constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
     4.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Nov 05 15:04:19 2007 +0100
     4.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Nov 05 15:37:41 2007 +0100
     4.3 @@ -206,17 +206,16 @@
     4.4  \isacommand{declare}\isamarkupfalse%
     4.5  \ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}%
     4.6  \begin{isamarkuptext}%
     4.7 -\noindent
     4.8 -The advantage is that now we have replaced \isa{substs} by
     4.9 -\isa{map}, we can profit from the large number of pre-proved lemmas
    4.10 -about \isa{map}.  Unfortunately inductive proofs about type
    4.11 -\isa{term} are still awkward because they expect a conjunction. One
    4.12 -could derive a new induction principle as well (see
    4.13 -\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
    4.14 -and to define functions with \isacommand{fun} instead.
    4.15 -Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
    4.16 -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can 
    4.17 -handle nested recursion.
    4.18 +\noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of
    4.19 +pre-proved lemmas about \isa{map}.  Unfortunately, inductive proofs
    4.20 +about type \isa{term} are still awkward because they expect a
    4.21 +conjunction. One could derive a new induction principle as well (see
    4.22 +\S\ref{sec:derive-ind}), but simpler is to stop using
    4.23 +\isacommand{primrec} and to define functions with \isacommand{fun}
    4.24 +instead.  Simple uses of \isacommand{fun} are described in
    4.25 +\S\ref{sec:fun} below.  Advanced applications, including functions
    4.26 +over nested datatypes like \isa{term}, are discussed in a
    4.27 +separate tutorial~\cite{isabelle-function}.
    4.28  
    4.29  Of course, you may also combine mutual and nested recursion of datatypes. For example,
    4.30  constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
     5.1 --- a/doc-src/TutorialI/IsaMakefile	Mon Nov 05 15:04:19 2007 +0100
     5.2 +++ b/doc-src/TutorialI/IsaMakefile	Mon Nov 05 15:37:41 2007 +0100
     5.3 @@ -4,7 +4,7 @@
     5.4  
     5.5  ## targets
     5.6  
     5.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \
     5.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
     5.9    HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
    5.10    HOL-Protocol HOL-Documents styles
    5.11  images:
    5.12 @@ -104,23 +104,11 @@
    5.13  	@rm -f tutorial.dvi
    5.14  
    5.15  
    5.16 -## HOL-Recdef
    5.17 -
    5.18 -HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
    5.19 -
    5.20 -$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \
    5.21 -  Recdef/simplification.thy Recdef/Induction.thy \
    5.22 -  Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy
    5.23 -	$(USEDIR) Recdef
    5.24 -	@rm -f tutorial.dvi
    5.25 -
    5.26 -
    5.27  ## HOL-Advanced
    5.28  
    5.29  HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz
    5.30  
    5.31 -$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \
    5.32 -	Advanced/Partial.thy
    5.33 +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
    5.34  	$(USEDIR) Advanced
    5.35  	@rm -f tutorial.dvi
    5.36  
    5.37 @@ -205,4 +193,4 @@
    5.38  ## clean
    5.39  
    5.40  clean:
    5.41 -	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex
    5.42 +	@rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Fun.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-Rules.gz $(LOG)/HOL-Sets.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz $(LOG)/HOL-Types.gz $(LOG)/HOL-Protocol.gz $(LOG)/HOL-Documents.gz Rules/document/*.tex Sets/document/*.tex
     6.1 --- a/doc-src/TutorialI/Sets/sets.tex	Mon Nov 05 15:04:19 2007 +0100
     6.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Mon Nov 05 15:37:41 2007 +0100
     6.3 @@ -876,8 +876,8 @@
     6.4  \index{relations!well-founded|(}%
     6.5  A well-founded relation captures the notion of a terminating
     6.6  process. Complex recursive functions definitions must specify a
     6.7 -well-founded relation that justifies their termination
     6.8 -({\S}\ref{sec:beyond-measure}).  Most of the forms of induction found
     6.9 +well-founded relation that justifies their
    6.10 +termination~\cite{isabelle-function}. Most of the forms of induction found
    6.11  in mathematics are merely special cases of induction over a
    6.12  well-founded relation.
    6.13  
     7.1 --- a/doc-src/TutorialI/fp.tex	Mon Nov 05 15:04:19 2007 +0100
     7.2 +++ b/doc-src/TutorialI/fp.tex	Mon Nov 05 15:37:41 2007 +0100
     7.3 @@ -469,8 +469,9 @@
     7.4  recursion need not involve datatypes, and termination is proved by showing
     7.5  that the arguments of all recursive calls are smaller in a suitable sense.
     7.6  In this section we restrict ourselves to functions where Isabelle can prove
     7.7 -termination automatically. User supplied termination proofs are discussed in
     7.8 -{\S}\ref{sec:beyond-measure}.
     7.9 +termination automatically. More advanced function definitions, including user
    7.10 +supplied termination proofs, nested recursion and partiality, are discussed
    7.11 +in a separate tutorial~\cite{isabelle-function}.
    7.12  
    7.13  \input{Fun/document/fun0.tex}
    7.14