src/HOL/Fun.thy
changeset 39075 a18e5946d63c
parent 39074 211e4f6aad63
child 39076 b3a9b6734663
equal deleted inserted replaced
39074:211e4f6aad63 39075:a18e5946d63c
   319     with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   319     with g[OF P] show "\<exists>b\<in>B. a = ?g b" by blast
   320   qed
   320   qed
   321   ultimately show ?thesis by(auto simp:bij_betw_def)
   321   ultimately show ?thesis by(auto simp:bij_betw_def)
   322 qed
   322 qed
   323 
   323 
       
   324 lemma bij_betw_combine:
       
   325   assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
       
   326   shows "bij_betw f (A \<union> C) (B \<union> D)"
       
   327   using assms unfolding bij_betw_def inj_on_Un image_Un by auto
       
   328 
   324 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   329 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   325 by (simp add: surj_range)
   330 by (simp add: surj_range)
   326 
   331 
   327 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   332 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   328 by (simp add: inj_on_def, blast)
   333 by (simp add: inj_on_def, blast)
   510   "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
   515   "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
   511 by (simp add: inj_on_def swap_def, blast)
   516 by (simp add: inj_on_def swap_def, blast)
   512 
   517 
   513 lemma inj_on_swap_iff [simp]:
   518 lemma inj_on_swap_iff [simp]:
   514   assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
   519   assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
   515 proof 
   520 proof
   516   assume "inj_on (swap a b f) A"
   521   assume "inj_on (swap a b f) A"
   517   with A have "inj_on (swap a b (swap a b f)) A" 
   522   with A have "inj_on (swap a b (swap a b f)) A"
   518     by (iprover intro: inj_on_imp_inj_on_swap) 
   523     by (iprover intro: inj_on_imp_inj_on_swap)
   519   thus "inj_on f A" by simp 
   524   thus "inj_on f A" by simp
   520 next
   525 next
   521   assume "inj_on f A"
   526   assume "inj_on f A"
   522   with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
   527   with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
   523 qed
   528 qed
   524 
   529 
   527 apply (case_tac "y = f b", blast)
   532 apply (case_tac "y = f b", blast)
   528 apply (case_tac "y = f a", auto)
   533 apply (case_tac "y = f a", auto)
   529 done
   534 done
   530 
   535 
   531 lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
   536 lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
   532 proof 
   537 proof
   533   assume "surj (swap a b f)"
   538   assume "surj (swap a b f)"
   534   hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap) 
   539   hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
   535   thus "surj f" by simp 
   540   thus "surj f" by simp
   536 next
   541 next
   537   assume "surj f"
   542   assume "surj f"
   538   thus "surj (swap a b f)" by (rule surj_imp_surj_swap) 
   543   thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
   539 qed
   544 qed
   540 
   545 
   541 lemma bij_swap_iff: "bij (swap a b f) = bij f"
   546 lemma bij_swap_iff: "bij (swap a b f) = bij f"
   542 by (simp add: bij_def)
   547 by (simp add: bij_def)
       
   548 
       
   549 lemma bij_betw_swap:
       
   550   assumes "bij_betw f A B" "x \<in> A" "y \<in> A"
       
   551   shows "bij_betw (Fun.swap x y f) A B"
       
   552 proof (unfold bij_betw_def, intro conjI)
       
   553   show "inj_on (Fun.swap x y f) A" using assms
       
   554     by (intro inj_on_imp_inj_on_swap) (auto simp: bij_betw_def)
       
   555   show "Fun.swap x y f ` A = B"
       
   556   proof safe
       
   557     fix z assume "z \<in> A"
       
   558     then show "Fun.swap x y f z \<in> B"
       
   559       using assms unfolding bij_betw_def
       
   560       by (auto simp: image_iff Fun.swap_def
       
   561                intro!: bexI[of _ "if z = x then y else if z = y then x else z"])
       
   562   next
       
   563     fix z assume "z \<in> B"
       
   564     then obtain v where "v \<in> A" "z = f v" using assms unfolding bij_betw_def by auto
       
   565     then show "z \<in> Fun.swap x y f ` A" unfolding image_iff
       
   566       using assms
       
   567       by (auto simp add: Fun.swap_def split: split_if_asm
       
   568                intro!: bexI[of _ "if v = x then y else if v = y then x else v"])
       
   569   qed
       
   570 qed
   543 
   571 
   544 hide_const (open) swap
   572 hide_const (open) swap
   545 
   573 
   546 
   574 
   547 subsection {* Inversion of injective functions *}
   575 subsection {* Inversion of injective functions *}