# HG changeset patch
# User berghofe
# Date 1255963425 -7200
# Node ID 31b19fa0de0b17b2ce806d77cbcb06d490443831
# Parent  e760950ba6c5536d86aeb6c690f0d3f67d59180e
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).

diff -r e760950ba6c5 -r 31b19fa0de0b src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Oct 18 22:19:05 2009 +0200
+++ b/src/HOL/Fun.thy	Mon Oct 19 16:43:45 2009 +0200
@@ -505,36 +505,6 @@
 
 subsection {* Inversion of injective functions *}
 
-definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
-  "inv f y = (THE x. f x = y)"
-
-lemma inv_f_f:
-  assumes "inj f"
-  shows "inv f (f x) = x"
-proof -
-  from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
-    by (simp add: inj_on_eq_iff)
-  also have "... = x" by (rule the_eq_trivial)
-  finally show ?thesis by (unfold inv_def)
-qed
-
-lemma f_inv_f:
-  assumes "inj f"
-  and "y \<in> range f"
-  shows "f (inv f y) = y"
-proof (unfold inv_def)
-  from `y \<in> range f` obtain x where "y = f x" ..
-  then have "f x = y" ..
-  then show "f (THE x. f x = y) = y"
-  proof (rule theI)
-    fix x' assume "f x' = y"
-    with `f x = y` have "f x' = f x" by simp
-    with `inj f` show "x' = x" by (rule injD)
-  qed
-qed
-
-hide (open) const inv
-
 definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
 "the_inv_onto A f == %x. THE y. y : A & f y = x"
 
@@ -587,6 +557,14 @@
   "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
 by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
 
+abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
+  "the_inv f \<equiv> the_inv_onto 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_onto_f_f)
+
 
 subsection {* Proof tool setup *}