531 qed |
531 qed |
532 qed |
532 qed |
533 |
533 |
534 hide (open) const inv |
534 hide (open) const inv |
535 |
535 |
|
536 definition the_inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where |
|
537 "the_inv_onto A f == %x. THE y. y : A & f y = x" |
|
538 |
|
539 lemma the_inv_onto_f_f: |
|
540 "[| inj_on f A; x : A |] ==> the_inv_onto A f (f x) = x" |
|
541 apply (simp add: the_inv_onto_def inj_on_def) |
|
542 apply (blast intro: the_equality) |
|
543 done |
|
544 |
|
545 lemma f_the_inv_onto_f: |
|
546 "inj_on f A ==> y : f`A ==> f (the_inv_onto A f y) = y" |
|
547 apply (simp add: the_inv_onto_def) |
|
548 apply (rule the1I2) |
|
549 apply(blast dest: inj_onD) |
|
550 apply blast |
|
551 done |
|
552 |
|
553 lemma the_inv_onto_into: |
|
554 "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_onto A f x : B" |
|
555 apply (simp add: the_inv_onto_def) |
|
556 apply (rule the1I2) |
|
557 apply(blast dest: inj_onD) |
|
558 apply blast |
|
559 done |
|
560 |
|
561 lemma the_inv_onto_onto[simp]: |
|
562 "inj_on f A ==> the_inv_onto A f ` (f ` A) = A" |
|
563 by (fast intro:the_inv_onto_into the_inv_onto_f_f[symmetric]) |
|
564 |
|
565 lemma the_inv_onto_f_eq: |
|
566 "[| inj_on f A; f x = y; x : A |] ==> the_inv_onto A f y = x" |
|
567 apply (erule subst) |
|
568 apply (erule the_inv_onto_f_f, assumption) |
|
569 done |
|
570 |
|
571 lemma the_inv_onto_comp: |
|
572 "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==> |
|
573 the_inv_onto A (f o g) x = (the_inv_onto A g o the_inv_onto (g ` A) f) x" |
|
574 apply (rule the_inv_onto_f_eq) |
|
575 apply (fast intro: comp_inj_on) |
|
576 apply (simp add: f_the_inv_onto_f the_inv_onto_into) |
|
577 apply (simp add: the_inv_onto_into) |
|
578 done |
|
579 |
|
580 lemma inj_on_the_inv_onto: |
|
581 "inj_on f A \<Longrightarrow> inj_on (the_inv_onto A f) (f ` A)" |
|
582 by (auto intro: inj_onI simp: image_def the_inv_onto_f_f) |
|
583 |
|
584 lemma bij_betw_the_inv_onto: |
|
585 "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_onto A f) B A" |
|
586 by (auto simp add: bij_betw_def inj_on_the_inv_onto the_inv_onto_into) |
|
587 |
536 |
588 |
537 subsection {* Proof tool setup *} |
589 subsection {* Proof tool setup *} |
538 |
590 |
539 text {* simplifies terms of the form |
591 text {* simplifies terms of the form |
540 f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} |
592 f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} |