diff -r c7d76708379f -r 6b13586ef1a2 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Thu Dec 08 15:21:18 2016 +0100 +++ b/src/HOL/Library/Permutations.thy Thu Dec 08 17:22:51 2016 +0100 @@ -31,7 +31,7 @@ using surj_f_inv_f[OF bij_is_surj[OF bp]] by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp]) -lemma bij_swap_ompose_bij: "bij p \ bij (Fun.swap a b id \ p)" +lemma bij_swap_compose_bij: "bij p \ bij (Fun.swap a b id \ p)" proof - assume H: "bij p" show ?thesis @@ -756,18 +756,10 @@ let ?q = "Fun.swap a (p a) id \ ?r" have raa: "?r a = a" by (simp add: Fun.swap_def) - from bij_swap_ompose_bij[OF insert(4)] - have br: "bij ?r" . - + from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r" . from insert raa have th: "\x. x \ F \ ?r x = x" - apply (clarsimp simp add: Fun.swap_def) - apply (erule_tac x="x" in allE) - apply auto - unfolding bij_iff - apply metis - done - from insert(3)[OF br th] - have rp: "permutation ?r" . + by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) + from insert(3)[OF br th] have rp: "permutation ?r" . have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp) then show ?case @@ -926,7 +918,7 @@ using permutes_in_image[OF assms] by auto have "count (mset (permute_list f xs)) y = card ((\i. xs ! f i) -` {y} \ {..i. xs ! f i) -` {y} \ {.. y = xs ! i}" by auto also from assms have "card \ = card {i. i < length xs \ y = xs ! i}"