author | nipkow |

Mon Nov 05 15:37:41 2007 +0100 (2007-11-05) | |

changeset 25281 | 8d309beb66d6 |

parent 25280 | c7686ac6c240 |

child 25282 | 1cc04c8e1253 |

removed advanced recdef section and replaced it by citation of Alex's tutorial.

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