# HG changeset patch # User nipkow # Date 1255780015 -7200 # Node ID 4772d8dd18f8e63d85807a07d99b8b2b8479974a # Parent c39860141415ecf8102f377eba5f37788a2c0d1d# Parent 61431a41ddd5afa2937339a682ab63e2f850041b merged diff -r c39860141415 -r 4772d8dd18f8 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Fri Oct 16 10:55:07 2009 +0200 +++ b/src/HOL/Fun.thy Sat Oct 17 13:46:55 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 \ 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 \ 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 *}