src/HOL/Library/Permutation.thy
 changeset 39075 a18e5946d63c parent 36903 489c1fbbb028 child 39078 39f8f6d1eb74
```     1.1 --- a/src/HOL/Library/Permutation.thy	Thu Sep 02 10:36:45 2010 +0200
1.2 +++ b/src/HOL/Library/Permutation.thy	Thu Sep 02 10:45:51 2010 +0200
1.3 @@ -183,4 +183,55 @@
1.4  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
1.5    by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
1.6
1.7 +lemma permutation_Ex_bij:
1.8 +  assumes "xs <~~> ys"
1.9 +  shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
1.10 +using assms proof induct
1.11 +  case Nil then show ?case unfolding bij_betw_def by simp
1.12 +next
1.13 +  case (swap y x l)
1.14 +  show ?case
1.15 +  proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
1.16 +    show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
1.17 +      by (rule bij_betw_swap) (auto simp: bij_betw_def)
1.18 +    fix i assume "i < length(y#x#l)"
1.19 +    show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
1.20 +      by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
1.21 +  qed
1.22 +next
1.23 +  case (Cons xs ys z)
1.24 +  then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
1.25 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
1.26 +  let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
1.27 +  show ?case
1.28 +  proof (intro exI[of _ ?f] allI conjI impI)
1.29 +    have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
1.30 +            "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
1.31 +      by (simp_all add: lessThan_eq_Suc_image)
1.32 +    show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
1.33 +    proof (rule bij_betw_combine)
1.34 +      show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
1.35 +        using bij unfolding bij_betw_def
1.36 +        by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
1.37 +    qed (auto simp: bij_betw_def)
1.38 +    fix i assume "i < length (z#xs)"
1.39 +    then show "(z # xs) ! i = (z # ys) ! (?f i)"
1.40 +      using perm by (cases i) auto
1.41 +  qed
1.42 +next
1.43 +  case (trans xs ys zs)
1.44 +  then obtain f g where
1.45 +    bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
1.46 +    perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
1.47 +  show ?case
1.48 +  proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
1.49 +    show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
1.50 +      using bij by (rule bij_betw_trans)
1.51 +    fix i assume "i < length xs"
1.52 +    with bij have "f i < length ys" unfolding bij_betw_def by force
1.53 +    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
1.54 +      using trans(1,3)[THEN perm_length] perm by force
1.55 +  qed
1.56 +qed
1.57 +
1.58  end
```