src/HOL/Fun.thy

 hide (open) const swap
 
 
 subsection {* Inversion of injective functions *}
 
-definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
-"the_inv_onto A f == %x. THE y. y : A & f y = x"
-
-lemma the_inv_onto_f_f:
-  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
-apply (simp add: the_inv_onto_def inj_on_def)
+definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
+"the_inv_into A f == %x. THE y. y : A & f y = x"
+
+lemma the_inv_into_f_f:
+  "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
+apply (simp add: the_inv_into_def inj_on_def)
 apply (blast intro: the_equality)
 done
 
-lemma f_the_inv_onto_f:
-  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
-apply (simp add: the_inv_onto_def)
+lemma f_the_inv_into_f:
+  "inj_on f A ==> y : f`A  ==> f (the_inv_into A f y) = y"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_into:
-  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
-apply (simp add: the_inv_onto_def)
+lemma the_inv_into_into:
+  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B"
+apply (simp add: the_inv_into_def)
 apply (rule the1I2)
  apply(blast dest: inj_onD)
 apply blast
 done
 
-lemma the_inv_onto_onto[simp]:
-  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
-by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
-
-lemma the_inv_onto_f_eq:
-  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
+lemma the_inv_into_onto[simp]:
+  "inj_on f A ==> the_inv_into A f ` (f ` A) = A"
+by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric])
+
+lemma the_inv_into_f_eq:
+  "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x"
   apply (erule subst)
-  apply (erule the_inv_onto_f_f, assumption)
+  apply (erule the_inv_into_f_f, assumption)
   done
 
-lemma the_inv_onto_comp:
+lemma the_inv_into_comp:
   "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
-  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
-apply (rule the_inv_onto_f_eq)
+  the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x"
+apply (rule the_inv_into_f_eq)
   apply (fast intro: comp_inj_on)
- apply (simp add: f_the_inv_onto_f the_inv_onto_into)
-apply (simp add: the_inv_onto_into)
-done
-
-lemma inj_on_the_inv_onto:
-  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
-by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
-
-lemma bij_betw_the_inv_onto:
-  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
-by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
+ apply (simp add: f_the_inv_into_f the_inv_into_into)
+apply (simp add: the_inv_into_into)
+done
+
+lemma inj_on_the_inv_into:
+  "inj_on f A \<Longrightarrow> inj_on (the_inv_into A f) (f ` A)"
+by (auto intro: inj_onI simp: image_def the_inv_into_f_f)
+
+lemma bij_betw_the_inv_into:
+  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
+by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
 
 abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where
-  "the_inv f \<equiv> the_inv_onto UNIV f"
+  "the_inv f \<equiv> the_inv_into UNIV f"
 
 lemma the_inv_f_f:
   assumes "inj f"
   shows "the_inv f (f x) = x" using assms UNIV_I
-  by (rule the_inv_onto_f_f)
+  by (rule the_inv_into_f_f)
 
 
 subsection {* Proof tool setup *} 
 
 text {* simplifies terms of the form