author  blanchet 
Thu, 09 Apr 2015 18:00:58 +0200  
changeset 59986  f38b94549dc8 
parent 59958  4538d41e8e54 
child 59997  90fb391a15c1 
child 59998  c54d36be22ef 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
15072  2 
Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker 
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
54868
diff
changeset

3 
Author: Andrei Popescu, TU Muenchen 
59813  4 
Author: Jasmin Blanchette, Inria, LORIA, MPII 
5 
Author: Dmitriy Traytel, TU Muenchen 

6 
Author: Mathias Fleury, MPII 

10249  7 
*) 
8 

58881  9 
section {* (Finite) multisets *} 
10249  10 

15131  11 
theory Multiset 
51599
1559e9266280
optionalized very specific code setup for multisets
haftmann
parents:
51548
diff
changeset

12 
imports Main 
15131  13 
begin 
10249  14 

15 
subsection {* The type of multisets *} 

16 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

17 
definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

18 

49834  19 
typedef 'a multiset = "multiset :: ('a => nat) set" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

20 
morphisms count Abs_multiset 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

21 
unfolding multiset_def 
10249  22 
proof 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45608
diff
changeset

23 
show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp 
10249  24 
qed 
25 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

26 
setup_lifting type_definition_multiset 
19086  27 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

28 
abbreviation Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where 
25610  29 
"a :# M == 0 < count M a" 
30 

26145  31 
notation (xsymbols) 
32 
Melem (infix "\<in>#" 50) 

10249  33 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

34 
lemma multiset_eq_iff: 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

35 
"M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

