# 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: "\n::nat. m = n \ m \ 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: "\x::nat. (\y. y < x \ P y) \ P x" + shows "P z" +proof (rule R) + show "\y. y < z \ 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 \ 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: "\x::nat. P x \ \ P x" + shows "(\x \ (\xx (\x P z" + have "\ (\xxx