# HG changeset patch
# User paulson
# Date 1194017894 -3600
# Node ID 7007bc8ddae44ab6a22c8391c3f5ded7daec359c
# Parent  b5474493503639168a2d82f3500c47e6a0dffffe
recdef to fun

diff -r b54744935036 -r 7007bc8ddae4 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Fri Nov 02 15:56:49 2007 +0100
+++ b/doc-src/TutorialI/Rules/Forward.thy	Fri Nov 02 16:38:14 2007 +0100
@@ -102,6 +102,14 @@
 
 
 text {*
+@{thm[display] gcd_mult}
+\rulename{gcd_mult}
+
+@{thm[display] gcd_self0}
+\rulename{gcd_self0}
+*};
+
+text {*
 Rules handy with THEN
 
 @{thm[display] iffD1}
@@ -161,13 +169,18 @@
 lemma relprime_dvd_mult: 
       "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
 apply (insert gcd_mult_distrib2 [of m k n])
+txt{*@{subgoals[display,indent=0,margin=65]}*}
 apply simp
+txt{*@{subgoals[display,indent=0,margin=65]}*}
 apply (erule_tac t="m" in ssubst);
 apply simp
 done
 
 
 text {*
+@{thm[display] relprime_dvd_mult}
+\rulename{relprime_dvd_mult}
+
 Another example of "insert"
 
 @{thm[display] mod_div_equality}
diff -r b54744935036 -r 7007bc8ddae4 doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Nov 02 15:56:49 2007 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Nov 02 16:38:14 2007 +0100
@@ -1,4 +1,5 @@
 % $Id$
+%!TEX root = ../tutorial.tex
 \chapter{The Rules of the Game}
 \label{chap:rules}
  
@@ -1844,15 +1845,14 @@
 {\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
-\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline
-\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
+\isacommand{fun}\ gcd\ ::\ "nat\ \isasymRightarrow \ nat\ \isasymRightarrow \ nat"\ \isakeyword{where}\isanewline
+\ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
 \end{isabelle}
 %
 From this definition, it is possible to prove the distributive law.  
 That takes us to the starting point for our example.
 \begin{isabelle}
-?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
+?k\ *\ gcd\ ?m\ ?n\ =\ gcd\ (?k\ *\ ?m)\ (?k\ *\ ?n)
 \rulename{gcd_mult_distrib2}
 \end{isabelle}
 %
@@ -1872,7 +1872,7 @@
 \isa{thm gcd_mult_0}
 displays the result:
 \begin{isabelle}
-\ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
+\ \ \ \ \ k\ *\ gcd\ 1\ ?n\ =\ gcd\ (k\ *\ 1)\ (k\ *\ ?n)
 \end{isabelle}
 Something is odd: \isa{k} is an ordinary variable, while \isa{?n} 
 is schematic.  We did not specify an instantiation 
@@ -1910,7 +1910,7 @@
 %
 Again, we display the resulting theorem:
 \begin{isabelle}
-\ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n)
+\ \ \ \ \ k\ =\ gcd\ k\ (k\ *\ ?n)
 \end{isabelle}
 %
 To re-orient the equation requires the symmetry rule:
@@ -1927,7 +1927,7 @@
 %
 Here is the result:
 \begin{isabelle}
-\ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k%
+\ \ \ \ \ gcd\ k\ (k\ *\ ?n)\ =\ k%
 \end{isabelle}
 \isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the
 rule \isa{sym} and returns the resulting conclusion.  The effect is to
@@ -1959,9 +1959,7 @@
 is to state the new lemma explicitly and to prove it using a single
 \isa{rule} method whose operand is expressed using forward reasoning:
 \begin{isabelle}
-\isacommand{lemma}\ gcd_mult\
-[simp]:\
-"gcd(k,\ k*n)\ =\ k"\isanewline
+\isacommand{lemma}\ gcd\_mult\ [simp]:\ "gcd\ k\ (k*n)\ =\ k"\isanewline
 \isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])
 \end{isabelle}
 Compared with the previous proof of \isa{gcd_mult}, this
