--- a/src/HOL/Library/Permutations.thy Sat Jun 27 20:26:33 2015 +0200
+++ b/src/HOL/Library/Permutations.thy Sun Jun 28 14:30:53 2015 +0200
@@ -44,8 +44,11 @@
lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
unfolding permutes_def surj_def by metis
+lemma permutes_bij: "p permutes s \<Longrightarrow> bij p"
+unfolding bij_def by (metis permutes_inj permutes_surj)
+
lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S"
- by (metis UNIV_I bij_betw_def permutes_image permutes_inj subsetI subset_inj_on)
+by (metis UNIV_I bij_betw_subset permutes_bij permutes_image subsetI)
lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S"
unfolding permutes_def bij_betw_def inj_on_def