src/HOL/Library/Permutations.thy
changeset 64284 f3b905b2eee2
parent 64267 b9a1486e79be
child 64543 6b13586ef1a2
equal deleted 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 
   727 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
       
   728   using surj_f_inv_f[of p] by (auto simp add: bij_def)
       
   729 
       
   730 lemma bij_swap_comp:
       
   731   assumes bp: "bij p"
       
   732   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
       
   733   using surj_f_inv_f[OF bij_is_surj[OF bp]]
       
   734   by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
       
   735 
       
   736 lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
       
   737 proof -
       
   738   assume H: "bij p"
       
   739   show ?thesis
       
   740     unfolding bij_swap_comp[OF H] bij_swap_iff
       
   741     using H .
       
   742 qed
       
   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]: