--- a/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Nov 02 08:59:15 2007 +0100
@@ -149,9 +149,9 @@
@{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{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,
--- a/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Fun/document/fun0.tex Fri Nov 02 08:59:15 2007 +0100
@@ -104,9 +104,9 @@
show that the size of one fixed argument becomes smaller with each
recursive call.
-More generally, \isa{fun} allows any \emph{lexicographic
+More generally, \isacommand{fun} allows any \emph{lexicographic
combination} of size measures in case there are multiple
-arguments. For example the following version of \rmindex{Ackermann's
+arguments. For example, the following version of \rmindex{Ackermann's
function} is accepted:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -133,8 +133,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
-\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymtimes}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
-\ \ {\isachardoublequoteopen}gcd{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
+\ gcd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ \ {\isachardoublequoteopen}gcd\ m\ n\ {\isacharequal}\ {\isacharparenleft}if\ n{\isacharequal}{\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The second argument decreases with each recursive call.
@@ -152,17 +152,17 @@
condition simplifies to \isa{True} or \isa{False}. For
example, simplification reduces
\begin{isabelle}%
-\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ gcd\ m\ n\ {\isacharequal}\ k%
\end{isabelle}
in one step to
\begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
+\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
\end{isabelle}
where the condition cannot be reduced further, and splitting leads to
\begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
+\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
\end{isabelle}
-Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
+Since the recursive call \isa{gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}} is no longer protected by
an \isa{if}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.
@@ -206,7 +206,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}gcd{\isacharparenleft}m{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
+\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}gcd\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
@@ -226,7 +226,7 @@
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd{\isacharparenleft}m{\isacharcomma}n{\isacharparenright}\ {\isacharequal}\ gcd{\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ gcd\ m\ n\ {\isacharequal}\ gcd\ n\ {\isacharparenleft}m\ mod\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
--- a/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy Fri Nov 02 08:59:15 2007 +0100
@@ -88,9 +88,9 @@
show that the size of one fixed argument becomes smaller with each
recursive call.
-More generally, @{text fun} allows any \emph{lexicographic
+More generally, \isacommand{fun} allows any \emph{lexicographic
combination} of size measures in case there are multiple
-arguments. For example the following version of \rmindex{Ackermann's
+arguments. For example, the following version of \rmindex{Ackermann's
function} is accepted: *}
fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
@@ -114,8 +114,8 @@
Let us look at an example:
*}
-fun gcd :: "nat \<times> nat \<Rightarrow> nat" where
- "gcd(m,n) = (if n=0 then m else gcd(n, m mod n))"
+fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "gcd m n = (if n=0 then m else gcd n (m mod n))"
text{*\noindent
The second argument decreases with each recursive call.
@@ -130,12 +130,12 @@
each @{text "if"}-expression unless its
condition simplifies to @{term True} or @{term False}. For
example, simplification reduces
-@{prop[display]"gcd(m,n) = k"}
+@{prop[display]"gcd m n = k"}
in one step to
-@{prop[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
+@{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}
where the condition cannot be reduced further, and splitting leads to
-@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
-Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
+@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}
+Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by
an @{text "if"}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.
@@ -176,11 +176,11 @@
these lemmas:
*}
-lemma [simp]: "gcd(m,0) = m"
+lemma [simp]: "gcd m 0 = m"
apply(simp)
done
-lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m,n) = gcd(n, m mod n)"
+lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
apply(simp)
done
--- a/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 08:59:15 2007 +0100
@@ -14,18 +14,18 @@
apply (auto simp add: is_gcd_def);
done
-lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
+lemma gcd_commute: "gcd m n = gcd n m"
apply (rule is_gcd_unique)
apply (rule is_gcd)
apply (subst is_gcd_commute)
apply (simp add: is_gcd)
done
-lemma gcd_1 [simp]: "gcd(m, Suc 0) = Suc 0"
+lemma gcd_1 [simp]: "gcd m (Suc 0) = Suc 0"
apply simp
done
-lemma gcd_1_left [simp]: "gcd(Suc 0, m) = Suc 0"
+lemma gcd_1_left [simp]: "gcd (Suc 0) m = Suc 0"
apply (simp add: gcd_commute [of "Suc 0"])
done
@@ -37,7 +37,7 @@
SKIP THIS PROOF
*}
-lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
+lemma gcd_mult_distrib2: "k * gcd m n = gcd (k*m) (k*n)"
apply (induct_tac m n rule: gcd.induct)
apply (case_tac "n=0")
apply simp
@@ -94,7 +94,7 @@
more legible, and variables properly generalized
*};
-lemma gcd_mult [simp]: "gcd(k, k*n) = k"
+lemma gcd_mult [simp]: "gcd k (k*n) = k"
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
@@ -116,7 +116,7 @@
again: more legible, and variables properly generalized
*};
-lemma gcd_self [simp]: "gcd(k,k) = k"
+lemma gcd_self [simp]: "gcd k k = k"
by (rule gcd_mult [of k 1, simplified])
@@ -159,7 +159,7 @@
*}
lemma relprime_dvd_mult:
- "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
+ "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
apply (insert gcd_mult_distrib2 [of m k n])
apply simp
apply (erule_tac t="m" in ssubst);
@@ -178,11 +178,11 @@
lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
*)
-lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
+lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
by (blast intro: relprime_dvd_mult dvd_trans)
-lemma relprime_20_81: "gcd(20,81) = 1";
+lemma relprime_20_81: "gcd 20 81 = 1";
by (simp add: gcd.simps)
text {*
--- a/doc-src/TutorialI/Rules/Primes.thy Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy Fri Nov 02 08:59:15 2007 +0100
@@ -4,11 +4,9 @@
(*Euclid's algorithm
This material now appears AFTER that of Forward.thy *)
theory Primes imports Main begin
-consts
- gcd :: "nat*nat \<Rightarrow> nat"
-recdef gcd "measure snd"
- "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
+fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+ "gcd m n = (if n=0 then m else gcd n (m mod n))"
ML "Pretty.setmargin 64"
@@ -23,18 +21,18 @@
(*** Euclid's Algorithm ***)
-lemma gcd_0 [simp]: "gcd(m,0) = m"
+lemma gcd_0 [simp]: "gcd m 0 = m"
apply (simp);
done
-lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd(m,n) = gcd (n, m mod n)"
+lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd m n = gcd n (m mod n)"
apply (simp)
done;
declare gcd.simps [simp del];
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
-lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)"
+lemma gcd_dvd_both: "(gcd m n dvd m) \<and> (gcd m n dvd n)"
apply (induct_tac m n rule: gcd.induct)
--{* @{subgoals[display,indent=0,margin=65]} *}
apply (case_tac "n=0")
@@ -72,7 +70,7 @@
(*Maximality: for all m,n,k naturals,
if k divides m and k divides n then k divides gcd(m,n)*)
lemma gcd_greatest [rule_format]:
- "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
+ "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd m n"
apply (induct_tac m n rule: gcd.induct)
apply (case_tac "n=0")
txt{*subgoals after the case tac
@@ -87,7 +85,7 @@
*}
(*just checking the claim that case_tac "n" works too*)
-lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)"
+lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd m n"
apply (induct_tac m n rule: gcd.induct)
apply (case_tac "n")
apply (simp_all add: dvd_mod)
@@ -95,7 +93,7 @@
theorem gcd_greatest_iff [iff]:
- "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"
+ "(k dvd gcd m n) = (k dvd m \<and> k dvd n)"
by (blast intro!: gcd_greatest intro: dvd_trans)
@@ -107,7 +105,7 @@
(ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
(*Function gcd yields the Greatest Common Divisor*)
-lemma is_gcd: "is_gcd (gcd(m,n)) m n"
+lemma is_gcd: "is_gcd (gcd m n) m n"
apply (simp add: is_gcd_def gcd_greatest);
done
@@ -133,12 +131,12 @@
\end{isabelle}
*};
-lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
+lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
apply (rule is_gcd_unique)
apply (rule is_gcd)
apply (simp add: is_gcd_def);
apply (blast intro: dvd_trans);
- done
+ done
text{*
\begin{isabelle}
@@ -152,12 +150,12 @@
*}
-lemma gcd_dvd_gcd_mult: "gcd(m,n) dvd gcd(k*m, n)"
+lemma gcd_dvd_gcd_mult: "gcd m n dvd gcd (k*m) n"
apply (blast intro: dvd_trans);
done
(*This is half of the proof (by dvd_anti_sym) of*)
-lemma gcd_mult_cancel: "gcd(k,n) = 1 \<Longrightarrow> gcd(k*m, n) = gcd(m,n)"
+lemma gcd_mult_cancel: "gcd k n = 1 \<Longrightarrow> gcd (k*m) n = gcd m n"
oops
end
--- a/doc-src/TutorialI/Sets/sets.tex Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Fri Nov 02 08:59:15 2007 +0100
@@ -874,12 +874,12 @@
\label{sec:Well-founded}
\index{relations!well-founded|(}%
-A well-founded relation captures the notion of a terminating process.
-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.
+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
+in mathematics are merely special cases of induction over a
+well-founded relation.
Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
infinite descending chains
--- a/doc-src/TutorialI/fp.tex Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/fp.tex Fri Nov 02 08:59:15 2007 +0100
@@ -459,7 +459,7 @@
\input{Trie/document/Trie.tex}
\index{tries|)}
-\section{Total Recursive Functions}
+\section{Total Recursive Functions: \isacommand{fun}}
\label{sec:fun}
\index{fun@\isacommand {fun} (command)|(}\index{functions!total|(}