src/HOL/Library/Permutations.thy
changeset 32989 c28279b29ff1
parent 32960 69916a850301
parent 32988 d1d4d7a08a66
child 33057 764547b68538
     1.1 --- a/src/HOL/Library/Permutations.thy	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -5,11 +5,9 @@
     1.4  header {* Permutations, both general and specifically on finite sets.*}
     1.5  
     1.6  theory Permutations
     1.7 -imports Finite_Cartesian_Product Parity Fact Main
     1.8 +imports Finite_Cartesian_Product Parity Fact
     1.9  begin
    1.10  
    1.11 -  (* Why should I import Main just to solve the Typerep problem! *)
    1.12 -
    1.13  definition permutes (infixr "permutes" 41) where
    1.14    "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
    1.15  
    1.16 @@ -85,7 +83,7 @@
    1.17    unfolding permutes_def by simp
    1.18  
    1.19  lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
    1.20 -  unfolding permutes_def inv_def apply auto
    1.21 +  unfolding permutes_def inv_onto_def apply auto
    1.22    apply (erule allE[where x=y])
    1.23    apply (erule allE[where x=y])
    1.24    apply (rule someI_ex) apply blast
    1.25 @@ -95,10 +93,11 @@
    1.26    done
    1.27  
    1.28  lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
    1.29 -  unfolding permutes_def swap_def fun_upd_def  apply auto apply metis done
    1.30 +  unfolding permutes_def swap_def fun_upd_def  by auto metis
    1.31  
    1.32 -lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    1.33 -apply (simp add: Ball_def permutes_def Diff_iff) by metis
    1.34 +lemma permutes_superset:
    1.35 +  "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
    1.36 +by (simp add: Ball_def permutes_def Diff_iff) metis
    1.37  
    1.38  (* ------------------------------------------------------------------------- *)
    1.39  (* Group properties.                                                         *)