# HG changeset patch
# User nipkow
# Date 1306921885 -7200
# Node ID 32b888e1a1701a3c074865207d7b9c80887e8600
# Parent  cf5cda219058966ea8afcc115c4b89c8ccfcfbbd
new lemmas

diff -r cf5cda219058 -r 32b888e1a170 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Jun 01 11:51:25 2011 +0200
@@ -860,6 +860,26 @@
   qed
 qed
 
+text{* Bounded increase must terminate: *}
+
+lemma wf_bounded_measure:
+fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
+assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
+shows "wf r"
+apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
+apply (auto dest: assms)
+done
+
+lemma wf_bounded_set:
+fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
+assumes "!!a b. (b,a) : r \<Longrightarrow>
+  finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
+shows "wf r"
+apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
+apply(drule assms)
+apply (blast intro: card_mono finite_subset  psubset_card_mono dest: psubset_eq[THEN iffD2])
+done
+
 
 subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
    stabilize.*}