src/HOL/Library/Permutations.thy
 changeset 64284 f3b905b2eee2 parent 64267 b9a1486e79be child 64543 6b13586ef1a2
equal inserted replaced
64283:979cdfdf7a79 64284:f3b905b2eee2
`    20 `
`    20 `
`    21 lemma swap_id_eq:`
`    21 lemma swap_id_eq:`
`    22   "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"`
`    22   "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"`
`    23   by (simp add: Fun.swap_def)`
`    23   by (simp add: Fun.swap_def)`
`    24 `
`    24 `
`       `
`    25 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"`
`       `
`    26   using surj_f_inv_f[of p] by (auto simp add: bij_def)`
`       `
`    27 `
`       `
`    28 lemma bij_swap_comp:`
`       `
`    29   assumes bp: "bij 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]]`
`       `
`    32   by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])`
`       `
`    33 `
`       `
`    34 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"`
`       `
`    35 proof -`
`       `
`    36   assume H: "bij p"`
`       `
`    37   show ?thesis`
`       `
`    38     unfolding bij_swap_comp[OF H] bij_swap_iff`
`       `
`    39     using H .`
`       `
`    40 qed`
`       `
`    41 `
`    25 `
`    42 `
`    26 subsection \<open>Basic consequences of the definition\<close>`
`    43 subsection \<open>Basic consequences of the definition\<close>`
`    27 `
`    44 `
`    28 definition permutes  (infixr "permutes" 41)`
`    45 definition permutes  (infixr "permutes" 41)`
`    29   where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"`
`    46   where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"`
`    30 `
`    47 `
`    31 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"`
`    48 lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"`
`    32   unfolding permutes_def by metis`
`    49   unfolding permutes_def by metis`
`    33   `
`    50 `
`    34 lemma permutes_not_in:`
`    51 lemma permutes_not_in:`
`    35   assumes "f permutes S" "x \<notin> S" shows "f x = x"`
`    52   assumes "f permutes S" "x \<notin> S" shows "f x = x"`
`    36   using assms by (auto simp: permutes_def)`
`    53   using assms by (auto simp: permutes_def)`
`    37 `
`    54 `
`    38 lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"`
`    55 lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"`
`   105 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"`
`   122 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"`
`   106   by (simp add: Ball_def permutes_def) metis`
`   123   by (simp add: Ball_def permutes_def) metis`
`   107 `
`   124 `
`   108 (* Next three lemmas contributed by Lukas Bulwahn *)`
`   125 (* Next three lemmas contributed by Lukas Bulwahn *)`
`   109 lemma permutes_bij_inv_into:`
`   126 lemma permutes_bij_inv_into:`
`   110   fixes A :: "'a set" and B :: "'b set" `
`   127   fixes A :: "'a set" and B :: "'b set"`
`   111   assumes "p permutes A"`
`   128   assumes "p permutes A"`
`   112   assumes "bij_betw f A B"`
`   129   assumes "bij_betw f A B"`
`   113   shows "(\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) permutes B"`
`   130   shows "(\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) permutes B"`
`   114 proof (rule bij_imp_permutes)`
`   131 proof (rule bij_imp_permutes)`
`   115   have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A"`
`   132   have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A"`
`   165   assumes pS: "p permutes S"`
`   182   assumes pS: "p permutes S"`
`   166   shows "inv (inv p) = p"`
`   183   shows "inv (inv p) = p"`
`   167   unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]`
`   184   unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]`
`   168   by blast`
`   185   by blast`
`   169 `
`   186 `
`   170 lemma permutes_invI: `
`   187 lemma permutes_invI:`
`   171   assumes perm: "p permutes S"`
`   188   assumes perm: "p permutes S"`
`   172       and inv:  "\<And>x. x \<in> S \<Longrightarrow> p' (p x) = x" `
`   189       and inv:  "\<And>x. x \<in> S \<Longrightarrow> p' (p x) = x"`
`   173       and outside: "\<And>x. x \<notin> S \<Longrightarrow> p' x = x"`
`   190       and outside: "\<And>x. x \<notin> S \<Longrightarrow> p' x = x"`
`   174   shows   "inv p = p'"`
`   191   shows   "inv p = p'"`
`   175 proof`
`   192 proof`
`   176   fix x show "inv p x = p' x"`
`   193   fix x show "inv p x = p' x"`
`   177   proof (cases "x \<in> S")`
`   194   proof (cases "x \<in> S")`
`   178     assume [simp]: "x \<in> S"`
`   195     assume [simp]: "x \<in> S"`
`   179     from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses)`
`   196     from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses)`
`   180     also from permutes_inv[OF perm] `
`   197     also from permutes_inv[OF perm]`
`   181       have "\<dots> = inv p x" by (subst inv) (simp_all add: permutes_in_image)`
`   198       have "\<dots> = inv p x" by (subst inv) (simp_all add: permutes_in_image)`
`   182     finally show "inv p x = p' x" ..`
`   199     finally show "inv p x = p' x" ..`
`   183   qed (insert permutes_inv[OF perm], simp_all add: outside permutes_not_in)`
`   200   qed (insert permutes_inv[OF perm], simp_all add: outside permutes_not_in)`
`   184 qed`
`   201 qed`
`   185 `
`   202 `
`   186 lemma permutes_vimage: "f permutes A \<Longrightarrow> f -` A = A"`
`   203 lemma permutes_vimage: "f permutes A \<Longrightarrow> f -` A = A"`
`   187   by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])  `
`   204   by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])`
`   188 `
`   205 `
`   189 `
`   206 `
`   190 subsection \<open>The number of permutations on a finite set\<close>`
`   207 subsection \<open>The number of permutations on a finite set\<close>`
`   191 `
`   208 `
`   192 lemma permutes_insert_lemma:`
`   209 lemma permutes_insert_lemma:`
`   327 qed`
`   344 qed`
`   328 `
`   345 `
`   329 lemma finite_permutations:`
`   346 lemma finite_permutations:`
`   330   assumes fS: "finite S"`
`   347   assumes fS: "finite S"`
`   331   shows "finite {p. p permutes S}"`
`   348   shows "finite {p. p permutes S}"`
`   332   using card_permutations[OF refl fS] `
`   349   using card_permutations[OF refl fS]`
`   333   by (auto intro: card_ge_0_finite)`
`   350   by (auto intro: card_ge_0_finite)`
`   334 `
`   351 `
`   335 `
`   352 `
`   336 subsection \<open>Permutations of index set for iterated operations\<close>`
`   353 subsection \<open>Permutations of index set for iterated operations\<close>`
`   337 `
`   354 `
`   722       by (auto simp add: Fun.swap_def)`
`   739       by (auto simp add: Fun.swap_def)`
`   723     from finite_subset[OF th fS] show ?case  .`
`   740     from finite_subset[OF th fS] show ?case  .`
`   724   qed`
`   741   qed`
`   725 qed`
`   742 qed`
`   726 `
`   743 `
`   744 lemma permutation_lemma:`
`   744 lemma permutation_lemma:`
`   745   assumes fS: "finite S"`
`   745   assumes fS: "finite S"`
`   746     and p: "bij p"`
`   746     and p: "bij p"`
`   747     and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"`
`   747     and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"`
`   748   shows "permutation p"`
`   748   shows "permutation p"`
`   879   by (simp add: sign_def evenperm_swap)`
`   879   by (simp add: sign_def evenperm_swap)`
`   880 `
`   880 `
`   881 lemma sign_idempotent: "sign p * sign p = 1"`
`   881 lemma sign_idempotent: "sign p * sign p = 1"`
`   882   by (simp add: sign_def)`
`   882   by (simp add: sign_def)`
`   883 `
`   883 `
`   884  `
`   884 `
`   885 subsection \<open>Permuting a list\<close>`
`   885 subsection \<open>Permuting a list\<close>`
`   886 `
`   886 `
`   887 text \<open>This function permutes a list by applying a permutation to the indices.\<close>`
`   887 text \<open>This function permutes a list by applying a permutation to the indices.\<close>`
`   888 `
`   888 `
`   889 definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where`
`   889 definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where`
`   890   "permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]"`
`   890   "permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]"`
`   891 `
`   891 `
`   892 lemma permute_list_map: `
`   892 lemma permute_list_map:`
`   893   assumes "f permutes {..<length xs}"`
`   893   assumes "f permutes {..<length xs}"`
`   894   shows   "permute_list f (map g xs) = map g (permute_list f xs)"`
`   894   shows   "permute_list f (map g xs) = map g (permute_list f xs)"`
`   895   using permutes_in_image[OF assms] by (auto simp: permute_list_def)`
`   895   using permutes_in_image[OF assms] by (auto simp: permute_list_def)`
`   896 `
`   896 `
`   897 lemma permute_list_nth:`
`   897 lemma permute_list_nth:`
`   898   assumes "f permutes {..<length xs}" "i < length xs"`
`   898   assumes "f permutes {..<length xs}" "i < length xs"`
`   899   shows   "permute_list f xs ! i = xs ! f i"`
`   899   shows   "permute_list f xs ! i = xs ! f i"`
`   900   using permutes_in_image[OF assms(1)] assms(2) `
`   900   using permutes_in_image[OF assms(1)] assms(2)`
`   901   by (simp add: permute_list_def)`
`   901   by (simp add: permute_list_def)`
`   902 `
`   902 `
`   903 lemma permute_list_Nil [simp]: "permute_list f [] = []"`
`   903 lemma permute_list_Nil [simp]: "permute_list f [] = []"`
`   904   by (simp add: permute_list_def)`
`   904   by (simp add: permute_list_def)`
`   905 `
`   905 `
`   906 lemma length_permute_list [simp]: "length (permute_list f xs) = length xs"`
`   906 lemma length_permute_list [simp]: "length (permute_list f xs) = length xs"`
`   907   by (simp add: permute_list_def)`
`   907   by (simp add: permute_list_def)`
`   908 `
`   908 `
`   909 lemma permute_list_compose: `
`   909 lemma permute_list_compose:`
`   910   assumes "g permutes {..<length xs}"`
`   910   assumes "g permutes {..<length xs}"`
`   911   shows   "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)"`
`   911   shows   "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)"`
`   912   using assms[THEN permutes_in_image] by (auto simp add: permute_list_def)`
`   912   using assms[THEN permutes_in_image] by (auto simp add: permute_list_def)`
`   913 `
`   913 `
`   914 lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs"`
`   914 lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs"`
`   922   shows   "mset (permute_list f xs) = mset xs"`
`   922   shows   "mset (permute_list f xs) = mset xs"`
`   923 proof (rule multiset_eqI)`
`   923 proof (rule multiset_eqI)`
`   924   fix y :: 'a`
`   924   fix y :: 'a`
`   925   from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x`
`   925   from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x`
`   926     using permutes_in_image[OF assms] by auto`
`   926     using permutes_in_image[OF assms] by auto`
`   927   have "count (mset (permute_list f xs)) y = `
`   927   have "count (mset (permute_list f xs)) y =`
`   928           card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"`
`   928           card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"`
`   929     by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)`
`   929     by (simp add: permute_list_def mset_map 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}"`
`   930   also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"`
`   931     by auto`
`   931     by auto`
`   932   also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"`
`   932   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)`
`   933     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)`
`   934   also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card)`
`   935   finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp`
`   935   finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp`
`   936 qed`
`   936 qed`
`   937 `
`   937 `
`   938 lemma set_permute_list [simp]:                   `
`   938 lemma set_permute_list [simp]:`
`   939   assumes "f permutes {..<length xs}"`
`   939   assumes "f permutes {..<length xs}"`
`   940   shows   "set (permute_list f xs) = set xs"`
`   940   shows   "set (permute_list f xs) = set xs"`
`   941   by (rule mset_eq_setD[OF mset_permute_list]) fact`
`   941   by (rule mset_eq_setD[OF mset_permute_list]) fact`
`   942 `
`   942 `
`   943 lemma distinct_permute_list [simp]:`
`   943 lemma distinct_permute_list [simp]:`
`   944   assumes "f permutes {..<length xs}"`
`   944   assumes "f permutes {..<length xs}"`
`   945   shows   "distinct (permute_list f xs) = distinct xs"`
`   945   shows   "distinct (permute_list f xs) = distinct xs"`
`   946   by (simp add: distinct_count_atmost_1 assms)`
`   946   by (simp add: distinct_count_atmost_1 assms)`
`   947 `
`   947 `
`   948 lemma permute_list_zip: `
`   948 lemma permute_list_zip:`
`   949   assumes "f permutes A" "A = {..<length xs}"`
`   949   assumes "f permutes A" "A = {..<length xs}"`
`   950   assumes [simp]: "length xs = length ys"`
`   950   assumes [simp]: "length xs = length ys"`
`   951   shows   "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)"`
`   951   shows   "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)"`
`   952 proof -`
`   952 proof -`
`   953   from permutes_in_image[OF assms(1)] assms(2)`
`   953   from permutes_in_image[OF assms(1)] assms(2)`
`   959   also have "\<dots> = zip (permute_list f xs) (permute_list f ys)"`
`   959   also have "\<dots> = zip (permute_list f xs) (permute_list f ys)"`
`   960     by (simp_all add: permute_list_def zip_map_map)`
`   960     by (simp_all add: permute_list_def zip_map_map)`
`   961   finally show ?thesis .`
`   961   finally show ?thesis .`
`   962 qed`
`   962 qed`
`   963 `
`   963 `
`   964 lemma map_of_permute: `
`   964 lemma map_of_permute:`
`   965   assumes "\<sigma> permutes fst ` set xs"`
`   965   assumes "\<sigma> permutes fst ` set xs"`
`   966   shows   "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)")`
`   966   shows   "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)")`
`   967 proof`
`   967 proof`
`   968   fix x`
`   968   fix x`
`   969   from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj)`
`   969   from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj)`
`   991   proof cases`
`   991   proof cases`
`   992     assume "f x = b"`
`   992     assume "f x = b"`
`   993     from this have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \<in> F. f a = f x})"`
`   993     from this have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \<in> F. f a = f x})"`
`   994       using insert.hyps by auto`
`   994       using insert.hyps by auto`
`   995     also have "\<dots> = card (insert x {a \<in> F. f a = f x})"`
`   995     also have "\<dots> = card (insert x {a \<in> F. f a = f x})"`
`   996       using insert.hyps(1,2) by simp  `
`   996       using insert.hyps(1,2) by simp`
`   997     also have "card (insert x {a \<in> F. f a = f x}) = card {a \<in> insert x F. f a = b}"`
`   997     also have "card (insert x {a \<in> F. f a = f x}) = card {a \<in> insert x F. f a = b}"`
`   998       using \<open>f x = b\<close> by (auto intro: arg_cong[where f="card"])`
`   998       using \<open>f x = b\<close> by (auto intro: arg_cong[where f="card"])`
`   999     finally show ?thesis using insert by auto`
`   999     finally show ?thesis using insert by auto`
`  1000   next`
`  1000   next`
`  1001     assume A: "f x \<noteq> b"`
`  1001     assume A: "f x \<noteq> b"`
`  1002     hence "{a \<in> F. f a = b} = {a \<in> insert x F. f a = b}" by auto`
`  1002     hence "{a \<in> F. f a = b} = {a \<in> insert x F. f a = b}" by auto`
`  1003     with insert A show ?thesis by simp`
`  1003     with insert A show ?thesis by simp`
`  1004   qed`
`  1004   qed`
`  1005 qed`
`  1005 qed`
`  1006   `
`  1006 `
`  1007 (* Prove image_mset_eq_implies_permutes *)`
`  1007 (* Prove image_mset_eq_implies_permutes *)`
`  1008 lemma image_mset_eq_implies_permutes:`
`  1008 lemma image_mset_eq_implies_permutes:`
`  1009   fixes f :: "'a \<Rightarrow> 'b"`
`  1009   fixes f :: "'a \<Rightarrow> 'b"`
`  1010   assumes "finite A"`
`  1010   assumes "finite A"`
`  1011   assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)"`
`  1011   assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)"`
`  1315 `
`  1315 `
`  1316 `
`  1316 `
`  1317 subsection \<open>Constructing permutations from association lists\<close>`
`  1317 subsection \<open>Constructing permutations from association lists\<close>`
`  1318 `
`  1318 `
`  1319 definition list_permutes where`
`  1319 definition list_permutes where`
`  1320   "list_permutes xs A \<longleftrightarrow> set (map fst xs) \<subseteq> A \<and> set (map snd xs) = set (map fst xs) \<and> `
`  1320   "list_permutes xs A \<longleftrightarrow> set (map fst xs) \<subseteq> A \<and> set (map snd xs) = set (map fst xs) \<and>`
`  1321      distinct (map fst xs) \<and> distinct (map snd xs)"`
`  1321      distinct (map fst xs) \<and> distinct (map snd xs)"`
`  1322 `
`  1322 `
`  1323 lemma list_permutesI [simp]:`
`  1323 lemma list_permutesI [simp]:`
`  1324   assumes "set (map fst xs) \<subseteq> A" "set (map snd xs) = set (map fst xs)" "distinct (map fst xs)"`
`  1324   assumes "set (map fst xs) \<subseteq> A" "set (map snd xs) = set (map fst xs)" "distinct (map fst xs)"`
`  1325   shows   "list_permutes xs A"`
`  1325   shows   "list_permutes xs A"`
`  1347   assumes "distinct (map snd xs)"`
`  1347   assumes "distinct (map snd xs)"`
`  1348   shows   "inj_on (map_of xs) (set (map fst xs))"`
`  1348   shows   "inj_on (map_of xs) (set (map fst xs))"`
`  1349 proof (rule inj_onI)`
`  1349 proof (rule inj_onI)`
`  1350   fix x y assume xy: "x \<in> set (map fst xs)" "y \<in> set (map fst xs)"`
`  1350   fix x y assume xy: "x \<in> set (map fst xs)" "y \<in> set (map fst xs)"`
`  1351   assume eq: "map_of xs x = map_of xs y"`
`  1351   assume eq: "map_of xs x = map_of xs y"`
`  1352   from xy obtain x' y' `
`  1352   from xy obtain x' y'`
`  1353     where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'" `
`  1353     where x'y': "map_of xs x = Some x'" "map_of xs y = Some y'"`
`  1354     by (cases "map_of xs x"; cases "map_of xs y")`
`  1354     by (cases "map_of xs x"; cases "map_of xs y")`
`  1355        (simp_all add: map_of_eq_None_iff)`
`  1355        (simp_all add: map_of_eq_None_iff)`
`  1356   moreover from x'y' have *: "(x,x') \<in> set xs" "(y,y') \<in> set xs"`
`  1356   moreover from x'y' have *: "(x,x') \<in> set xs" "(y,y') \<in> set xs"`
`  1357     by (force dest: map_of_SomeD)+`
`  1357     by (force dest: map_of_SomeD)+`
`  1358   moreover from * eq x'y' have "x' = y'" by simp`
`  1358   moreover from * eq x'y' have "x' = y'" by simp`
`  1396   finally have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))"`
`  1396   finally have "bij_betw ?f (set (map fst xs)) (?f ` set (map fst xs))"`
`  1397     by (rule inj_on_imp_bij_betw)`
`  1397     by (rule inj_on_imp_bij_betw)`
`  1398   also from assms have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)"`
`  1398   also from assms have "?f ` set (map fst xs) = (the \<circ> map_of xs) ` set (map fst xs)"`
`  1399     by (intro image_cong refl)`
`  1399     by (intro image_cong refl)`
`  1400        (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)`
`  1400        (auto simp: permutation_of_list_def map_of_eq_None_iff split: option.splits)`
`  1401   also from assms have "\<dots> = set (map fst xs)" `
`  1401   also from assms have "\<dots> = set (map fst xs)"`
`  1402     by (subst image_map_of') (simp_all add: list_permutes_def)`
`  1402     by (subst image_map_of') (simp_all add: list_permutes_def)`
`  1403   finally show "bij_betw ?f (set (map fst xs)) (set (map fst xs))" .`
`  1403   finally show "bij_betw ?f (set (map fst xs)) (set (map fst xs))" .`
`  1404 qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+`
`  1404 qed (force simp: permutation_of_list_def dest!: map_of_SomeD split: option.splits)+`
`  1405 `
`  1405 `
`  1406 lemma eval_permutation_of_list [simp]:`
`  1406 lemma eval_permutation_of_list [simp]:`