# 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 \<open>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}\<close>
-
-text\<open>A compact version without explicit base case:\<close>
+text \<open>
+  The method of infinite descent, frequently used in number theory.
+  Provided by Roelof Oosterhuis.
+  \<open>P n\<close> is true for all natural numbers if
+  \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close>
+  \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
+    a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
+\<close>
+
 lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
+  \<comment> \<open>compact version without explicit base case\<close>
   by (induct n rule: less_induct) auto
 
-lemma infinite_descent0[case_names 0 smaller]:
+lemma infinite_descent0 [case_names 0 smaller]:
   fixes P :: "nat \<Rightarrow> bool"
-  assumes "P 0" and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m. m < n \<and> \<not> P m)"
+  assumes "P 0"
+    and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
   shows "P n"
   apply (rule infinite_descent)
   using assms
@@ -975,14 +976,12 @@
   done
 
 text \<open>
-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)<V(x)$ and $~\neg P(y)$.
-\end{itemize}
-NB: the proof also shows how to use the previous lemma.\<close>
-
+  Infinite descent using a mapping to \<open>nat\<close>:
+  \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and
+  \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
+  \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
+  there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
+\<close>
 corollary infinite_descent0_measure [case_names 0 smaller]:
   fixes V :: "'a \<Rightarrow> nat"
   assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
@@ -998,7 +997,7 @@
     case (smaller n)
     then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
     with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
-    with * obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
+    with * obtain m where "m = V y \<and> m < n \<and> \<not> 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 "\<And>x. V x = n \<Longrightarrow> P x"
   proof (induct n rule: infinite_descent, auto)
-    fix x
-    assume "\<not> P x"
-    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
+    show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
+      using assms and that by auto
   qed
   ultimately show "P x" by auto
 qed
 
-text \<open>A [clumsy] way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
+text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
 lemma less_mono_imp_le_mono:
   fixes f :: "nat \<Rightarrow> nat"
     and i j :: nat