# HG changeset patch
# User nipkow
# Date 1188806424 -7200
# Node ID cd723b2209ea32d40f24e21ca0762c9f4495ad8f
# Parent  ec3e5c1a0479cd69cb3b5bf8421fa4af853d09ad
added variations on infinite descent

diff -r ec3e5c1a0479 -r cd723b2209ea src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Sep 03 08:07:39 2007 +0200
+++ b/src/HOL/Nat.thy	Mon Sep 03 10:00:24 2007 +0200
@@ -802,10 +802,15 @@
         a smaller integer $m$ such that $\neg P(m)$.
 \end{itemize} *}
 
-lemma infinite_descent[case_names 0 smaller]: 
+lemma infinite_descent0[case_names 0 smaller]: 
   "\<lbrakk> P 0; !!n. n>0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m::nat. m < n \<and> \<not>P m) \<rbrakk> \<Longrightarrow> P n"
 by (induct n rule: less_induct, case_tac "n>0", auto)
 
+text{* A compact version without explicit base case: *}
+lemma infinite_descent:
+  "\<lbrakk> !!n::nat. \<not> P n \<Longrightarrow>  \<exists>m<n. \<not>  P m \<rbrakk> \<Longrightarrow>  P n"
+by (induct n rule: less_induct, auto)
+
 
 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
@@ -814,15 +819,14 @@
 \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. *}
-corollary infinite_descent_measure[case_names 0 smaller]:
-fixes V :: "'a \<Rightarrow> nat" 
-assumes 0: "!!x. V x = 0 \<Longrightarrow> P x" 
-and 1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
+corollary infinite_descent0_measure[case_names 0 smaller]:
+assumes 0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
+and     1: "!!x. V x > 0 \<Longrightarrow> \<not>P x \<Longrightarrow> (\<exists>y. V y < V x \<and> \<not>P y)"
 shows "P x"
 proof -
   obtain n where "n = V x" by auto
-  moreover have "!!x. V x = (n::nat) \<Longrightarrow> P x"
-  proof (induct n rule: infinite_descent)
+  moreover have "!!x. V x = n \<Longrightarrow> P x"
+  proof (induct n rule: infinite_descent0)
     case 0 -- "i.e. $V(x) = 0$"
     with 0 show "P x" by auto
   next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
@@ -835,6 +839,21 @@
   ultimately show "P x" by auto
 qed
 
+text{* Again, without explicit base case: *}
+lemma infinite_descent_measure:
+assumes "!!x. \<not> P x \<Longrightarrow> \<exists>y. (V::'a\<Rightarrow>nat) y < V x \<and> \<not> P y" shows "P x"
+proof -
+  from assms obtain n where "n = V x" by auto
+  moreover have "!!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
+  qed
+  ultimately show "P x" by auto
+qed
+
+
+
 text {* A [clumsy] way of lifting @{text "<"}
   monotonicity to @{text "\<le>"} monotonicity *}
 lemma less_mono_imp_le_mono: