src/HOL/Library/Multiset_Permutations.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64272 f76b6dda2e56
child 65366 10ca63a18e56
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     1
(*
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     2
  File:      Multiset_Permutations.thy
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     3
  Author:    Manuel Eberl (TU M√ľnchen)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     4
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     5
  Defines the set of permutations of a given multiset (or set), i.e. the set of all lists whose 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     6
  entries correspond to the multiset (resp. set).
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     7
*)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     8
section \<open>Permutations of a Multiset\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     9
theory Multiset_Permutations
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    10
imports 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    11
  Complex_Main 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    12
  "~~/src/HOL/Library/Multiset" 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    13
  "~~/src/HOL/Library/Permutations"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    14
begin
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    15
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    16
(* TODO Move *)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    17
lemma mset_tl: "xs \<noteq> [] \<Longrightarrow> mset (tl xs) = mset xs - {#hd xs#}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    18
  by (cases xs) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    19
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    20
lemma mset_set_image_inj:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    21
  assumes "inj_on f A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    22
  shows   "mset_set (f ` A) = image_mset f (mset_set A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    23
proof (cases "finite A")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    24
  case True
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    25
  from this and assms show ?thesis by (induction A) auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    26
qed (insert assms, simp add: finite_image_iff)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    27
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    28
lemma multiset_remove_induct [case_names empty remove]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    29
  assumes "P {#}" "\<And>A. A \<noteq> {#} \<Longrightarrow> (\<And>x. x \<in># A \<Longrightarrow> P (A - {#x#})) \<Longrightarrow> P A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    30
  shows   "P A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    31
