remove simp attribute from range_composition
authorhuffman
Tue Jul 01 06:51:59 2008 +0200 (2008-07-01)
changeset 27418564117b58d73
parent 27417 6cc897e2468a
child 27419 ff2a2b8fcd09
remove simp attribute from range_composition
src/HOL/Finite_Set.thy
src/HOL/Set.thy
src/HOL/SizeChange/Correctness.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Jul 01 06:21:28 2008 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 01 06:51:59 2008 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4  
     1.5  lemma finite_range_imageI:
     1.6      "finite (range g) ==> finite (range (%x. f (g x)))"
     1.7 -  apply (drule finite_imageI, simp)
     1.8 +  apply (drule finite_imageI, simp add: range_composition)
     1.9    done
    1.10  
    1.11  lemma finite_imageD: "finite (f`A) ==> inj_on f A ==> finite A"
     2.1 --- a/src/HOL/Set.thy	Tue Jul 01 06:21:28 2008 +0200
     2.2 +++ b/src/HOL/Set.thy	Tue Jul 01 06:51:59 2008 +0200
     2.3 @@ -1324,7 +1324,7 @@
     2.4  lemma full_SetCompr_eq [noatp]: "{u. \<exists>x. u = f x} = range f"
     2.5    by auto
     2.6  
     2.7 -lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
     2.8 +lemma range_composition: "range (\<lambda>x. f (g x)) = f`range g"
     2.9  by (subst image_image, simp)
    2.10  
    2.11  
     3.1 --- a/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 06:21:28 2008 +0200
     3.2 +++ b/src/HOL/SizeChange/Correctness.thy	Tue Jul 01 06:51:59 2008 +0200
     3.3 @@ -52,7 +52,7 @@
     3.4      neq: "\<And>x i. j x < i \<Longrightarrow> f i \<noteq> x" by blast
     3.5  
     3.6    from fin have "finite (range (j o f))" 
     3.7 -    by (auto simp:comp_def)
     3.8 +    by (auto simp:comp_def range_composition)
     3.9    with finite_nat_bounded
    3.10    obtain m where "range (j o f) \<subseteq> {..<m}" by blast
    3.11    hence "j (f m) < m" unfolding comp_def by auto