@@ -1972,7 +1970,7 @@
 At the start  of this section, we also saw a proof of $\gcd(k,k)=k$.  Here
 is the Isabelle version:\index{*gcd (constant)|)}
 \begin{isabelle}
-\isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline
+\isacommand{lemma}\ gcd\_self\ [simp]:\ "gcd\ k\ k\ =\ k"\isanewline
 \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
 \end{isabelle}
 
@@ -2010,7 +2008,7 @@
 It states that if $k$ and $n$ are relatively prime
 and if $k$ divides $m\times n$ then $k$ divides $m$.
 \begin{isabelle}
-\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
+\isasymlbrakk gcd ?k ?n {=} 1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
 \isasymLongrightarrow\ ?k\ dvd\ ?m
 \rulename{relprime_dvd_mult}
 \end{isabelle}
@@ -2018,7 +2016,7 @@
 First, we
 prove an instance of its first premise:
 \begin{isabelle}
-\isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
+\isacommand{lemma}\ relprime\_20\_81:\ "gcd\ 20\ 81\ =\ 1"\isanewline
 \isacommand{by}\ (simp\ add:\ gcd.simps)
 \end{isabelle}
 We have evaluated an application of the \isa{gcd} function by
@@ -2151,29 +2149,22 @@
 proof step inserts the distributive law for
 \isa{gcd}.  We specify its variables as shown. 
 \begin{isabelle}
-\isacommand{lemma}\
-relprime_dvd_mult:\isanewline
-\ \ \ \ \ \ \ "\isasymlbrakk gcd(k,n){=}1;\ k\ dvd\ m*n\isasymrbrakk\
-\isasymLongrightarrow\ k\ dvd\
-m"\isanewline
-\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
-n])
+\isacommand{lemma}\ relprime\_dvd\_mult:\ \isanewline
+\ \ \ \ \ \ "\isasymlbrakk \ gcd\ k\ n\ =\ 1;\ k\ dvd\ m*n\ \isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ m"\isanewline
+\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ n])
 \end{isabelle}
 In the resulting subgoal, note how the equation has been 
 inserted: 
 \begin{isabelle}
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
-(k,\ n)\
-=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
+\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ 1;\ k\ dvd\ m\ *\ n;\ m\ *\ gcd\ k\ n\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
+\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
 \end{isabelle}
-The next proof step utilizes the assumption \isa{gcd(k,n)\ =\ 1}: 
+The next proof step utilizes the assumption \isa{gcd\ k\ n\ =\ 1}
+(note that \isa{Suc\ 0} is another expression for 1):
 \begin{isabelle}
 \isacommand{apply}(simp)\isanewline
-\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\
-(m\ *\ n){;}
-\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
-\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
+\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ Suc\ 0;\ k\ dvd\ m\ *\ n;\ m\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
+\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
 \end{isabelle}
 Simplification has yielded an equation for~\isa{m}.  The rest of the proof
 is omitted.
@@ -2472,22 +2463,19 @@
 divisor of its two arguments.  
 %
 We use induction: \isa{gcd.induct} is the
-induction rule returned by \isa{recdef}.  We simplify using
+induction rule returned by \isa{fun}.  We simplify using
 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\
-n)"
+\isacommand{lemma}\ gcd\_dvd\_both:\ "(gcd\ m\ n\ dvd\ m)\ \isasymand \ (gcd\ m\ n\ dvd\ n)"
 \end{isabelle}
 The induction formula must be a conjunction.  In the
 inductive step, each conjunct establishes the other. 
 \begin{isabelle}
-\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
-\ 1.\ \isasymAnd m\ n.\ n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand
-\ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n\isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow\ gcd\ (m,\ n)\
-dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
+\ 1.\ \isasymAnd m\ n.\ (n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n)\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
 \end{isabelle}
 
 The conditional induction hypothesis suggests doing a case
