1.1 --- a/src/HOL/Fun.thy	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Jul 06 14:19:13 2009 +0200
     1.3 @@ -496,6 +496,40 @@
     1.4  
     1.5  hide (open) const swap
     1.6  
     1.7 +
     1.8 +subsection {* Inversion of injective functions *}
     1.9 +
    1.10 +definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    1.11 +  "inv f y = (THE x. f x = y)"
    1.12 +
    1.13 +lemma inv_f_f:
    1.14 +  assumes "inj f"
    1.15 +  shows "inv f (f x) = x"
    1.16 +proof -
    1.17 +  from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
    1.18 +    by (simp only: inj_eq)
    1.19 +  also have "... = x" by (rule the_eq_trivial)
    1.20 +  finally show ?thesis by (unfold inv_def)
    1.21 +qed
    1.22 +
    1.23 +lemma f_inv_f:
    1.24 +  assumes "inj f"
    1.25 +  and "y \<in> range f"
    1.26 +  shows "f (inv f y) = y"
    1.27 +proof (unfold inv_def)
    1.28 +  from `y \<in> range f` obtain x where "y = f x" ..
    1.29 +  then have "f x = y" ..
    1.30 +  then show "f (THE x. f x = y) = y"
    1.31 +  proof (rule theI)
    1.32 +    fix x' assume "f x' = y"
    1.33 +    with `f x = y` have "f x' = f x" by simp
    1.34 +    with `inj f` show "x' = x" by (rule injD)
    1.35 +  qed
    1.36 +qed
    1.37 +
    1.38 +hide (open) const inv
    1.39 +
    1.40 +
    1.41  subsection {* Proof tool setup *} 
    1.42  
    1.43  text {* simplifies terms of the form