src/HOL/Library/Permutation.thy
 changeset 39075 a18e5946d63c parent 36903 489c1fbbb028 child 39078 39f8f6d1eb74
equal inserted replaced
`   181   done`
`   181   done`
`   182 `
`   182 `
`   183 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"`
`   183 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"`
`   184   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)`
`   184   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)`
`   185 `
`   185 `
`       `
`   186 lemma permutation_Ex_bij:`
`       `
`   187   assumes "xs <~~> ys"`
`       `
`   188   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"`
`       `
`   189 using assms proof induct`
`       `
`   190   case Nil then show ?case unfolding bij_betw_def by simp`
`       `
`   191 next`
`       `
`   192   case (swap y x l)`
`       `
`   193   show ?case`
`       `
`   194   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)`
`       `
`   195     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"`
`       `
`   196       by (rule bij_betw_swap) (auto simp: bij_betw_def)`
`       `
`   197     fix i assume "i < length(y#x#l)"`
`       `
`   198     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"`
`       `
`   199       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)`
`       `
`   200   qed`
`       `
`   201 next`
`       `
`   202   case (Cons xs ys z)`
`       `
`   203   then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and`
`       `
`   204     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast`
`       `
`   205   let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"`
`       `
`   206   show ?case`
`       `
`   207   proof (intro exI[of _ ?f] allI conjI impI)`
`       `
`   208     have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"`
`       `
`   209             "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"`
`       `
`   210       by (simp_all add: lessThan_eq_Suc_image)`
`       `
`   211     show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *`
`       `
`   212     proof (rule bij_betw_combine)`
`       `
`   213       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"`
`       `
`   214         using bij unfolding bij_betw_def`
`       `
`   215         by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)`
`       `
`   216     qed (auto simp: bij_betw_def)`
`       `
`   217     fix i assume "i < length (z#xs)"`
`       `
`   218     then show "(z # xs) ! i = (z # ys) ! (?f i)"`
`       `
`   219       using perm by (cases i) auto`
`       `
`   220   qed`
`       `
`   221 next`
`       `
`   222   case (trans xs ys zs)`
`       `
`   223   then obtain f g where`
`       `
`   224     bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and`
`       `
`   225     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast`
`       `
`   226   show ?case`
`       `
`   227   proof (intro exI[of _ "g\<circ>f"] conjI allI impI)`
`       `
`   228     show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"`
`       `
`   229       using bij by (rule bij_betw_trans)`
`       `
`   230     fix i assume "i < length xs"`
`       `
`   231     with bij have "f i < length ys" unfolding bij_betw_def by force`
`       `
`   232     with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"`
`       `
`   233       using trans(1,3)[THEN perm_length] perm by force`
`       `
`   234   qed`
`       `
`   235 qed`
`       `
`   236 `
`   186 end`
`   237 end`