# HG changeset patch
# User wenzelm
# Date 1485707222 -3600
# Node ID d53d7ca3303eae7a192b7bc028dcfcd6992d4bb4
# Parent  d55d743c45a2d66b1e2b883cd995891688a481d7
added inj_def (redundant, analogous to surj_def, bij_def);
tuned proofs;

diff -r d55d743c45a2 -r d53d7ca3303e src/HOL/Complete_Lattices.thy
--- 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)
diff -r d55d743c45a2 -r d53d7ca3303e src/HOL/Fun.thy
--- 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
diff -r d55d743c45a2 -r d53d7ca3303e src/HOL/Library/Indicator_Function.thy
--- 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)
diff -r d55d743c45a2 -r d53d7ca3303e src/HOL/Library/Permutations.thy
--- 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
         }
diff -r d55d743c45a2 -r d53d7ca3303e src/HOL/List.thy
--- 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)