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