--- a/src/HOL/Finite_Set.thy Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Finite_Set.thy Tue Jul 01 06:51:59 2008 +0200
@@ -255,7 +255,7 @@
lemma finite_range_imageI:
"finite (range g) ==> finite (range (%x. f (g x)))"
- apply (drule finite_imageI, simp)
+ apply (drule finite_imageI, simp add: range_composition)
done
lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
--- a/src/HOL/Set.thy Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/Set.thy Tue Jul 01 06:51:59 2008 +0200
@@ -1324,7 +1324,7 @@
lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
by auto
-lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
+lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
by (subst image_image, simp)
--- a/src/HOL/SizeChange/Correctness.thy Tue Jul 01 06:21:28 2008 +0200
+++ b/src/HOL/SizeChange/Correctness.thy Tue Jul 01 06:51:59 2008 +0200
@@ -52,7 +52,7 @@
neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
from fin have "finite (range (j o f))"
- by (auto simp:comp_def)
+ by (auto simp:comp_def range_composition)
with finite_nat_bounded
obtain m where "range (j o f) \<subseteq> {..<m}" by blast
hence "j (f m) < m" unfolding comp_def by auto