src/HOL/Nat.thy
 changeset 63111 caa0c513bbca parent 63110 ccbdce905fca child 63113 fe31996e3898
     1.1 --- a/src/HOL/Nat.thy	Mon May 23 14:43:14 2016 +0200
1.2 +++ b/src/HOL/Nat.thy	Mon May 23 14:56:48 2016 +0200
1.3 @@ -951,22 +951,23 @@
1.4    then show "P i j" by (simp add: j)
1.5  qed
1.6
1.7 -text \<open>The method of infinite descent, frequently used in number theory.
1.8 -Provided by Roelof Oosterhuis.
1.9 -$P(n)$ is true for all $n\in\mathbb{N}$ if
1.10 -\begin{itemize}
1.11 -  \item case 0'': given $n=0$ prove $P(n)$,
1.12 -  \item case smaller'': given $n>0$ and $\neg P(n)$ prove there exists
1.13 -        a smaller integer $m$ such that $\neg P(m)$.
1.14 -\end{itemize}\<close>
1.15 -
1.16 -text\<open>A compact version without explicit base case:\<close>
1.17 +text \<open>
1.18 +  The method of infinite descent, frequently used in number theory.
1.19 +  Provided by Roelof Oosterhuis.
1.20 +  \<open>P n\<close> is true for all natural numbers if
1.21 +  \<^item> case 0'': given \<open>n = 0\<close> prove \<open>P n\<close>
1.22 +  \<^item> case smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
1.23 +    a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
1.24 +\<close>
1.25 +
1.26  lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool"
1.27 +  \<comment> \<open>compact version without explicit base case\<close>
1.28    by (induct n rule: less_induct) auto
1.29
1.30 -lemma infinite_descent0[case_names 0 smaller]:
1.31 +lemma infinite_descent0 [case_names 0 smaller]:
1.32    fixes P :: "nat \<Rightarrow> bool"
1.33 -  assumes "P 0" and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m. m < n \<and> \<not> P m)"
1.34 +  assumes "P 0"
1.35 +    and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
1.36    shows "P n"
1.37    apply (rule infinite_descent)
1.38    using assms
1.39 @@ -975,14 +976,12 @@
1.40    done
1.41
1.42  text \<open>
1.43 -Infinite descent using a mapping to $\mathbb{N}$:
1.44 -$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and
1.45 -\begin{itemize}
1.46 -\item case 0'': given $V(x)=0$ prove $P(x)$,
1.47 -\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)$.
1.48 -\end{itemize}
1.49 -NB: the proof also shows how to use the previous lemma.\<close>
1.50 -
1.51 +  Infinite descent using a mapping to \<open>nat\<close>:
1.52 +  \<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
1.53 +  \<^item> case 0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
1.54 +  \<^item> smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
1.55 +  there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
1.56 +\<close>
1.57  corollary infinite_descent0_measure [case_names 0 smaller]:
1.58    fixes V :: "'a \<Rightarrow> nat"
1.59    assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x"
1.60 @@ -998,7 +997,7 @@
1.61      case (smaller n)
1.62      then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
1.63      with 2 obtain y where "V y < V x \<and> \<not> P y" by auto
1.64 -    with * obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
1.65 +    with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto
1.66      then show ?case by auto
1.67    qed
1.68    ultimately show "P x" by auto
1.69 @@ -1013,14 +1012,13 @@
1.70    from assms obtain n where "n = V x" by auto
1.71    moreover have "\<And>x. V x = n \<Longrightarrow> P x"
1.72    proof (induct n rule: infinite_descent, auto)
1.73 -    fix x
1.74 -    assume "\<not> P x"
1.75 -    with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto
1.76 +    show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x
1.77 +      using assms and that by auto
1.78    qed
1.79    ultimately show "P x" by auto
1.80  qed
1.81
1.82 -text \<open>A [clumsy] way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
1.83 +text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
1.84  lemma less_mono_imp_le_mono:
1.85    fixes f :: "nat \<Rightarrow> nat"
1.86      and i j :: nat