src/HOL/Fun.thy
changeset 32998 31b19fa0de0b
parent 32988 d1d4d7a08a66
child 33044 fd0a9c794ec1
     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