proof (induction A rule: full_multiset_induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    32
  case (less A)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    33
  hence IH: "P B" if "B \<subset># A" for B using that by blast
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    34
  show ?case
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    35
  proof (cases "A = {#}")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    36
    case True
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    37
    thus ?thesis by (simp add: assms)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    38
  next
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    39
    case False
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    40
    hence "P (A - {#x#})" if "x \<in># A" for x
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    41
      using that by (intro IH) (simp add: mset_subset_diff_self)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    42
    from False and this show "P A" by (rule assms)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    43
  qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    44
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    45
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    46
lemma map_list_bind: "map g (List.bind xs f) = List.bind xs (map g \<circ> f)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    47
  by (simp add: List.bind_def map_concat)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    48
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    49
lemma mset_eq_mset_set_imp_distinct:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    50
  "finite A \<Longrightarrow> mset_set A = mset xs \<Longrightarrow> distinct xs"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    51
proof (induction xs arbitrary: A)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    52
  case (Cons x xs A)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    53
  from Cons.prems(2) have "x \<in># mset_set A" by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    54
  with Cons.prems(1) have [simp]: "x \<in> A" by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    55
  from Cons.prems have "x \<notin># mset_set (A - {x})" by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    56
  also from Cons.prems have "mset_set (A - {x}) = mset_set A - {#x#}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    57
    by (subst mset_set_Diff) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    58
  also have "mset_set A = mset (x#xs)" by (simp add: Cons.prems)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    59
  also have "\<dots> - {#x#} = mset xs" by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    60
  finally have [simp]: "x \<notin> set xs" by (simp add: in_multiset_in_set)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    61
  from Cons.prems show ?case by (auto intro!: Cons.IH[of "A - {x}"] simp: mset_set_Diff)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    62
qed simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    63
(* END TODO *)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    64
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    65
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    66
subsection \<open>Permutations of a multiset\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    67
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    68
definition permutations_of_multiset :: "'a multiset \<Rightarrow> 'a list set" where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    69
  "permutations_of_multiset A = {xs. mset xs = A}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    70
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    71
lemma permutations_of_multisetI: "mset xs = A \<Longrightarrow> xs \<in> permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    72
  by (simp add: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    73
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    74
lemma permutations_of_multisetD: "xs \<in> permutations_of_multiset A \<Longrightarrow> mset xs = A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    75
  by (simp add: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    76
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    77
lemma permutations_of_multiset_Cons_iff:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    78
  "x # xs \<in> permutations_of_multiset A \<longleftrightarrow> x \<in># A \<and> xs \<in> permutations_of_multiset (A - {#x#})"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    79
  by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    80
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    81
lemma permutations_of_multiset_empty [simp]: "permutations_of_multiset {#} = {[]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    82
  unfolding permutations_of_multiset_def by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    83
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    84
lemma permutations_of_multiset_nonempty: 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    85
  assumes nonempty: "A \<noteq> {#}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    86
  shows   "permutations_of_multiset A = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    87
             (\<Union>x\<in>set_mset A. (op # x) ` permutations_of_multiset (A - {#x#}))" (is "_ = ?rhs")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    88
proof safe
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    89
  fix xs assume "xs \<in> permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    90
  hence mset_xs: "mset xs = A" by (simp add: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    91
  hence "xs \<noteq> []" by (auto simp: nonempty)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    92
  then obtain x xs' where xs: "xs = x # xs'" by (cases xs) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    93
  with mset_xs have "x \<in> set_mset A" "xs' \<in> permutations_of_multiset (A - {#x#})"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    94
    by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    95
  with xs show "xs \<in> ?rhs" by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    96
qed (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    97
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    98
lemma permutations_of_multiset_singleton [simp]: "permutations_of_multiset {#x#} = {[x]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    99
  by (simp add: permutations_of_multiset_nonempty)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   100
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   101
lemma permutations_of_multiset_doubleton: 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   102
  "permutations_of_multiset {#x,y#} = {[x,y], [y,x]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   103
  by (simp add: permutations_of_multiset_nonempty insert_commute)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   104
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   105
lemma rev_permutations_of_multiset [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   106
  "rev ` permutations_of_multiset A = permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   107
proof
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   108
  have "rev ` rev ` permutations_of_multiset A \<subseteq> rev ` permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   109
    unfolding permutations_of_multiset_def by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   110
  also have "rev ` rev ` permutations_of_multiset A = permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   111
    by (simp add: image_image)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   112
  finally show "permutations_of_multiset A \<subseteq> rev ` permutations_of_multiset A" .
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   113
next
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   114
  show "rev ` permutations_of_multiset A \<subseteq> permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   115
    unfolding permutations_of_multiset_def by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   116
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   117
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   118
lemma length_finite_permutations_of_multiset:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   119
  "xs \<in> permutations_of_multiset A \<Longrightarrow> length xs = size A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   120
  by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   121
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   122
lemma permutations_of_multiset_lists: "permutations_of_multiset A \<subseteq> lists (set_mset A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   123
  by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   124
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   125
lemma finite_permutations_of_multiset [simp]: "finite (permutations_of_multiset A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   126
proof (rule finite_subset)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   127
  show "permutations_of_multiset A \<subseteq> {xs. set xs \<subseteq> set_mset A \<and> length xs = size A}" 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   128
    by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   129
  show "finite {xs. set xs \<subseteq> set_mset A \<and> length xs = size A}" 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   130
    by (rule finite_lists_length_eq) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   131
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   132
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   133
lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \<noteq> {}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   134
proof -
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   135
  from ex_mset[of A] guess xs ..
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   136
  thus ?thesis by (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   137
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   138
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   139
lemma permutations_of_multiset_image:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   140
  "permutations_of_multiset (image_mset f A) = map f ` permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   141
proof safe
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   142
  fix xs assume A: "xs \<in> permutations_of_multiset (image_mset f A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   143
  from ex_mset[of A] obtain ys where ys: "mset ys = A" ..
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   144
  with A have "mset xs = mset (map f ys)" 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   145
    by (simp add: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   146
  from mset_eq_permutation[OF this] guess \<sigma> . note \<sigma> = this
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   147
  with ys have "xs = map f (permute_list \<sigma> ys)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   148
    by (simp add: permute_list_map)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   149
  moreover from \<sigma> ys have "permute_list \<sigma> ys \<in> permutations_of_multiset A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   150
    by (simp add: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   151
  ultimately show "xs \<in> map f ` permutations_of_multiset A" by blast
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   152
qed (auto simp: permutations_of_multiset_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   153
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   154
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   155
subsection \<open>Cardinality of permutations\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   156
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   157
text \<open>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   158
  In this section, we prove some basic facts about the number of permutations of a multiset.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   159
\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   160
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   161
context
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   162
begin
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   163
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   164
private lemma multiset_prod_fact_insert:
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   165
  "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   166
     (count A x + 1) * (\<Prod>y\<in>set_mset A. fact (count A y))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   167
proof -
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   168
  have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count (A+{#x#}) y)) =
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   169
          (\<Prod>y\<in>set_mset (A+{#x#}). (if y = x then count A x + 1 else 1) * fact (count A y))"
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   170
    by (intro prod.cong) simp_all
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   171
  also have "\<dots> = (count A x + 1) * (\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y))"
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   172
    by (simp add: prod.distrib prod.delta)
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   173
  also have "(\<Prod>y\<in>set_mset (A+{#x#}). fact (count A y)) = (\<Prod>y\<in>set_mset A. fact (count A y))"
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   174
    by (intro prod.mono_neutral_right) (auto simp: not_in_iff)
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   175
  finally show ?thesis .
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   176
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   177
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   178
private lemma multiset_prod_fact_remove:
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   179
  "x \<in># A \<Longrightarrow> (\<Prod>y\<in>set_mset A. fact (count A y)) =
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   180
                   count A x * (\<Prod>y\<in>set_mset (A-{#x#}). fact (count (A-{#x#}) y))"
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   181
  using multiset_prod_fact_insert[of "A - {#x#}" x] by simp
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   182
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   183
lemma card_permutations_of_multiset_aux:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   184
  "card (permutations_of_multiset A) * (\<Prod>x\<in>set_mset A. fact (count A x)) = fact (size A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   185
proof (induction A rule: multiset_remove_induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   186
  case (remove A)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   187
  have "card (permutations_of_multiset A) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   188
          card (\<Union>x\<in>set_mset A. op # x ` permutations_of_multiset (A - {#x#}))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   189
    by (simp add: permutations_of_multiset_nonempty remove.hyps)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   190
  also have "\<dots> = (\<Sum>x\<in>set_mset A. card (permutations_of_multiset (A - {#x#})))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   191
    by (subst card_UN_disjoint) (auto simp: card_image)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   192
  also have "\<dots> * (\<Prod>x\<in>set_mset A. fact (count A x)) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   193
               (\<Sum>x\<in>set_mset A. card (permutations_of_multiset (A - {#x#})) * 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   194
                 (\<Prod>y\<in>set_mset A. fact (count A y)))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63965
diff changeset
   195
    by (subst sum_distrib_right) simp_all
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   196
  also have "\<dots> = (\<Sum>x\<in>set_mset A. count A x * fact (size A - 1))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63965
diff changeset
   197
  proof (intro sum.cong refl)
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   198
    fix x assume x: "x \<in># A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   199
    have "card (permutations_of_multiset (A - {#x#})) * (\<Prod>y\<in>set_mset A. fact (count A y)) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   200
            count A x * (card (permutations_of_multiset (A - {#x#})) * 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   201
              (\<Prod>y\<in>set_mset (A - {#x#}). fact (count (A - {#x#}) y)))" (is "?lhs = _")
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   202
      by (subst multiset_prod_fact_remove[OF x]) simp_all
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   203
    also note remove.IH[OF x]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   204
    also from x have "size (A - {#x#}) = size A - 1" by (simp add: size_Diff_submset)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   205
    finally show "?lhs = count A x * fact (size A - 1)" .
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   206
  qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   207
  also have "(\<Sum>x\<in>set_mset A. count A x * fact (size A - 1)) =
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   208
                size A * fact (size A - 1)"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63965
diff changeset
   209
    by (simp add: sum_distrib_right size_multiset_overloaded_eq)
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   210
  also from remove.hyps have "\<dots> = fact (size A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   211
    by (cases "size A") auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   212
  finally show ?case .
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   213
qed simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   214
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   215
theorem card_permutations_of_multiset:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   216
  "card (permutations_of_multiset A) = fact (size A) div (\<Prod>x\<in>set_mset A. fact (count A x))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   217
  "(\<Prod>x\<in>set_mset A. fact (count A x) :: nat) dvd fact (size A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   218
  by (simp_all add: card_permutations_of_multiset_aux[of A, symmetric])
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   219
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   220
lemma card_permutations_of_multiset_insert_aux:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   221
  "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   222
      (size A + 1) * card (permutations_of_multiset A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   223
proof -
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   224
  note card_permutations_of_multiset_aux[of "A + {#x#}"]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   225
  also have "fact (size (A + {#x#})) = (size A + 1) * fact (size A)" by simp
64272
f76b6dda2e56 setprod -> prod
nipkow
parents: 64267
diff changeset
   226
  also note multiset_prod_fact_insert[of A x]
63965
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   227
  also note card_permutations_of_multiset_aux[of A, symmetric]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   228
  finally have "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) *
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   229
                    (\<Prod>y\<in>set_mset A. fact (count A y)) =
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   230
                (size A + 1) * card (permutations_of_multiset A) *
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   231
                    (\<Prod>x\<in>set_mset A. fact (count A x))" by (simp only: mult_ac)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   232
  thus ?thesis by (subst (asm) mult_right_cancel) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   233
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   234
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   235
lemma card_permutations_of_multiset_remove_aux:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   236
  assumes "x \<in># A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   237
  shows   "card (permutations_of_multiset A) * count A x = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   238
             size A * card (permutations_of_multiset (A - {#x#}))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   239
proof -
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   240
  from assms have A: "A - {#x#} + {#x#} = A" by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   241
  from assms have B: "size A = size (A - {#x#}) + 1" 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   242
    by (subst A [symmetric], subst size_union) simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   243
  show ?thesis
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   244
    using card_permutations_of_multiset_insert_aux[of "A - {#x#}" x, unfolded A] assms
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   245
    by (simp add: B)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   246
qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   247
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   248
lemma real_card_permutations_of_multiset_remove:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   249
  assumes "x \<in># A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   250
  shows   "real (card (permutations_of_multiset (A - {#x#}))) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   251
             real (card (permutations_of_multiset A) * count A x) / real (size A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   252
  using assms by (subst card_permutations_of_multiset_remove_aux[OF assms]) auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   253
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   254
lemma real_card_permutations_of_multiset_remove':
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   255
  assumes "x \<in># A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   256
  shows   "real (card (permutations_of_multiset A)) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   257
             real (size A * card (permutations_of_multiset (A - {#x#}))) / real (count A x)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   258
  using assms by (subst card_permutations_of_multiset_remove_aux[OF assms, symmetric]) simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   259
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   260
end
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   261
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   262
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   263
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   264
subsection \<open>Permutations of a set\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   265
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   266
definition permutations_of_set :: "'a set \<Rightarrow> 'a list set" where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   267
  "permutations_of_set A = {xs. set xs = A \<and> distinct xs}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   268
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   269
lemma permutations_of_set_altdef:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   270
  "finite A \<Longrightarrow> permutations_of_set A = permutations_of_multiset (mset_set A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   271
  by (auto simp add: permutations_of_set_def permutations_of_multiset_def mset_set_set 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   272
        in_multiset_in_set [symmetric] mset_eq_mset_set_imp_distinct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   273
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   274
lemma permutations_of_setI [intro]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   275
  assumes "set xs = A" "distinct xs"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   276
  shows   "xs \<in> permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   277
  using assms unfolding permutations_of_set_def by simp
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   278
  
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   279
lemma permutations_of_setD:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   280
  assumes "xs \<in> permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   281
  shows   "set xs = A" "distinct xs"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   282
  using assms unfolding permutations_of_set_def by simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   283
  
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   284
lemma permutations_of_set_lists: "permutations_of_set A \<subseteq> lists A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   285
  unfolding permutations_of_set_def by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   286
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   287
lemma permutations_of_set_empty [simp]: "permutations_of_set {} = {[]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   288
  by (auto simp: permutations_of_set_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   289
  
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   290
lemma UN_set_permutations_of_set [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   291
  "finite A \<Longrightarrow> (\<Union>xs\<in>permutations_of_set A. set xs) = A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   292
  using finite_distinct_list by (auto simp: permutations_of_set_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   293
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   294
lemma permutations_of_set_infinite:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   295
  "\<not>finite A \<Longrightarrow> permutations_of_set A = {}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   296
  by (auto simp: permutations_of_set_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   297
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   298
lemma permutations_of_set_nonempty:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   299
  "A \<noteq> {} \<Longrightarrow> permutations_of_set A = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   300
                  (\<Union>x\<in>A. (\<lambda>xs. x # xs) ` permutations_of_set (A - {x}))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   301
  by (cases "finite A")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   302
     (simp_all add: permutations_of_multiset_nonempty mset_set_empty_iff mset_set_Diff 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   303
                    permutations_of_set_altdef permutations_of_set_infinite)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   304
    
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   305
lemma permutations_of_set_singleton [simp]: "permutations_of_set {x} = {[x]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   306
  by (subst permutations_of_set_nonempty) auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   307
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   308
lemma permutations_of_set_doubleton: 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   309
  "x \<noteq> y \<Longrightarrow> permutations_of_set {x,y} = {[x,y], [y,x]}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   310
  by (subst permutations_of_set_nonempty) 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   311
     (simp_all add: insert_Diff_if insert_commute)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   312
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   313
lemma rev_permutations_of_set [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   314
  "rev ` permutations_of_set A = permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   315
  by (cases "finite A") (simp_all add: permutations_of_set_altdef permutations_of_set_infinite)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   316
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   317
lemma length_finite_permutations_of_set:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   318
  "xs \<in> permutations_of_set A \<Longrightarrow> length xs = card A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   319
  by (auto simp: permutations_of_set_def distinct_card)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   320
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   321
lemma finite_permutations_of_set [simp]: "finite (permutations_of_set A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   322
  by (cases "finite A") (simp_all add: permutations_of_set_infinite permutations_of_set_altdef)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   323
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   324
lemma permutations_of_set_empty_iff [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   325
  "permutations_of_set A = {} \<longleftrightarrow> \<not>finite A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   326
  unfolding permutations_of_set_def using finite_distinct_list[of A] by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   327
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   328
lemma card_permutations_of_set [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   329
  "finite A \<Longrightarrow> card (permutations_of_set A) = fact (card A)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   330
  by (simp add: permutations_of_set_altdef card_permutations_of_multiset del: One_nat_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   331
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   332
lemma permutations_of_set_image_inj:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   333
  assumes inj: "inj_on f A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   334
  shows   "permutations_of_set (f ` A) = map f ` permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   335
  by (cases "finite A")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   336
     (simp_all add: permutations_of_set_infinite permutations_of_set_altdef
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   337
                    permutations_of_multiset_image mset_set_image_inj inj finite_image_iff)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   338
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   339
lemma permutations_of_set_image_permutes:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   340
  "\<sigma> permutes A \<Longrightarrow> map \<sigma> ` permutations_of_set A = permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   341
  by (subst permutations_of_set_image_inj [symmetric])
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   342
     (simp_all add: permutes_inj_on permutes_image)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   343
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   344
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   345
subsection \<open>Code generation\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   346
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   347
text \<open>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   348
  First, we give code an implementation for permutations of lists.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   349
\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   350
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   351
declare length_remove1 [termination_simp] 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   352
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   353
fun permutations_of_list_impl where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   354
  "permutations_of_list_impl xs = (if xs = [] then [[]] else
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   355
     List.bind (remdups xs) (\<lambda>x. map (op # x) (permutations_of_list_impl (remove1 x xs))))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   356
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   357
fun permutations_of_list_impl_aux where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   358
  "permutations_of_list_impl_aux acc xs = (if xs = [] then [acc] else
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   359
     List.bind (remdups xs) (\<lambda>x. permutations_of_list_impl_aux (x#acc) (remove1 x xs)))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   360
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   361
declare permutations_of_list_impl_aux.simps [simp del]    
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   362
declare permutations_of_list_impl.simps [simp del]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   363
    
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   364
lemma permutations_of_list_impl_Nil [simp]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   365
  "permutations_of_list_impl [] = [[]]"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   366
  by (simp add: permutations_of_list_impl.simps)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   367
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   368
lemma permutations_of_list_impl_nonempty:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   369
  "xs \<noteq> [] \<Longrightarrow> permutations_of_list_impl xs = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   370
     List.bind (remdups xs) (\<lambda>x. map (op # x) (permutations_of_list_impl (remove1 x xs)))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   371
  by (subst permutations_of_list_impl.simps) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   372
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   373
lemma set_permutations_of_list_impl:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   374
  "set (permutations_of_list_impl xs) = permutations_of_multiset (mset xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   375
  by (induction xs rule: permutations_of_list_impl.induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   376
     (subst permutations_of_list_impl.simps, 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   377
      simp_all add: permutations_of_multiset_nonempty set_list_bind)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   378
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   379
lemma distinct_permutations_of_list_impl:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   380
  "distinct (permutations_of_list_impl xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   381
  by (induction xs rule: permutations_of_list_impl.induct, 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   382
      subst permutations_of_list_impl.simps)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   383
     (auto intro!: distinct_list_bind simp: distinct_map o_def disjoint_family_on_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   384
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   385
lemma permutations_of_list_impl_aux_correct':
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   386
  "permutations_of_list_impl_aux acc xs = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   387
     map (\<lambda>xs. rev xs @ acc) (permutations_of_list_impl xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   388
  by (induction acc xs rule: permutations_of_list_impl_aux.induct,
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   389
      subst permutations_of_list_impl_aux.simps, subst permutations_of_list_impl.simps)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   390
     (auto simp: map_list_bind intro!: list_bind_cong)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   391
    
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   392
lemma permutations_of_list_impl_aux_correct:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   393
  "permutations_of_list_impl_aux [] xs = map rev (permutations_of_list_impl xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   394
  by (simp add: permutations_of_list_impl_aux_correct')
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   395
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   396
lemma distinct_permutations_of_list_impl_aux:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   397
  "distinct (permutations_of_list_impl_aux acc xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   398
  by (simp add: permutations_of_list_impl_aux_correct' distinct_map 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   399
        distinct_permutations_of_list_impl inj_on_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   400
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   401
lemma set_permutations_of_list_impl_aux:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   402
  "set (permutations_of_list_impl_aux [] xs) = permutations_of_multiset (mset xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   403
  by (simp add: permutations_of_list_impl_aux_correct set_permutations_of_list_impl)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   404
  
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   405
declare set_permutations_of_list_impl_aux [symmetric, code]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   406
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   407
value [code] "permutations_of_multiset {#1,2,3,4::int#}"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   408
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   409
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   410
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   411
text \<open>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   412
  Now we turn to permutations of sets. We define an auxiliary version with an 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   413
  accumulator to avoid having to map over the results.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   414
\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   415
function permutations_of_set_aux where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   416
  "permutations_of_set_aux acc A = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   417
     (if \<not>finite A then {} else if A = {} then {acc} else 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   418
        (\<Union>x\<in>A. permutations_of_set_aux (x#acc) (A - {x})))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   419
by auto
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   420
termination by (relation "Wellfounded.measure (card \<circ> snd)") (simp_all add: card_gt_0_iff)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   421
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   422
lemma permutations_of_set_aux_altdef:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   423
  "permutations_of_set_aux acc A = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   424
proof (cases "finite A")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   425
  assume "finite A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   426
  thus ?thesis
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   427
  proof (induction A arbitrary: acc rule: finite_psubset_induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   428
    case (psubset A acc)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   429
    show ?case
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   430
    proof (cases "A = {}")
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   431
      case False
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   432
      note [simp del] = permutations_of_set_aux.simps
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   433
      from psubset.hyps False 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   434
        have "permutations_of_set_aux acc A = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   435
                (\<Union>y\<in>A. permutations_of_set_aux (y#acc) (A - {y}))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   436
        by (subst permutations_of_set_aux.simps) simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   437
      also have "\<dots> = (\<Union>y\<in>A. (\<lambda>xs. rev xs @ acc) ` (\<lambda>xs. y # xs) ` permutations_of_set (A - {y}))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   438
        by (intro SUP_cong refl, subst psubset) (auto simp: image_image)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   439
      also from False have "\<dots> = (\<lambda>xs. rev xs @ acc) ` permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   440
        by (subst (2) permutations_of_set_nonempty) (simp_all add: image_UN)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   441
      finally show ?thesis .
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   442
    qed simp_all
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   443
  qed
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   444
qed (simp_all add: permutations_of_set_infinite)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   445
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   446
declare permutations_of_set_aux.simps [simp del]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   447
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   448
lemma permutations_of_set_aux_correct:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   449
  "permutations_of_set_aux [] A = permutations_of_set A"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   450
  by (simp add: permutations_of_set_aux_altdef)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   451
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   452
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   453
text \<open>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   454
  In another refinement step, we define a version on lists.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   455
\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   456
declare length_remove1 [termination_simp]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   457
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   458
fun permutations_of_set_aux_list where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   459
  "permutations_of_set_aux_list acc xs = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   460
     (if xs = [] then [acc] else 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   461
        List.bind xs (\<lambda>x. permutations_of_set_aux_list (x#acc) (List.remove1 x xs)))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   462
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   463
definition permutations_of_set_list where
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   464
  "permutations_of_set_list xs = permutations_of_set_aux_list [] xs"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   465
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   466
declare permutations_of_set_aux_list.simps [simp del]
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   467
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   468
lemma permutations_of_set_aux_list_refine:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   469
  assumes "distinct xs"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   470
  shows   "set (permutations_of_set_aux_list acc xs) = permutations_of_set_aux acc (set xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   471
  using assms
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   472
  by (induction acc xs rule: permutations_of_set_aux_list.induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   473
     (subst permutations_of_set_aux_list.simps,
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   474
      subst permutations_of_set_aux.simps,
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   475
      simp_all add: set_list_bind cong: SUP_cong)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   476
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   477
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   478
text \<open>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   479
  The permutation lists contain no duplicates if the inputs contain no duplicates.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   480
  Therefore, these functions can easily be used when working with a representation of
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   481
  sets by distinct lists.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   482
  The same approach should generalise to any kind of set implementation that supports
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   483
  a monadic bind operation, and since the results are disjoint, merging should be cheap.
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   484
\<close>
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   485
lemma distinct_permutations_of_set_aux_list:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   486
  "distinct xs \<Longrightarrow> distinct (permutations_of_set_aux_list acc xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   487
  by (induction acc xs rule: permutations_of_set_aux_list.induct)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   488
     (subst permutations_of_set_aux_list.simps,
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   489
      auto intro!: distinct_list_bind simp: disjoint_family_on_def 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   490
         permutations_of_set_aux_list_refine permutations_of_set_aux_altdef)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   491
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   492
lemma distinct_permutations_of_set_list:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   493
    "distinct xs \<Longrightarrow> distinct (permutations_of_set_list xs)"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   494
  by (simp add: permutations_of_set_list_def distinct_permutations_of_set_aux_list)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   495
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   496
lemma permutations_of_list:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   497
    "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   498
  by (simp add: permutations_of_set_aux_correct [symmetric] 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   499
        permutations_of_set_aux_list_refine permutations_of_set_list_def)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   500
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   501
lemma permutations_of_list_code [code]:
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   502
  "permutations_of_set (set xs) = set (permutations_of_set_list (remdups xs))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   503
  "permutations_of_set (List.coset xs) = 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   504
     Code.abort (STR ''Permutation of set complement not supported'') 
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   505
       (\<lambda>_. permutations_of_set (List.coset xs))"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   506
  by (simp_all add: permutations_of_list)
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   507
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   508
value [code] "permutations_of_set (set ''abcd'')"
d510b816ea41 Set_Permutations replaced by more general Multiset_Permutations
eberlm <eberlm@in.tum.de>
parents:
diff changeset
   509
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63965
diff changeset
   510
end