src/HOL/Fun.thy
changeset 32961 61431a41ddd5
parent 32740 9dd0a2f83429
child 32988 d1d4d7a08a66
     1.1 --- a/src/HOL/Fun.thy	Fri Oct 16 00:26:19 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Oct 17 13:46:39 2009 +0200
     1.3 @@ -533,6 +533,58 @@
     1.4  
     1.5  hide (open) const inv
     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 +
    1.10 +lemma the_inv_onto_f_f:
    1.11 +  "[| inj_on f A;  x : A |] ==> the_inv_onto A f (f x) = x"
    1.12 +apply (simp add: the_inv_onto_def inj_on_def)
    1.13 +apply (blast intro: the_equality)
    1.14 +done
    1.15 +
    1.16 +lemma f_the_inv_onto_f:
    1.17 +  "inj_on f A ==> y : f`A  ==> f (the_inv_onto A f y) = y"
    1.18 +apply (simp add: the_inv_onto_def)
    1.19 +apply (rule the1I2)
    1.20 + apply(blast dest: inj_onD)
    1.21 +apply blast
    1.22 +done
    1.23 +
    1.24 +lemma the_inv_onto_into:
    1.25 +  "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B"
    1.26 +apply (simp add: the_inv_onto_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_onto[simp]:
    1.33 +  "inj_on f A ==> the_inv_onto A f ` (f ` A) = A"
    1.34 +by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric])
    1.35 +
    1.36 +lemma the_inv_onto_f_eq:
    1.37 +  "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x"
    1.38 +  apply (erule subst)
    1.39 +  apply (erule the_inv_onto_f_f, assumption)
    1.40 +  done
    1.41 +
    1.42 +lemma the_inv_onto_comp:
    1.43 +  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
    1.44 +  the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x"
    1.45 +apply (rule the_inv_onto_f_eq)
    1.46 +  apply (fast intro: comp_inj_on)
    1.47 + apply (simp add: f_the_inv_onto_f the_inv_onto_into)
    1.48 +apply (simp add: the_inv_onto_into)
    1.49 +done
    1.50 +
    1.51 +lemma inj_on_the_inv_onto:
    1.52 +  "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)"
    1.53 +by (auto intro: inj_onI simp: image_def the_inv_onto_f_f)
    1.54 +
    1.55 +lemma bij_betw_the_inv_onto:
    1.56 +  "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A"
    1.57 +by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into)
    1.58 +
    1.59  
    1.60  subsection {* Proof tool setup *} 
    1.61