# HG changeset patch
# User nipkow
# Date 1255779999 -7200
# Node ID 61431a41ddd5afa2937339a682ab63e2f850041b
# Parent  c054b03c7881061d8b211954460a687e51a8abdc
added the_inv_onto

diff -r c054b03c7881 -r 61431a41ddd5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Fun.thy	Sat Oct 17 13:46:39 2009 +0200
@@ -533,6 +533,58 @@
 
 hide (open) const inv
 
+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)
+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)
+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)
+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"
+  apply (erule subst)
+  apply (erule the_inv_onto_f_f, assumption)
+  done
+
+lemma the_inv_onto_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)
+  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)
+
 
 subsection {* Proof tool setup *}