@@ -2497,31 +2485,28 @@
 \isa{case_tac~n} instead of \isa{case_tac~"n=0"}.  However, the definition
 of \isa{gcd} makes a Boolean decision:
 \begin{isabelle}
-\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
+\ \ \ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
 \end{isabelle}
 Proofs about a function frequently follow the function's definition, so we perform
 case analysis over the same formula.
 \begin{isabelle}
 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
-\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
+\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline
-\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
-\isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
+\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n\isanewline
+\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
 \end{isabelle}
 %
 Simplification leaves one subgoal: 
 \begin{isabelle}
 \isacommand{apply}\ (simp_all)\isanewline
-\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\
-\isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\
-n\isasymrbrakk \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m%
+\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }0\ <\ n\isasymrbrakk \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ n\ (m\ mod\ n)\ dvd\ m%
 \end{isabelle}
 %
 Here, we can use \isa{blast}.  
@@ -2560,13 +2545,13 @@
 frequently used with destruction rules; \isa{THEN conjunct1} extracts the
 first half of a conjunctive theorem.  Given \isa{gcd_dvd_both} it yields
 \begin{isabelle}
-\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1
+\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?m1
 \end{isabelle}
 The variable names \isa{?m1} and \isa{?n1} arise because
 Isabelle renames schematic variables to prevent 
 clashes.  The second \isacommand{lemmas} declaration yields
 \begin{isabelle}
-\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1
+\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?n1
 \end{isabelle}
 
 \medskip
@@ -2574,10 +2559,8 @@
 prove that it returns the greatest of all the common divisors 
 of its arguments.  The proof is by induction, case analysis and simplification.
 \begin{isabelle}
-\isacommand{lemma}\ gcd_greatest\
-[rule_format]:\isanewline
-\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
-k\ dvd\ gcd(m,n)"
+\isacommand{lemma}\ gcd\_greatest\ [rule\_format]:\isanewline
+\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
 \end{isabelle}
 %
 The goal is expressed using HOL implication,
@@ -2590,28 +2573,23 @@
 \isa{THEN} to the rules \isa{mp} and \isa{spec}.  We did not have to
 write this:
 \begin{isabelle}
-\ \ \ \ \ \isacommand{lemma}\ gcd_greatest\
+\isacommand{lemma}\ gcd_greatest\
 [THEN mp, THEN mp]:\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\
-\isasymlongrightarrow\ k\ dvd\ gcd(m,n)"
+\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
 \end{isabelle}
 
 Because we are again reasoning about \isa{gcd}, we perform the same
 induction and case analysis as in the previous proof:
 \begingroup\samepage
 \begin{isabelle}
-\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
-\isacommand{apply}\ (case_tac\ "n=0")\isanewline
-\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\
-\isasymlongrightarrow \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
+\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
+\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
-\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)\isanewline
-\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
-\isanewline
-\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)
+\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n\isanewline
+\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
+\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n%
 \end{isabelle}
 \endgroup
 
@@ -2621,7 +2599,7 @@
 \isacommand{done}
 \end{isabelle}
 In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\
-gcd\ (m,\ n)} goes to~\isa{k\ dvd\ m}.  The second subgoal is proved by
+gcd\ m\ n} goes to~\isa{k\ dvd\ m}.  The second subgoal is proved by
 an unfolding of \isa{gcd}, using this rule about divides:
 \begin{isabelle}
 \isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \
@@ -2635,9 +2613,8 @@
 equivalence.  This step gives us a chance to see another application
 of \isa{blast}.
 \begin{isabelle}
-\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline
-\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\
-n)"\isanewline
+\isacommand{theorem}\ gcd\_greatest\_iff\ [iff]:\ \isanewline
+\ \ \ \ \ \ \ \ "(k\ dvd\ gcd\ m\ n)\ =\ (k\ dvd\ m\ \isasymand \ k\ dvd\ n)"\isanewline
 \isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)
 \end{isabelle}
 This theorem concisely expresses the correctness of the \isa{gcd}