src/HOL/Fun.thy
 changeset 31949 3f933687fae9 parent 31775 2b04504fcb69 child 32139 e271a64f03ff
```     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
```