author  desharna 
Mon, 23 May 2022 10:13:08 +0200  
changeset 75459  ec4b514bcfad 
parent 75457  cbf011677235 
child 75467  9e34819a7ca1 
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 

74803  7 
Author: Martin Desharnais, MPIINF Saarbruecken 
10249  8 
*) 
9 

65048  10 
section \<open>(Finite) Multisets\<close> 
10249  11 

15131  12 
theory Multiset 
74865
b5031a8f7718
added lemmas irreflp_{less,greater} to preorder and {trans,irrefl}_mult{,p} to Multiset
desharna
parents:
74864
diff
changeset

13 
imports Cancellation 
15131  14 
begin 
10249  15 

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

73270  18 
typedef 'a multiset = \<open>{f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}\<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

19 
morphisms count Abs_multiset 
10249  20 
proof 
73270  21 
show \<open>(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}\<close> 
22 
by simp 

10249  23 
qed 
24 

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

25 
setup_lifting type_definition_multiset 
19086  26 

73270  27 
lemma count_Abs_multiset: 
28 
\<open>count (Abs_multiset f) = f\<close> if \<open>finite {x. f x > 0}\<close> 

29 
by (rule Abs_multiset_inverse) (simp add: that) 

30 

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

32 
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

33 

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

35 
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

36 

69593  37 
text \<open>Preservation of the representing set \<^term>\<open>multiset\<close>.\<close> 
60606  38 

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

39 
lemma diff_preserves_multiset: 
73270  40 
\<open>finite {x. 0 < M x  N x}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close> 
41 
using that by (rule rev_finite_subset) 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

42 

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

43 
lemma filter_preserves_multiset: 
73270  44 
\<open>finite {x. 0 < (if P x then M x else 0)}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close> 
45 
using that by (rule rev_finite_subset) auto 

46 

47 
lemmas in_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

48 

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

60500  50 
subsection \<open>Representing multisets\<close> 
51 

52 
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

53 

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

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

56 

73393  57 
lift_definition zero_multiset :: \<open>'a multiset\<close> 
58 
is \<open>\<lambda>a. 0\<close> 

73270  59 
by simp 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

60 

73393  61 
abbreviation empty_mset :: \<open>'a multiset\<close> (\<open>{#}\<close>) 
62 
where \<open>empty_mset \<equiv> 0\<close> 

63 

64 
lift_definition plus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close> 

65 
is \<open>\<lambda>M N a. M a + N a\<close> 

73270  66 
by simp 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

67 

73393  68 
lift_definition minus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close> 
69 
is \<open>\<lambda>M N a. M a  N a\<close> 

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

71 

48008  72 
instance 
73270  73 
by (standard; transfer) (simp_all add: fun_eq_iff) 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

74 

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

75 
end 
10249  76 

63195  77 
context 
78 
begin 

79 

80 
qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where 

81 
[code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}" 

82 

83 
end 

84 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

85 
lemma add_mset_in_multiset: 
73270  86 
\<open>finite {x. 0 < (if x = a then Suc (M x) else M x)}\<close> 
87 
if \<open>finite {x. 0 < M x}\<close> 

88 
using that by (simp add: flip: insert_Collect) 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

89 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

90 
lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

91 
"\<lambda>a M b. if b = a then Suc (M b) else M b" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

92 
by (rule add_mset_in_multiset) 
15869  93 

26145  94 
syntax 
60606  95 
"_multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}") 
25507  96 
translations 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

97 
"{#x, xs#}" == "CONST add_mset x {#xs#}" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

98 
"{#x#}" == "CONST add_mset x {#}" 
25507  99 

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

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

101 
by (simp add: zero_multiset.rep_eq) 
10249  102 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

103 
lemma count_add_mset [simp]: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

104 
"count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

105 
by (simp add: add_mset.rep_eq) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

106 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

107 
lemma count_single: "count {#b#} a = (if b = a then 1 else 0)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

108 
by simp 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

109 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

110 
lemma 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

111 
add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

112 
empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

113 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

114 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

115 
lemma add_mset_add_mset_same_iff [simp]: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

116 
"add_mset a A = add_mset a B \<longleftrightarrow> A = B" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

117 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

118 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

119 
lemma add_mset_commute: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

120 
"add_mset x (add_mset y M) = add_mset y (add_mset x M)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

121 
by (auto simp: multiset_eq_iff) 
29901  122 

10249  123 

60500  124 
subsection \<open>Basic operations\<close> 
125 

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

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

127 

73393  128 
definition set_mset :: \<open>'a multiset \<Rightarrow> 'a set\<close> 
129 
where \<open>set_mset M = {x. count M x > 0}\<close> 

130 

131 
abbreviation member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close> 

132 
where \<open>member_mset a M \<equiv> a \<in> set_mset M\<close> 

