new lemmas
authornipkow
Wed Jun 01 11:51:25 2011 +0200 (2011-06-01)
changeset 4313732b888e1a170
parent 43136 cf5cda219058
child 43138 818521a90356
child 43140 504d72a39638
new lemmas
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Jun 01 10:29:43 2011 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Jun 01 11:51:25 2011 +0200
     1.3 @@ -860,6 +860,26 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +text{* Bounded increase must terminate: *}
     1.8 +
     1.9 +lemma wf_bounded_measure:
    1.10 +fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
    1.11 +assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
    1.12 +shows "wf r"
    1.13 +apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
    1.14 +apply (auto dest: assms)
    1.15 +done
    1.16 +
    1.17 +lemma wf_bounded_set:
    1.18 +fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
    1.19 +assumes "!!a b. (b,a) : r \<Longrightarrow>
    1.20 +  finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
    1.21 +shows "wf r"
    1.22 +apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
    1.23 +apply(drule assms)
    1.24 +apply (blast intro: card_mono finite_subset  psubset_card_mono dest: psubset_eq[THEN iffD2])
    1.25 +done
    1.26 +
    1.27  
    1.28  subsection{*Weakly decreasing sequences (w.r.t. some well-founded order) 
    1.29     stabilize.*}