--- a/src/HOL/Complete_Lattices.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Jan 29 17:27:02 2017 +0100
@@ -1320,11 +1320,7 @@
by (auto simp add: inj_on_def) blast
lemma bij_image_INT: "bij f \<Longrightarrow> f ` (INTER A B) = (INT x:A. f ` B x)"
- apply (simp only: bij_def)
- apply (simp only: inj_on_def surj_def)
- apply auto
- apply blast
- done
+ by (auto simp: bij_def inj_def surj_def) blast
lemma UNION_fun_upd: "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
by (auto simp add: set_eq_iff)
--- a/src/HOL/Fun.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/Fun.thy Sun Jan 29 17:27:02 2017 +0100
@@ -155,29 +155,32 @@
abbreviation "bij f \<equiv> bij_betw f UNIV UNIV"
+lemma inj_def: "inj f \<longleftrightarrow> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
+ unfolding inj_on_def by blast
+
lemma injI: "(\<And>x y. f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj f"
- unfolding inj_on_def by auto
+ unfolding inj_def by blast
theorem range_ex1_eq: "inj f \<Longrightarrow> b \<in> range f \<longleftrightarrow> (\<exists>!x. b = f x)"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
lemma injD: "inj f \<Longrightarrow> f x = f y \<Longrightarrow> x = y"
- by (simp add: inj_on_def)
+ by (simp add: inj_def)
lemma inj_on_eq_iff: "inj_on f A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
- by (force simp add: inj_on_def)
+ by (auto simp: inj_on_def)
lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A \<longleftrightarrow> inj_on g A"
- unfolding inj_on_def by auto
+ by (auto simp: inj_on_def)
lemma inj_on_strict_subset: "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)"
- by (simp add: inj_on_def)
+ by (simp add: inj_def)
lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
- by (simp add: inj_on_def fun_eq_iff)
+ by (simp add: inj_def fun_eq_iff)
lemma inj_eq: "inj f \<Longrightarrow> f x = f y \<longleftrightarrow> x = y"
by (simp add: inj_on_eq_iff)
@@ -423,7 +426,7 @@
"bij_betw f A B \<Longrightarrow> bij_betw f C D \<Longrightarrow> B \<inter> D = {} \<Longrightarrow> bij_betw f (A \<union> C) (B \<union> D)"
unfolding bij_betw_def inj_on_Un image_Un by auto
-lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<le> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
+lemma bij_betw_subset: "bij_betw f A A' \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f ` B = B' \<Longrightarrow> bij_betw f B B'"
by (auto simp add: bij_betw_def inj_on_def)
lemma bij_pointE:
@@ -447,13 +450,13 @@
by (intro iffI) fastforce+
lemma inj_vimage_image_eq: "inj f \<Longrightarrow> f -` (f ` A) = A"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
lemma vimage_subsetD: "surj f \<Longrightarrow> f -` B \<subseteq> A \<Longrightarrow> B \<subseteq> f ` A"
by (blast intro: sym)
lemma vimage_subsetI: "inj f \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> f -` B \<subseteq> A"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
lemma vimage_subset_eq: "bij f \<Longrightarrow> f -` B \<subseteq> A \<longleftrightarrow> B \<subseteq> f ` A"
unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
@@ -471,10 +474,10 @@
unfolding inj_on_def by blast
lemma image_Int: "inj f \<Longrightarrow> f ` (A \<inter> B) = f ` A \<inter> f ` B"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
lemma image_set_diff: "inj f \<Longrightarrow> f ` (A - B) = f ` A - f ` B"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
lemma inj_on_image_mem_iff: "inj_on f B \<Longrightarrow> a \<in> B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
by (auto simp: inj_on_def)
@@ -496,14 +499,14 @@
by auto
lemma inj_image_Compl_subset: "inj f \<Longrightarrow> f ` (- A) \<subseteq> - (f ` A)"
- by (auto simp add: inj_on_def)
+ by (auto simp: inj_def)
lemma bij_image_Compl_eq: "bij f \<Longrightarrow> f ` (- A) = - (f ` A)"
by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI)
lemma inj_vimage_singleton: "inj f \<Longrightarrow> f -` {a} \<subseteq> {THE x. f x = a}"
\<comment> \<open>The inverse image of a singleton under an injective function is included in a singleton.\<close>
- by (simp add: inj_on_def) (blast intro: the_equality [symmetric])
+ by (simp add: inj_def) (blast intro: the_equality [symmetric])
lemma inj_on_vimage_singleton: "inj_on f A \<Longrightarrow> f -` {a} \<inter> A \<subseteq> {THE x. x \<in> A \<and> f x = a}"
by (auto simp add: inj_on_def intro: the_equality [symmetric])
@@ -642,7 +645,7 @@
by (rule ext) auto
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)
+ by (auto 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)"
by auto
--- a/src/HOL/Library/Indicator_Function.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/Library/Indicator_Function.thy Sun Jan 29 17:27:02 2017 +0100
@@ -69,7 +69,7 @@
unfolding indicator_def by (cases x) auto
lemma indicator_image: "inj f \<Longrightarrow> indicator (f ` X) (f x) = (indicator X x::_::zero_neq_one)"
- by (auto simp: indicator_def inj_on_def)
+ by (auto simp: indicator_def inj_def)
lemma indicator_vimage: "indicator (f -` A) x = indicator A (f x)"
by (auto split: split_indicator)
--- a/src/HOL/Library/Permutations.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/Library/Permutations.thy Sun Jan 29 17:27:02 2017 +0100
@@ -60,7 +60,7 @@
done
lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
- unfolding permutes_def inj_on_def by blast
+ unfolding permutes_def inj_def by blast
lemma permutes_inj_on: "f permutes S \<Longrightarrow> inj_on f A"
unfolding permutes_def inj_on_def by auto
@@ -699,7 +699,7 @@
subsection \<open>A more abstract characterization of permutations\<close>
lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
- unfolding bij_def inj_on_def surj_def
+ unfolding bij_def inj_def surj_def
apply auto
apply metis
apply metis
@@ -758,7 +758,7 @@
by (simp add: Fun.swap_def)
from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r" .
from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
- by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))
+ by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))
from insert(3)[OF br th] have rp: "permutation ?r" .
have "permutation ?q"
by (simp add: permutation_compose permutation_swap_id rp)
@@ -1104,7 +1104,7 @@
from H h have "p (p n) = p n"
by metis
with permutes_inj[OF H(2)] have "p n = n"
- unfolding inj_on_def by blast
+ unfolding inj_def by blast
with h have False
by simp
}
--- a/src/HOL/List.thy Sun Jan 29 13:58:03 2017 +0100
+++ b/src/HOL/List.thy Sun Jan 29 17:27:02 2017 +0100
@@ -1175,11 +1175,12 @@
by (iprover dest: map_injective injD intro: inj_onI)
lemma inj_mapD: "inj (map f) ==> inj f"
-apply (unfold inj_on_def, clarify)
-apply (erule_tac x = "[x]" in ballE)
- apply (erule_tac x = "[y]" in ballE, simp, blast)
-apply blast
-done
+ apply (unfold inj_def)
+ apply clarify
+ apply (erule_tac x = "[x]" in allE)
+ apply (erule_tac x = "[y]" in allE)
+ apply auto
+ done
lemma inj_map[iff]: "inj (map f) = inj f"
by (blast dest: inj_mapD intro: inj_mapI)