src/HOL/Fun.thy
changeset 33057 764547b68538
parent 33044 fd0a9c794ec1
child 33318 ddd97d9dfbfb
     1.1 --- a/src/HOL/Fun.thy	Wed Oct 21 17:34:35 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Oct 22 09:27:48 2009 +0200
     1.3 @@ -508,65 +508,65 @@
     1.4  
     1.5  subsection {* Inversion of injective functions *}
     1.6  
     1.7 -definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
     1.8 -"the_inv_onto A f == %x. THE y. y : A & f y = x"
     1.9 +definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
    1.10 +"the_inv_into A f == %x. THE y. y : A & f y = x"
    1.11  
    1.12 -lemma the_inv_onto_f_f:
    1.13 -  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
    1.14 -apply (simp add: the_inv_onto_def inj_on_def)
    1.15 +lemma the_inv_into_f_f:
    1.16 +  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
    1.17 +apply (simp add: the_inv_into_def inj_on_def)
    1.18  apply (blast intro: the_equality)
    1.19  done
    1.20  
    1.21 -lemma f_the_inv_onto_f:
    1.22 -  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
    1.23 -apply (simp add: the_inv_onto_def)
    1.24 +lemma f_the_inv_into_f:
    1.25 +  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
    1.26 +apply (simp add: the_inv_into_def)
    1.27  apply (rule the1I2)
    1.28   apply(blast dest: inj_onD)
    1.29  apply blast
    1.30  done
    1.31  
    1.32 -lemma the_inv_onto_into:
    1.33 -  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
    1.34 -apply (simp add: the_inv_onto_def)
    1.35 +lemma the_inv_into_into:
    1.36 +  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
    1.37 +apply (simp add: the_inv_into_def)
    1.38  apply (rule the1I2)
    1.39   apply(blast dest: inj_onD)
    1.40  apply blast
    1.41  done
    1.42  
    1.43 -lemma the_inv_onto_onto[simp]:
    1.44 -  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
    1.45 -by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
    1.46 +lemma the_inv_into_onto[simp]:
    1.47 +  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
    1.48 +by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
    1.49  
    1.50 -lemma the_inv_onto_f_eq:
    1.51 -  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
    1.52 +lemma the_inv_into_f_eq:
    1.53 +  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
    1.54    apply (erule subst)
    1.55 -  apply (erule the_inv_onto_f_f, assumption)
    1.56 +  apply (erule the_inv_into_f_f, assumption)
    1.57    done
    1.58  
    1.59 -lemma the_inv_onto_comp:
    1.60 +lemma the_inv_into_comp:
    1.61    "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
    1.62 -  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
    1.63 -apply (rule the_inv_onto_f_eq)
    1.64 +  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
    1.65 +apply (rule the_inv_into_f_eq)
    1.66    apply (fast intro: comp_inj_on)
    1.67 - apply (simp add: f_the_inv_onto_f the_inv_onto_into)
    1.68 -apply (simp add: the_inv_onto_into)
    1.69 + apply (simp add: f_the_inv_into_f the_inv_into_into)
    1.70 +apply (simp add: the_inv_into_into)
    1.71  done
    1.72  
    1.73 -lemma inj_on_the_inv_onto:
    1.74 -  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
    1.75 -by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
    1.76 +lemma inj_on_the_inv_into:
    1.77 +  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
    1.78 +by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
    1.79  
    1.80 -lemma bij_betw_the_inv_onto:
    1.81 -  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
    1.82 -by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
    1.83 +lemma bij_betw_the_inv_into:
    1.84 +  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
    1.85 +by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
    1.86  
    1.87  abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
    1.88 -  "the_inv f \<equiv> the_inv_onto UNIV f"
    1.89 +  "the_inv f \<equiv> the_inv_into UNIV f"
    1.90  
    1.91  lemma the_inv_f_f:
    1.92    assumes "inj f"
    1.93    shows "the_inv f (f x) = x" using assms UNIV_I
    1.94 -  by (rule the_inv_onto_f_f)
    1.95 +  by (rule the_inv_into_f_f)
    1.96  
    1.97  
    1.98  subsection {* Proof tool setup *}