# HG changeset patch
# User nipkow
# Date 1193990355 -3600
# Node ID 3dc292be0b5476c182891593b714d8d5e0976121
# Parent  71b2a1fefb846e36274ebacb8afdab5c23e3a078
recdef -> fun

diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Datatype/Nested.thy
--- 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,
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Fun/document/fun0.tex
--- 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
 %
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Fun/fun0.thy
--- 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
 
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Rules/Forward.thy
--- 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 {*
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Rules/Primes.thy
--- 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
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Sets/sets.tex
--- 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
diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/fp.tex
--- 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|(}