Permutation implies bij function
authorhoelzl
Thu Sep 02 10:45:51 2010 +0200 (2010-09-02)
changeset 39075a18e5946d63c
parent 39074 211e4f6aad63
child 39076 b3a9b6734663
Permutation implies bij function
src/HOL/Fun.thy
src/HOL/Library/Permutation.thy
     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.6  
     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.14  
    1.15 @@ -512,11 +517,11 @@
    1.16  
    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.33  
    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.47  
    1.48  lemma bij_swap_iff: "bij (swap a b f) = bij f"
    1.49  by (simp add: bij_def)
    1.50  
    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
    1.75  
    1.76  
     2.1 --- a/src/HOL/Library/Permutation.thy	Thu Sep 02 10:36:45 2010 +0200
     2.2 +++ b/src/HOL/Library/Permutation.thy	Thu Sep 02 10:45:51 2010 +0200
     2.3 @@ -183,4 +183,55 @@
     2.4  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
     2.5    by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
     2.6  
     2.7 +lemma permutation_Ex_bij:
     2.8 +  assumes "xs <~~> ys"
     2.9 +  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
    2.10 +using assms proof induct
    2.11 +  case Nil then show ?case unfolding bij_betw_def by simp
    2.12 +next
    2.13 +  case (swap y x l)
    2.14 +  show ?case
    2.15 +  proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
    2.16 +    show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
    2.17 +      by (rule bij_betw_swap) (auto simp: bij_betw_def)
    2.18 +    fix i assume "i < length(y#x#l)"
    2.19 +    show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
    2.20 +      by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
    2.21 +  qed
    2.22 +next
    2.23 +  case (Cons xs ys z)
    2.24 +  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
    2.25 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
    2.26 +  let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
    2.27 +  show ?case
    2.28 +  proof (intro exI[of _ ?f] allI conjI impI)
    2.29 +    have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
    2.30 +            "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
    2.31 +      by (simp_all add: lessThan_eq_Suc_image)
    2.32 +    show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
    2.33 +    proof (rule bij_betw_combine)
    2.34 +      show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
    2.35 +        using bij unfolding bij_betw_def
    2.36 +        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
    2.37 +    qed (auto simp: bij_betw_def)
    2.38 +    fix i assume "i < length (z#xs)"
    2.39 +    then show "(z # xs) ! i = (z # ys) ! (?f i)"
    2.40 +      using perm by (cases i) auto
    2.41 +  qed
    2.42 +next
    2.43 +  case (trans xs ys zs)
    2.44 +  then obtain f g where
    2.45 +    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
    2.46 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
    2.47 +  show ?case
    2.48 +  proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
    2.49 +    show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
    2.50 +      using bij by (rule bij_betw_trans)
    2.51 +    fix i assume "i < length xs"
    2.52 +    with bij have "f i < length ys" unfolding bij_betw_def by force
    2.53 +    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
    2.54 +      using trans(1,3)[THEN perm_length] perm by force
    2.55 +  qed
    2.56 +qed
    2.57 +
    2.58  end