author  haftmann 
Thu, 12 May 2016 14:38:53 +0200  
changeset 63089  40134ddec3bf 
parent 63088  f2177f5d2aed 
child 63092  a949b2a5f51d 
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 

60500  9 
section \<open>(Finite) multisets\<close> 
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 

60500  15 
subsection \<open>The type of multisets\<close> 
10249  16 

60606  17 
definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}" 
18 

19 
typedef 'a multiset = "multiset :: ('a \<Rightarrow> 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 

60606  28 
lemma multiset_eq_iff: "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

29 
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

30 

60606  31 
lemma multiset_eqI: "(\<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

32 
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

33 

60606  34 
text \<open>Preservation of the representing set @{term multiset}.\<close> 
35 

36 
lemma const0_in_multiset: "(\<lambda>a. 0) \<in> 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

37 
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

38 

60606  39 
lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> 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

40 
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

41 

60606  42 
lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> 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

43 
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

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 
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

46 
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

47 
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

48 
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

49 
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

50 
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

51 
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

52 
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

53 
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

54 

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

55 
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

56 
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

57 
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

58 
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

59 
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

60 
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

61 
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

62 
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

63 
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

64 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
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

66 
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

67 

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

68 

60500  69 
subsection \<open>Representing multisets\<close> 
70 

71 
text \<open>Multiset enumeration\<close> 

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

72 

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

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

75 

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

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

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

78 

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

79 
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

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

81 

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

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

84 

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

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

87 

48008  88 
instance 
60678  89 
by (standard; transfer; simp add: fun_eq_iff) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

90 

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

91 
end 
10249  92 

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

94 
by (rule only1_in_multiset) 
15869  95 

26145  96 
syntax 
60606  97 
"_multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}") 
25507  98 
translations 
99 
"{#x, xs#}" == "{#x#} + {#xs#}" 

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

101 

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

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

103 
by (simp add: zero_multiset.rep_eq) 
10249  104 

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

105 
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

106 
by (simp add: single.rep_eq) 
29901  107 

10249  108 

60500  109 
subsection \<open>Basic operations\<close> 
110 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

111 
subsubsection \<open>Conversion to set and membership\<close> 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

112 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

113 
definition set_mset :: "'a multiset \<Rightarrow> 'a set" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

114 
where "set_mset M = {x. count M x > 0}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

115 

62537
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

116 
abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

117 
where "Melem a M \<equiv> a \<in> set_mset M" 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

118 

7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

119 
notation 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

120 
Melem ("op \<in>#") and 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

121 
Melem ("(_/ \<in># _)" [51, 51] 50) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

122 

7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

123 
notation (ASCII) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

124 
Melem ("op :#") and 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

125 
Melem ("(_/ :# _)" [51, 51] 50) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

126 

7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

127 
abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

128 
where "not_Melem a M \<equiv> a \<notin> set_mset M" 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

129 

7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

130 
notation 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

131 
not_Melem ("op \<notin>#") and 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

132 
not_Melem ("(_/ \<notin># _)" [51, 51] 50) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

133 

7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

134 
notation (ASCII) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

135 
not_Melem ("op ~:#") and 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

136 
not_Melem ("(_/ ~:# _)" [51, 51] 50) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

137 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

138 
context 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

139 
begin 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

140 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

141 
qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

142 
where "Ball M \<equiv> Set.Ball (set_mset M)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

143 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

144 
qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

145 
where "Bex M \<equiv> Set.Bex (set_mset M)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

146 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

147 
end 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

148 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

149 
syntax 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

150 
"_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

151 
"_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

152 

62537
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

153 
syntax (ASCII) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

154 
"_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_:#_./ _)" [0, 0, 10] 10) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

155 
"_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_:#_./ _)" [0, 0, 10] 10) 
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

156 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

157 
translations 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

158 
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

159 
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

160 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

161 
lemma count_eq_zero_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

162 
"count M x = 0 \<longleftrightarrow> x \<notin># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

