diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/Nat.thy	Fri Apr 25 15:30:33 2008 +0200
@@ -734,7 +734,55 @@
 by simp
 
 
-subsubsection {* Additional theorems about "less than" *}
+subsubsection {* Additional theorems about @{term "op \<le>"} *}
+
+text {* Complete induction, aka course-of-values induction *}
+
+lemma less_induct [case_names less]:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes step: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  shows "P a"
+proof - 
+  have "\<And>z. z\<le>a \<Longrightarrow> P z"
+  proof (induct a)
+    case (0 z)
+    have "P 0" by (rule step) auto
+    thus ?case using 0 by auto
+  next
+    case (Suc x z)
+    then have "z \<le> x \<or> z = Suc x" by (simp add: le_Suc_eq)
+    thus ?case
+    proof
+      assume "z \<le> x" thus "P z" by (rule Suc(1))
+    next
+      assume z: "z = Suc x"
+      show "P z"
+        by (rule step) (rule Suc(1), simp add: z le_simps)
+    qed
+  qed
+  thus ?thesis by auto
+qed
+
+lemma nat_less_induct:
+  assumes "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
+  using assms less_induct by blast
+
+lemma measure_induct_rule [case_names less]:
+  fixes f :: "'a \<Rightarrow> nat"
+  assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  shows "P a"
+by (induct m\<equiv>"f a" arbitrary: a rule: less_induct) (auto intro: step)
+
+text {* old style induction rules: *}
+lemma measure_induct:
+  fixes f :: "'a \<Rightarrow> nat"
+  shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
+  by (rule measure_induct_rule [of f P a]) iprover
+
+lemma full_nat_induct:
+  assumes step: "(!!n. (ALL m. Suc m <= n --> P m) ==> P n)"
+  shows "P n"
+  by (rule less_induct) (auto intro: step simp:le_simps)
 
 text{*An induction rule for estabilishing binary relations*}
 lemma less_Suc_induct:
@@ -755,6 +803,73 @@
   thus "P i j" by (simp add: j)
 qed
 
+lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
+  apply (rule nat_less_induct)
+  apply (case_tac n)
+  apply (case_tac [2] nat)
+  apply (blast intro: less_trans)+
+  done
+
+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: *}
+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)
+
+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 (rule infinite_descent) (case_tac "n>0", 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
+\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)<V(x)$ and $~\neg P(y)$.
+\end{itemize}
+NB: the proof also shows how to use the previous lemma. *}
+
+corollary infinite_descent0_measure [case_names 0 smaller]:
+  assumes A0: "!!x. V x = (0::nat) \<Longrightarrow> P x"
+    and   A1: "!!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 "\<And>x. V x = n \<Longrightarrow> P x"
+  proof (induct n rule: infinite_descent0)
+    case 0 -- "i.e. $V(x) = 0$"
+    with A0 show "P x" by auto
+  next -- "now $n>0$ and $P(x)$ does not hold for some $x$ with $V(x)=n$"
+    case (smaller n)
+    then obtain x where vxn: "V x = n " and "V x > 0 \<and> \<not> P x" by auto
+    with A1 obtain y where "V y < V x \<and> \<not> P y" by auto
+    with vxn obtain m where "m = V y \<and> m<n \<and> \<not> P y" by auto
+    then show ?case by auto
+  qed
+  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:
@@ -809,7 +924,7 @@
 done
 
 lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
-by (simp add: add_commute not_add_less1)
+by (simp add: add_commute)
 
 lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
 apply (rule order_trans [of _ "m+k"])
@@ -841,7 +956,7 @@
 by (simp add: add_diff_inverse linorder_not_less)
 
 lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
-by (simp add: le_add_diff_inverse add_commute)
+by (simp add: add_commute)
 
 lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
 by (induct m n rule: diff_induct) simp_all
@@ -1328,6 +1443,6 @@
 subsection {* size of a datatype value *}
 
 class size = type +
-  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded_Recursion} *}
+  fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
 
 end