src/HOL/Fun.thy
 changeset 39075 a18e5946d63c parent 39074 211e4f6aad63 child 39076 b3a9b6734663
1.1 --- a/src/HOL/Fun.thy	Thu Sep 02 10:36:45 2010 +0200
1.2 +++ b/src/HOL/Fun.thy	Thu Sep 02 10:45:51 2010 +0200
1.3 @@ -321,6 +321,11 @@
1.4    ultimately show ?thesis by(auto simp:bij_betw_def)
1.5  qed
1.7 +lemma bij_betw_combine:
1.8 +  assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
1.9 +  shows "bij_betw f (A \<union> C) (B \<union> D)"
1.10 +  using assms unfolding bij_betw_def inj_on_Un image_Un by auto
1.11 +
1.12  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
1.13  by (simp add: surj_range)
1.15 @@ -512,11 +517,11 @@
1.17  lemma inj_on_swap_iff [simp]:
1.18    assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
1.19 -proof
1.20 +proof
1.21    assume "inj_on (swap a b f) A"
1.22 -  with A have "inj_on (swap a b (swap a b f)) A"
1.23 -    by (iprover intro: inj_on_imp_inj_on_swap)
1.24 -  thus "inj_on f A" by simp
1.25 +  with A have "inj_on (swap a b (swap a b f)) A"
1.26 +    by (iprover intro: inj_on_imp_inj_on_swap)
1.27 +  thus "inj_on f A" by simp
1.28  next
1.29    assume "inj_on f A"
1.30    with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
1.31 @@ -529,18 +534,41 @@
1.32  done
1.34  lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
1.35 -proof
1.36 +proof
1.37    assume "surj (swap a b f)"
1.38 -  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
1.39 -  thus "surj f" by simp
1.40 +  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
1.41 +  thus "surj f" by simp
1.42  next
1.43    assume "surj f"
1.44 -  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
1.45 +  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
1.46  qed
1.48  lemma bij_swap_iff: "bij (swap a b f) = bij f"
1.49  by (simp add: bij_def)
1.51 +lemma bij_betw_swap:
1.52 +  assumes "bij_betw f A B" "x \<in> A" "y \<in> A"
1.53 +  shows "bij_betw (Fun.swap x y f) A B"
1.54 +proof (unfold bij_betw_def, intro conjI)
1.55 +  show "inj_on (Fun.swap x y f) A" using assms
1.56 +    by (intro inj_on_imp_inj_on_swap) (auto simp: bij_betw_def)
1.57 +  show "Fun.swap x y f ` A = B"
1.58 +  proof safe
1.59 +    fix z assume "z \<in> A"
1.60 +    then show "Fun.swap x y f z \<in> B"
1.61 +      using assms unfolding bij_betw_def
1.62 +      by (auto simp: image_iff Fun.swap_def
1.63 +               intro!: bexI[of _ "if z = x then y else if z = y then x else z"])
1.64 +  next
1.65 +    fix z assume "z \<in> B"
1.66 +    then obtain v where "v \<in> A" "z = f v" using assms unfolding bij_betw_def by auto
1.67 +    then show "z \<in> Fun.swap x y f ` A" unfolding image_iff
1.68 +      using assms
1.69 +      by (auto simp add: Fun.swap_def split: split_if_asm
1.70 +               intro!: bexI[of _ "if v = x then y else if v = y then x else v"])
1.71 +  qed
1.72 +qed
1.73 +
1.74  hide_const (open) swap