author berghofe Mon Oct 19 16:43:45 2009 +0200 (2009-10-19) changeset 32998 31b19fa0de0b parent 32997 e760950ba6c5 child 32999 d603c567170b
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
 src/HOL/Fun.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Fun.thy	Sun Oct 18 22:19:05 2009 +0200
1.2 +++ b/src/HOL/Fun.thy	Mon Oct 19 16:43:45 2009 +0200
1.3 @@ -505,36 +505,6 @@
1.4
1.5  subsection {* Inversion of injective functions *}
1.6
1.7 -definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
1.8 -  "inv f y = (THE x. f x = y)"
1.9 -
1.10 -lemma inv_f_f:
1.11 -  assumes "inj f"
1.12 -  shows "inv f (f x) = x"
1.13 -proof -
1.14 -  from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
1.15 -    by (simp add: inj_on_eq_iff)
1.16 -  also have "... = x" by (rule the_eq_trivial)
1.17 -  finally show ?thesis by (unfold inv_def)
1.18 -qed
1.19 -
1.20 -lemma f_inv_f:
1.21 -  assumes "inj f"
1.22 -  and "y \<in> range f"
1.23 -  shows "f (inv f y) = y"
1.24 -proof (unfold inv_def)
1.25 -  from `y \<in> range f` obtain x where "y = f x" ..
1.26 -  then have "f x = y" ..
1.27 -  then show "f (THE x. f x = y) = y"
1.28 -  proof (rule theI)
1.29 -    fix x' assume "f x' = y"
1.30 -    with `f x = y` have "f x' = f x" by simp
1.31 -    with `inj f` show "x' = x" by (rule injD)
1.32 -  qed
1.33 -qed
1.34 -
1.35 -hide (open) const inv
1.36 -
1.37  definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
1.38  "the_inv_onto A f == %x. THE y. y : A & f y = x"
1.39
1.40 @@ -587,6 +557,14 @@
1.41    "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
1.42  by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
1.43
1.44 +abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
1.45 +  "the_inv f \<equiv> the_inv_onto UNIV f"
1.46 +
1.47 +lemma the_inv_f_f:
1.48 +  assumes "inj f"
1.49 +  shows "the_inv f (f x) = x" using assms UNIV_I
1.50 +  by (rule the_inv_onto_f_f)
1.51 +
1.52
1.53  subsection {* Proof tool setup *}
1.54
```