--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Thu Mar 13 08:56:08 2014 +0100
@@ -600,7 +600,7 @@
shows "|B| \<le>o |B \<times> A|"
proof(cases "B = {}", simp add: card_of_empty)
assume *: "B \<noteq> {}"
- have "fst `(B \<times> A) = B" unfolding image_def using assms by auto
+ have "fst `(B \<times> A) = B" using assms by auto
thus ?thesis using inj_on_iff_surj[of B "B \<times> A"]
card_of_ordLeq[of B "B \<times> A"] * by blast
qed
@@ -1652,7 +1652,7 @@
hence "\<forall> a. \<exists> b. h a = b" unfolding Func_def by auto
then obtain f where f: "\<forall> a. h a = f a" by blast
hence "range f \<subseteq> B" using h unfolding Func_def by auto
- thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f unfolding image_def by auto
+ thus "h \<in> (\<lambda>f a. f a) ` {f. range f \<subseteq> B}" using f by auto
qed(unfold Func_def fun_eq_iff, auto)
qed
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy Thu Mar 13 08:56:08 2014 +0100
@@ -1653,9 +1653,9 @@
qed(insert h, unfold Func_def Func_map_def, auto)
qed
moreover have "g \<in> Func A2 A1" unfolding g_def apply(rule Func_map[OF h])
- using j2A2 B1 A2 unfolding j1_def image_def by (fast intro: inv_into_into)+
+ using j2A2 B1 A2 unfolding j1_def by (fast intro: inv_into_into)+
ultimately show "h \<in> Func_map B2 f1 f2 ` Func A2 A1"
- unfolding Func_map_def[abs_def] unfolding image_def by auto
+ unfolding Func_map_def[abs_def] by auto
qed(insert B1 Func_map[OF _ _ A2(2)], auto)
qed
--- a/src/HOL/Basic_BNFs.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Basic_BNFs.thy Thu Mar 13 08:56:08 2014 +0100
@@ -175,7 +175,7 @@
thus "f \<circ> x = g \<circ> x" by auto
next
fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
- unfolding image_def comp_def[abs_def] by auto
+ by (auto simp add: fun_eq_iff)
next
show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
apply (rule card_order_csum)
--- a/src/HOL/Fun.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Fun.thy Thu Mar 13 08:56:08 2014 +0100
@@ -159,8 +159,8 @@
unfolding inj_on_def by auto
lemma inj_on_strict_subset:
- "\<lbrakk> inj_on f B; A < B \<rbrakk> \<Longrightarrow> f`A < f`B"
-unfolding inj_on_def unfolding image_def by blast
+ "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
+ unfolding inj_on_def by blast
lemma inj_comp:
"inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
@@ -198,16 +198,14 @@
by (unfold inj_on_def, blast)
lemma inj_on_iff: "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"
-by (blast dest!: inj_onD)
+ by (fact inj_on_eq_iff)
lemma comp_inj_on:
"[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A"
by (simp add: comp_def inj_on_def)
lemma inj_on_imageI: "inj_on (g o f) A \<Longrightarrow> inj_on g (f ` A)"
-apply(simp add:inj_on_def image_def)
-apply blast
-done
+ by (simp add: inj_on_def) blast
lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
@@ -368,26 +366,26 @@
using assms by(auto simp:bij_betw_def)
let ?P = "%b a. a:A \<and> f a = b" let ?g = "%b. The (?P b)"
{ fix a b assume P: "?P b a"
- hence ex1: "\<exists>a. ?P b a" using s unfolding image_def by blast
+ hence ex1: "\<exists>a. ?P b a" using s by blast
hence uex1: "\<exists>!a. ?P b a" by(blast dest:inj_onD[OF i])
hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp
} note g = this
have "inj_on ?g B"
proof(rule inj_onI)
fix x y assume "x:B" "y:B" "?g x = ?g y"
- from s `x:B` obtain a1 where a1: "?P x a1" unfolding image_def by blast
- from s `y:B` obtain a2 where a2: "?P y a2" unfolding image_def by blast
+ from s `x:B` obtain a1 where a1: "?P x a1" by blast
+ from s `y:B` obtain a2 where a2: "?P y a2" by blast
from g[OF a1] a1 g[OF a2] a2 `?g x = ?g y` show "x=y" by simp
qed
moreover have "?g ` B = A"
- proof(auto simp:image_def)
+ proof(auto simp: image_def)
fix b assume "b:B"
- with s obtain a where P: "?P b a" unfolding image_def by blast
+ with s obtain a where P: "?P b a" by blast
thus "?g b \<in> A" using g[OF P] by auto
next
fix a assume "a:A"
- then obtain b where P: "?P b a" using s unfolding image_def by blast
- then have "b:B" using s unfolding image_def by blast
+ then obtain b where P: "?P b a" using s by blast
+ then have "b:B" using s by blast
with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
qed
ultimately show ?thesis by(auto simp:bij_betw_def)
@@ -614,8 +612,9 @@
lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
by (rule ext, auto)
-lemma inj_on_fun_updI: "\<lbrakk> inj_on f A; y \<notin> f`A \<rbrakk> \<Longrightarrow> inj_on (f(x:=y)) A"
-by (fastforce simp:inj_on_def image_def)
+lemma inj_on_fun_updI:
+ "inj_on f A \<Longrightarrow> y \<notin> f ` A \<Longrightarrow> inj_on (f(x := y)) A"
+ by (fastforce simp: inj_on_def)
lemma fun_upd_image:
"f(x:=y) ` A = (if x \<in> A then insert y (f ` (A-{x})) else f ` A)"
@@ -750,7 +749,7 @@
lemma inj_on_the_inv_into:
"inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
-by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
+by (auto intro: inj_onI simp: the_inv_into_f_f)
lemma bij_betw_the_inv_into:
"bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
--- a/src/HOL/Product_Type.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 13 08:56:08 2014 +0100
@@ -1125,7 +1125,7 @@
lemma swap_product:
"(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
- by (simp add: split_def image_def) blast
+ by (simp add: split_def image_def set_eq_iff)
lemma image_split_eq_Sigma:
"(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))"
--- a/src/HOL/Set.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Set.thy Thu Mar 13 08:56:08 2014 +0100
@@ -1003,7 +1003,7 @@
lemma if_image_distrib [simp]:
"(\<lambda>x. if P x then f x else g x) ` S
= (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
- by (auto simp add: image_def)
+ by auto
lemma image_cong:
"M = N \<Longrightarrow> (\<And>x. x \<in> N \<Longrightarrow> f x = g x) \<Longrightarrow> f ` M = g ` N"
@@ -1054,7 +1054,7 @@
lemma range_composition:
"range (\<lambda>x. f (g x)) = f ` range g"
- by (subst image_image) simp
+ by auto
subsubsection {* Some rules with @{text "if"} *}