src/HOL/Library/Permutations.thy
 changeset 64543 6b13586ef1a2 parent 64284 f3b905b2eee2 child 64966 d53d7ca3303e
equal inserted replaced
64542:c7d76708379f 64543:6b13586ef1a2
`    29   assumes bp: "bij p"`
`    29   assumes bp: "bij p"`
`    30   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"`
`    30   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"`
`    31   using surj_f_inv_f[OF bij_is_surj[OF bp]]`
`    31   using surj_f_inv_f[OF bij_is_surj[OF bp]]`
`    32   by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])`
`    32   by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])`
`    33 `
`    33 `
`    34 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"`
`    34 lemma bij_swap_compose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"`
`    35 proof -`
`    35 proof -`
`    36   assume H: "bij p"`
`    36   assume H: "bij p"`
`    37   show ?thesis`
`    37   show ?thesis`
`    38     unfolding bij_swap_comp[OF H] bij_swap_iff`
`    38     unfolding bij_swap_comp[OF H] bij_swap_iff`
`    39     using H .`
`    39     using H .`
`   754   case (insert a F p)`
`   754   case (insert a F p)`
`   755   let ?r = "Fun.swap a (p a) id \<circ> p"`
`   755   let ?r = "Fun.swap a (p a) id \<circ> p"`
`   756   let ?q = "Fun.swap a (p a) id \<circ> ?r"`
`   756   let ?q = "Fun.swap a (p a) id \<circ> ?r"`
`   757   have raa: "?r a = a"`
`   757   have raa: "?r a = a"`
`   758     by (simp add: Fun.swap_def)`
`   758     by (simp add: Fun.swap_def)`
`   759   from bij_swap_ompose_bij[OF insert(4)]`
`   759   from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r"  .`
`   760   have br: "bij ?r"  .`
`       `
`   761 `
`       `
`   762   from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"`
`   760   from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"`
`   763     apply (clarsimp simp add: Fun.swap_def)`
`   761     by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))    `
`   764     apply (erule_tac x="x" in allE)`
`   762   from insert(3)[OF br th] have rp: "permutation ?r" .`
`   765     apply auto`
`       `
`   766     unfolding bij_iff`
`       `
`   767     apply metis`
`       `
`   768     done`
`       `
`   769   from insert(3)[OF br th]`
`       `
`   770   have rp: "permutation ?r" .`
`       `
`   771   have "permutation ?q"`
`   763   have "permutation ?q"`
`   772     by (simp add: permutation_compose permutation_swap_id rp)`
`   764     by (simp add: permutation_compose permutation_swap_id rp)`
`   773   then show ?case`
`   765   then show ?case`
`   774     by (simp add: o_assoc)`
`   766     by (simp add: o_assoc)`
`   775 qed`
`   767 qed`
`   924   fix y :: 'a`
`   916   fix y :: 'a`
`   925   from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x`
`   917   from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x`
`   926     using permutes_in_image[OF assms] by auto`
`   918     using permutes_in_image[OF assms] by auto`
`   927   have "count (mset (permute_list f xs)) y =`
`   919   have "count (mset (permute_list f xs)) y =`
`   928           card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"`
`   920           card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"`
`   929     by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)`
`   921     by (simp add: permute_list_def count_image_mset atLeast0LessThan)`
`   930   also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"`
`   922   also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"`
`   931     by auto`
`   923     by auto`
`   932   also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"`
`   924   also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"`
`   933     by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)`
`   925     by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj)`
`   934   also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card)`
`   926   also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card)`