
diff -r 046fe7ddfc4b -r f65a7fa2da6c src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Fri Feb 15 16:09:10 2008 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Fri Feb 15 16:09:12 2008 +0100
@@ -6,7 +6,8 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded_Recursion
-imports Transitive_Closure
+imports Transitive_Closure Nat
+uses ("Tools/function_package/size.ML")
 begin
 
 inductive
@@ -479,6 +480,169 @@
 apply (erule Least_le)
 done
 
+subsection {* @{typ nat} is well-founded *}
+
+lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)^++"
+proof (rule ext, rule ext, rule iffI)
+  fix n m :: nat
+  assume "m < n"
+  then show "(\<lambda>m n. n = Suc m)^++ m n"
+  proof (induct n)
+    case 0 then show ?case by auto
+  next
+    case (Suc n) then show ?case
+    by (auto simp add: less_Suc_eq_le le_less intro: tranclp.trancl_into_trancl)
+  qed
+next
+  fix n m :: nat
+  assume "(\<lambda>m n. n = Suc m)^++ m n"
+  then show "m < n"
+    by (induct n)
+      (simp_all add: less_Suc_eq_le reflexive le_less)
+qed
+
+definition
+  pred_nat :: "(nat * nat) set" where
+  "pred_nat = {(m, n). n = Suc m}"
+
+definition
+  less_than :: "(nat * nat)set" where
+  "less_than = pred_nat^+"
+
+lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n"
+  unfolding less_nat_rel pred_nat_def trancl_def by simp
+
+lemma pred_nat_trancl_eq_le:
+  "(m, n) \<in> pred_nat^* \<longleftrightarrow> m \<le> n"
+  unfolding less_eq rtrancl_eq_or_trancl by auto
+
+lemma wf_pred_nat: "wf pred_nat"
+  apply (unfold wf_def pred_nat_def, clarify)
+  apply (induct_tac x, blast+)
+  done
+
+lemma wf_less_than [iff]: "wf less_than"
+  by (simp add: less_than_def wf_pred_nat [THEN wf_trancl])
+
+lemma trans_less_than [iff]: "trans less_than"
+  by (simp add: less_than_def trans_trancl)
+
+lemma less_than_iff [iff]: "((x,y): less_than) = (x<y)"
+  by (simp add: less_than_def less_eq)
+
+lemma wf_less: "wf {(x, y::nat). x < y}"
+  using wf_less_than by (simp add: less_than_def less_eq [symmetric])
+
+text {* Complete induction, aka course-of-values induction *}
+lemma nat_less_induct:
+  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
+  apply (induct n rule: wf_induct [OF wf_pred_nat [THEN wf_trancl]])
+  apply (rule prem)
+  apply (unfold less_eq [symmetric], assumption)
+  done
+
+lemmas less_induct = nat_less_induct [rule_format, case_names less]
+
+text {* Type @{typ nat} is a wellfounded order *}
+
+instance nat :: wellorder
+  by intro_classes
+    (assumption |
+      rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+
+
+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} *}
+
+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
+\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
+    thus ?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 {* @{text LEAST} theorems for type @{typ nat}*}
+
+lemma Least_Suc:
+     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+  apply (case_tac "n", auto)
+  apply (frule LeastI)
+  apply (drule_tac P = "%x. P (Suc x) " in LeastI)
+  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
+  apply (erule_tac [2] Least_le)
+  apply (case_tac "LEAST x. P x", auto)
+  apply (drule_tac P = "%x. P (Suc x) " in Least_le)
+  apply (blast intro: order_antisym)
+  done
+
+lemma Least_Suc2:
+   "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+by (erule (1) Least_Suc [THEN ssubst], simp)
+
+
+subsection {* size of a datatype value *}
+
+use "Tools/function_package/size.ML"
+
+setup Size.setup
+
+lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
+  by (induct n) simp_all
+
 ML
 {*
 val wf_def = thm "wf_def";




