# HG changeset patch
# User wenzelm
# Date 1464008208 7200
# Node ID caa0c513bbca08d8147fdd2909325b750d3f8959
# Parent ccbdce905fca72e247792318c533daf650a3fd83
tuned document;
diff r ccbdce905fca r caa0c513bbca src/HOL/Nat.thy
 a/src/HOL/Nat.thy Mon May 23 14:43:14 2016 +0200
+++ b/src/HOL/Nat.thy Mon May 23 14:56:48 2016 +0200
@@ 951,22 +951,23 @@
then show "P i j" by (simp add: j)
qed
text \The method of infinite descent, frequently used in number theory.
Provided by Roelof Oosterhuis.
$P(n)$ is true for all $n\in\mathbb{N}$ if
\begin{itemize}
 \item case ``0'': given $n=0$ prove $P(n)$,
 \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists
 a smaller integer $m$ such that $\neg P(m)$.
\end{itemize}\

text\A compact version without explicit base case:\
+text \
+ The method of infinite descent, frequently used in number theory.
+ Provided by Roelof Oosterhuis.
+ \P n\ is true for all natural numbers if
+ \<^item> case ``0'': given \n = 0\ prove \P n\
+ \<^item> case ``smaller'': given \n > 0\ and \\ P n\ prove there exists
+ a smaller natural number \m\ such that \\ P m\.
+\
+
lemma infinite_descent: "(\n. \ P n \ \m P m) \ P n" for P :: "nat \ bool"
+ \ \compact version without explicit base case\
by (induct n rule: less_induct) auto
lemma infinite_descent0[case_names 0 smaller]:
+lemma infinite_descent0 [case_names 0 smaller]:
fixes P :: "nat \ bool"
 assumes "P 0" and "\n. n > 0 \ \ P n \ (\m. m < n \ \ P m)"
+ assumes "P 0"
+ and "\n. n > 0 \ \ P n \ \m. m < n \ \ P m"
shows "P n"
apply (rule infinite_descent)
using assms
@@ 975,14 +976,12 @@
done
text \
Infinite descent using a mapping to $\mathbb{N}$:
$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
\begin{itemize}
\item case ``0'': given $V(x)=0$ prove $P(x)$,
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)

+ Infinite descent using a mapping to \nat\:
+ \P x\ is true for all \x \ D\ if there exists a \V \ D \ nat\ and
+ \<^item> case ``0'': given \V x = 0\ prove \P x\
+ \<^item> ``smaller'': given \V x > 0\ and \\ P x\ prove
+ there exists a \y \ D\ such that \V y < V x\ and \\ P y\.
+\
corollary infinite_descent0_measure [case_names 0 smaller]:
fixes V :: "'a \ nat"
assumes 1: "\x. V x = 0 \ P x"
@@ 998,7 +997,7 @@
case (smaller n)
then obtain x where *: "V x = n " and "V x > 0 \ \ P x" by auto
with 2 obtain y where "V y < V x \ \ P y" by auto
 with * obtain m where "m = V y \ m \ P y" by auto
+ with * obtain m where "m = V y \ m < n \ \ P y" by auto
then show ?case by auto
qed
ultimately show "P x" by auto
@@ 1013,14 +1012,13 @@
from assms obtain n where "n = V x" by auto
moreover have "\x. V x = n \ P x"
proof (induct n rule: infinite_descent, auto)
 fix x
 assume "\ P x"
 with assms show "\m < V x. \y. V y = m \ \ P y" by auto
+ show "\m < V x. \y. V y = m \ \ P y" if "\ P x" for x
+ using assms and that by auto
qed
ultimately show "P x" by auto
qed
text \A [clumsy] way of lifting \<\ monotonicity to \\\ monotonicity\
+text \A (clumsy) way of lifting \<\ monotonicity to \\\ monotonicity\
lemma less_mono_imp_le_mono:
fixes f :: "nat \ nat"
and i j :: nat