# HG changeset patch
# User berghofe
# Date 1194947867 -3600
# Node ID 1c5b8d54a339a0e92c72535def9fe27ec53ff684
# Parent  0fe95159787a020c0fed7a17afa0f9fb589aab65
Moved auxiliary lemmas to separate theory.

diff -r 0fe95159787a -r 1c5b8d54a339 src/HOL/Extraction/Util.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Extraction/Util.thy	Tue Nov 13 10:57:47 2007 +0100
@@ -0,0 +1,98 @@
+(*  Title:      HOL/Extraction/Util.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+*)
+
+header {* Auxiliary lemmas used in program extraction examples *}
+
+theory Util
+imports Main
+begin
+
+text {*
+Decidability of equality on natural numbers.
+*}
+
+lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
+  apply (induct m)
+  apply (case_tac n)
+  apply (case_tac [3] n)
+  apply (simp only: nat.simps, iprover?)+
+  done
+
+text {*
+Well-founded induction on natural numbers, derived using the standard
+structural induction rule.
+*}
+
+lemma nat_wf_ind:
+  assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  shows "P z"
+proof (rule R)
+  show "\<And>y. y < z \<Longrightarrow> P y"
+  proof (induct z)
+    case 0
+    thus ?case by simp
+  next
+    case (Suc n y)
+    from nat_eq_dec show ?case
+    proof
+      assume ny: "n = y"
+      have "P n"
+	by (rule R) (rule Suc)
+      with ny show ?case by simp
+    next
+      assume "n \<noteq> y"
+      with Suc have "y < n" by simp
+      thus ?case by (rule Suc)
+    qed
+  qed
+qed
+
+text {*
+Bounded search for a natural number satisfying a decidable predicate.
+*}
+
+lemma search:
+  assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
+  shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
+proof (induct y)
+  case 0 show ?case by simp
+next
+  case (Suc z)
+  thus ?case
+  proof
+    assume "\<exists>x<z. P x"
+    then obtain x where le: "x < z" and P: "P x" by iprover
+    from le have "x < Suc z" by simp
+    with P show ?case by iprover
+  next
+    assume nex: "\<not> (\<exists>x<z. P x)"
+    from dec show ?case
+    proof
+      assume P: "P z"
+      have "z < Suc z" by simp
+      with P show ?thesis by iprover
+    next
+      assume nP: "\<not> P z"
+      have "\<not> (\<exists>x<Suc z. P x)"
+      proof
+	assume "\<exists>x<Suc z. P x"
+	then obtain x where le: "x < Suc z" and P: "P x" by iprover
+	have "x < z"
+	proof (cases "x = z")
+	  case True
+	  with nP and P show ?thesis by simp
+	next
+	  case False
+	  with le show ?thesis by simp
+	qed
+	with P have "\<exists>x<z. P x" by iprover
+	with nex show False ..
+      qed
+      thus ?case by iprover
+    qed
+  qed
+qed
+
+end