# HG changeset patch # User nipkow # Date 1193944819 -3600 # Node ID 22d16596c3060321934e0efdf09c8ea113ad182d # Parent 8faf184ba5b15a93de473885a551e5e03fcfaa16 recdef -> fun diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Advanced/Partial.thy --- a/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 01 20:20:19 2007 +0100 @@ -22,7 +22,7 @@ We have already seen an instance of underdefinedness by means of non-exhaustive pattern matching: the definition of @{term last} in -\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec} +\S\ref{sec:fun}. The same is allowed for \isacommand{primrec} *} consts hd :: "'a list \ 'a" diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Thu Nov 01 20:20:19 2007 +0100 @@ -38,7 +38,7 @@ We have already seen an instance of underdefinedness by means of non-exhaustive pattern matching: the definition of \isa{last} in -\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}% +\S\ref{sec:fun}. The same is allowed for \isacommand{primrec}% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isamarkupfalse% diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Thu Nov 01 20:20:19 2007 +0100 @@ -213,9 +213,9 @@ \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{recdef} instead. -Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below, -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can +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. Of course, you may also combine mutual and nested recursion of datatypes. For example, diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/IsaMakefile Thu Nov 01 20:20:19 2007 +0100 @@ -4,7 +4,7 @@ ## targets -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \ +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \ HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Complex-Types HOL-Misc \ HOL-Protocol HOL-Documents styles images: @@ -95,6 +95,15 @@ @rm -f tutorial.dvi +## HOL-Fun + +HOL-Fun: HOL $(LOG)/HOL-Fun.gz + +$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy + $(USEDIR) Fun + @rm -f tutorial.dvi + + ## HOL-Recdef HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Nov 01 20:20:19 2007 +0100 @@ -155,7 +155,7 @@ txt{*\noindent To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use the same general induction method as for recursion induction (see -\S\ref{sec:recdef-induction}): +\S\ref{sec:fun-induction}): *}; apply(induct_tac k rule: nat_less_induct); diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Nov 01 20:20:19 2007 +0100 @@ -216,7 +216,7 @@ \noindent To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use the same general induction method as for recursion induction (see -\S\ref{sec:recdef-induction}):% +\S\ref{sec:fun-induction}):% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Rules/rules.tex --- a/doc-src/TutorialI/Rules/rules.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Thu Nov 01 20:20:19 2007 +0100 @@ -1841,7 +1841,7 @@ \label{sec:THEN} Let us reproduce our examples in Isabelle. Recall that in -{\S}\ref{sec:recdef-simplification} we declared the recursive function +{\S}\ref{sec:fun-simplification} we declared the recursive function \isa{gcd}:\index{*gcd (constant)|(} \begin{isabelle} \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline @@ -2473,7 +2473,7 @@ % We use induction: \isa{gcd.induct} is the induction rule returned by \isa{recdef}. We simplify using -rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the +rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the definition of \isa{gcd} can loop. \begin{isabelle} \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/Sets/sets.tex --- a/doc-src/TutorialI/Sets/sets.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Thu Nov 01 20:20:19 2007 +0100 @@ -875,9 +875,9 @@ \index{relations!well-founded|(}% A well-founded relation captures the notion of a terminating process. -Each \commdx{recdef} -declaration must specify a well-founded relation that -justifies the termination of the desired recursive function. Most of the +Complex recursive functions definitions \ref{sec:?????TN} +must specify a well-founded relation that +justifies their termination. Most of the forms of induction found in mathematics are merely special cases of induction over a well-founded relation. @@ -898,7 +898,7 @@ You may want to skip the rest of this section until you need to perform a complex recursive function definition or induction. The induction rule returned by -\isacommand{recdef} is good enough for most purposes. We use an explicit +\isacommand{fun} is good enough for most purposes. We use an explicit well-founded induction only in {\S}\ref{sec:CTL-revisited}. \end{warn} @@ -956,9 +956,9 @@ \rulenamedx{wf_lex_prod} \end{isabelle} -These constructions can be used in a -\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define -the well-founded relation used to prove termination. +%These constructions can be used in a +%\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define +%the well-founded relation used to prove termination. The \bfindex{multiset ordering}, useful for hard termination proofs, is available in the Library~\cite{HOL-Library}. diff -r 8faf184ba5b1 -r 22d16596c306 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Thu Nov 01 13:44:44 2007 +0100 +++ b/doc-src/TutorialI/fp.tex Thu Nov 01 20:20:19 2007 +0100 @@ -194,7 +194,7 @@ becomes smaller with every recursive call. There must be at most one equation for each constructor. Their order is immaterial. A more general method for defining total recursive functions is introduced in -{\S}\ref{sec:recdef}. +{\S}\ref{sec:fun}. \begin{exercise}\label{ex:Tree} \input{Misc/document/Tree.tex}% @@ -265,7 +265,7 @@ (nonrecursive!) definition from which the user-supplied recursion equations are automatically proved. This process is hidden from the user, who does not have to understand the details. Other commands described -later, like \isacommand{recdef} and \isacommand{inductive}, work similarly. +later, like \isacommand{fun} and \isacommand{inductive}, work similarly. This strict adherence to the definitional approach reduces the risk of soundness errors. @@ -281,9 +281,9 @@ study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced datatypes, including those involving function spaces, are covered in {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search -trees (``tries''). Finally we introduce \isacommand{recdef}, a general +trees (``tries''). Finally we introduce \isacommand{fun}, a general form of recursive function definition that goes well beyond -\isacommand{primrec} ({\S}\ref{sec:recdef}). +\isacommand{primrec} ({\S}\ref{sec:fun}). \section{Simplification} @@ -460,35 +460,18 @@ \index{tries|)} \section{Total Recursive Functions} -\label{sec:recdef} -\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(} +\label{sec:fun} +\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(} Although many total functions have a natural primitive recursive definition, this is not always the case. Arbitrary total recursive functions can be -defined by means of \isacommand{recdef}: you can use full pattern-matching, +defined by means of \isacommand{fun}: you can use full pattern-matching, recursion need not involve datatypes, and termination is proved by showing -that the arguments of all recursive calls are smaller in a suitable (user -supplied) sense. In this section we restrict ourselves to measure functions; -more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}. - -\subsection{Defining Recursive Functions} -\label{sec:recdef-examples} -\input{Recdef/document/examples.tex} - -\subsection{Proving Termination} -\input{Recdef/document/termination.tex} +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}. -\subsection{Simplification and Recursive Functions} -\label{sec:recdef-simplification} -\input{Recdef/document/simplification.tex} +\input{Fun/document/fun0.tex} -\subsection{Induction and Recursive Functions} -\index{induction!recursion|(} -\index{recursion induction|(} - -\input{Recdef/document/Induction.tex} -\label{sec:recdef-induction} - -\index{induction!recursion|)} -\index{recursion induction|)} -\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)} +\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}