# 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