# HG changeset patch
# User wenzelm
# Date 1485694683 -3600
# Node ID d55d743c45a2d66b1e2b883cd995891688a481d7
# Parent  a0c985a57f7e7395fda02cfab0ed26356134a062
tuned proofs;

diff -r a0c985a57f7e -r d55d743c45a2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Jan 29 13:43:17 2017 +0100
+++ b/src/HOL/Fun.thy	Sun Jan 29 13:58:03 2017 +0100
@@ -167,7 +167,7 @@
 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)
 
-lemma inj_on_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> inj_on f A = inj_on g A"
+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
 
 lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
@@ -205,7 +205,7 @@
   by (simp add: inj_on_def)
 
 lemma inj_on_inverseI: "(\<And>x. x \<in> A \<Longrightarrow> g (f x) = x) \<Longrightarrow> inj_on f A"
-  by (auto dest:  arg_cong [of concl: g] simp add: inj_on_def)
+  by (auto dest: arg_cong [of concl: g] simp add: inj_on_def)
 
 lemma inj_onD: "inj_on f A \<Longrightarrow> f x = f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
   unfolding inj_on_def by blast
@@ -220,8 +220,8 @@
   with assms have "a \<in> A" and "b \<in> A"
     by auto
   moreover assume "f a = f b"
-  ultimately show "a = b" using assms
-    by (auto dest: inj_onD)
+  ultimately show "a = b"
+    using assms by (auto dest: inj_onD)
 qed
 
 lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
@@ -231,7 +231,7 @@
   by (auto simp add: inj_on_def)
 
 lemma inj_on_image_iff:
-  "\<forall>x\<in>A. \<forall>y\<in>A. g (f x) = g (f y) \<longleftrightarrow> g x = g y \<Longrightarrow> inj_on f A \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
+  "\<forall>x\<in>A. \<forall>y\<in>A. g (f x) = g (f y) \<longleftrightarrow> g x = g y \<Longrightarrow> inj_on f A \<Longrightarrow> inj_on g (f ` A) \<longleftrightarrow> inj_on g A"
   unfolding inj_on_def by blast
 
 lemma inj_on_contraD: "inj_on f A \<Longrightarrow> x \<noteq> y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> f x \<noteq> f y"
@@ -256,10 +256,10 @@
   unfolding inj_on_def by blast
 
 lemma comp_inj_on_iff: "inj_on f A \<Longrightarrow> inj_on f' (f ` A) \<longleftrightarrow> inj_on (f' \<circ> f) A"
-  by (auto simp add: comp_inj_on inj_on_def)
+  by (auto simp: comp_inj_on inj_on_def)
 
 lemma inj_on_imageI2: "inj_on (f' \<circ> f) A \<Longrightarrow> inj_on f A"
-  by (auto simp add: comp_inj_on inj_on_def)
+  by (auto simp: comp_inj_on inj_on_def)
 
 lemma inj_img_insertE:
   assumes "inj_on f A"
@@ -276,21 +276,21 @@
 qed
 
 lemma linorder_injI:
-  assumes hyp: "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
+  assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
   shows "inj f"
   \<comment> \<open>Courtesy of Stephan Merz\<close>
 proof (rule inj_onI)
   show "x = y" if "f x = f y" for x y
-   by (rule linorder_cases) (auto dest: hyp simp: that)
+   by (rule linorder_cases) (auto dest: assms simp: that)
 qed
 
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   by auto
 
 lemma surjI:
-  assumes *: "\<And> x. g (f x) = x"
+  assumes "\<And>x. g (f x) = x"
   shows "surj g"
-  using *[symmetric] by auto
+  using assms [symmetric] by auto
 
 lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
   by (simp add: surj_def)
@@ -320,10 +320,10 @@
   unfolding bij_betw_def by simp
 
 lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
-  unfolding bij_betw_def ..
+  by (rule bij_betw_def)
 
 lemma bijI: "inj f \<Longrightarrow> surj f \<Longrightarrow> bij f"
-  by (simp add: bij_def)
+  by (rule bij_betw_imageI)
 
 lemma bij_is_inj: "bij f \<Longrightarrow> inj f"
   by (simp add: bij_def)
@@ -459,7 +459,7 @@
   unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
 
 lemma inj_on_image_eq_iff: "inj_on f C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> B \<subseteq> C \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
-  by (fastforce simp add: inj_on_def)
+  by (fastforce simp: inj_on_def)
 
 lemma inj_on_Un_image_eq_iff: "inj_on f (A \<union> B) \<Longrightarrow> f ` A = f ` B \<longleftrightarrow> A = B"
   by (erule inj_on_image_eq_iff) simp_all
@@ -660,19 +660,19 @@
   where "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
 
 lemma override_on_emptyset[simp]: "override_on f g {} = f"
-  by (simp add:override_on_def)
+  by (simp add: override_on_def)
 
 lemma override_on_apply_notin[simp]: "a \<notin> A \<Longrightarrow> (override_on f g A) a = f a"
-  by (simp add:override_on_def)
+  by (simp add: override_on_def)
 
 lemma override_on_apply_in[simp]: "a \<in> A \<Longrightarrow> (override_on f g A) a = g a"
-  by (simp add:override_on_def)
+  by (simp add: override_on_def)
 
 lemma override_on_insert: "override_on f g (insert x X) = (override_on f g X)(x:=g x)"
-  unfolding override_on_def by (simp add: fun_eq_iff)
+  by (simp add: override_on_def fun_eq_iff)
 
 lemma override_on_insert': "override_on f g (insert x X) = (override_on (f(x:=g x)) g X)"
-  unfolding override_on_def by (simp add: fun_eq_iff)
+  by (simp add: override_on_def fun_eq_iff)
 
 
 subsection \<open>\<open>swap\<close>\<close>
@@ -797,10 +797,8 @@
 abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
   where "the_inv f \<equiv> the_inv_into UNIV f"
 
-lemma the_inv_f_f:
-  assumes "inj f"
-  shows "the_inv f (f x) = x"
-  using assms UNIV_I by (rule the_inv_into_f_f)
+lemma the_inv_f_f: "the_inv f (f x) = x" if "inj f"
+  using that UNIV_I by (rule the_inv_into_f_f)
 
 
 subsection \<open>Cantor's Paradox\<close>