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