--- a/src/HOL/Fun.thy Thu Sep 02 10:36:45 2010 +0200
+++ b/src/HOL/Fun.thy Thu Sep 02 10:45:51 2010 +0200
@@ -321,6 +321,11 @@
ultimately show ?thesis by(auto simp:bij_betw_def)
qed
+lemma bij_betw_combine:
+ assumes "bij_betw f A B" "bij_betw f C D" "B \<inter> D = {}"
+ shows "bij_betw f (A \<union> C) (B \<union> D)"
+ using assms unfolding bij_betw_def inj_on_Un image_Un by auto
+
lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
by (simp add: surj_range)
@@ -512,11 +517,11 @@
lemma inj_on_swap_iff [simp]:
assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
-proof
+proof
assume "inj_on (swap a b f) A"
- with A have "inj_on (swap a b (swap a b f)) A"
- by (iprover intro: inj_on_imp_inj_on_swap)
- thus "inj_on f A" by simp
+ with A have "inj_on (swap a b (swap a b f)) A"
+ by (iprover intro: inj_on_imp_inj_on_swap)
+ thus "inj_on f A" by simp
next
assume "inj_on f A"
with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
@@ -529,18 +534,41 @@
done
lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
-proof
+proof
assume "surj (swap a b f)"
- hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
- thus "surj f" by simp
+ hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
+ thus "surj f" by simp
next
assume "surj f"
- thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
+ thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
qed
lemma bij_swap_iff: "bij (swap a b f) = bij f"
by (simp add: bij_def)
+lemma bij_betw_swap:
+ assumes "bij_betw f A B" "x \<in> A" "y \<in> A"
+ shows "bij_betw (Fun.swap x y f) A B"
+proof (unfold bij_betw_def, intro conjI)
+ show "inj_on (Fun.swap x y f) A" using assms
+ by (intro inj_on_imp_inj_on_swap) (auto simp: bij_betw_def)
+ show "Fun.swap x y f ` A = B"
+ proof safe
+ fix z assume "z \<in> A"
+ then show "Fun.swap x y f z \<in> B"
+ using assms unfolding bij_betw_def
+ by (auto simp: image_iff Fun.swap_def
+ intro!: bexI[of _ "if z = x then y else if z = y then x else z"])
+ next
+ fix z assume "z \<in> B"
+ then obtain v where "v \<in> A" "z = f v" using assms unfolding bij_betw_def by auto
+ then show "z \<in> Fun.swap x y f ` A" unfolding image_iff
+ using assms
+ by (auto simp add: Fun.swap_def split: split_if_asm
+ intro!: bexI[of _ "if v = x then y else if v = y then x else v"])
+ qed
+qed
+
hide_const (open) swap
--- a/src/HOL/Library/Permutation.thy Thu Sep 02 10:36:45 2010 +0200
+++ b/src/HOL/Library/Permutation.thy Thu Sep 02 10:45:51 2010 +0200
@@ -183,4 +183,55 @@
lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
+lemma permutation_Ex_bij:
+ assumes "xs <~~> ys"
+ shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
+using assms proof induct
+ case Nil then show ?case unfolding bij_betw_def by simp
+next
+ case (swap y x l)
+ show ?case
+ proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
+ show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
+ by (rule bij_betw_swap) (auto simp: bij_betw_def)
+ fix i assume "i < length(y#x#l)"
+ show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
+ by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
+ qed
+next
+ case (Cons xs ys z)
+ then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
+ perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
+ let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
+ show ?case
+ proof (intro exI[of _ ?f] allI conjI impI)
+ have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
+ "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
+ by (simp_all add: lessThan_eq_Suc_image)
+ show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
+ proof (rule bij_betw_combine)
+ show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
+ using bij unfolding bij_betw_def
+ by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
+ qed (auto simp: bij_betw_def)
+ fix i assume "i < length (z#xs)"
+ then show "(z # xs) ! i = (z # ys) ! (?f i)"
+ using perm by (cases i) auto
+ qed
+next
+ case (trans xs ys zs)
+ then obtain f g where
+ bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
+ perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
+ show ?case
+ proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
+ show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
+ using bij by (rule bij_betw_trans)
+ fix i assume "i < length xs"
+ with bij have "f i < length ys" unfolding bij_betw_def by force
+ with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
+ using trans(1,3)[THEN perm_length] perm by force
+ qed
+qed
+
end