1.1 --- a/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 15:56:49 2007 +0100
1.2 +++ b/doc-src/TutorialI/Rules/Forward.thy Fri Nov 02 16:38:14 2007 +0100
1.3 @@ -102,6 +102,14 @@
1.4
1.5
1.6 text {*
1.7 +@{thm[display] gcd_mult}
1.8 +\rulename{gcd_mult}
1.9 +
1.10 +@{thm[display] gcd_self0}
1.11 +\rulename{gcd_self0}
1.12 +*};
1.13 +
1.14 +text {*
1.15 Rules handy with THEN
1.16
1.17 @{thm[display] iffD1}
1.18 @@ -161,13 +169,18 @@
1.19 lemma relprime_dvd_mult:
1.20 "\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
1.21 apply (insert gcd_mult_distrib2 [of m k n])
1.22 +txt{*@{subgoals[display,indent=0,margin=65]}*}
1.23 apply simp
1.24 +txt{*@{subgoals[display,indent=0,margin=65]}*}
1.25 apply (erule_tac t="m" in ssubst);
1.26 apply simp
1.27 done
1.28
1.29
1.30 text {*
1.31 +@{thm[display] relprime_dvd_mult}
1.32 +\rulename{relprime_dvd_mult}
1.33 +
1.34 Another example of "insert"
1.35
1.36 @{thm[display] mod_div_equality}
2.1 --- a/doc-src/TutorialI/Rules/rules.tex Fri Nov 02 15:56:49 2007 +0100
2.2 +++ b/doc-src/TutorialI/Rules/rules.tex Fri Nov 02 16:38:14 2007 +0100
2.3 @@ -1,4 +1,5 @@
2.4 % $Id$
2.5 +%!TEX root = ../tutorial.tex
2.6 \chapter{The Rules of the Game}
2.7 \label{chap:rules}
2.8
2.9 @@ -1844,15 +1845,14 @@
2.10 {\S}\ref{sec:fun-simplification} we declared the recursive function
2.11 \isa{gcd}:\index{*gcd (constant)|(}
2.12 \begin{isabelle}
2.13 -\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline
2.14 -\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline
2.15 -\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
2.16 +\isacommand{fun}\ gcd\ ::\ "nat\ \isasymRightarrow \ nat\ \isasymRightarrow \ nat"\ \isakeyword{where}\isanewline
2.17 +\ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
2.18 \end{isabelle}
2.19 %
2.20 From this definition, it is possible to prove the distributive law.
2.21 That takes us to the starting point for our example.
2.22 \begin{isabelle}
2.23 -?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n)
2.24 +?k\ *\ gcd\ ?m\ ?n\ =\ gcd\ (?k\ *\ ?m)\ (?k\ *\ ?n)
2.25 \rulename{gcd_mult_distrib2}
2.26 \end{isabelle}
2.27 %
2.28 @@ -1872,7 +1872,7 @@
2.29 \isa{thm gcd_mult_0}
2.30 displays the result:
2.31 \begin{isabelle}
2.32 -\ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n)
2.33 +\ \ \ \ \ k\ *\ gcd\ 1\ ?n\ =\ gcd\ (k\ *\ 1)\ (k\ *\ ?n)
2.34 \end{isabelle}
2.35 Something is odd: \isa{k} is an ordinary variable, while \isa{?n}
2.36 is schematic. We did not specify an instantiation
2.37 @@ -1910,7 +1910,7 @@
2.38 %
2.39 Again, we display the resulting theorem:
2.40 \begin{isabelle}
2.41 -\ \ \ \ \ k\ =\ gcd\ (k,\ k\ *\ ?n)
2.42 +\ \ \ \ \ k\ =\ gcd\ k\ (k\ *\ ?n)
2.43 \end{isabelle}
2.44 %
2.45 To re-orient the equation requires the symmetry rule:
2.46 @@ -1927,7 +1927,7 @@
2.47 %
2.48 Here is the result:
2.49 \begin{isabelle}
2.50 -\ \ \ \ \ gcd\ (k,\ k\ *\ ?n)\ =\ k%
2.51 +\ \ \ \ \ gcd\ k\ (k\ *\ ?n)\ =\ k%
2.52 \end{isabelle}
2.53 \isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the
2.54 rule \isa{sym} and returns the resulting conclusion. The effect is to
2.55 @@ -1959,9 +1959,7 @@
2.56 is to state the new lemma explicitly and to prove it using a single
2.57 \isa{rule} method whose operand is expressed using forward reasoning:
2.58 \begin{isabelle}
2.59 -\isacommand{lemma}\ gcd_mult\
2.60 -[simp]:\
2.61 -"gcd(k,\ k*n)\ =\ k"\isanewline
2.62 +\isacommand{lemma}\ gcd\_mult\ [simp]:\ "gcd\ k\ (k*n)\ =\ k"\isanewline
2.63 \isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])
2.64 \end{isabelle}
2.65 Compared with the previous proof of \isa{gcd_mult}, this
2.66 @@ -1972,7 +1970,7 @@
2.67 At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here
2.68 is the Isabelle version:\index{*gcd (constant)|)}
2.69 \begin{isabelle}
2.70 -\isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline
2.71 +\isacommand{lemma}\ gcd\_self\ [simp]:\ "gcd\ k\ k\ =\ k"\isanewline
2.72 \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])
2.73 \end{isabelle}
2.74
2.75 @@ -2010,7 +2008,7 @@
2.76 It states that if $k$ and $n$ are relatively prime
2.77 and if $k$ divides $m\times n$ then $k$ divides $m$.
2.78 \begin{isabelle}
2.79 -\isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
2.80 +\isasymlbrakk gcd ?k ?n {=} 1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\
2.81 \isasymLongrightarrow\ ?k\ dvd\ ?m
2.82 \rulename{relprime_dvd_mult}
2.83 \end{isabelle}
2.84 @@ -2018,7 +2016,7 @@
2.85 First, we
2.86 prove an instance of its first premise:
2.87 \begin{isabelle}
2.88 -\isacommand{lemma}\ relprime_20_81:\ "gcd(20,81)\ =\ 1"\isanewline
2.89 +\isacommand{lemma}\ relprime\_20\_81:\ "gcd\ 20\ 81\ =\ 1"\isanewline
2.90 \isacommand{by}\ (simp\ add:\ gcd.simps)
2.91 \end{isabelle}
2.92 We have evaluated an application of the \isa{gcd} function by
2.93 @@ -2151,29 +2149,22 @@
2.94 proof step inserts the distributive law for
2.95 \isa{gcd}. We specify its variables as shown.
2.96 \begin{isabelle}
2.97 -\isacommand{lemma}\
2.98 -relprime_dvd_mult:\isanewline
2.99 -\ \ \ \ \ \ \ "\isasymlbrakk gcd(k,n){=}1;\ k\ dvd\ m*n\isasymrbrakk\
2.100 -\isasymLongrightarrow\ k\ dvd\
2.101 -m"\isanewline
2.102 -\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\
2.103 -n])
2.104 +\isacommand{lemma}\ relprime\_dvd\_mult:\ \isanewline
2.105 +\ \ \ \ \ \ "\isasymlbrakk \ gcd\ k\ n\ =\ 1;\ k\ dvd\ m*n\ \isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ m"\isanewline
2.106 +\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ n])
2.107 \end{isabelle}
2.108 In the resulting subgoal, note how the equation has been
2.109 inserted:
2.110 \begin{isabelle}
2.111 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ m\ *\ n{;}\ m\ *\ gcd\
2.112 -(k,\ n)\
2.113 -=\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
2.114 -\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
2.115 +\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ 1;\ k\ dvd\ m\ *\ n;\ m\ *\ gcd\ k\ n\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
2.116 +\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
2.117 \end{isabelle}
2.118 -The next proof step utilizes the assumption \isa{gcd(k,n)\ =\ 1}:
2.119 +The next proof step utilizes the assumption \isa{gcd\ k\ n\ =\ 1}
2.120 +(note that \isa{Suc\ 0} is another expression for 1):
2.121 \begin{isabelle}
2.122 \isacommand{apply}(simp)\isanewline
2.123 -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\
2.124 -(m\ *\ n){;}
2.125 -\ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline
2.126 -\ \ \ \ \isasymLongrightarrow\ k\ dvd\ m
2.127 +\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ Suc\ 0;\ k\ dvd\ m\ *\ n;\ m\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline
2.128 +\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m%
2.129 \end{isabelle}
2.130 Simplification has yielded an equation for~\isa{m}. The rest of the proof
2.131 is omitted.
2.132 @@ -2472,22 +2463,19 @@
2.133 divisor of its two arguments.
2.134 %
2.135 We use induction: \isa{gcd.induct} is the
2.136 -induction rule returned by \isa{recdef}. We simplify using
2.137 +induction rule returned by \isa{fun}. We simplify using
2.138 rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the
2.139 definition of \isa{gcd} can loop.
2.140 \begin{isabelle}
2.141 -\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\
2.142 -n)"
2.143 +\isacommand{lemma}\ gcd\_dvd\_both:\ "(gcd\ m\ n\ dvd\ m)\ \isasymand \ (gcd\ m\ n\ dvd\ n)"
2.144 \end{isabelle}
2.145 The induction formula must be a conjunction. In the
2.146 inductive step, each conjunct establishes the other.
2.147 \begin{isabelle}
2.148 -\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
2.149 -\ 1.\ \isasymAnd m\ n.\ n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2.150 -\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand
2.151 -\ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n\isanewline
2.152 -\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow\ gcd\ (m,\ n)\
2.153 -dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
2.154 +\ 1.\ \isasymAnd m\ n.\ (n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2.155 +\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \isanewline
2.156 +\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n)\ \isasymLongrightarrow \isanewline
2.157 +\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
2.158 \end{isabelle}
2.159
2.160 The conditional induction hypothesis suggests doing a case
2.161 @@ -2497,31 +2485,28 @@
2.162 \isa{case_tac~n} instead of \isa{case_tac~"n=0"}. However, the definition
2.163 of \isa{gcd} makes a Boolean decision:
2.164 \begin{isabelle}
2.165 -\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))"
2.166 +\ \ \ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))"
2.167 \end{isabelle}
2.168 Proofs about a function frequently follow the function's definition, so we perform
2.169 case analysis over the same formula.
2.170 \begin{isabelle}
2.171 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
2.172 -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2.173 -\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2.174 +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2.175 +\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2.176 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2.177 -\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline
2.178 -\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2.179 -\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2.180 -\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
2.181 -\isanewline
2.182 -\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n%
2.183 +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n\isanewline
2.184 +\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2.185 +\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2.186 +\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
2.187 +\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n%
2.188 \end{isabelle}
2.189 %
2.190 Simplification leaves one subgoal:
2.191 \begin{isabelle}
2.192 \isacommand{apply}\ (simp_all)\isanewline
2.193 -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\isanewline
2.194 -\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\
2.195 -\isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\
2.196 -n\isasymrbrakk \isanewline
2.197 -\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m%
2.198 +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline
2.199 +\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }0\ <\ n\isasymrbrakk \isanewline
2.200 +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ n\ (m\ mod\ n)\ dvd\ m%
2.201 \end{isabelle}
2.202 %
2.203 Here, we can use \isa{blast}.
2.204 @@ -2560,13 +2545,13 @@
2.205 frequently used with destruction rules; \isa{THEN conjunct1} extracts the
2.206 first half of a conjunctive theorem. Given \isa{gcd_dvd_both} it yields
2.207 \begin{isabelle}
2.208 -\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1
2.209 +\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?m1
2.210 \end{isabelle}
2.211 The variable names \isa{?m1} and \isa{?n1} arise because
2.212 Isabelle renames schematic variables to prevent
2.213 clashes. The second \isacommand{lemmas} declaration yields
2.214 \begin{isabelle}
2.215 -\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1
2.216 +\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?n1
2.217 \end{isabelle}
2.218
2.219 \medskip
2.220 @@ -2574,10 +2559,8 @@
2.221 prove that it returns the greatest of all the common divisors
2.222 of its arguments. The proof is by induction, case analysis and simplification.
2.223 \begin{isabelle}
2.224 -\isacommand{lemma}\ gcd_greatest\
2.225 -[rule_format]:\isanewline
2.226 -\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
2.227 -k\ dvd\ gcd(m,n)"
2.228 +\isacommand{lemma}\ gcd\_greatest\ [rule\_format]:\isanewline
2.229 +\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
2.230 \end{isabelle}
2.231 %
2.232 The goal is expressed using HOL implication,
2.233 @@ -2590,28 +2573,23 @@
2.234 \isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to
2.235 write this:
2.236 \begin{isabelle}
2.237 -\ \ \ \ \ \isacommand{lemma}\ gcd_greatest\
2.238 +\isacommand{lemma}\ gcd_greatest\
2.239 [THEN mp, THEN mp]:\isanewline
2.240 -\ \ \ \ \ \ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\
2.241 -\isasymlongrightarrow\ k\ dvd\ gcd(m,n)"
2.242 +\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n"
2.243 \end{isabelle}
2.244
2.245 Because we are again reasoning about \isa{gcd}, we perform the same
2.246 induction and case analysis as in the previous proof:
2.247 \begingroup\samepage
2.248 \begin{isabelle}
2.249 -\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline
2.250 -\isacommand{apply}\ (case_tac\ "n=0")\isanewline
2.251 -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\
2.252 -\isasymlongrightarrow \isanewline
2.253 -\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
2.254 +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2.255 +\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
2.256 \isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline
2.257 -\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)\isanewline
2.258 -\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline
2.259 -\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline
2.260 -\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk
2.261 -\isanewline
2.262 -\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)
2.263 +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n\isanewline
2.264 +\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline
2.265 +\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline
2.266 +\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline
2.267 +\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n%
2.268 \end{isabelle}
2.269 \endgroup
2.270
2.271 @@ -2621,7 +2599,7 @@
2.272 \isacommand{done}
2.273 \end{isabelle}
2.274 In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\
2.275 -gcd\ (m,\ n)} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by
2.276 +gcd\ m\ n} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by
2.277 an unfolding of \isa{gcd}, using this rule about divides:
2.278 \begin{isabelle}
2.279 \isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \
2.280 @@ -2635,9 +2613,8 @@
2.281 equivalence. This step gives us a chance to see another application
2.282 of \isa{blast}.
2.283 \begin{isabelle}
2.284 -\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline
2.285 -\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\
2.286 -n)"\isanewline
2.287 +\isacommand{theorem}\ gcd\_greatest\_iff\ [iff]:\ \isanewline
2.288 +\ \ \ \ \ \ \ \ "(k\ dvd\ gcd\ m\ n)\ =\ (k\ dvd\ m\ \isasymand \ k\ dvd\ n)"\isanewline
2.289 \isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)
2.290 \end{isabelle}
2.291 This theorem concisely expresses the correctness of the \isa{gcd}