163 
by (auto simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

164 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

165 
lemma not_in_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

166 
"x \<notin># M \<longleftrightarrow> count M x = 0" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

167 
by (auto simp add: count_eq_zero_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

168 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

169 
lemma count_greater_zero_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

170 
"count M x > 0 \<longleftrightarrow> x \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

171 
by (auto simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

172 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

173 
lemma count_inI: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

174 
assumes "count M x = 0 \<Longrightarrow> False" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

175 
shows "x \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

176 
proof (rule ccontr) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

177 
assume "x \<notin># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

178 
with assms show False by (simp add: not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

179 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

180 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

181 
lemma in_countE: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

182 
assumes "x \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

183 
obtains n where "count M x = Suc n" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

184 
proof  
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

185 
from assms have "count M x > 0" by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

186 
then obtain n where "count M x = Suc n" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

187 
using gr0_conv_Suc by blast 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

188 
with that show thesis . 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

189 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

190 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

191 
lemma count_greater_eq_Suc_zero_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

192 
"count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

193 
by (simp add: Suc_le_eq) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

194 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

195 
lemma count_greater_eq_one_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

196 
"count M x \<ge> 1 \<longleftrightarrow> x \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

197 
by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

198 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

199 
lemma set_mset_empty [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

200 
"set_mset {#} = {}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

201 
by (simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

202 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

203 
lemma set_mset_single [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

204 
"set_mset {#b#} = {b}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

205 
by (simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

206 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

207 
lemma set_mset_eq_empty_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

208 
"set_mset M = {} \<longleftrightarrow> M = {#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

209 
by (auto simp add: multiset_eq_iff count_eq_zero_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

210 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

211 
lemma finite_set_mset [iff]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

212 
"finite (set_mset M)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

213 
using count [of M] by (simp add: multiset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

214 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

215 

60500  216 
subsubsection \<open>Union\<close> 
10249  217 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

218 
lemma count_union [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

219 
"count (M + N) a = count M a + count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

220 
by (simp add: plus_multiset.rep_eq) 
10249  221 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

222 
lemma set_mset_union [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

223 
"set_mset (M + N) = set_mset M \<union> set_mset N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

224 
by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

225 

10249  226 

60500  227 
subsubsection \<open>Difference\<close> 
10249  228 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

229 
instance multiset :: (type) comm_monoid_diff 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

230 
by standard (transfer; simp add: fun_eq_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

231 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

232 
lemma count_diff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

233 
"count (M  N) a = count M a  count N a" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

234 
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

235 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

236 
lemma in_diff_count: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

237 
"a \<in># M  N \<longleftrightarrow> count N a < count M a" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

238 
by (simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

239 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

240 
lemma count_in_diffI: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

241 
assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

242 
shows "x \<in># M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

243 
proof (rule ccontr) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

244 
assume "x \<notin># M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

245 
then have "count N x = (count N x  count M x) + count M x" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

246 
by (simp add: in_diff_count not_less) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

247 
with assms show False by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

248 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

249 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

250 
lemma in_diff_countE: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

251 
assumes "x \<in># M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

252 
obtains n where "count M x = Suc n + count N x" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

253 
proof  
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

254 
from assms have "count M x  count N x > 0" by (simp add: in_diff_count) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

255 
then have "count M x > count N x" by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

256 
then obtain n where "count M x = Suc n + count N x" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

257 
using less_iff_Suc_add by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

258 
with that show thesis . 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

259 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

260 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

261 
lemma in_diffD: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

262 
assumes "a \<in># M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

263 
shows "a \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

264 
proof  
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

265 
have "0 \<le> count N a" by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

266 
also from assms have "count N a < count M a" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

267 
by (simp add: in_diff_count) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

268 
finally show ?thesis by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

269 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

270 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

271 
lemma set_mset_diff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

272 
"set_mset (M  N) = {a. count N a < count M a}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

273 
by (simp add: set_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

274 

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

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

278 
lemma diff_cancel [simp]: "A  A = {#}" 
52289  279 
by (fact Groups.diff_cancel) 
10249  280 

36903  281 
lemma diff_union_cancelR [simp]: "M + N  N = (M::'a multiset)" 
52289  282 
by (fact add_diff_cancel_right') 
10249  283 

36903  284 
lemma diff_union_cancelL [simp]: "N + M  N = (M::'a multiset)" 
52289  285 
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

286 

52289  287 
lemma diff_right_commute: 
60606  288 
fixes M N Q :: "'a multiset" 
289 
shows "M  N  Q = M  Q  N" 

52289  290 
by (fact diff_right_commute) 
291 

292 
lemma diff_add: 

60606  293 
fixes M N Q :: "'a multiset" 
294 
shows "M  (N + Q) = M  N  Q" 

52289  295 
by (rule sym) (fact diff_diff_add) 
58425  296 

60606  297 
lemma insert_DiffM: "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

298 
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

299 

60606  300 
lemma insert_DiffM2 [simp]: "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

301 
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

302 

60606  303 
lemma diff_union_swap: "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

304 
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

305 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

306 
lemma diff_union_single_conv: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

307 
"a \<in># J \<Longrightarrow> I + J  {#a#} = I + (J  {#a#})" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

308 
by (simp add: multiset_eq_iff Suc_le_eq) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

309 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

310 
lemma mset_add [elim?]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

311 
assumes "a \<in># A" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

312 
obtains B where "A = B + {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

313 
proof  
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

314 
from assms have "A = (A  {#a#}) + {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

315 
by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

316 
with that show thesis . 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

317 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

318 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

319 
lemma union_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

320 
"a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

321 
by auto 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

322 

10249  323 

60500  324 
subsubsection \<open>Equality of multisets\<close> 
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

325 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
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

327 
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

328 

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

329 
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

330 
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

331 

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

332 
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

333 
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

334 

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

335 
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

336 
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

337 

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

338 
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

339 
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

340 

60606  341 
lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M  {#x#} = M" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

342 
by (auto simp add: multiset_eq_iff not_in_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

343 

60606  344 
lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M  {#x#} = N \<longleftrightarrow> M = N + {#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

345 
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

346 

60606  347 
lemma union_single_eq_diff: "M + {#x#} = N \<Longrightarrow> M = N  {#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

348 
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

349 

60606  350 
lemma union_single_eq_member: "M + {#x#} = N \<Longrightarrow> x \<in># 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

351 
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

352 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

353 
lemma union_is_single: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

354 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}" 
60606  355 
(is "?lhs = ?rhs") 
46730  356 
proof 
60606  357 
show ?lhs if ?rhs using that by auto 
358 
show ?rhs if ?lhs 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

359 
by (metis Multiset.diff_cancel add.commute add_diff_cancel_left' diff_add_zero diff_single_trivial insert_DiffM that) 
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

360 
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

361 

60606  362 
lemma single_is_union: "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = 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

363 
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

364 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma add_eq_conv_diff: 
60606  366 
"M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#}" 
367 
(is "?lhs \<longleftrightarrow> ?rhs") 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44339
diff
changeset

368 
(* 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

369 
proof 
60606  370 
show ?lhs if ?rhs 
371 
using that 

372 
by (auto simp add: add.assoc add.commute [of "{#b#}"]) 

373 
(drule sym, simp add: add.assoc [symmetric]) 

374 
show ?rhs if ?lhs 

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

375 
proof (cases "a = b") 
60500  376 
case True with \<open>?lhs\<close> show ?thesis 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

377 
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

378 
case False 
60500  379 
from \<open>?lhs\<close> have "a \<in># N + {#b#}" by (rule union_single_eq_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

380 
with False have "a \<in># N" by auto 
60500  381 
moreover from \<open>?lhs\<close> have "M = N + {#b#}  {#a#}" by (rule union_single_eq_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

382 
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

383 
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

384 
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

385 
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

386 

58425  387 
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

388 
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

389 
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

390 
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

391 
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

392 
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

393 
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

394 
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

395 
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

396 
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

397 

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

398 
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

399 
"(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

400 
(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

401 
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

402 

60606  403 
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" 
60678  404 
by (rule exI [where x = "M  {#x#}"]) simp 
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

405 

58425  406 
lemma multiset_add_sub_el_shuffle: 
60606  407 
assumes "c \<in># B" 
408 
and "b \<noteq> c" 

58098  409 
shows "B  {#c#} + {#b#} = B + {#b#}  {#c#}" 
410 
proof  

60500  411 
from \<open>c \<in># B\<close> obtain A where B: "B = A + {#c#}" 
58098  412 
by (blast dest: multi_member_split) 
413 
have "A + {#b#} = A + {#b#} + {#c#}  {#c#}" by simp 

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

417 
qed 

418 

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

419 

60500  420 
subsubsection \<open>Pointwise ordering induced by count\<close> 
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

421 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

422 
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

423 
where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

424 

e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

425 
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

426 
where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

427 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

428 
abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<supseteq>#" 50) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

429 
where "supseteq_mset A B \<equiv> B \<subseteq># A" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

430 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

431 
abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<supset>#" 50) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

432 
where "supset_mset A B \<equiv> B \<subset># A" 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62082
diff
changeset

433 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

434 
notation (input) 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62082
diff
changeset

435 
subseteq_mset (infix "\<le>#" 50) and 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

436 
supseteq_mset (infix "\<ge>#" 50) 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

437 

e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

438 
notation (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

439 
subseteq_mset (infix "<=#" 50) and 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62082
diff
changeset

440 
subset_mset (infix "<#" 50) and 
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62082
diff
changeset

441 
supseteq_mset (infix ">=#" 50) and 
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62082
diff
changeset

442 
supset_mset (infix ">#" 50) 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

443 

60606  444 
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op " "op \<subseteq>#" "op \<subset>#" 
60678  445 
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) 
62837  446 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

447 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

448 
lemma mset_less_eqI: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

449 
"(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

450 
by (simp add: subseteq_mset_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

451 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

452 
lemma mset_less_eq_count: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

453 
"A \<subseteq># B \<Longrightarrow> count A a \<le> count B a" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

454 
by (simp add: subseteq_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

455 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

456 
lemma mset_le_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)" 
60678  457 
unfolding subseteq_mset_def 
458 
apply (rule iffI) 

459 
apply (rule exI [where x = "B  A"]) 

460 
apply (auto intro: multiset_eq_iff [THEN iffD2]) 

461 
done 

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

462 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62366
diff
changeset

463 
interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op " 
60678  464 
by standard (simp, fact mset_le_exists_conv) 
52289  465 

62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

466 
declare subset_mset.zero_order[simp del] 
62837  467 
\<comment> \<open>this removes some simp rules not in the usual order for multisets\<close> 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

468 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

469 
lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

470 
by (fact subset_mset.add_le_cancel_right) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

471 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

472 
lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

473 
by (fact subset_mset.add_le_cancel_left) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

474 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

475 
lemma mset_le_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

476 
by (fact subset_mset.add_mono) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

477 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

478 
lemma mset_le_add_left [simp]: "(A::'a multiset) \<subseteq># A + B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

479 
unfolding subseteq_mset_def by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

480 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

481 
lemma mset_le_add_right [simp]: "B \<subseteq># (A::'a multiset) + B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

482 
unfolding subseteq_mset_def by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

483 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

484 
lemma single_subset_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

485 
"{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

486 
by (auto simp add: subseteq_mset_def Suc_le_eq) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

487 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

488 
lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

489 
by (simp add: subseteq_mset_def Suc_le_eq) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

490 

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

491 
lemma multiset_diff_union_assoc: 
60606  492 
fixes A B C D :: "'a multiset" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

493 
shows "C \<subseteq># B \<Longrightarrow> A + B  C = A + (B  C)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

494 
by (fact subset_mset.diff_add_assoc) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

495 

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

496 
lemma mset_le_multiset_union_diff_commute: 
60606  497 
fixes A B C D :: "'a multiset" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

498 
shows "B \<subseteq># A \<Longrightarrow> A  B + C = A + C  B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

499 
by (fact subset_mset.add_diff_assoc2) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

500 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

501 
lemma diff_le_self[simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

502 
"(M::'a multiset)  N \<subseteq># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

503 
by (simp add: subseteq_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

504 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

505 
lemma mset_leD: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

506 
assumes "A \<subseteq># B" and "x \<in># A" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

507 
shows "x \<in># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

508 
proof  
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

509 
from \<open>x \<in># A\<close> have "count A x > 0" by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

510 
also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

511 
by (simp add: subseteq_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

512 
finally show ?thesis by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

513 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

514 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

515 
lemma mset_lessD: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

516 
"A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

517 
by (auto intro: mset_leD [of A]) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

518 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

519 
lemma set_mset_mono: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

520 
"A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

521 
by (metis mset_leD subsetI) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

522 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

523 
lemma mset_le_insertD: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

524 
"A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># 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

525 
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

526 
apply (simp add: mset_leD) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

527 
apply (clarsimp simp: subset_mset_def subseteq_mset_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

528 
apply safe 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

529 
apply (erule_tac x = a in allE) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

530 
apply (auto split: if_split_asm) 
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

531 
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

532 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

533 
lemma mset_less_insertD: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

534 
"A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

535 
by (rule mset_le_insertD) simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

536 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

537 
lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

538 
by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff) 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

539 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

541 
unfolding mset_le_exists_conv by auto 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

542 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

543 
lemma insert_subset_eq_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

544 
"{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B  {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

545 
using le_diff_conv2 [of "Suc 0" "count B a" "count A a"] 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

546 
apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

547 
apply (rule ccontr) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

548 
apply (auto simp add: not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

549 
done 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

550 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

551 
lemma insert_union_subset_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

552 
"{#a#} + A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B  {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

553 
by (auto simp add: insert_subset_eq_iff subset_mset_def insert_DiffM) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

554 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

555 
lemma subset_eq_diff_conv: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

556 
"A  C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

557 
by (simp add: subseteq_mset_def le_diff_conv) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

558 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

559 
lemma le_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

560 
unfolding mset_le_exists_conv by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

561 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

562 
lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

563 
by (auto simp: subset_mset_def subseteq_mset_def) 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

564 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

566 
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

567 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

568 
lemma mset_less_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

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

570 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

571 
lemma mset_less_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}" 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

572 
by (fact subset_mset.zero_less_iff_neq_zero) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

573 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

574 
lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B  {#c#} \<subset># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

575 
by (auto simp: subset_mset_def elim: mset_add) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

576 

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

577 

60500  578 
subsubsection \<open>Intersection\<close> 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

579 

60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

580 
definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

581 
multiset_inter_def: "inf_subset_mset A B = A  (A  B)" 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

582 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

583 
interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#" 
46921  584 
proof  
60678  585 
have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n  (n  q)" for m n q :: nat 
586 
by arith 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

587 
show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#" 
60678  588 
by standard (auto simp add: multiset_inter_def subseteq_mset_def) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

589 
qed 
62837  590 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
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

591 

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

592 
lemma multiset_inter_count [simp]: 
60606  593 
fixes A B :: "'a multiset" 
594 
shows "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

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

596 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

597 
lemma set_mset_inter [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

598 
"set_mset (A #\<inter> B) = set_mset A \<inter> set_mset B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

599 
by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

600 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

601 
lemma diff_intersect_left_idem [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

602 
"M  M #\<inter> N = M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

603 
by (simp add: multiset_eq_iff min_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

604 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

605 
lemma diff_intersect_right_idem [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

606 
"M  N #\<inter> M = M  N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

607 
by (simp add: multiset_eq_iff min_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

608 

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

609 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
46730  610 
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

611 

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

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

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

614 
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

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

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

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

619 
then have "count B x = 0 \<or> count C x = 0" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

620 
unfolding min_def by (auto split: if_splits) 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

621 
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

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

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

624 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

625 
lemma disjunct_not_in: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

626 
"A #\<inter> B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q") 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

627 
proof 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

628 
assume ?P 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

629 
show ?Q 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

630 
proof 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

631 
fix a 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

632 
from \<open>?P\<close> have "min (count A a) (count B a) = 0" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

633 
by (simp add: multiset_eq_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

634 
then have "count A a = 0 \<or> count B a = 0" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

635 
by (cases "count A a \<le> count B a") (simp_all add: min_def) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

636 
then show "a \<notin># A \<or> a \<notin># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

637 
by (simp add: not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

638 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

639 
next 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

640 
assume ?Q 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

641 
show ?P 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

642 
proof (rule multiset_eqI) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

643 
fix a 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

644 
from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

645 
by (auto simp add: not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

646 
then show "count (A #\<inter> B) a = count {#} a" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

647 
by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

648 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

649 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

650 

60606  651 
lemma empty_inter [simp]: "{#} #\<inter> M = {#}" 
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

652 
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

653 

60606  654 
lemma inter_empty [simp]: "M #\<inter> {#} = {#}" 
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

655 
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

656 

60606  657 
lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

659 

60606  660 
lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N  {#x#})) + {#x#}" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

662 

60606  663 
lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

665 

60606  666 
lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N  {#x#}) #\<inter> M) + {#x#}" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

667 
by (auto simp add: multiset_eq_iff elim: mset_add) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

668 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

669 
lemma disjunct_set_mset_diff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

670 
assumes "M #\<inter> N = {#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

671 
shows "set_mset (M  N) = set_mset M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

672 
proof (rule set_eqI) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

673 
fix a 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

674 
from assms have "a \<notin># M \<or> a \<notin># N" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

675 
by (simp add: disjunct_not_in) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

676 
then show "a \<in># M  N \<longleftrightarrow> a \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

677 
by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

678 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

679 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

680 
lemma at_most_one_mset_mset_diff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

681 
assumes "a \<notin># M  {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

682 
shows "set_mset (M  {#a#}) = set_mset M  {a}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

683 
using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

684 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

685 
lemma more_than_one_mset_mset_diff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

686 
assumes "a \<in># M  {#a#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

687 
shows "set_mset (M  {#a#}) = set_mset M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

688 
proof (rule set_eqI) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

689 
fix b 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

690 
have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

691 
then show "b \<in># M  {#a#} \<longleftrightarrow> b \<in># M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

692 
using assms by (auto simp add: in_diff_count) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

693 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

694 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

695 
lemma inter_iff: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

696 
"a \<in># A #\<inter> B \<longleftrightarrow> a \<in># A \<and> a \<in># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

697 
by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

698 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

699 
lemma inter_union_distrib_left: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

700 
"A #\<inter> B + C = (A + C) #\<inter> (B + C)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

701 
by (simp add: multiset_eq_iff min_add_distrib_left) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

702 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

703 
lemma inter_union_distrib_right: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

704 
"C + A #\<inter> B = (C + A) #\<inter> (C + B)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

705 
using inter_union_distrib_left [of A B C] by (simp add: ac_simps) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

706 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

707 
lemma inter_subset_eq_union: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

708 
"A #\<inter> B \<subseteq># A + B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

709 
by (auto simp add: subseteq_mset_def) 
51600
197e25f13f0c
default implementation of multisets by list with reasonable coverage of operations on multisets
haftmann
parents:
51599
diff
changeset

710 

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

711 

60500  712 
subsubsection \<open>Bounded union\<close> 
60678  713 

714 
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70) 

62837  715 
where "sup_subset_mset A B = A + (B  A)" \<comment> \<open>FIXME irregular fact name\<close> 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

716 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

717 
interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#" 
51623  718 
proof  
60678  719 
have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q  m) \<le> n" for m n q :: nat 
720 
by arith 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

721 
show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#" 
60678  722 
by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) 
51623  723 
qed 
62837  724 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
725 

726 
lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close> 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

727 
"count (A #\<union> B) x = max (count A x) (count B x)" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

728 
by (simp add: sup_subset_mset_def) 
51623  729 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

730 
lemma set_mset_sup [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

731 
"set_mset (A #\<union> B) = set_mset A \<union> set_mset B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

732 
by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

733 
(auto simp add: not_in_iff elim: mset_add) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

734 

60606  735 
lemma empty_sup [simp]: "{#} #\<union> M = M" 
51623  736 
by (simp add: multiset_eq_iff) 
737 

60606  738 
lemma sup_empty [simp]: "M #\<union> {#} = M" 
51623  739 
by (simp add: multiset_eq_iff) 
740 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

741 
lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

742 
by (simp add: multiset_eq_iff not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

743 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

744 
lemma sup_union_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N  {#x#})) + {#x#}" 
51623  745 
by (simp add: multiset_eq_iff) 
746 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

747 
lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

748 
by (simp add: multiset_eq_iff not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

749 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

750 
lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N  {#x#}) #\<union> M) + {#x#}" 
51623  751 
by (simp add: multiset_eq_iff) 
752 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

753 
lemma sup_union_distrib_left: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

754 
"A #\<union> B + C = (A + C) #\<union> (B + C)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

755 
by (simp add: multiset_eq_iff max_add_distrib_left) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

756 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

757 
lemma union_sup_distrib_right: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

758 
"C + A #\<union> B = (C + A) #\<union> (C + B)" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

759 
using sup_union_distrib_left [of A B C] by (simp add: ac_simps) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

760 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

761 
lemma union_diff_inter_eq_sup: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

762 
"A + B  A #\<inter> B = A #\<union> B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

763 
by (auto simp add: multiset_eq_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

764 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

765 
lemma union_diff_sup_eq_inter: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

766 
"A + B  A #\<union> B = A #\<inter> B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

767 
by (auto simp add: multiset_eq_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

768 

51623  769 

60500  770 
subsubsection \<open>Subset is an order\<close> 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

771 

60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

772 
interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto 
51623  773 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

774 

60500  775 
subsubsection \<open>Filter (with comprehension syntax)\<close> 
776 

777 
text \<open>Multiset comprehension\<close> 

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

778 

59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

779 
lift_definition filter_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" 
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

780 
is "\<lambda>P M. \<lambda>x. if P x then M x else 0" 
47429
ec64d94cbf9c
multiset operations are defined with lift_definitions;
bulwahn
parents:
47308
diff
changeset

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

782 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

783 
syntax (ASCII) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

784 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})") 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

785 
syntax 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

786 
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})") 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

787 
translations 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

788 
"{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

789 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

790 
lemma count_filter_mset [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

791 
"count (filter_mset P M) a = (if P a then count M a else 0)" 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

792 
by (simp add: filter_mset.rep_eq) 
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

793 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

794 
lemma set_mset_filter [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

795 
"set_mset (filter_mset P M) = {a \<in> set_mset M. P a}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

796 
by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

797 

60606  798 
lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}" 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

799 
by (rule multiset_eqI) simp 
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

800 

60606  801 
lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39301
diff
changeset

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

803 

60606  804 
lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N" 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

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

806 

60606  807 
lemma filter_diff_mset [simp]: "filter_mset P (M  N) = filter_mset P M  filter_mset 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

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

809 

60606  810 
lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N" 
41069
6fabc0414055
name filter operation just filter (c.f. List.filter and list comprehension syntax)
haftmann
parents:
40968
diff
changeset

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

812 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

813 
lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M" 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

814 
by (simp add: mset_less_eqI) 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
59999
diff
changeset

815 

60606  816 
lemma multiset_filter_mono: 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

817 
assumes "A \<subseteq># B" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

818 
shows "filter_mset f A \<subseteq># filter_mset f B" 
58035  819 
proof  
820 
from assms[unfolded mset_le_exists_conv] 

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

822 
show ?thesis unfolding B by auto 

823 
qed 

824 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

825 
lemma filter_mset_eq_conv: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

826 
"filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M  N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q") 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

827 
proof 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

828 
assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

829 
next 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

830 
assume ?Q 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

831 
then obtain Q where M: "M = N + Q" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

832 
by (auto simp add: mset_le_exists_conv) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

833 
then have MN: "M  N = Q" by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

834 
show ?P 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

835 
proof (rule multiset_eqI) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

836 
fix a 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

837 
from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

838 
by auto 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

839 
show "count (filter_mset P M) a = count N a" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

840 
proof (cases "a \<in># M") 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

841 
case True 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

842 
with * show ?thesis 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

843 
by (simp add: not_in_iff M) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

844 
next 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

845 
case False then have "count M a = 0" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

846 
by (simp add: not_in_iff) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

847 
with M show ?thesis by simp 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

848 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

849 
qed 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

850 
qed 
59813  851 

852 

60500  853 
subsubsection \<open>Size\<close> 
10249  854 

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

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

858 
by (auto simp: wcount_def add_mult_distrib) 

859 

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

60495  861 
"size_multiset f M = setsum (wcount f M) (set_mset M)" 
56656  862 

863 
lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def] 

864 

60606  865 
instantiation multiset :: (type) size 
866 
begin 

867 

56656  868 
definition size_multiset where 
869 
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

870 
instance .. 
60606  871 

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

872 
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

873 

56656  874 
lemmas size_multiset_overloaded_eq = 
875 
size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified] 

876 

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

878 
by (simp add: size_multiset_def) 

879 

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

880 
lemma size_empty [simp]: "size {#} = 0" 
56656  881 
by (simp add: size_multiset_overloaded_def) 
882 

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

884 
by (simp add: size_multiset_eq) 

10249  885 

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

886 
lemma size_single [simp]: "size {#b#} = 1" 
56656  887 
by (simp add: size_multiset_overloaded_def) 
888 

889 
lemma setsum_wcount_Int: 

60495  890 
"finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

891 
by (induct rule: finite_induct) 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

892 
(simp_all add: Int_insert_left wcount_def count_eq_zero_iff) 
56656  893 

894 
lemma size_multiset_union [simp]: 

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

57418  896 
apply (simp add: size_multiset_def setsum_Un_nat setsum.distrib setsum_wcount_Int wcount_union) 
56656  897 
apply (subst Int_commute) 
898 
apply (simp add: setsum_wcount_Int) 

26178  899 
done 
10249  900 

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

901 
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" 
56656  902 
by (auto simp add: size_multiset_overloaded_def) 
903 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

904 
lemma size_multiset_eq_0_iff_empty [iff]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

905 
"size_multiset f M = 0 \<longleftrightarrow> M = {#}" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

906 
by (auto simp add: size_multiset_eq count_eq_zero_iff) 
10249  907 

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

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

26178  912 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  913 

60607  914 
lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M" 
56656  915 
apply (unfold size_multiset_overloaded_eq) 
26178  916 
apply (drule setsum_SucD) 
917 
apply auto 

918 
done 

10249  919 

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

920 
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

921 
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

922 
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

923 
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

924 
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

925 
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

926 
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

927 
then show ?thesis by blast 
23611  928 
qed 
15869  929 

60606  930 
lemma size_mset_mono: 
931 
fixes A B :: "'a multiset" 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

932 
assumes "A \<subseteq># B" 
60606  933 
shows "size A \<le> size B" 
59949  934 
proof  
935 
from assms[unfolded mset_le_exists_conv] 

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

60606  937 
show ?thesis unfolding B by (induct C) auto 
59949  938 
qed 
939 

59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

940 
lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M" 
59949  941 
by (rule size_mset_mono[OF multiset_filter_subset]) 
942 

943 
lemma size_Diff_submset: 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

944 
"M \<subseteq># M' \<Longrightarrow> size (M'  M) = size M'  size(M::'a multiset)" 
59949  945 
by (metis add_diff_cancel_left' size_union mset_le_exists_conv) 
26016  946 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

947 

60500  948 
subsection \<open>Induction and case splits\<close> 
10249  949 

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

953 
shows "P M" 

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

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

956 
next 

957 
case (Suc k) 

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

60500  959 
using \<open>Suc k = size M\<close> [symmetric] 
48009  960 
using size_eq_Suc_imp_eq_union by fast 
961 
with Suc add show "P M" by simp 

10249  962 
qed 
963 

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

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

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

970 
using assms by (induct M) simp_all 

25610  971 

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

972 
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

973 
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

974 

60607  975 
lemma multiset_partition: "M = {# x\<in>#M. P x #} + {# x\<in>#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

976 
apply (subst multiset_eq_iff) 
26178  977 
apply auto 
978 
done 

10249  979 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

980 
lemma mset_less_size: "(A::'a multiset) \<subset># 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

981 
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

982 
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

983 
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) 
58425  984 
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

985 
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

986 
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

987 
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

988 
case (add S x T) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

989 
have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

990 
have SxsubT: "S + {#x#} \<subset># T" by fact 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

991 
then have "x \<in># T" and "S \<subset># T" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

992 
by (auto dest: mset_less_insertD) 
58425  993 
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

994 
by (blast dest: multi_member_split) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

995 
then have "S \<subset># 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

996 
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

997 
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

998 
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

999 
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

1000 

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

1003 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1004 

60500  1005 
subsubsection \<open>Strong induction and subset induction for multisets\<close> 
1006 

1007 
text \<open>Wellfoundedness of strict subset relation\<close> 

58098  1008 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1009 
lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># 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

1010 
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

1011 
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

1012 
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

1013 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 
lemma full_multiset_induct [case_names less]: 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1015 
assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># 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

1016 
shows "P B" 
58098  1017 
apply (rule wf_less_mset_rel [THEN wf_induct]) 
1018 
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

1019 
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

1020 

e97b22500a5c
cleanup of Multiset.thy: less duplication, tuned and 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 multi_subset_induct [consumes 2, case_names empty add]: 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1022 
assumes "F \<subseteq># A" 
60606  1023 
and empty: "P {#}" 
1024 
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" 

1025 
shows "P F" 

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

1026 
proof  
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1027 
from \<open>F \<subseteq># A\<close> 
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

1028 
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

1029 
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

1030 
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

1031 
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

1032 
fix x F 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1033 
assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># 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

1034 
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

1035 
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

1036 
from i show "x \<in># A" by (auto dest: mset_le_insertD) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1037 
from i have "F \<subseteq># 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

1038 
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

1039 
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

1040 
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

1041 
qed 
26145  1042 

17161  1043 

60500  1044 
subsection \<open>The fold combinator\<close> 
48023  1045 

59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

1046 
definition fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" 
48023  1047 
where 
60495  1048 
"fold_mset f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_mset M)" 
48023  1049 

60606  1050 
lemma fold_mset_empty [simp]: "fold_mset f s {#} = s" 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

1051 
by (simp add: fold_mset_def) 
48023  1052 

1053 
context comp_fun_commute 

1054 
begin 

1055 

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

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

1058 
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

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

1060 
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

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

1062 
show ?thesis 
60495  1063 
proof (cases "x \<in> set_mset M") 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1064 
case False 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1065 
then have *: "count (M + {#x#}) x = 1" 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1066 
by (simp add: not_in_iff) 
60495  1067 
from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) = 
1068 
Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)" 

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

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

1070 
with False * show ?thesis 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

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

1073 
case True 
63040  1074 
define N where "N = set_mset M  {x}" 
60495  1075 
from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1076 
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

1077 
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

1078 
by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

1079 
with * show ?thesis by (simp add: fold_mset_def del: count_union) simp 
48023  1080 
qed 
1081 
qed 

1082 

60606  1083 
corollary fold_mset_single [simp]: "fold_mset f s {#x#} = f x s" 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1084 
proof  
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

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

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

1087 
qed 
48023  1088 

60606  1089 
lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M" 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1090 
by (induct M) (simp_all add: fold_mset_insert fun_left_comm) 
48023  1091 

60606  1092 
lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N" 
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49717
diff
changeset

1093 
proof (induct M) 
48023  1094 
case empty then show ?case by simp 
1095 
next 

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

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

1097 
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

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

1099 
with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm) 
48023  1100 
qed 
1101 

1102 
lemma fold_mset_fusion: 

1103 
assumes "comp_fun_commute g" 

60606  1104 
and *: "\<And>x y. h (g x y) = f x (h y)" 
1105 
shows "h (fold_mset g w A) = fold_mset f (h w) A" 

48023  1106 
proof  
1107 
interpret comp_fun_commute g by (fact assms) 

60606  1108 
from * show ?thesis by (induct A) auto 
48023  1109 
qed 
1110 

1111 
end 

1112 

60500  1113 
text \<open> 
48023  1114 
A note on code generation: When defining some function containing a 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

1115 
subterm @{term "fold_mset F"}, code generation is not automatic. When 
61585  1116 
interpreting locale \<open>left_commutative\<close> with \<open>F\<close>, the 
59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59986
diff
changeset

1117 
would be code thms for @{const fold_mset} become thms like 
61585  1118 
@{term "fold_mset F z {#} = z"} where \<open>F\<close> is not a pattern but 
48023  1119 
contains defined symbols, i.e.\ is not a code thm. Hence a separate 
61585  1120 
constant with its own code thms needs to be introduced for \<open>F\<close>. See the image operator below. 
60500  1121 
\<close> 
1122 

1123 

1124 
subsection \<open>Image\<close> 

48023  1125 

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

60607  1127 
"image_mset f = fold_mset (plus \<circ> single \<circ> f) {#}" 
1128 

1129 
lemma comp_fun_commute_mset_image: "comp_fun_commute (plus \<circ> single \<circ> f)" 

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

1131 
qed (simp add: ac_simps fun_eq_iff) 
48023  1132 

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

49823  1134 
by (simp add: image_mset_def) 
48023  1135 

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

49823  1137 
proof  
60607  1138 
interpret comp_fun_commute "plus \<circ> single \<circ> f" 
49823  1139 
by (fact comp_fun_commute_mset_image) 
1140 
show ?thesis by (simp add: image_mset_def) 

1141 
qed 

48023  1142 

60606  1143 
lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N" 
49823  1144 
proof  
60607  1145 
interpret comp_fun_commute "plus \<circ> single \<circ> f" 
49823  1146 
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

1147 
show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps) 
49823  1148 
qed 
1149 

60606  1150 
corollary image_mset_insert: "image_mset f (M + {#a#}) = image_mset f M + {#f a#}" 
49823  1151 
by simp 
48023  1152 

60606  1153 
lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)" 
49823  1154 
by (induct M) simp_all 
48040  1155 

60606  1156 
lemma size_image_mset [simp]: "size (image_mset f M) = size M" 
49823  1157 
by (induct M) simp_all 
48023  1158 

60606  1159 
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}" 
49823  1160 
by (cases M) auto 
48023  1161 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1162 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1163 
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ :# _#})") 
48023  1164 
syntax 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1165 
"_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ \<in># _#})") 
59813  1166 
translations 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1167 
"{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1168 

e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1169 
syntax (ASCII) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1170 
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/  _ :# _./ _#})") 
48023  1171 
syntax 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

1172 
"_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/  _ \<in># _./ _#})") 
59813  1173 
translations 
60606  1174 
"{#e  x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}" 
59813  1175 

60500  1176 
text \<open> 
60607  1177 
This allows to write not just filters like @{term "{#x\<in>#M. x<c#}"} 
1178 
but also images like @{term "{#x+x. x\<in>#M #}"} and @{term [source] 

1179 
"{#x+xx\<in>#M. x<c#}"}, where the latter is currently displayed as 

1180 
@{term "{#x+xx\<in>#M. x<c#}"}. 

60500  1181 
\<close> 
48023  1182 

60495  1183 
lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

1184 
by (metis set_image_mset) 
59813  1185 

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

1186 
functor image_mset: image_mset 
48023  1187 
proof  
1188 
fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)" 

1189 
proof 

1190 
fix A 

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

1192 
by (induct A) simp_all 

1193 
qed 

1194 
show "image_mset id = id" 

1195 
proof 

1196 
fix A 

1197 
show "image_mset id A = id A" 

1198 
by (induct A) simp_all 

1199 
qed 

1200 
qed 

1201 

59813  1202 
declare 
1203 
image_mset.id [simp] 

1204 
image_mset.identity [simp] 

1205 

1206 
lemma image_mset_id[simp]: "image 