# HG changeset patch # User nipkow # Date 1194273461 -3600 # Node ID 8d309beb66d6e79561a40872117105d6a5cee5b2 # Parent c7686ac6c240bba202bdf809ddf028c2b23cb7dc removed advanced recdef section and replaced it by citation of Alex's tutorial. diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Advanced/ROOT.ML --- a/doc-src/TutorialI/Advanced/ROOT.ML Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/Advanced/ROOT.ML Mon Nov 05 15:37:41 2007 +0100 @@ -1,5 +1,2 @@ use "../settings.ML"; -no_document use_thy "While_Combinator"; use_thy "simp"; -use_thy "WFrec"; -use_thy "Partial"; diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/Advanced/advanced.tex Mon Nov 05 15:37:41 2007 +0100 @@ -1,51 +1,49 @@ -\chapter{Advanced Simplification, Recursion and Induction} +\chapter{Advanced Simplification and Induction} -Although we have already learned a lot about simplification, recursion and +Although we have already learned a lot about simplification and induction, there are some advanced proof techniques that we have not covered -yet and which are worth learning. The three sections of this chapter are almost -independent of each other and can be read in any order. Only the notion of -\emph{congruence rules}, introduced in the section on simplification, is -required for parts of the section on recursion. +yet and which are worth learning. The sections of this chapter are +independent of each other and can be read in any order. \input{Advanced/document/simp.tex} -\section{Advanced Forms of Recursion} -\index{recdef@\isacommand {recdef} (command)|(} - -This section introduces advanced forms of -\isacommand{recdef}: how to establish termination by means other than measure -functions, how to define recursive functions over nested recursive datatypes -and how to deal with partial functions. - -If, after reading this section, you feel that the definition of recursive -functions is overly complicated by the requirement of -totality, you should ponder the alternatives. In a logic of partial functions, -recursive definitions are always accepted. But there are many -such logics, and no clear winner has emerged. And in all of these logics you -are (more or less frequently) required to reason about the definedness of -terms explicitly. Thus one shifts definedness arguments from definition time to -proof time. In HOL you may have to work hard to define a function, but proofs -can then proceed unencumbered by worries about undefinedness. - -\subsection{Beyond Measure} -\label{sec:beyond-measure} -\input{Advanced/document/WFrec.tex} - -\subsection{Recursion Over Nested Datatypes} -\label{sec:nested-recdef} -\input{Recdef/document/Nested0.tex} -\input{Recdef/document/Nested1.tex} -\input{Recdef/document/Nested2.tex} - -\subsection{Partial Functions} -\index{functions!partial} -\input{Advanced/document/Partial.tex} - -\index{recdef@\isacommand {recdef} (command)|)} - \section{Advanced Induction Techniques} \label{sec:advanced-ind} \index{induction|(} \input{Misc/document/AdvancedInd.tex} \input{CTL/document/CTLind.tex} \index{induction|)} + +%\section{Advanced Forms of Recursion} +%\index{recdef@\isacommand {recdef} (command)|(} + +%This section introduces advanced forms of +%\isacommand{recdef}: how to establish termination by means other than measure +%functions, how to define recursive functions over nested recursive datatypes +%and how to deal with partial functions. +% +%If, after reading this section, you feel that the definition of recursive +%functions is overly complicated by the requirement of +%totality, you should ponder the alternatives. In a logic of partial functions, +%recursive definitions are always accepted. But there are many +%such logics, and no clear winner has emerged. And in all of these logics you +%are (more or less frequently) required to reason about the definedness of +%terms explicitly. Thus one shifts definedness arguments from definition time to +%proof time. In HOL you may have to work hard to define a function, but proofs +%can then proceed unencumbered by worries about undefinedness. + +%\subsection{Beyond Measure} +%\label{sec:beyond-measure} +%\input{Advanced/document/WFrec.tex} +% +%\subsection{Recursion Over Nested Datatypes} +%\label{sec:nested-recdef} +%\input{Recdef/document/Nested0.tex} +%\input{Recdef/document/Nested1.tex} +%\input{Recdef/document/Nested2.tex} +% +%\subsection{Partial Functions} +%\index{functions!partial} +%\input{Advanced/document/Partial.tex} +% +%\index{recdef@\isacommand {recdef} (command)|)} diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/Datatype/Nested.thy Mon Nov 05 15:37:41 2007 +0100 @@ -142,17 +142,17 @@ declare subst_App [simp del] -text{*\noindent -The advantage is that now we have replaced @{const substs} by -@{term map}, we can profit from the large number of pre-proved lemmas -about @{term map}. Unfortunately inductive proofs about type -@{text term} are still awkward because they expect a conjunction. One -could derive a new induction principle as well (see -\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} -and to define functions with \isacommand{fun} instead. -Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below, -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can -handle nested recursion. +text{*\noindent The advantage is that now we have replaced @{const +substs} by @{const map}, we can profit from the large number of +pre-proved lemmas about @{const map}. Unfortunately, inductive proofs +about type @{text term} are still awkward because they expect a +conjunction. One could derive a new induction principle as well (see +\S\ref{sec:derive-ind}), but simpler is to stop using +\isacommand{primrec} and to define functions with \isacommand{fun} +instead. Simple uses of \isacommand{fun} are described in +\S\ref{sec:fun} below. Advanced applications, including functions +over nested datatypes like @{text term}, are discussed in a +separate tutorial~\cite{isabelle-function}. Of course, you may also combine mutual and nested recursion of datatypes. For example, constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Nov 05 15:37:41 2007 +0100 @@ -206,17 +206,16 @@ \isacommand{declare}\isamarkupfalse% \ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}% \begin{isamarkuptext}% -\noindent -The advantage is that now we have replaced \isa{substs} by -\isa{map}, we can profit from the large number of pre-proved lemmas -about \isa{map}. Unfortunately inductive proofs about type -\isa{term} are still awkward because they expect a conjunction. One -could derive a new induction principle as well (see -\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} -and to define functions with \isacommand{fun} instead. -Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below, -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can -handle nested recursion. +\noindent The advantage is that now we have replaced \isa{substs} by \isa{map}, we can profit from the large number of +pre-proved lemmas about \isa{map}. Unfortunately, inductive proofs +about type \isa{term} are still awkward because they expect a +conjunction. One could derive a new induction principle as well (see +\S\ref{sec:derive-ind}), but simpler is to stop using +\isacommand{primrec} and to define functions with \isacommand{fun} +instead. Simple uses of \isacommand{fun} are described in +\S\ref{sec:fun} below. Advanced applications, including functions +over nested datatypes like \isa{term}, are discussed in a +separate tutorial~\cite{isabelle-function}. Of course, you may also combine mutual and nested recursion of datatypes. For example, constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/IsaMakefile Mon Nov 05 15:37:41 2007 +0100 @@ -4,7 +4,7 @@ ## targets -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \ +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \ HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \ HOL-Protocol HOL-Documents styles images: @@ -104,23 +104,11 @@ @rm -f tutorial.dvi -## HOL-Recdef - -HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz - -$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ - Recdef/simplification.thy Recdef/Induction.thy \ - Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy - $(USEDIR) Recdef - @rm -f tutorial.dvi - - ## HOL-Advanced HOL-Advanced: HOL $(LOG)/HOL-Advanced.gz -$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy \ - Advanced/Partial.thy +$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML $(USEDIR) Advanced @rm -f tutorial.dvi @@ -205,4 +193,4 @@ ## clean clean: - @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 + @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 diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/Sets/sets.tex --- a/doc-src/TutorialI/Sets/sets.tex Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Mon Nov 05 15:37:41 2007 +0100 @@ -876,8 +876,8 @@ \index{relations!well-founded|(}% A well-founded relation captures the notion of a terminating process. Complex recursive functions definitions must specify a -well-founded relation that justifies their termination -({\S}\ref{sec:beyond-measure}). Most of the forms of induction found +well-founded relation that justifies their +termination~\cite{isabelle-function}. Most of the forms of induction found in mathematics are merely special cases of induction over a well-founded relation. diff -r c7686ac6c240 -r 8d309beb66d6 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Mon Nov 05 15:04:19 2007 +0100 +++ b/doc-src/TutorialI/fp.tex Mon Nov 05 15:37:41 2007 +0100 @@ -469,8 +469,9 @@ recursion need not involve datatypes, and termination is proved by showing that the arguments of all recursive calls are smaller in a suitable sense. In this section we restrict ourselves to functions where Isabelle can prove -termination automatically. User supplied termination proofs are discussed in -{\S}\ref{sec:beyond-measure}. +termination automatically. More advanced function definitions, including user +supplied termination proofs, nested recursion and partiality, are discussed +in a separate tutorial~\cite{isabelle-function}. \input{Fun/document/fun0.tex}