62537
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 
73393  135 
member_mset (\<open>'(\<in>#')\<close>) and 
73394  136 
member_mset (\<open>(_/ \<in># _)\<close> [50, 51] 50) 
62537
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

137 

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

138 
notation (ASCII) 
73393  139 
member_mset (\<open>'(:#')\<close>) and 
73394  140 
member_mset (\<open>(_/ :# _)\<close> [50, 51] 50) 
73393  141 

142 
abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close> 

143 
where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close> 

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

144 

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

145 
notation 
73393  146 
not_member_mset (\<open>'(\<notin>#')\<close>) and 
73394  147 
not_member_mset (\<open>(_/ \<notin># _)\<close> [50, 51] 50) 
62537
7a9aa69f9b38
syntax for multiset membership modelled after syntax for set membership
haftmann
parents:
62430
diff
changeset

148 

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

149 
notation (ASCII) 
73393  150 
not_member_mset (\<open>'(~:#')\<close>) and 
73394  151 
not_member_mset (\<open>(_/ ~:# _)\<close> [50, 51] 50) 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

152 

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

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

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

155 

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

156 
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

157 
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

158 

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

159 
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

160 
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

161 

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

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

163 

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

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

165 
"_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

166 
"_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

167 

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

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

169 
"_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

170 
"_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

171 

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

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

173 
"\<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

174 
"\<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

175 

71917
4c5778d8a53d
should have been copied across from Set.thy as well for better printing
nipkow
parents:
71398
diff
changeset

176 
print_translation \<open> 
4c5778d8a53d
should have been copied across from Set.thy as well for better printing
nipkow
parents:
71398
diff
changeset

177 
[Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Ball\<close> \<^syntax_const>\<open>_MBall\<close>, 
4c5778d8a53d
should have been copied across from Set.thy as well for better printing
nipkow
parents:
71398
diff
changeset

178 
Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>Multiset.Bex\<close> \<^syntax_const>\<open>_MBex\<close>] 
4c5778d8a53d
should have been copied across from Set.thy as well for better printing
nipkow
parents:
71398
diff
changeset

179 
\<close> \<comment> \<open>to avoid etacontraction of body\<close> 
4c5778d8a53d
should have been copied across from Set.thy as well for better printing
nipkow
parents:
71398
diff
changeset

180 

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

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

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

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

184 

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

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

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

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

188 

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

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

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

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

192 

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

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

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

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

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

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

198 
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

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

200 

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

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

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

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

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

205 
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

206 
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

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

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

209 
qed 
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 count_greater_eq_Suc_zero_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

213 
by (simp add: Suc_le_eq) 
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 
lemma count_greater_eq_one_iff [simp]: 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

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

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

218 

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

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

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

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

222 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

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

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

226 

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

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

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

229 
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

230 

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

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

232 
"finite (set_mset M)" 
73270  233 
using count [of M] by simp 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

234 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

235 
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close> 
68406  236 
by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

237 

63924  238 
lemma multiset_nonemptyE [elim]: 
239 
assumes "A \<noteq> {#}" 

240 
obtains x where "x \<in># A" 

241 
proof  

242 
have "\<exists>x. x \<in># A" by (rule ccontr) (insert assms, auto) 

243 
with that show ?thesis by blast 

244 
qed 

245 

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

246 

60500  247 
subsubsection \<open>Union\<close> 
10249  248 

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

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

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

251 
by (simp add: plus_multiset.rep_eq) 
10249  252 

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

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

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

255 
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

256 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

257 
lemma union_mset_add_mset_left [simp]: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

258 
"add_mset a A + B = add_mset a (A + B)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

259 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

260 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

261 
lemma union_mset_add_mset_right [simp]: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

262 
"A + add_mset a B = add_mset a (A + B)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

263 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

264 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

265 
lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

266 
by (subst union_mset_add_mset_right, subst add.comm_neutral) standard 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

267 

10249  268 

60500  269 
subsubsection \<open>Difference\<close> 
10249  270 

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

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

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

273 

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

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

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

276 
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

277 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

278 
lemma add_mset_diff_bothsides: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

279 
\<open>add_mset a M  add_mset a A = M  A\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

280 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

281 

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

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

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

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

285 

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

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

287 
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

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

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

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

291 
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

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

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

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

295 

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

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

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

298 
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

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

300 
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

301 
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

302 
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

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

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

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

306 

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

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

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

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

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

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

312 
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

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

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

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

316 

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

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

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

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

320 

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

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

324 
lemma diff_cancel: "A  A = {#}" 
52289  325 
by (fact Groups.diff_cancel) 
10249  326 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

327 
lemma diff_union_cancelR: "M + N  N = (M::'a multiset)" 
52289  328 
by (fact add_diff_cancel_right') 
10249  329 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

330 
lemma diff_union_cancelL: "N + M  N = (M::'a multiset)" 
52289  331 
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

332 

52289  333 
lemma diff_right_commute: 
60606  334 
fixes M N Q :: "'a multiset" 
335 
shows "M  N  Q = M  Q  N" 

52289  336 
by (fact diff_right_commute) 
337 

338 
lemma diff_add: 

60606  339 
fixes M N Q :: "'a multiset" 
340 
shows "M  (N + Q) = M  N  Q" 

52289  341 
by (rule sym) (fact diff_diff_add) 
58425  342 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

343 
lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset 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

344 
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

345 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

346 
lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M  {#x#}) + {#x#} = M" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

347 
by simp 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

348 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

349 
lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M  {#a#}) = add_mset b M  {#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

350 
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

351 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

352 
lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M  A = add_mset b (M  A)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

353 
by (auto simp add: multiset_eq_iff simp: not_in_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

354 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

355 
lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M  {#y#} = add_mset x (M  {#y#})" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

356 
by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

357 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

358 
lemma diff_diff_add_mset [simp]: "(M::'a multiset)  N  P = M  (N + P)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

359 
by (rule diff_diff_add) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

360 

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

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

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

363 
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

364 

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

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

366 
assumes "a \<in># A" 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

367 
obtains B where "A = add_mset a B" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

368 
proof  
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

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

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

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

373 

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

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

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

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

377 

10249  378 

66425  379 
subsubsection \<open>Min and Max\<close> 
380 

381 
abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where 

382 
"Min_mset m \<equiv> Min (set_mset m)" 

383 

384 
abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where 

385 
"Max_mset m \<equiv> Max (set_mset m)" 

386 

387 

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

389 

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

391 
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

392 

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

394 
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

395 

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

397 
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

398 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

399 
lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<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

400 
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

401 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

402 
lemma add_mset_remove_trivial [simp]: \<open>add_mset x M  {#x#} = M\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

403 
by (auto simp: multiset_eq_iff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

404 

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

406 
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

407 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

408 
lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M  {#x#} = N \<longleftrightarrow> M = add_mset x N" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

409 
by auto 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

410 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

411 
lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N  {#x#}" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

412 
unfolding add_mset_add_single[of _ M] by (fact add_implies_diff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

413 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

414 
lemma union_single_eq_member: "add_mset x M = 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

415 
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

416 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

417 
lemma add_mset_remove_trivial_If: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

418 
"add_mset a (N  {#a#}) = (if a \<in># N then N else add_mset a N)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

419 
by (simp add: diff_single_trivial) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

420 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

421 
lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N  {#a#}) \<longleftrightarrow> a \<in># N\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

422 
by (auto simp: add_mset_remove_trivial_If) 
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

423 

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

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

425 
"M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}" 
60606  426 
(is "?lhs = ?rhs") 
46730  427 
proof 
60606  428 
show ?lhs if ?rhs using that by auto 
429 
show ?rhs if ?lhs 

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

430 
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

431 
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

432 

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

434 
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

435 

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

436 
lemma add_eq_conv_diff: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

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

440 
proof 
60606  441 
show ?lhs if ?rhs 
442 
using that 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

443 
by (auto simp add: add_mset_commute[of a b]) 
60606  444 
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

445 
proof (cases "a = b") 
60500  446 
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

447 
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

448 
case False 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

449 
from \<open>?lhs\<close> have "a \<in># add_mset b N" 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

450 
with False have "a \<in># N" by auto 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

451 
moreover from \<open>?lhs\<close> have "M = add_mset b N  {#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

452 
moreover note False 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

453 
ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#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

454 
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

455 
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

456 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

457 
lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

458 
by (auto simp: add_eq_conv_diff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

459 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

460 
lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

461 
by (auto simp: add_eq_conv_diff) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

462 

58425  463 
lemma insert_noteq_member: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

465 
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

466 
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

467 
proof  
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

468 
have "c \<in># add_mset c C" 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

469 
have nc: "\<not> c \<in># {#b#}" using bnotc by simp 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

470 
then have "c \<in># add_mset b B" using BC 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

471 
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

472 
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

473 

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

474 
lemma add_eq_conv_ex: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

475 
"(add_mset a M = add_mset b N) = 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

476 
(M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))" 
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

477 
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

478 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

479 
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A" 
60678  480 
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

481 

58425  482 
lemma multiset_add_sub_el_shuffle: 
60606  483 
assumes "c \<in># B" 
484 
and "b \<noteq> c" 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

485 
shows "add_mset b (B  {#c#}) = add_mset b B  {#c#}" 
58098  486 
proof  
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

487 
from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A" 
58098  488 
by (blast dest: multi_member_split) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

489 
have "add_mset b A = add_mset c (add_mset b A)  {#c#}" by simp 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

490 
then have "add_mset b A = add_mset b (add_mset c A)  {#c#}" 
63794
bcec0534aeea
clean argument of simp add
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

491 
by (simp add: \<open>b \<noteq> c\<close>) 
58098  492 
then show ?thesis using B by simp 
493 
qed 

494 

64418  495 
lemma add_mset_eq_singleton_iff[iff]: 
496 
"add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y" 

497 
by auto 

498 

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

499 

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

501 

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

502 
definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) 
65466  503 
where "A \<subseteq># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)" 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

504 

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

505 
definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) 
65466  506 
where "A \<subset># B \<longleftrightarrow> A \<subseteq># B \<and> A \<noteq> B" 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61890
diff
changeset

507 

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

508 
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

509 
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

510 

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

511 
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

512 
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

513 

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

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

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

516 
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

517 

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

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

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

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

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

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

523 

73411  524 
global_interpretation subset_mset: ordering \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close> 
525 
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order.trans order.antisym) 

526 

73451  527 
interpretation subset_mset: ordered_ab_semigroup_add_imp_le \<open>(+)\<close> \<open>()\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close> 
60678  528 
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym) 
64585
2155c0c1ecb6
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents:
64531
diff
changeset

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

530 

67398  531 
interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "(+)" 0 "()" "(\<subseteq>#)" "(\<subset>#)" 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

532 
by standard 
64585
2155c0c1ecb6
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents:
64531
diff
changeset

533 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

534 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

536 
"(\<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

537 
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

538 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

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

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

542 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

543 
lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)" 
60678  544 
unfolding subseteq_mset_def 
545 
apply (rule iffI) 

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

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

548 
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

549 

67398  550 
interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "()" 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

551 
by standard (simp, fact mset_subset_eq_exists_conv) 
64585
2155c0c1ecb6
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents:
64531
diff
changeset

552 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

553 

64017
6e7bf7678518
more multiset simp rules
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63924
diff
changeset

554 
declare subset_mset.add_diff_assoc[simp] subset_mset.add_diff_assoc2[simp] 
6e7bf7678518
more multiset simp rules
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63924
diff
changeset

555 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

557 
by (fact subset_mset.add_le_cancel_right) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

558 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

560 
by (fact subset_mset.add_le_cancel_left) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

561 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

563 
by (fact subset_mset.add_mono) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

564 

63560
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63547
diff
changeset

565 
lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B" 
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63547
diff
changeset

566 
by simp 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

567 

63560
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63547
diff
changeset

568 
lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B" 
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63547
diff
changeset

569 
by simp 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

570 

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

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

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

573 
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

574 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

575 
lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B" 
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

576 
by simp 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

577 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

578 
lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

579 
unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

580 
by (rule mset_subset_eq_mono_add_right_cancel) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

581 

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

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

584 
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

585 
by (fact subset_mset.diff_add_assoc) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

586 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

589 
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

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

591 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

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

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

595 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

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

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

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

600 
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

601 
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

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

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

604 
qed 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

605 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

607 
"A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

609 

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

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

611 
"A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B" 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

612 
by (metis mset_subset_eqD subsetI) 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

613 

caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

614 
lemma mset_subset_eq_insertD: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

615 
"add_mset x A \<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

616 
apply (rule conjI) 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

618 
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

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

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

621 
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

622 
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

623 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

624 
lemma mset_subset_insertD: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

625 
"add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B" 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

626 
by (rule mset_subset_eq_insertD) simp 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

627 

63831  628 
lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False" 
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

629 
by (simp only: subset_mset.not_less_zero) 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

630 

64587  631 
lemma empty_subset_add_mset[simp]: "{#} \<subset># add_mset x M" 
632 
by (auto intro: subset_mset.gr_zeroI) 

63831  633 

63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

634 
lemma empty_le: "{#} \<subseteq># A" 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

635 
by (fact subset_mset.zero_le) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

636 

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

637 
lemma insert_subset_eq_iff: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

639 
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

640 
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

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

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

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

644 

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

645 
lemma insert_union_subset_iff: 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

646 
"add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B  {#a#}" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

648 

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

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

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

651 
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

652 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

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

655 

64076  656 
lemma multi_psub_self: "A \<subset># A = False" 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

657 
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

658 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

659 
lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

660 
unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

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

662 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63290
diff
changeset

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

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

665 

64077  666 
lemma Diff_eq_empty_iff_mset: "A  B = {#} \<longleftrightarrow> A \<subseteq># B" 
667 
by (auto simp: multiset_eq_iff subseteq_mset_def) 

668 

64418  669 
lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b" 
670 
proof 

671 
assume A: "add_mset a M \<subseteq># {#b#}" 

672 
then have \<open>a = b\<close> 

673 
by (auto dest: mset_subset_eq_insertD) 

674 
then show "M={#} \<and> a=b" 

675 
using A by (simp add: mset_subset_eq_add_mset_cancel) 

676 
qed simp 

677 

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

678 

64076  679 
subsubsection \<open>Intersection and bounded union\<close> 
35268
04673275441a
switched notations for pointwise and multiset order
haftmann
parents:
35028
diff
changeset

680 

73393  681 
definition inter_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close> (infixl \<open>\<inter>#\<close> 70) 
682 
where \<open>A \<inter># B = A  (A  B)\<close> 

683 

73451  684 
lemma count_inter_mset [simp]: 
685 
\<open>count (A \<inter># B) x = min (count A x) (count B x)\<close> 

686 
by (simp add: inter_mset_def) 

687 

688 
(*global_interpretation subset_mset: semilattice_order \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close> 

689 
by standard (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def min_def)*) 

690 

73393  691 
interpretation subset_mset: semilattice_inf \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close> 
73451  692 
by standard (simp_all add: multiset_eq_iff subseteq_mset_def) 
693 
\<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

694 

73393  695 
definition union_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close> (infixl \<open>\<union>#\<close> 70) 
696 
where \<open>A \<union># B = A + (B  A)\<close> 

697 

73451  698 
lemma count_union_mset [simp]: 
699 
\<open>count (A \<union># B) x = max (count A x) (count B x)\<close> 

700 
by (simp add: union_mset_def) 

701 

702 
global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close> 

703 
apply standard 

704 
apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def) 

705 
apply (auto simp add: le_antisym dest: sym) 

706 
apply (metis nat_le_linear)+ 

707 
done 

708 

73393  709 
interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close> 
64076  710 
proof  
711 
have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q  m) \<le> n" for m n q :: nat 

712 
by arith 

67398  713 
show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)" 
73393  714 
by standard (auto simp add: union_mset_def subseteq_mset_def) 
64585
2155c0c1ecb6
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents:
64531
diff
changeset

715 
qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
64076  716 

67398  717 
interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" 
718 
"(\<union>#)" "{#}" 

64076  719 
by standard auto 
64585
2155c0c1ecb6
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
haftmann
parents:
64531
diff
changeset

720 
\<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> 
64076  721 

722 

723 
subsubsection \<open>Additional intersection facts\<close> 

724 

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

725 
lemma set_mset_inter [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

726 
"set_mset (A \<inter># B) = set_mset A \<inter> set_mset B" 
73393  727 
by (simp only: set_mset_def) auto 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

728 

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

729 
lemma diff_intersect_left_idem [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

732 

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

733 
lemma diff_intersect_right_idem [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

736 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

737 
lemma multiset_inter_single[simp]: "a \<noteq> b \<Longrightarrow> {#a#} \<inter># {#b#} = {#}" 
46730  738 
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

739 

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

740 
lemma multiset_union_diff_commute: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

742 
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

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

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

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

747 
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

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

749 
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

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

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

752 

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

753 
lemma disjunct_not_in: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

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

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

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

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

760 
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

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

762 
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

763 
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

764 
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

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

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

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

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

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

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

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

772 
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

773 
by (auto simp add: not_in_iff) 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

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

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

778 

64077  779 
lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}" 
780 
by (meson disjunct_not_in union_iff) 

781 

782 
lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}" 

783 
by (meson disjunct_not_in union_iff) 

784 

73393  785 
lemma add_mset_inter_add_mset [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

786 
"add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)" 
73393  787 
by (rule multiset_eqI) simp 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

788 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

789 
lemma add_mset_disjoint [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

790 
"add_mset a A \<inter># B = {#} \<longleftrightarrow> a \<notin># B \<and> A \<inter># B = {#}" 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

791 
"{#} = add_mset a A \<inter># B \<longleftrightarrow> a \<notin># B \<and> {#} = A \<inter># B" 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

792 
by (auto simp: disjunct_not_in) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

793 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

794 
lemma disjoint_add_mset [simp]: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

795 
"B \<inter># add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B \<inter># A = {#}" 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

796 
"{#} = A \<inter># add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A \<inter># B" 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

797 
by (auto simp: disjunct_not_in) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

798 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

800 
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

801 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

803 
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

804 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

806 
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

807 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

809 
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

810 

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

811 
lemma disjunct_set_mset_diff: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

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

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

816 
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

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

818 
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

819 
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

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

821 

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

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

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

824 
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

825 
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

826 

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

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

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

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

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

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

832 
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

833 
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

834 
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

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

836 

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

837 
lemma inter_iff: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

840 

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

841 
lemma inter_union_distrib_left: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

843 
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

844 

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

845 
lemma inter_union_distrib_right: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

847 
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

848 

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

849 
lemma inter_subset_eq_union: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

851 
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

852 

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

853 

64076  854 
subsubsection \<open>Additional bounded union facts\<close> 
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63794
diff
changeset

855 

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

856 
lemma set_mset_sup [simp]: 
73393  857 
\<open>set_mset (A \<union># B) = set_mset A \<union> set_mset B\<close> 
858 
by (simp only: set_mset_def) (auto simp add: less_max_iff_disj) 

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

859 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

860 
lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># N)" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

861 
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

862 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

863 
lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># (N  {#x#}))" 
51623  864 
by (simp add: multiset_eq_iff) 
865 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

866 
lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x (N \<union># M)" 
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62390
diff
changeset

867 
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

868 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

869 
lemma sup_union_right2: "x \<in># N \<Longrightarrow> N \<union># (add_mset x M) = add_mset x ((N  {#x#}) \<union># M)" 
51623  870 
by (simp add: multiset_eq_iff) 
871 

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

872 
lemma sup_union_distrib_left: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

874 
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

875 

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

876 
lemma union_sup_distrib_right: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

878 
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

879 

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

880 
lemma union_diff_inter_eq_sup: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

883 

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

884 
lemma union_diff_sup_eq_inter: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

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

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

887 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

888 
lemma add_mset_union: 
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63908
diff
changeset

889 
\<open>add_mset a A \<union># add_mset a B = add_mset a (A \<union># B)\<close> 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

890 
by (auto simp: multiset_eq_iff max_def) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

891 

51623  892 

63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

893 
subsection \<open>Replicate and repeat operations\<close> 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

894 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

895 
definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

896 
"replicate_mset n x = (add_mset x ^^ n) {#}" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

897 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

898 
lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

899 
unfolding replicate_mset_def by simp 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

900 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

901 
lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

902 
unfolding replicate_mset_def by (induct n) (auto intro: add.commute) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

903 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

904 
lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

905 
unfolding replicate_mset_def by (induct n) auto 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

906 

73393  907 
lift_definition repeat_mset :: \<open>nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close> 
908 
is \<open>\<lambda>n M a. n * M a\<close> by simp 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

909 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

910 
lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a" 
73393  911 
by transfer rule 
912 

913 
lemma repeat_mset_0 [simp]: 

914 
\<open>repeat_mset 0 M = {#}\<close> 

915 
by transfer simp 

916 

917 
lemma repeat_mset_Suc [simp]: 

918 
\<open>repeat_mset (Suc n) M = M + repeat_mset n M\<close> 

919 
by transfer simp 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

920 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

921 
lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

922 
by (auto simp: multiset_eq_iff left_diff_distrib') 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

923 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

924 
lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i  j) u = repeat_mset i u  repeat_mset j u\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

925 
by (auto simp: multiset_eq_iff left_diff_distrib') 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

926 

63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

927 
lemma left_add_mult_distrib_mset: 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

928 
"repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

929 
by (auto simp: multiset_eq_iff add_mult_distrib) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

930 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

931 
lemma repeat_mset_distrib: 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

932 
"repeat_mset (m + n) A = repeat_mset m A + repeat_mset n A" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

933 
by (auto simp: multiset_eq_iff Nat.add_mult_distrib) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

934 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

935 
lemma repeat_mset_distrib2[simp]: 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

936 
"repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

937 
by (auto simp: multiset_eq_iff add_mult_distrib2) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

938 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

939 
lemma repeat_mset_replicate_mset[simp]: 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

940 
"repeat_mset n {#a#} = replicate_mset n a" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

941 
by (auto simp: multiset_eq_iff) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

942 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

943 
lemma repeat_mset_distrib_add_mset[simp]: 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

944 
"repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A" 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

945 
by (auto simp: multiset_eq_iff) 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

946 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

947 
lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}" 
73393  948 
by transfer simp 
63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

949 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

950 

ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

951 
subsubsection \<open>Simprocs\<close> 
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

952 

65031
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

953 
lemma repeat_mset_iterate_add: \<open>repeat_mset n M = iterate_add n M\<close> 
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

954 
unfolding iterate_add_def by (induction n) auto 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

955 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

956 
lemma mset_subseteq_add_iff1: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

957 
"j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (ij) u + m \<subseteq># n)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

958 
by (auto simp add: subseteq_mset_def nat_le_add_iff1) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

959 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

960 
lemma mset_subseteq_add_iff2: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

961 
"i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (ji) u + n)" 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

962 
by (auto simp add: subseteq_mset_def nat_le_add_iff2) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

963 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

964 
lemma mset_subset_add_iff1: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

965 
"j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (ij) u + m \<subset># n)" 
65031
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

966 
unfolding subset_mset_def repeat_mset_iterate_add 
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

967 
by (simp add: iterate_add_eq_add_iff1 mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]) 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

968 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

969 
lemma mset_subset_add_iff2: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

970 
"i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (ji) u + n)" 
65031
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

971 
unfolding subset_mset_def repeat_mset_iterate_add 
52e2c99f3711
use the cancellation simprocs directly
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65029
diff
changeset

972 
by (simp add: iterate_add_eq_add_iff2 mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]) 
65029
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

973 

69605  974 
ML_file \<open>multiset_simprocs.ML\<close> 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

975 

65029
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

976 
lemma add_mset_replicate_mset_safe[cancelation_simproc_pre]: \<open>NO_MATCH {#} M \<Longrightarrow> add_mset a M = {#a#} + M\<close> 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

977 
by simp 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

978 

00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

979 
declare repeat_mset_iterate_add[cancelation_simproc_pre] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

980 

00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

981 
declare iterate_add_distrib[cancelation_simproc_pre] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

982 
declare repeat_mset_iterate_add[symmetric, cancelation_simproc_post] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

983 

00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

984 
declare add_mset_not_empty[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

985 
empty_not_add_mset[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

986 
subset_mset.le_zero_eq[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

987 
empty_not_add_mset[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

988 
add_mset_not_empty[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

989 
subset_mset.le_zero_eq[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

990 
le_zero_eq[cancelation_simproc_eq_elim] 
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

991 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64911
diff
changeset

992 
simproc_setup mseteq_cancel 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

993 
("(l::'a multiset) + m = n"  "(l::'a multiset) = m + n"  
63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

994 
"add_mset a m = n"  "m = add_mset a n"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

995 
"replicate_mset p a = n"  "m = replicate_mset p a"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

996 
"repeat_mset p m = n"  "m = repeat_mset p m") = 
65029
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

997 
\<open>fn phi => Cancel_Simprocs.eq_cancel\<close> 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

998 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64911
diff
changeset

999 
simproc_setup msetsubset_cancel 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1000 
("(l::'a multiset) + m \<subset># n"  "(l::'a multiset) \<subset># m + n"  
63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1001 
"add_mset a m \<subset># n"  "m \<subset># add_mset a n"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1002 
"replicate_mset p r \<subset># n"  "m \<subset># replicate_mset p r"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1003 
"repeat_mset p m \<subset># n"  "m \<subset># repeat_mset p m") = 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1004 
\<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1005 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64911
diff
changeset

1006 
simproc_setup msetsubset_eq_cancel 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1007 
("(l::'a multiset) + m \<subseteq># n"  "(l::'a multiset) \<subseteq># m + n"  
63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1008 
"add_mset a m \<subseteq># n"  "m \<subseteq># add_mset a n"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1009 
"replicate_mset p r \<subseteq># n"  "m \<subseteq># replicate_mset p r"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1010 
"repeat_mset p m \<subseteq># n"  "m \<subseteq># repeat_mset p m") = 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1011 
\<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close> 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1012 

65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64911
diff
changeset

1013 
simproc_setup msetdiff_cancel 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1014 
("((l::'a multiset) + m)  n"  "(l::'a multiset)  (m + n)"  
63908
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1015 
"add_mset a m  n"  "m  add_mset a n"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1016 
"replicate_mset p r  n"  "m  replicate_mset p r"  
ca41b6670904
support replicate_mset in multiset simproc
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63882
diff
changeset

1017 
"repeat_mset p m  n"  "m  repeat_mset p m") = 
65029
00731700e54f
cancellation simprocs generalising the multiset simprocs
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
65027
diff
changeset

1018 
\<open>fn phi => Cancel_Simprocs.diff_cancel\<close> 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1019 

e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63689
diff
changeset

1020 

63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1021 
subsubsection \<open>Conditionally complete lattice\<close> 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1022 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1023 
instantiation multiset :: (type) Inf 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1024 
begin 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1025 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1026 
lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1027 
"\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1028 
proof  
73270  1029 
fix A :: "('a \<Rightarrow> nat) set" 
1030 
assume *: "\<And>f. f \<in> A \<Longrightarrow> finite {x. 0 < f x}" 

1031 
show \<open>finite {i. 0 < (if A = {} then 0 else INF f\<in>A. f i)}\<close> 

63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1032 
proof (cases "A = {}") 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1033 
case False 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1034 
then obtain f where "f \<in> A" by blast 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1035 
hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1036 
by (auto intro: less_le_trans[OF _ cInf_lower]) 
73270  1037 
moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by simp 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1038 
ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1039 
with False show ?thesis by simp 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1040 
qed simp_all 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1041 
qed 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1042 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1043 
instance .. 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1044 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1045 
end 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1046 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1047 
lemma Inf_multiset_empty: "Inf {} = {#}" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1048 
by transfer simp_all 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1049 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1050 
lemma count_Inf_multiset_nonempty: "A \<noteq> {} \<Longrightarrow> count (Inf A) x = Inf ((\<lambda>X. count X x) ` A)" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1051 
by transfer simp_all 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1052 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1053 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1054 
instantiation multiset :: (type) Sup 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1055 
begin 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1056 

63360  1057 
definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" where 
1058 
"Sup_multiset A = (if A \<noteq> {} \<and> subset_mset.bdd_above A then 

1059 
Abs_multiset (\<lambda>i. Sup ((\<lambda>X. count X i) ` A)) else {#})" 

1060 

1061 
lemma Sup_multiset_empty: "Sup {} = {#}" 

1062 
by (simp add: Sup_multiset_def) 

1063 

73451  1064 
lemma Sup_multiset_unbounded: "\<not> subset_mset.bdd_above A \<Longrightarrow> Sup A = {#}" 
63360  1065 
by (simp add: Sup_multiset_def) 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1066 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1067 
instance .. 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1068 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1069 
end 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1070 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1071 
lemma bdd_above_multiset_imp_bdd_above_count: 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1072 
assumes "subset_mset.bdd_above (A :: 'a multiset set)" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1073 
shows "bdd_above ((\<lambda>X. count X x) ` A)" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1074 
proof  
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1075 
from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y" 
73451  1076 
by (meson subset_mset.bdd_above.E) 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1077 
hence "count X x \<le> count Y x" if "X \<in> A" for X 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1078 
using that by (auto intro: mset_subset_eq_count) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1079 
thus ?thesis by (intro bdd_aboveI[of _ "count Y x"]) auto 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1080 
qed 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1081 

a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1082 
lemma bdd_above_multiset_imp_finite_support: 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1083 
assumes "A \<noteq> {}" "subset_mset.bdd_above (A :: 'a multiset set)" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1084 
shows "finite (\<Union>X\<in>A. {x. count X x > 0})" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1085 
proof  
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1086 
from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y" 
73451  1087 
by (meson subset_mset.bdd_above.E) 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1088 
hence "count X x \<le> count Y x" if "X \<in> A" for X x 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1089 
using that by (auto intro: mset_subset_eq_count) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1090 
hence "(\<Union>X\<in>A. {x. count X x > 0}) \<subseteq> {x. count Y x > 0}" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1091 
by safe (erule less_le_trans) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1092 
moreover have "finite \<dots>" by simp 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1093 
ultimately show ?thesis by (rule finite_subset) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1094 
qed 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1095 

63360  1096 
lemma Sup_multiset_in_multiset: 
73270  1097 
\<open>finite {i. 0 < (SUP M\<in>A. count M i)}\<close> 
1098 
if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close> 

1099 
proof  

63360  1100 
have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})" 
1101 
proof safe 

69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69107
diff
changeset

1102 
fix i assume pos: "(SUP X\<in>A. count X i) > 0" 
63360  1103 
show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})" 
1104 
proof (rule ccontr) 

1105 
assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})" 

1106 
hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff) 

73270  1107 
with that have "(SUP X\<in>A. count X i) \<le> 0" 
63360  1108 
by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto 
1109 
with pos show False by simp 

1110 
qed 

1111 
qed 

73270  1112 
moreover from that have "finite \<dots>" 
1113 
by (rule bdd_above_multiset_imp_finite_support) 

1114 
ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}" 

1115 
by (rule finite_subset) 

63360  1116 
qed 
1117 

63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1118 
lemma count_Sup_multiset_nonempty: 
73270  1119 
\<open>count (Sup A) x = (SUP X\<in>A. count X x)\<close> 
1120 
if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close> 

1121 
using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset) 

63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1122 

67398  1123 
interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)" 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1124 
proof 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1125 
fix X :: "'a multiset" and A 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1126 
assume "X \<in> A" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1127 
show "Inf A \<subseteq># X" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1128 
proof (rule mset_subset_eqI) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1129 
fix x 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1130 
from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto 
69260
0a9688695a1b
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
69107
diff
changeset

1131 
hence "count (Inf A) x = (INF X\<in>A. count X x)" 
63358
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1132 
by (simp add: count_Inf_multiset_nonempty) 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1133 
also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1134 
by (intro cInf_lower) simp_all 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1135 
finally show "count (Inf A) x \<le> count X x" . 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1136 
qed 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1137 
next 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1138 
fix X :: "'a multiset" and A 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1139 
assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eberl <eberlm@in.tum.de>
parents:
63310
diff
changeset

1140 
show "X \<subseteq># Inf A" 
a500677d4cec
Conditionally complete lattice of multisets
Manuel Eber&# 