tuned lemmas
authornipkow
Wed Jun 01 15:53:47 2011 +0200 (2011-06-01)
changeset 43140504d72a39638
parent 43137 32b888e1a170
child 43141 11fce8564415
tuned lemmas
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Wed Jun 01 11:51:25 2011 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed Jun 01 15:53:47 2011 +0200
     1.3 @@ -864,7 +864,7 @@
     1.4  
     1.5  lemma wf_bounded_measure:
     1.6  fixes ub :: "'a \<Rightarrow> nat" and f :: "'a \<Rightarrow> nat"
     1.7 -assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a > f b & f b > f a"
     1.8 +assumes "!!a b. (b,a) : r \<Longrightarrow> ub b \<le> ub a & ub a \<ge> f b & f b > f a"
     1.9  shows "wf r"
    1.10  apply(rule wf_subset[OF wf_measure[of "%a. ub a - f a"]])
    1.11  apply (auto dest: assms)
    1.12 @@ -873,11 +873,11 @@
    1.13  lemma wf_bounded_set:
    1.14  fixes ub :: "'a \<Rightarrow> 'b set" and f :: "'a \<Rightarrow> 'b set"
    1.15  assumes "!!a b. (b,a) : r \<Longrightarrow>
    1.16 -  finite(ub a) & ub b \<subseteq> ub a & ub a \<supset> f b & f b \<supset> f a"
    1.17 +  finite(ub a) & ub b \<subseteq> ub a & ub a \<supseteq> f b & f b \<supset> f a"
    1.18  shows "wf r"
    1.19  apply(rule wf_bounded_measure[of r "%a. card(ub a)" "%a. card(f a)"])
    1.20  apply(drule assms)
    1.21 -apply (blast intro: card_mono finite_subset  psubset_card_mono dest: psubset_eq[THEN iffD2])
    1.22 +apply (blast intro: card_mono finite_subset psubset_card_mono dest: psubset_eq[THEN iffD2])
    1.23  done
    1.24  
    1.25