494 lemma bij_swap_iff: "bij (swap a b f) = bij f" |
494 lemma bij_swap_iff: "bij (swap a b f) = bij f" |
495 by (simp add: bij_def) |
495 by (simp add: bij_def) |
496 |
496 |
497 hide (open) const swap |
497 hide (open) const swap |
498 |
498 |
|
499 |
|
500 subsection {* Inversion of injective functions *} |
|
501 |
|
502 definition inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)" where |
|
503 "inv f y = (THE x. f x = y)" |
|
504 |
|
505 lemma inv_f_f: |
|
506 assumes "inj f" |
|
507 shows "inv f (f x) = x" |
|
508 proof - |
|
509 from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)" |
|
510 by (simp only: inj_eq) |
|
511 also have "... = x" by (rule the_eq_trivial) |
|
512 finally show ?thesis by (unfold inv_def) |
|
513 qed |
|
514 |
|
515 lemma f_inv_f: |
|
516 assumes "inj f" |
|
517 and "y \<in> range f" |
|
518 shows "f (inv f y) = y" |
|
519 proof (unfold inv_def) |
|
520 from `y \<in> range f` obtain x where "y = f x" .. |
|
521 then have "f x = y" .. |
|
522 then show "f (THE x. f x = y) = y" |
|
523 proof (rule theI) |
|
524 fix x' assume "f x' = y" |
|
525 with `f x = y` have "f x' = f x" by simp |
|
526 with `inj f` show "x' = x" by (rule injD) |
|
527 qed |
|
528 qed |
|
529 |
|
530 hide (open) const inv |
|
531 |
|
532 |
499 subsection {* Proof tool setup *} |
533 subsection {* Proof tool setup *} |
500 |
534 |
501 text {* simplifies terms of the form |
535 text {* simplifies terms of the form |
502 f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} |
536 f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} |
503 |
537 |