36 
by (simp only: count_inject [symmetric] fun_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

37 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

38 
lemma multiset_eqI: 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

39 
"(\<And>x. count A x = count B x) \<Longrightarrow> A = B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

40 
using multiset_eq_iff by auto 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

41 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

42 
text {* 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

43 
\medskip Preservation of the representing set @{term multiset}. 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

44 
*} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

45 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

46 
lemma const0_in_multiset: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

47 
"(\<lambda>a. 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

48 
by (simp add: multiset_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

49 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

50 
lemma only1_in_multiset: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

51 
"(\<lambda>b. if b = a then n else 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

52 
by (simp add: multiset_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

53 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

54 
lemma union_preserves_multiset: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

55 
"M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

56 
by (simp add: multiset_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

57 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

58 
lemma diff_preserves_multiset: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

59 
assumes "M \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

60 
shows "(\<lambda>a. M a  N a) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

61 
proof  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

62 
have "{x. N x < M x} \<subseteq> {x. 0 < M x}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

63 
by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

64 
with assms show ?thesis 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

65 
by (auto simp add: multiset_def intro: finite_subset) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

66 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

67 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

68 
lemma filter_preserves_multiset: 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

69 
assumes "M \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

70 
shows "(\<lambda>x. if P x then M x else 0) \<in> multiset" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

71 
proof  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

72 
have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

73 
by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

74 
with assms show ?thesis 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

75 
by (auto simp add: multiset_def intro: finite_subset) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

76 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

77 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

78 
lemmas in_multiset = const0_in_multiset only1_in_multiset 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

79 
union_preserves_multiset diff_preserves_multiset filter_preserves_multiset 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

80 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

81 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

82 
subsection {* Representing multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

83 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

84 
text {* Multiset enumeration *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

85 

48008  86 
instantiation multiset :: (type) cancel_comm_monoid_add 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

87 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

88 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

89 
lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

90 
by (rule const0_in_multiset) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

91 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

92 
abbreviation Mempty :: "'a multiset" ("{#}") where 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

93 
"Mempty \<equiv> 0" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

94 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

95 
lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

96 
by (rule union_preserves_multiset) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

97 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59813
diff
changeset

98 
lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a  N a" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59813
diff
changeset

99 
by (rule diff_preserves_multiset) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59813
diff
changeset

100 

48008  101 
instance 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59813
diff
changeset

102 
by default (transfer, simp add: fun_eq_iff)+ 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

103 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

104 
end 
10249  105 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

106 
lift_definition single :: "'a => 'a multiset" is "\<lambda>a b. if b = a then 1 else 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

107 
by (rule only1_in_multiset) 
15869  108 

26145  109 
syntax 
26176  110 
"_multiset" :: "args => 'a multiset" ("{#(_)#}") 
25507  111 
translations 
112 
"{#x, xs#}" == "{#x#} + {#xs#}" 

113 
"{#x#}" == "CONST single x" 

114 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

115 
lemma count_empty [simp]: "count {#} a = 0" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

116 
by (simp add: zero_multiset.rep_eq) 
10249  117 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

118 
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

119 
by (simp add: single.rep_eq) 
29901  120 

10249  121 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

122 
subsection {* Basic operations *} 
10249  123 

124 
subsubsection {* Union *} 

125 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

126 
lemma count_union [simp]: "count (M + N) a = count M a + count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

127 
by (simp add: plus_multiset.rep_eq) 
10249  128 

129 

130 
subsubsection {* Difference *} 

131 

49388  132 
instantiation multiset :: (type) comm_monoid_diff 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

133 
begin 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

134 

49388  135 
instance 
136 
by default (transfer, simp add: fun_eq_iff)+ 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

137 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

138 
end 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

139 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

140 
lemma count_diff [simp]: "count (M  N) a = count M a  count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

141 
by (simp add: minus_multiset.rep_eq) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

142 

17161  143 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
52289  144 
by rule (fact Groups.diff_zero, fact Groups.zero_diff) 
36903  145 

146 
lemma diff_cancel[simp]: "A  A = {#}" 

52289  147 
by (fact Groups.diff_cancel) 
10249  148 

36903  149 
lemma diff_union_cancelR [simp]: "M + N  N = (M::'a multiset)" 
52289  150 
by (fact add_diff_cancel_right') 
10249  151 

36903  152 
lemma diff_union_cancelL [simp]: "N + M  N = (M::'a multiset)" 
52289  153 
by (fact add_diff_cancel_left') 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

154 

52289  155 
lemma diff_right_commute: 
156 
"(M::'a multiset)  N  Q = M  Q  N" 

157 
by (fact diff_right_commute) 

158 

159 
lemma diff_add: 

160 
"(M::'a multiset)  (N + Q) = M  N  Q" 

161 
by (rule sym) (fact diff_diff_add) 

58425  162 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

163 
lemma insert_DiffM: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

164 
"x \<in># M \<Longrightarrow> {#x#} + (M  {#x#}) = M" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

165 
by (clarsimp simp: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

166 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

167 
lemma insert_DiffM2 [simp]: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

168 
"x \<in># M \<Longrightarrow> M  {#x#} + {#x#} = M" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

169 
by (clarsimp simp: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

170 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

171 
lemma diff_union_swap: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

172 
"a \<noteq> b \<Longrightarrow> M  {#a#} + {#b#} = M + {#b#}  {#a#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

173 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

174 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

175 
lemma diff_union_single_conv: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

176 
"a \<in># J \<Longrightarrow> I + J  {#a#} = I + (J  {#a#})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

177 
by (simp add: multiset_eq_iff) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

178 

10249  179 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

180 
subsubsection {* Equality of multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

181 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

182 
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

183 
by (simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

184 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

185 
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

186 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

187 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

188 
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

189 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

190 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

191 
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

192 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

193 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

194 
lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

195 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

196 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

197 
lemma diff_single_trivial: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

198 
"\<not> x \<in># M \<Longrightarrow> M  {#x#} = M" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

199 
by (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

200 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

201 
lemma diff_single_eq_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

202 
"x \<in># M \<Longrightarrow> M  {#x#} = N \<longleftrightarrow> M = N + {#x#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

203 
by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

204 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

205 
lemma union_single_eq_diff: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

206 
"M + {#x#} = N \<Longrightarrow> M = N  {#x#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

207 
by (auto dest: sym) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

208 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

209 
lemma union_single_eq_member: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

210 
"M + {#x#} = N \<Longrightarrow> x \<in># N" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

211 
by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

212 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

213 
lemma union_is_single: 
46730  214 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs") 
215 
proof 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

216 
assume ?rhs then show ?lhs by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

217 
next 
46730  218 
assume ?lhs then show ?rhs 
219 
by (simp add: multiset_eq_iff split:if_splits) (metis add_is_1) 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

220 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

221 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

222 
lemma single_is_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

223 
"{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

224 
by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

225 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

226 
lemma add_eq_conv_diff: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

227 
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#}" (is "?lhs = ?rhs") 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44339
diff
changeset

228 
(* shorter: by (simp add: multiset_eq_iff) fastforce *) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

229 
proof 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

230 
assume ?rhs then show ?lhs 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

231 
by (auto simp add: add.assoc add.commute [of "{#b#}"]) 
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

232 
(drule sym, simp add: add.assoc [symmetric]) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

233 
next 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

234 
assume ?lhs 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

235 
show ?rhs 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

236 
proof (cases "a = b") 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

237 
case True with `?lhs` show ?thesis by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

238 
next 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

239 
case False 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

240 
from `?lhs` have "a \<in># N + {#b#}" by (rule union_single_eq_member) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

241 
with False have "a \<in># N" by auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

242 
moreover from `?lhs` have "M = N + {#b#}  {#a#}" by (rule union_single_eq_diff) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

243 
moreover note False 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

244 
ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

245 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

246 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

247 

58425  248 
lemma insert_noteq_member: 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

249 
assumes BC: "B + {#b#} = C + {#c#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

250 
and bnotc: "b \<noteq> c" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

251 
shows "c \<in># B" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

252 
proof  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

253 
have "c \<in># C + {#c#}" by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

254 
have nc: "\<not> c \<in># {#b#}" using bnotc by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

255 
then have "c \<in># B + {#b#}" using BC by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

256 
then show "c \<in># B" using nc by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

257 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

258 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

259 
lemma add_eq_conv_ex: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

260 
"(M + {#a#} = N + {#b#}) = 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

261 
(M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

262 
by (auto simp add: add_eq_conv_diff) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

263 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

264 
lemma multi_member_split: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

265 
"x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

266 
by (rule_tac x = "M  {#x#}" in exI, simp) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

267 

58425  268 
lemma multiset_add_sub_el_shuffle: 
269 
assumes "c \<in># B" and "b \<noteq> c" 

58098  270 
shows "B  {#c#} + {#b#} = B + {#b#}  {#c#}" 
271 
proof  

58425  272 
from `c \<in># B` obtain A where B: "B = A + {#c#}" 
58098  273 
by (blast dest: multi_member_split) 
274 
have "A + {#b#} = A + {#b#} + {#c#}  {#c#}" by simp 

58425  275 
then have "A + {#b#} = A + {#c#} + {#b#}  {#c#}" 
58098  276 
by (simp add: ac_simps) 
277 
then show ?thesis using B by simp 

278 
qed 

279 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

280 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

281 
subsubsection {* Pointwise ordering induced by count *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

282 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

283 
instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

284 
begin 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

285 

55565
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55467
diff
changeset

286 
lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" . 
f663fc1e653b
simplify proofs because of the stronger reflexivity prover
kuncar
parents:
55467
diff
changeset

287 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

288 
lemmas mset_le_def = less_eq_multiset_def 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

289 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

290 
definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

291 
mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

292 

46921  293 
instance 
294 
by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym) 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

295 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

296 
end 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

297 

59986
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

298 
abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

299 
"A <# B \<equiv> A < B" 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

300 
abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

301 
"A \<subset># B \<equiv> A < B" 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

302 

f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

303 
abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

304 
"A <=# B \<equiv> A \<le> B" 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

305 
abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

306 
"A \<le># B \<equiv> A \<le> B" 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

307 
abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

308 
"A \<subseteq># B \<equiv> A \<le> B" 
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59958
diff
changeset

309 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

310 
lemma mset_less_eqI: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

311 
"(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

312 
by (simp add: mset_le_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

313 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

314 
lemma mset_le_exists_conv: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

315 
"(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

316 
apply (unfold mset_le_def, rule iffI, rule_tac x = "B  A" in exI) 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

317 
apply (auto intro: multiset_eq_iff [THEN iffD2]) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

318 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

319 

52289  320 
instance multiset :: (type) ordered_cancel_comm_monoid_diff 
321 
by default (simp, fact mset_le_exists_conv) 

322 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

323 
lemma mset_le_mono_add_right_cancel [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

324 
"(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

325 
by (fact add_le_cancel_right) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

326 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

327 
lemma mset_le_mono_add_left_cancel [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

328 
"C + (A::'a multiset) \<le> C + B \<longleftrightarrow> A \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

329 
by (fact add_le_cancel_left) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

330 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

331 
lemma mset_le_mono_add: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

332 
"(A::'a multiset) \<le> B \<Longrightarrow> C \<le> D \<Longrightarrow> A + C \<le> B + D" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

333 
by (fact add_mono) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

334 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

335 
lemma mset_le_add_left [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

336 
"(A::'a multiset) \<le> A + B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

337 
unfolding mset_le_def by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

338 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

339 
lemma mset_le_add_right [simp]: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

340 
"B \<le> (A::'a multiset) + B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

341 
unfolding mset_le_def by auto 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

342 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

343 
lemma mset_le_single: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

344 
"a :# B \<Longrightarrow> {#a#} \<le> B" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

345 
by (simp add: mset_le_def) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

346 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

347 
lemma multiset_diff_union_assoc: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

348 
"C \<le> B \<Longrightarrow> (A::'a multiset) + B  C = A + (B  C)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

349 
by (simp add: multiset_eq_iff mset_le_def) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

350 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

351 
lemma mset_le_multiset_union_diff_commute: 
36867  352 
"B \<le> A \<Longrightarrow> (A::'a multiset)  B + C = A + C  B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

353 
by (simp add: multiset_eq_iff mset_le_def) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

354 

39301  355 
lemma diff_le_self[simp]: "(M::'a multiset)  N \<le> M" 
356 
by(simp add: mset_le_def) 

357 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

358 
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

359 
apply (clarsimp simp: mset_le_def mset_less_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

360 
apply (erule_tac x=x in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

361 
apply auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

362 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

363 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

364 
lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

365 
apply (clarsimp simp: mset_le_def mset_less_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

366 
apply (erule_tac x = x in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

367 
apply auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

368 
done 
58425  369 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

370 
lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

371 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

372 
apply (simp add: mset_lessD) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

373 
apply (clarsimp simp: mset_le_def mset_less_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

374 
apply safe 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

375 
apply (erule_tac x = a in allE) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

376 
apply (auto split: split_if_asm) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

377 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

378 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

379 
lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

380 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

381 
apply (simp add: mset_leD) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

382 
apply (force simp: mset_le_def mset_less_def split: split_if_asm) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

383 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

384 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

385 
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

386 
by (auto simp add: mset_less_def mset_le_def multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

387 

55808
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

388 
lemma empty_le[simp]: "{#} \<le> A" 
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

389 
unfolding mset_le_exists_conv by auto 
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

390 

488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

391 
lemma le_empty[simp]: "(M \<le> {#}) = (M = {#})" 
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

392 
unfolding mset_le_exists_conv by auto 
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

393 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

394 
lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

395 
by (auto simp: mset_le_def mset_less_def) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

396 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

397 
lemma multi_psub_self[simp]: "(A::'a multiset) < A = False" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

398 
by simp 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

399 

59813  400 
lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M" 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

401 
by (fact add_less_imp_less_right) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

402 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

403 
lemma mset_less_empty_nonempty: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

404 
"{#} < S \<longleftrightarrow> S \<noteq> {#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

405 
by (auto simp: mset_le_def mset_less_def) 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

406 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

407 
lemma mset_less_diff_self: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

408 
"c \<in># B \<Longrightarrow> B  {#c#} < B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

409 
by (auto simp: mset_le_def mset_less_def multiset_eq_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

410 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

411 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

412 
subsubsection {* Intersection *} 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

413 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

414 
instantiation multiset :: (type) semilattice_inf 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

415 
begin 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

416 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

417 
definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

418 
multiset_inter_def: "inf_multiset A B = A  (A  B)" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

419 

46921  420 
instance 
421 
proof  

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

422 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n  (n  q)" by arith 
46921  423 
show "OFCLASS('a multiset, semilattice_inf_class)" 
424 
by default (auto simp add: multiset_inter_def mset_le_def aux) 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

425 
qed 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

426 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

427 
end 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

428 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

429 
abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

430 
"multiset_inter \<equiv> inf" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

431 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

432 
lemma multiset_inter_count [simp]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

433 
"count (A #\<inter> B) x = min (count A x) (count B x)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

434 
by (simp add: multiset_inter_def) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

435 

04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

436 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
46730  437 
by (rule multiset_eqI) auto 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

438 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

439 
lemma multiset_union_diff_commute: 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

440 
assumes "B #\<inter> C = {#}" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

441 
shows "A + B  C = A  C + B" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

442 
proof (rule multiset_eqI) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

443 
fix x 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

444 
from assms have "min (count B x) (count C x) = 0" 
46730  445 
by (auto simp add: multiset_eq_iff) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

446 
then have "count B x = 0 \<or> count C x = 0" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

447 
by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

448 
then show "count (A + B  C) x = count (A  C + B) x" 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

449 
by auto 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

450 
qed 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

451 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

452 
lemma empty_inter [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

453 
"{#} #\<inter> M = {#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

454 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

455 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

456 
lemma inter_empty [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

457 
"M #\<inter> {#} = {#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

458 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

459 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

460 
lemma inter_add_left1: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

461 
"\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

462 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

463 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

464 
lemma inter_add_left2: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

465 
"x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N  {#x#})) + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

466 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

467 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

468 
lemma inter_add_right1: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

469 
"\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

470 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

471 

197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

472 
lemma inter_add_right2: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

473 
"x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N  {#x#}) #\<inter> M) + {#x#}" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

474 
by (simp add: multiset_eq_iff) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

475 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

476 

51623  477 
subsubsection {* Bounded union *} 
478 

479 
instantiation multiset :: (type) semilattice_sup 

480 
begin 

481 

482 
definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where 

483 
"sup_multiset A B = A + (B  A)" 

484 

485 
instance 

486 
proof  

487 
have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q  m) \<le> n" by arith 

488 
show "OFCLASS('a multiset, semilattice_sup_class)" 

489 
by default (auto simp add: sup_multiset_def mset_le_def aux) 

490 
qed 

491 

492 
end 

493 

494 
abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where 

495 
"sup_multiset \<equiv> sup" 

496 

497 
lemma sup_multiset_count [simp]: 

498 
"count (A #\<union> B) x = max (count A x) (count B x)" 

499 
by (simp add: sup_multiset_def) 

500 

501 
lemma empty_sup [simp]: 

502 
"{#} #\<union> M = M" 

503 
by (simp add: multiset_eq_iff) 

504 

505 
lemma sup_empty [simp]: 

506 
"M #\<union> {#} = M" 

507 
by (simp add: multiset_eq_iff) 

508 

509 
lemma sup_add_left1: 

510 
"\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}" 

511 
by (simp add: multiset_eq_iff) 

512 

513 
lemma sup_add_left2: 

514 
"x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N  {#x#})) + {#x#}" 

515 
by (simp add: multiset_eq_iff) 

516 

517 
lemma sup_add_right1: 

518 
"\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}" 

519 
by (simp add: multiset_eq_iff) 

520 

521 
lemma sup_add_right2: 

522 
"x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N  {#x#}) #\<union> M) + {#x#}" 

523 
by (simp add: multiset_eq_iff) 

524 

525 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

526 
subsubsection {* Filter (with comprehension syntax) *} 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

527 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

528 
text {* Multiset comprehension *} 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

529 

47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

530 
lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0" 
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

531 
by (rule filter_preserves_multiset) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

532 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

533 
hide_const (open) filter 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

534 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

535 
lemma count_filter [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

536 
"count (Multiset.filter P M) a = (if P a then count M a else 0)" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

537 
by (simp add: filter.rep_eq) 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

538 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

539 
lemma filter_empty [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

540 
"Multiset.filter P {#} = {#}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

541 
by (rule multiset_eqI) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

542 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

543 
lemma filter_single [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

544 
"Multiset.filter P {#x#} = (if P x then {#x#} else {#})" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

545 
by (rule multiset_eqI) simp 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

546 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

547 
lemma filter_union [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

548 
"Multiset.filter P (M + N) = Multiset.filter P M + Multiset.filter P N" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

549 
by (rule multiset_eqI) simp 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

550 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

551 
lemma filter_diff [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

552 
"Multiset.filter P (M  N) = Multiset.filter P M  Multiset.filter P N" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

553 
by (rule multiset_eqI) simp 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

554 

6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

555 
lemma filter_inter [simp]: 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

556 
"Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

557 
by (rule multiset_eqI) simp 
10249  558 

58035  559 
lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M" 
560 
unfolding less_eq_multiset.rep_eq by auto 

561 

562 
lemma multiset_filter_mono: assumes "A \<le> B" 

563 
shows "Multiset.filter f A \<le> Multiset.filter f B" 

564 
proof  

565 
from assms[unfolded mset_le_exists_conv] 

566 
obtain C where B: "B = A + C" by auto 

567 
show ?thesis unfolding B by auto 

568 
qed 

569 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

570 
syntax 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

571 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})") 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

572 
syntax (xsymbol) 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

573 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})") 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

574 
translations 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

575 
"{#x \<in># M. P#}" == "CONST Multiset.filter (\<lambda>x. P) M" 
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

576 

10249  577 

578 
subsubsection {* Set of elements *} 

579 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

580 
definition set_of :: "'a multiset => 'a set" where 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

581 
"set_of M = {x. x :# M}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

582 

17161  583 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  584 
by (simp add: set_of_def) 
10249  585 

17161  586 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
26178  587 
by (simp add: set_of_def) 
10249  588 

17161  589 
lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
26178  590 
by (auto simp add: set_of_def) 
10249  591 

17161  592 
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

593 
by (auto simp add: set_of_def multiset_eq_iff) 
10249  594 

17161  595 
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
26178  596 
by (auto simp add: set_of_def) 
26016  597 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

598 
lemma set_of_filter [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}" 
26178  599 
by (auto simp add: set_of_def) 
10249  600 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

601 
lemma finite_set_of [iff]: "finite (set_of M)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

602 
using count [of M] by (simp add: multiset_def set_of_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

603 

46756
faf62905cd53
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents:
46730
diff
changeset

604 
lemma finite_Collect_mem [iff]: "finite {x. x :# M}" 
faf62905cd53
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
bulwahn
parents:
46730
diff
changeset

605 
unfolding set_of_def[symmetric] by simp 
10249  606 

58425  607 
lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B" 
55808
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

608 
by (metis mset_leD subsetI mem_set_of_iff) 
488c3e8282c8
added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets
nipkow
parents:
55565
diff
changeset

609 

59813  610 
lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)" 
611 
by auto 

612 

613 

10249  614 
subsubsection {* Size *} 
615 

56656  616 
definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))" 
617 

618 
lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a" 

619 
by (auto simp: wcount_def add_mult_distrib) 

620 

621 
definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where 

622 
"size_multiset f M = setsum (wcount f M) (set_of M)" 

623 

624 
lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def] 

625 

626 
instantiation multiset :: (type) size begin 

627 
definition size_multiset where 

628 
size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)" 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

629 
instance .. 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

630 
end 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

631 

56656  632 
lemmas size_multiset_overloaded_eq = 
633 
size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified] 

634 

635 
lemma size_multiset_empty [simp]: "size_multiset f {#} = 0" 

636 
by (simp add: size_multiset_def) 

637 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

638 
lemma size_empty [simp]: "size {#} = 0" 
56656  639 
by (simp add: size_multiset_overloaded_def) 
640 

641 
lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)" 

642 
by (simp add: size_multiset_eq) 

10249  643 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

644 
lemma size_single [simp]: "size {#b#} = 1" 
56656  645 
by (simp add: size_multiset_overloaded_def) 
646 

647 
lemma setsum_wcount_Int: 

648 
"finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A" 

26178  649 
apply (induct rule: finite_induct) 
650 
apply simp 

56656  651 
apply (simp add: Int_insert_left set_of_def wcount_def) 
652 
done 

653 

654 
lemma size_multiset_union [simp]: 

655 
"size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N" 

57418  656 
apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union) 
56656  657 
apply (subst Int_commute) 
658 
apply (simp add: setsum_wcount_Int) 

26178  659 
done 
10249  660 

28708
a1a436f09ec6
explicit check for pattern discipline before code translation
haftmann
parents:
28562
diff
changeset

661 
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" 
56656  662 
by (auto simp add: size_multiset_overloaded_def) 
663 

664 
lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})" 

665 
by (auto simp add: size_multiset_eq multiset_eq_iff) 

10249  666 

17161  667 
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" 
56656  668 
by (auto simp add: size_multiset_overloaded_def) 
26016  669 

670 
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)" 

26178  671 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  672 

17161  673 
lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
56656  674 
apply (unfold size_multiset_overloaded_eq) 
26178  675 
apply (drule setsum_SucD) 
676 
apply auto 

677 
done 

10249  678 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

679 
lemma size_eq_Suc_imp_eq_union: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

680 
assumes "size M = Suc n" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

681 
shows "\<exists>a N. M = N + {#a#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

682 
proof  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

683 
from assms obtain a where "a \<in># M" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

684 
by (erule size_eq_Suc_imp_elem [THEN exE]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

685 
then have "M = M  {#a#} + {#a#}" by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

686 
then show ?thesis by blast 
23611  687 
qed 
15869  688 

59949  689 
lemma size_mset_mono: assumes "A \<le> B" 
690 
shows "size A \<le> size(B::_ multiset)" 

691 
proof  

692 
from assms[unfolded mset_le_exists_conv] 

693 
obtain C where B: "B = A + C" by auto 

694 
show ?thesis unfolding B by (induct C, auto) 

695 
qed 

696 

697 
lemma size_filter_mset_lesseq[simp]: "size (Multiset.filter f M) \<le> size M" 

698 
by (rule size_mset_mono[OF multiset_filter_subset]) 

699 

700 
lemma size_Diff_submset: 

701 
"M \<le> M' \<Longrightarrow> size (M'  M) = size M'  size(M::'a multiset)" 

702 
by (metis add_diff_cancel_left' size_union mset_le_exists_conv) 

26016  703 

704 
subsection {* Induction and case splits *} 

10249  705 

18258  706 
theorem multiset_induct [case_names empty add, induct type: multiset]: 
48009  707 
assumes empty: "P {#}" 
708 
assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})" 

709 
shows "P M" 

710 
proof (induct n \<equiv> "size M" arbitrary: M) 

711 
case 0 thus "P M" by (simp add: empty) 

712 
next 

713 
case (Suc k) 

714 
obtain N x where "M = N + {#x#}" 

715 
using `Suc k = size M` [symmetric] 

716 
using size_eq_Suc_imp_eq_union by fast 

717 
with Suc add show "P M" by simp 

10249  718 
qed 
719 

25610  720 
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}" 
26178  721 
by (induct M) auto 
25610  722 

55913  723 
lemma multiset_cases [cases type]: 
724 
obtains (empty) "M = {#}" 

725 
 (add) N x where "M = N + {#x#}" 

726 
using assms by (induct M) simp_all 

25610  727 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

728 
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B  {#c#} \<noteq> B" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

729 
by (cases "B = {#}") (auto dest: multi_member_split) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

730 

26033  731 
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

732 
apply (subst multiset_eq_iff) 
26178  733 
apply auto 
734 
done 

10249  735 

35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

736 
lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

737 
proof (induct A arbitrary: B) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

738 
case (empty M) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

739 
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) 
58425  740 
then obtain M' x where "M = M' + {#x#}" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

741 
by (blast dest: multi_nonempty_split) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

742 
then show ?case by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

743 
next 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

744 
case (add S x T) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

745 
have IH: "\<And>B. S < B \<Longrightarrow> size S < size B" by fact 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

746 
have SxsubT: "S + {#x#} < T" by fact 
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

747 
then have "x \<in># T" and "S < T" by (auto dest: mset_less_insertD) 
58425  748 
then obtain T' where T: "T = T' + {#x#}" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

749 
by (blast dest: multi_member_split) 
58425  750 
then have "S < T'" using SxsubT 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

751 
by (blast intro: mset_less_add_bothsides) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

752 
then have "size S < size T'" using IH by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

753 
then show ?case using T by simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

754 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

755 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

756 

59949  757 
lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}" 
758 
by (cases M) auto 

759 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

760 
subsubsection {* Strong induction and subset induction for multisets *} 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

761 

58098  762 
text {* Wellfoundedness of strict subset relation *} 
763 

764 
lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}" 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

765 
apply (rule wf_measure [THEN wf_subset, where f1=size]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

766 
apply (clarsimp simp: measure_def inv_image_def mset_less_size) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

767 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

768 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

769 
lemma full_multiset_induct [case_names less]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

770 
assumes ih: "\<And>B. \<forall>(A::'a multiset). A < B \<longrightarrow> P A \<Longrightarrow> P B" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

771 
shows "P B" 
58098  772 
apply (rule wf_less_mset_rel [THEN wf_induct]) 
773 
apply (rule ih, auto) 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

774 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

775 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

776 
lemma multi_subset_induct [consumes 2, case_names empty add]: 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

777 
assumes "F \<le> A" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

778 
and empty: "P {#}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

779 
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

780 
shows "P F" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

781 
proof  
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

782 
from `F \<le> A` 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

783 
show ?thesis 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

784 
proof (induct F) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

785 
show "P {#}" by fact 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

786 
next 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

787 
fix x F 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

788 
assume P: "F \<le> A \<Longrightarrow> P F" and i: "F + {#x#} \<le> A" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

789 
show "P (F + {#x#})" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

790 
proof (rule insert) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

791 
from i show "x \<in># A" by (auto dest: mset_le_insertD) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

792 
from i have "F \<le> A" by (auto dest: mset_le_insertD) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

793 
with P show "P F" . 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

794 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

795 
qed 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

796 
qed 
26145  797 

17161  798 

48023  799 
subsection {* The fold combinator *} 
800 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

801 
definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" 
48023  802 
where 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

803 
"fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)" 
48023  804 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

805 
lemma fold_mset_empty [simp]: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

806 
"fold f s {#} = s" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

807 
by (simp add: fold_def) 
48023  808 

809 
context comp_fun_commute 

810 
begin 

811 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

812 
lemma fold_mset_insert: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

813 
"fold f s (M + {#x#}) = f x (fold f s M)" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

814 
proof  
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

815 
interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

816 
by (fact comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

817 
interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

818 
by (fact comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

819 
show ?thesis 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

820 
proof (cases "x \<in> set_of M") 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

821 
case False 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

822 
then have *: "count (M + {#x#}) x = 1" by simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

823 
from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) = 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

824 
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

825 
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

826 
with False * show ?thesis 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

827 
by (simp add: fold_def del: count_union) 
48023  828 
next 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

829 
case True 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

830 
def N \<equiv> "set_of M  {x}" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

831 
from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

832 
then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N = 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

833 
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

834 
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

835 
with * show ?thesis by (simp add: fold_def del: count_union) simp 
48023  836 
qed 
837 
qed 

838 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

839 
corollary fold_mset_single [simp]: 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

840 
"fold f s {#x#} = f x s" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

841 
proof  
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

842 
have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

843 
then show ?thesis by simp 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

844 
qed 
48023  845 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

846 
lemma fold_mset_fun_left_comm: 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

847 
"f x (fold f s M) = fold f (f x s) M" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

848 
by (induct M) (simp_all add: fold_mset_insert fun_left_comm) 
48023  849 

850 
lemma fold_mset_union [simp]: 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

851 
"fold f s (M + N) = fold f (fold f s M) N" 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

852 
proof (induct M) 
48023  853 
case empty then show ?case by simp 
854 
next 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

855 
case (add M x) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

856 
have "M + {#x#} + N = (M + N) + {#x#}" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

857 
by (simp add: ac_simps) 
51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

858 
with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm) 
48023  859 
qed 
860 

861 
lemma fold_mset_fusion: 

862 
assumes "comp_fun_commute g" 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

863 
shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P") 
48023  864 
proof  
865 
interpret comp_fun_commute g by (fact assms) 

866 
show "PROP ?P" by (induct A) auto 

867 
qed 

868 

869 
end 

870 

871 
text {* 

872 
A note on code generation: When defining some function containing a 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

873 
subterm @{term "fold F"}, code generation is not automatic. When 
48023  874 
interpreting locale @{text left_commutative} with @{text F}, the 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

875 
would be code thms for @{const fold} become thms like 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

876 
@{term "fold F z {#} = z"} where @{text F} is not a pattern but 
48023  877 
contains defined symbols, i.e.\ is not a code thm. Hence a separate 
878 
constant with its own code thms needs to be introduced for @{text 

879 
F}. See the image operator below. 

880 
*} 

881 

882 

883 
subsection {* Image *} 

884 

885 
definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where 

49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

886 
"image_mset f = fold (plus o single o f) {#}" 
48023  887 

49823  888 
lemma comp_fun_commute_mset_image: 
889 
"comp_fun_commute (plus o single o f)" 

890 
proof 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

891 
qed (simp add: ac_simps fun_eq_iff) 
48023  892 

893 
lemma image_mset_empty [simp]: "image_mset f {#} = {#}" 

49823  894 
by (simp add: image_mset_def) 
48023  895 

896 
lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" 

49823  897 
proof  
898 
interpret comp_fun_commute "plus o single o f" 

899 
by (fact comp_fun_commute_mset_image) 

900 
show ?thesis by (simp add: image_mset_def) 

901 
qed 

48023  902 

903 
lemma image_mset_union [simp]: 

49823  904 
"image_mset f (M + N) = image_mset f M + image_mset f N" 
905 
proof  

906 
interpret comp_fun_commute "plus o single o f" 

907 
by (fact comp_fun_commute_mset_image) 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

908 
show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps) 
49823  909 
qed 
910 

911 
corollary image_mset_insert: 

912 
"image_mset f (M + {#a#}) = image_mset f M + {#f a#}" 

913 
by simp 

48023  914 

49823  915 
lemma set_of_image_mset [simp]: 
916 
"set_of (image_mset f M) = image f (set_of M)" 

917 
by (induct M) simp_all 

48040  918 

49823  919 
lemma size_image_mset [simp]: 
920 
"size (image_mset f M) = size M" 

921 
by (induct M) simp_all 

48023  922 

49823  923 
lemma image_mset_is_empty_iff [simp]: 
924 
"image_mset f M = {#} \<longleftrightarrow> M = {#}" 

925 
by (cases M) auto 

48023  926 

927 
syntax 

928 
"_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" 

929 
("({#_/. _ :# _#})") 

930 
translations 

931 
"{#e. x:#M#}" == "CONST image_mset (%x. e) M" 

932 

59813  933 
syntax (xsymbols) 
934 
"_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" 

935 
("({#_/. _ \<in># _#})") 

936 
translations 

937 
"{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M" 

938 

48023  939 
syntax 
59813  940 
"_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" 
48023  941 
("({#_/  _ :# _./ _#})") 
942 
translations 

943 
"{#e  x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}" 

944 

59813  945 
syntax 
946 
"_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" 

947 
("({#_/  _ \<in># _./ _#})") 

948 
translations 

949 
"{#e  x\<in>#M. P#}" => "{#e. x \<in># {# x\<in>#M. P#}#}" 

950 

48023  951 
text {* 
952 
This allows to write not just filters like @{term "{#x:#M. x<c#}"} 

953 
but also images like @{term "{#x+x. x:#M #}"} and @{term [source] 

954 
"{#x+xx:#M. x<c#}"}, where the latter is currently displayed as 

955 
@{term "{#x+xx:#M. x<c#}"}. 

956 
*} 

957 

59813  958 
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_of M" 
959 
by (metis mem_set_of_iff set_of_image_mset) 

960 

55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55417
diff
changeset

961 
functor image_mset: image_mset 
48023  962 
proof  
963 
fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)" 

964 
proof 

965 
fix A 

966 
show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A" 

967 
by (induct A) simp_all 

968 
qed 

969 
show "image_mset id = id" 

970 
proof 

971 
fix A 

972 
show "image_mset id A = id A" 

973 
by (induct A) simp_all 

974 
qed 

975 
qed 

976 

59813  977 
declare 
978 
image_mset.id [simp] 

979 
image_mset.identity [simp] 

980 

981 
lemma image_mset_id[simp]: "image_mset id x = x" 

982 
unfolding id_def by auto 

983 

984 
lemma image_mset_cong: "(\<And>x. x \<in># M \<Longrightarrow> f x = g x) \<Longrightarrow> {#f x. x \<in># M#} = {#g x. x \<in># M#}" 

985 
by (induct M) auto 

986 

987 
lemma image_mset_cong_pair: 

988 
"(\<forall>x y. (x, y) \<in># M \<longrightarrow> f x y = g x y) \<Longrightarrow> {#f x y. (x, y) \<in># M#} = {#g x y. (x, y) \<in># M#}" 

989 
by (metis image_mset_cong split_cong) 

49717  990 

48023  991 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

992 
subsection {* Further conversions *} 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

993 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

994 
primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

995 
"multiset_of [] = {#}"  
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

996 
"multiset_of (a # x) = multiset_of x + {# a #}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

997 

37107  998 
lemma in_multiset_in_set: 
999 
"x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs" 

1000 
by (induct xs) simp_all 

1001 

1002 
lemma count_multiset_of: 

1003 
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" 

1004 
by (induct xs) simp_all 

1005 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1006 
lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])" 
59813  1007 
by (induct x) auto 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1008 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1009 
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1010 
by (induct x) auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1011 

40950  1012 
lemma set_of_multiset_of[simp]: "set_of (multiset_of x) = set x" 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1013 
by (induct x) auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1014 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1015 
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1016 
by (induct xs) auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1017 

48012  1018 
lemma size_multiset_of [simp]: "size (multiset_of xs) = length xs" 
1019 
by (induct xs) simp_all 

1020 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1021 
lemma multiset_of_append [simp]: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1022 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

1023 
by (induct xs arbitrary: ys) (auto simp: ac_simps) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1024 

40303
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1025 
lemma multiset_of_filter: 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1026 
"multiset_of (filter P xs) = {#x :# multiset_of xs. P x #}" 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1027 
by (induct xs) simp_all 
2d507370e879
lemmas multiset_of_filter, sort_key_by_quicksort
haftmann
parents:
40250
diff
changeset

1028 

40950  1029 
lemma multiset_of_rev [simp]: 
1030 
"multiset_of (rev xs) = multiset_of xs" 

1031 
by (induct xs) simp_all 

1032 

34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1033 
lemma surj_multiset_of: "surj multiset_of" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1034 
apply (unfold surj_def) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1035 
apply (rule allI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1036 
apply (rule_tac M = y in multiset_induct) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1037 
apply auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1038 
apply (rule_tac x = "x # xa" in exI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1039 
apply auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1040 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1041 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1042 
lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1043 
by (induct x) auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1044 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1045 
lemma distinct_count_atmost_1: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1046 
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1047 
apply (induct x, simp, rule iffI, simp_all) 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55129
diff
changeset

1048 
apply (rename_tac a b) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1049 
apply (rule conjI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1050 
apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1051 
apply (erule_tac x = a in allE, simp, clarify) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1052 
apply (erule_tac x = aa in allE, simp) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1053 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1054 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1055 
lemma multiset_of_eq_setD: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1056 
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1057 
by (rule) (auto simp add:multiset_eq_iff set_count_greater_0) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1058 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1059 
lemma set_eq_iff_multiset_of_eq_distinct: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1060 
"distinct x \<Longrightarrow> distinct y \<Longrightarrow> 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1061 
(set x = set y) = (multiset_of x = multiset_of y)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1062 
by (auto simp: multiset_eq_iff distinct_count_atmost_1) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1063 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1064 
lemma set_eq_iff_multiset_of_remdups_eq: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1065 
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1066 
apply (rule iffI) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1067 
apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1068 
apply (drule distinct_remdups [THEN distinct_remdups 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1069 
[THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]]) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1070 
apply simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1071 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1072 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1073 
lemma multiset_of_compl_union [simp]: 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1074 
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

1075 
by (induct xs) (auto simp: ac_simps) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1076 

41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

1077 
lemma count_multiset_of_length_filter: 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1078 
"count (multiset_of xs) x = length (filter (\<lambda>y. x = y) xs)" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1079 
by (induct xs) auto 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1080 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1081 
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1082 
apply (induct ls arbitrary: i) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1083 
apply simp 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1084 
apply (case_tac i) 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1085 
apply auto 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1086 
done 
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1087 

36903  1088 
lemma multiset_of_remove1[simp]: 
1089 
"multiset_of (remove1 a xs) = multiset_of xs  {#a#}" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

1090 
by (induct xs) (auto simp add: multiset_eq_iff) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1091 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1092 
lemma multiset_of_eq_length: 
37107  1093 
assumes "multiset_of xs = multiset_of ys" 
1094 
shows "length xs = length ys" 

48012  1095 
using assms by (metis size_multiset_of) 
34943
e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
haftmann
parents:
33102
diff
changeset

1096 

39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1097 
lemma multiset_of_eq_length_filter: 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1098 
assumes "multiset_of xs = multiset_of ys" 
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1099 
shows "length (filter (\<lambda>x. z = x) xs) = length (filter (\<lambda>y. z = y) ys)" 
48012  1100 
using assms by (metis count_multiset_of) 
39533
91a0ff0ff237
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
haftmann
parents:
39314
diff
changeset

1101 

45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1102 
lemma fold_multiset_equiv: 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1103 
assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1104 
and equiv: "multiset_of xs = multiset_of ys" 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1105 
shows "List.fold f xs = List.fold f ys" 
46921  1106 
using f equiv [symmetric] 
1107 
proof (induct xs arbitrary: ys) 

45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1108 
case Nil then show ?case by simp 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1109 
next 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1110 
case (Cons x xs) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1111 
then have *: "set ys = set (x # xs)" by (blast dest: multiset_of_eq_setD) 
58425  1112 
have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1113 
by (rule Cons.prems(1)) (simp_all add: *) 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1114 
moreover from * have "x \<in> set ys" by simp 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1115 
ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split) 
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1116 
moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps) 
45989
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1117 
ultimately show ?case by simp 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1118 
qed 
b39256df5f8a
moved theorem requiring multisets from More_List to Multiset
haftmann
parents:
45866
diff
changeset

1119 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1120 
lemma multiset_of_insort [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1121 
"multiset_of (insort x xs) = multiset_of xs + {#x#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1122 
by (induct xs) (simp_all add: ac_simps) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1123 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1124 
lemma multiset_of_map: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1125 
"multiset_of (map f xs) = image_mset f (multiset_of xs)" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1126 
by (induct xs) simp_all 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1127 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1128 
definition multiset_of_set :: "'a set \<Rightarrow> 'a multiset" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1129 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1130 
"multiset_of_set = folding.F (\<lambda>x M. {#x#} + M) {#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1131 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1132 
interpretation multiset_of_set!: folding "\<lambda>x M. {#x#} + M" "{#}" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1133 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1134 
"folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1135 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1136 
interpret comp_fun_commute "\<lambda>x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1137 
show "folding (\<lambda>x M. {#x#} + M)" by default (fact comp_fun_commute) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1138 
from multiset_of_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" .. 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1139 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1140 

51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1141 
lemma count_multiset_of_set [simp]: 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1142 
"finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (multiset_of_set A) x = 1" (is "PROP ?P") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1143 
"\<not> finite A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?Q") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1144 
"x \<notin> A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?R") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1145 
proof  
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1146 
{ fix A 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1147 
assume "x \<notin> A" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1148 
have "count (multiset_of_set A) x = 0" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1149 
proof (cases "finite A") 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1150 
case False then show ?thesis by simp 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1151 
next 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1152 
case True from True `x \<notin> A` show ?thesis by (induct A) auto 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1153 
qed 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1154 
} note * = this 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1155 
then show "PROP ?P" "PROP ?Q" "PROP ?R" 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1156 
by (auto elim!: Set.set_insert) 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1157 
qed  {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *} 
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

1158 

59813  1159 
lemma elem_multiset_of_set[simp, intro]: "finite A \<Longrightarrow> x \<in># multiset_of_set A \<longleftrightarrow> x \<in> A" 
1160 
by (induct A rule: finite_induct) simp_all 

1161 

51548
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1162 
context linorder 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1163 
begin 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1164 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1165 
definition sorted_list_of_multiset :: "'a multiset \<Rightarrow> 'a list" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1166 
where 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1167 
"sorted_list_of_multiset M = fold insort [] M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1168 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1169 
lemma sorted_list_of_multiset_empty [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1170 
"sorted_list_of_multiset {#} = []" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1171 
by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1172 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1173 
lemma sorted_list_of_multiset_singleton [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1174 
"sorted_list_of_multiset {#x#} = [x]" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1175 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1176 
interpret comp_fun_commute insort by (fact comp_fun_commute_insort) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1177 
show ?thesis by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1178 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1179 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1180 
lemma sorted_list_of_multiset_insert [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1181 
"sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1182 
proof  
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1183 
interpret comp_fun_commute insort by (fact comp_fun_commute_insort) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1184 
show ?thesis by (simp add: sorted_list_of_multiset_def) 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1185 
qed 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1186 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1187 
end 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1188 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1189 
lemma multiset_of_sorted_list_of_multiset [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1190 
"multiset_of (sorted_list_of_multiset M) = M" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1191 
by (induct M) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1192 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1193 
lemma sorted_list_of_multiset_multiset_of [simp]: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1194 
"sorted_list_of_multiset (multiset_of xs) = sort xs" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1195 
by (induct xs) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1196 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1197 
lemma finite_set_of_multiset_of_set: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1198 
assumes "finite A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1199 
shows "set_of (multiset_of_set A) = A" 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1200 
using assms by (induct A) simp_all 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1201 

757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1202 
lemma infinite_set_of_multiset_of_set: 
757fa47af981
centralized various multiset operations in theory multiset;
haftmann
parents:
51161
diff
changeset

1203 
assumes "\<not> finite A" 
