diff -r 63466160ff27 -r 3f933687fae9 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy Sat Jul 04 23:25:28 2009 +0200
+++ b/src/HOL/Fun.thy Mon Jul 06 14:19:13 2009 +0200
@@ -496,6 +496,40 @@
hide (open) const swap
+
+subsection {* Inversion of injective functions *}
+
+definition inv :: "('a \ 'b) \ ('b \ '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 only: inj_eq)
+ 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 \ range f"
+ shows "f (inv f y) = y"
+proof (unfold inv_def)
+ from `y \ 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
+
+
subsection {* Proof tool setup *}
text {* simplifies terms of the form