949 show ?case by simp |
949 show ?case by simp |
950 qed |
950 qed |
951 then show "P i j" by (simp add: j) |
951 then show "P i j" by (simp add: j) |
952 qed |
952 qed |
953 |
953 |
954 text \<open>The method of infinite descent, frequently used in number theory. |
954 text \<open> |
955 Provided by Roelof Oosterhuis. |
955 The method of infinite descent, frequently used in number theory. |
956 $P(n)$ is true for all $n\in\mathbb{N}$ if |
956 Provided by Roelof Oosterhuis. |
957 \begin{itemize} |
957 \<open>P n\<close> is true for all natural numbers if |
958 \item case ``0'': given $n=0$ prove $P(n)$, |
958 \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close> |
959 \item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists |
959 \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists |
960 a smaller integer $m$ such that $\neg P(m)$. |
960 a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>. |
961 \end{itemize}\<close> |
961 \<close> |
962 |
962 |
963 text\<open>A compact version without explicit base case:\<close> |
|
964 lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" |
963 lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" |
|
964 \<comment> \<open>compact version without explicit base case\<close> |
965 by (induct n rule: less_induct) auto |
965 by (induct n rule: less_induct) auto |
966 |
966 |
967 lemma infinite_descent0[case_names 0 smaller]: |
967 lemma infinite_descent0 [case_names 0 smaller]: |
968 fixes P :: "nat \<Rightarrow> bool" |
968 fixes P :: "nat \<Rightarrow> bool" |
969 assumes "P 0" and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m. m < n \<and> \<not> P m)" |
969 assumes "P 0" |
|
970 and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m" |
970 shows "P n" |
971 shows "P n" |
971 apply (rule infinite_descent) |
972 apply (rule infinite_descent) |
972 using assms |
973 using assms |
973 apply (case_tac "n > 0") |
974 apply (case_tac "n > 0") |
974 apply auto |
975 apply auto |
975 done |
976 done |
976 |
977 |
977 text \<open> |
978 text \<open> |
978 Infinite descent using a mapping to $\mathbb{N}$: |
979 Infinite descent using a mapping to \<open>nat\<close>: |
979 $P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and |
980 \<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 |
980 \begin{itemize} |
981 \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close> |
981 \item case ``0'': given $V(x)=0$ prove $P(x)$, |
982 \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove |
982 \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)$. |
983 there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>. |
983 \end{itemize} |
984 \<close> |
984 NB: the proof also shows how to use the previous lemma.\<close> |
|
985 |
|
986 corollary infinite_descent0_measure [case_names 0 smaller]: |
985 corollary infinite_descent0_measure [case_names 0 smaller]: |
987 fixes V :: "'a \<Rightarrow> nat" |
986 fixes V :: "'a \<Rightarrow> nat" |
988 assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x" |
987 assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x" |
989 and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" |
988 and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" |
990 shows "P x" |
989 shows "P x" |
996 with 1 show "P x" by auto |
995 with 1 show "P x" by auto |
997 next |
996 next |
998 case (smaller n) |
997 case (smaller n) |
999 then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto |
998 then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto |
1000 with 2 obtain y where "V y < V x \<and> \<not> P y" by auto |
999 with 2 obtain y where "V y < V x \<and> \<not> P y" by auto |
1001 with * obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto |
1000 with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto |
1002 then show ?case by auto |
1001 then show ?case by auto |
1003 qed |
1002 qed |
1004 ultimately show "P x" by auto |
1003 ultimately show "P x" by auto |
1005 qed |
1004 qed |
1006 |
1005 |
1011 shows "P x" |
1010 shows "P x" |
1012 proof - |
1011 proof - |
1013 from assms obtain n where "n = V x" by auto |
1012 from assms obtain n where "n = V x" by auto |
1014 moreover have "\<And>x. V x = n \<Longrightarrow> P x" |
1013 moreover have "\<And>x. V x = n \<Longrightarrow> P x" |
1015 proof (induct n rule: infinite_descent, auto) |
1014 proof (induct n rule: infinite_descent, auto) |
1016 fix x |
1015 show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x |
1017 assume "\<not> P x" |
1016 using assms and that by auto |
1018 with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto |
|
1019 qed |
1017 qed |
1020 ultimately show "P x" by auto |
1018 ultimately show "P x" by auto |
1021 qed |
1019 qed |
1022 |
1020 |
1023 text \<open>A [clumsy] way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close> |
1021 text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close> |
1024 lemma less_mono_imp_le_mono: |
1022 lemma less_mono_imp_le_mono: |
1025 fixes f :: "nat \<Rightarrow> nat" |
1023 fixes f :: "nat \<Rightarrow> nat" |
1026 and i j :: nat |
1024 and i j :: nat |
1027 assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j" |
1025 assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j" |
1028 and "i \<le> j" |
1026 and "i \<le> j" |