# HG changeset patch
# User hoelzl
# Date 1422635381 -3600
# Node ID 4475b1a0141d682a02943d4e63221a1e41c281a4
# Parent  b0ac740fc5104707f40cee14a2102f387543e893
related permutations with bij functions

diff -r b0ac740fc510 -r 4475b1a0141d src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri Jan 30 17:35:03 2015 +0100
+++ b/src/HOL/Library/Permutations.thy	Fri Jan 30 17:29:41 2015 +0100
@@ -44,6 +44,13 @@
 lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
   unfolding permutes_def surj_def by metis
 
+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)
+   
+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
+  by auto (metis image_iff)+
+
 lemma permutes_inv_o:
   assumes pS: "p permutes S"
   shows "p \<circ> inv p = id"