recdef -> fun
authornipkow
Thu Nov 01 20:20:19 2007 +0100 (2007-11-01)
changeset 2525822d16596c306
parent 25257 8faf184ba5b1
child 25259 8d6b03eef9c9
recdef -> fun
doc-src/TutorialI/Advanced/Partial.thy
doc-src/TutorialI/Advanced/document/Partial.tex
doc-src/TutorialI/Datatype/document/Nested.tex
doc-src/TutorialI/IsaMakefile
doc-src/TutorialI/Misc/AdvancedInd.thy
doc-src/TutorialI/Misc/document/AdvancedInd.tex
doc-src/TutorialI/Rules/rules.tex
doc-src/TutorialI/Sets/sets.tex
doc-src/TutorialI/fp.tex
     1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy	Thu Nov 01 13:44:44 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy	Thu Nov 01 20:20:19 2007 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5  We have already seen an instance of underdefinedness by means of
     1.6  non-exhaustive pattern matching: the definition of @{term last} in
     1.7 -\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}
     1.8 +\S\ref{sec:fun}. The same is allowed for \isacommand{primrec}
     1.9  *}
    1.10  
    1.11  consts hd :: "'a list \<Rightarrow> 'a"
     2.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex	Thu Nov 01 13:44:44 2007 +0100
     2.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Thu Nov 01 20:20:19 2007 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4  
     2.5  We have already seen an instance of underdefinedness by means of
     2.6  non-exhaustive pattern matching: the definition of \isa{last} in
     2.7 -\S\ref{sec:recdef-examples}. The same is allowed for \isacommand{primrec}%
     2.8 +\S\ref{sec:fun}. The same is allowed for \isacommand{primrec}%
     2.9  \end{isamarkuptext}%
    2.10  \isamarkuptrue%
    2.11  \isacommand{consts}\isamarkupfalse%
     3.1 --- a/doc-src/TutorialI/Datatype/document/Nested.tex	Thu Nov 01 13:44:44 2007 +0100
     3.2 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Thu Nov 01 20:20:19 2007 +0100
     3.3 @@ -213,9 +213,9 @@
     3.4  \isa{term} are still awkward because they expect a conjunction. One
     3.5  could derive a new induction principle as well (see
     3.6  \S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec}
     3.7 -and to define functions with \isacommand{recdef} instead.
     3.8 -Simple uses of \isacommand{recdef} are described in \S\ref{sec:recdef} below,
     3.9 -and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{recdef} can 
    3.10 +and to define functions with \isacommand{fun} instead.
    3.11 +Simple uses of \isacommand{fun} are described in \S\ref{sec:fun} below,
    3.12 +and later (\S\ref{sec:nested-recdef}) we shall see how \isacommand{fun} can 
    3.13  handle nested recursion.
    3.14  
    3.15  Of course, you may also combine mutual and nested recursion of datatypes. For example,
     4.1 --- a/doc-src/TutorialI/IsaMakefile	Thu Nov 01 13:44:44 2007 +0100
     4.2 +++ b/doc-src/TutorialI/IsaMakefile	Thu Nov 01 20:20:19 2007 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  
     4.5  ## targets
     4.6  
     4.7 -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef \
     4.8 +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Recdef \
     4.9    HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive  HOL-Complex-Types HOL-Misc \
    4.10    HOL-Protocol HOL-Documents styles
    4.11  images:
    4.12 @@ -95,6 +95,15 @@
    4.13  	@rm -f tutorial.dvi
    4.14  
    4.15  
    4.16 +## HOL-Fun
    4.17 +
    4.18 +HOL-Fun: HOL $(LOG)/HOL-Fun.gz
    4.19 +
    4.20 +$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
    4.21 +	$(USEDIR) Fun
    4.22 +	@rm -f tutorial.dvi
    4.23 +
    4.24 +
    4.25  ## HOL-Recdef
    4.26  
    4.27  HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
     5.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Nov 01 13:44:44 2007 +0100
     5.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Thu Nov 01 20:20:19 2007 +0100
     5.3 @@ -155,7 +155,7 @@
     5.4  txt{*\noindent
     5.5  To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
     5.6  the same general induction method as for recursion induction (see
     5.7 -\S\ref{sec:recdef-induction}):
     5.8 +\S\ref{sec:fun-induction}):
     5.9  *};
    5.10  
    5.11  apply(induct_tac k rule: nat_less_induct);
     6.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Nov 01 13:44:44 2007 +0100
     6.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Thu Nov 01 20:20:19 2007 +0100
     6.3 @@ -216,7 +216,7 @@
     6.4  \noindent
     6.5  To perform induction on \isa{k} using \isa{nat{\isacharunderscore}less{\isacharunderscore}induct}, we use
     6.6  the same general induction method as for recursion induction (see
     6.7 -\S\ref{sec:recdef-induction}):%
     6.8 +\S\ref{sec:fun-induction}):%
     6.9  \end{isamarkuptxt}%
    6.10  \isamarkuptrue%
    6.11  \isacommand{apply}\isamarkupfalse%
     7.1 --- a/doc-src/TutorialI/Rules/rules.tex	Thu Nov 01 13:44:44 2007 +0100
     7.2 +++ b/doc-src/TutorialI/Rules/rules.tex	Thu Nov 01 20:20:19 2007 +0100
     7.3 @@ -1841,7 +1841,7 @@
     7.4  \label{sec:THEN}
     7.5  
     7.6  Let us reproduce our examples in Isabelle.  Recall that in
     7.7 -{\S}\ref{sec:recdef-simplification} we declared the recursive function
     7.8 +{\S}\ref{sec:fun-simplification} we declared the recursive function
     7.9  \isa{gcd}:\index{*gcd (constant)|(}
    7.10  \begin{isabelle}
    7.11  \isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
    7.12 @@ -2473,7 +2473,7 @@
    7.13  %
    7.14  We use induction: \isa{gcd.induct} is the
    7.15  induction rule returned by \isa{recdef}.  We simplify using
    7.16 -rules proved in {\S}\ref{sec:recdef-simplification}, since rewriting by the
    7.17 +rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
    7.18  definition of \isa{gcd} can loop.
    7.19  \begin{isabelle}
    7.20  \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
     8.1 --- a/doc-src/TutorialI/Sets/sets.tex	Thu Nov 01 13:44:44 2007 +0100
     8.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Thu Nov 01 20:20:19 2007 +0100
     8.3 @@ -875,9 +875,9 @@
     8.4  
     8.5  \index{relations!well-founded|(}%
     8.6  A well-founded relation captures the notion of a terminating process. 
     8.7 -Each \commdx{recdef}
     8.8 -declaration must specify a well-founded relation that
     8.9 -justifies the termination of the desired recursive function.  Most of the
    8.10 +Complex recursive functions definitions \ref{sec:?????TN}
    8.11 +must specify a well-founded relation that
    8.12 +justifies their termination.  Most of the
    8.13  forms of induction found in mathematics are merely special cases of
    8.14  induction over a well-founded relation.
    8.15  
    8.16 @@ -898,7 +898,7 @@
    8.17  You may want to skip the rest of this section until you need to perform a
    8.18  complex recursive function definition or induction.  The induction rule
    8.19  returned by
    8.20 -\isacommand{recdef} is good enough for most purposes.  We use an explicit
    8.21 +\isacommand{fun} is good enough for most purposes.  We use an explicit
    8.22  well-founded induction only in {\S}\ref{sec:CTL-revisited}.
    8.23  \end{warn}
    8.24  
    8.25 @@ -956,9 +956,9 @@
    8.26  \rulenamedx{wf_lex_prod}
    8.27  \end{isabelle}
    8.28  
    8.29 -These constructions can be used in a
    8.30 -\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
    8.31 -the well-founded relation used to prove termination.
    8.32 +%These constructions can be used in a
    8.33 +%\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
    8.34 +%the well-founded relation used to prove termination.
    8.35  
    8.36  The \bfindex{multiset ordering}, useful for hard termination proofs, is
    8.37  available in the Library~\cite{HOL-Library}.
     9.1 --- a/doc-src/TutorialI/fp.tex	Thu Nov 01 13:44:44 2007 +0100
     9.2 +++ b/doc-src/TutorialI/fp.tex	Thu Nov 01 20:20:19 2007 +0100
     9.3 @@ -194,7 +194,7 @@
     9.4  becomes smaller with every recursive call. There must be at most one equation
     9.5  for each constructor.  Their order is immaterial.
     9.6  A more general method for defining total recursive functions is introduced in
     9.7 -{\S}\ref{sec:recdef}.
     9.8 +{\S}\ref{sec:fun}.
     9.9  
    9.10  \begin{exercise}\label{ex:Tree}
    9.11  \input{Misc/document/Tree.tex}%
    9.12 @@ -265,7 +265,7 @@
    9.13  (nonrecursive!) definition from which the user-supplied recursion equations are
    9.14  automatically proved.  This process is
    9.15  hidden from the user, who does not have to understand the details.  Other commands described
    9.16 -later, like \isacommand{recdef} and \isacommand{inductive}, work similarly.  
    9.17 +later, like \isacommand{fun} and \isacommand{inductive}, work similarly.  
    9.18  This strict adherence to the definitional approach reduces the risk of 
    9.19  soundness errors.
    9.20  
    9.21 @@ -281,9 +281,9 @@
    9.22  study: a compiler for expressions ({\S}\ref{sec:ExprCompiler}). Advanced
    9.23  datatypes, including those involving function spaces, are covered in
    9.24  {\S}\ref{sec:advanced-datatypes}; it closes with another case study, search
    9.25 -trees (``tries'').  Finally we introduce \isacommand{recdef}, a general
    9.26 +trees (``tries'').  Finally we introduce \isacommand{fun}, a general
    9.27  form of recursive function definition that goes well beyond 
    9.28 -\isacommand{primrec} ({\S}\ref{sec:recdef}).
    9.29 +\isacommand{primrec} ({\S}\ref{sec:fun}).
    9.30  
    9.31  
    9.32  \section{Simplification}
    9.33 @@ -460,35 +460,18 @@
    9.34  \index{tries|)}
    9.35  
    9.36  \section{Total Recursive Functions}
    9.37 -\label{sec:recdef}
    9.38 -\index{recdef@\isacommand {recdef} (command)|(}\index{functions!total|(}
    9.39 +\label{sec:fun}
    9.40 +\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}
    9.41  
    9.42  Although many total functions have a natural primitive recursive definition,
    9.43  this is not always the case. Arbitrary total recursive functions can be
    9.44 -defined by means of \isacommand{recdef}: you can use full pattern-matching,
    9.45 +defined by means of \isacommand{fun}: you can use full pattern-matching,
    9.46  recursion need not involve datatypes, and termination is proved by showing
    9.47 -that the arguments of all recursive calls are smaller in a suitable (user
    9.48 -supplied) sense. In this section we restrict ourselves to measure functions;
    9.49 -more advanced termination proofs are discussed in {\S}\ref{sec:beyond-measure}.
    9.50 -
    9.51 -\subsection{Defining Recursive Functions}
    9.52 -\label{sec:recdef-examples}
    9.53 -\input{Recdef/document/examples.tex}
    9.54 -
    9.55 -\subsection{Proving Termination}
    9.56 -\input{Recdef/document/termination.tex}
    9.57 +that the arguments of all recursive calls are smaller in a suitable sense.
    9.58 +In this section we restrict ourselves to functions where Isabelle can prove
    9.59 +termination automatically. User supplied termination proofs are discussed in
    9.60 +{\S}\ref{sec:beyond-measure}.
    9.61  
    9.62 -\subsection{Simplification and Recursive Functions}
    9.63 -\label{sec:recdef-simplification}
    9.64 -\input{Recdef/document/simplification.tex}
    9.65 +\input{Fun/document/fun0.tex}
    9.66  
    9.67 -\subsection{Induction and Recursive Functions}
    9.68 -\index{induction!recursion|(}
    9.69 -\index{recursion induction|(}
    9.70 -
    9.71 -\input{Recdef/document/Induction.tex}
    9.72 -\label{sec:recdef-induction}
    9.73 -
    9.74 -\index{induction!recursion|)}
    9.75 -\index{recursion induction|)}
    9.76 -\index{recdef@\isacommand {recdef} (command)|)}\index{functions!total|)}
    9.77 +\index{fun@\isacommand {fun} (command)|)}\index{functions!total|)}