author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64272  f76b6dda2e56 
child 65366  10ca63a18e56 
permissions  rwrr 
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  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  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  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  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  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  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  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  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  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  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  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  510 
end 