author | wenzelm |
Mon, 06 Jul 2015 22:06:02 +0200 | |
changeset 60678 | 17ba2df56dee |
parent 60502 | aa58872267ee |
child 60679 | ade12ef2773c |
permissions | -rw-r--r-- |
59813 | 1 |
(* Title: HOL/Library/Multiset_Order.thy |
2 |
Author: Dmitriy Traytel, TU Muenchen |
|
3 |
Author: Jasmin Blanchette, Inria, LORIA, MPII |
|
4 |
*) |
|
5 |
||
60500 | 6 |
section \<open>More Theorems about the Multiset Order\<close> |
59813 | 7 |
|
8 |
theory Multiset_Order |
|
9 |
imports Multiset |
|
10 |
begin |
|
11 |
||
60500 | 12 |
subsubsection \<open>Alternative characterizations\<close> |
59813 | 13 |
|
14 |
context order |
|
15 |
begin |
|
16 |
||
17 |
lemma reflp_le: "reflp (op \<le>)" |
|
18 |
unfolding reflp_def by simp |
|
19 |
||
20 |
lemma antisymP_le: "antisymP (op \<le>)" |
|
21 |
unfolding antisym_def by auto |
|
22 |
||
23 |
lemma transp_le: "transp (op \<le>)" |
|
24 |
unfolding transp_def by auto |
|
25 |
||
26 |
lemma irreflp_less: "irreflp (op <)" |
|
27 |
unfolding irreflp_def by simp |
|
28 |
||
29 |
lemma antisymP_less: "antisymP (op <)" |
|
30 |
unfolding antisym_def by auto |
|
31 |
||
32 |
lemma transp_less: "transp (op <)" |
|
33 |
unfolding transp_def by auto |
|
34 |
||
35 |
lemmas le_trans = transp_le[unfolded transp_def, rule_format] |
|
36 |
||
37 |
lemma order_mult: "class.order |
|
38 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) |
|
39 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})" |
|
40 |
(is "class.order ?le ?less") |
|
41 |
proof - |
|
42 |
have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M" |
|
43 |
proof |
|
44 |
fix M :: "'a multiset" |
|
45 |
have "trans {(x'::'a, x). x' < x}" |
|
46 |
by (rule transI) simp |
|
47 |
moreover |
|
48 |
assume "(M, M) \<in> mult {(x, y). x < y}" |
|
49 |
ultimately have "\<exists>I J K. M = I + J \<and> M = I + K |
|
60495 | 50 |
\<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" |
59813 | 51 |
by (rule mult_implies_one_step) |
52 |
then obtain I J K where "M = I + J" and "M = I + K" |
|
60495 | 53 |
and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast |
54 |
then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto |
|
55 |
have "finite (set_mset K)" by simp |
|
59813 | 56 |
moreover note aux2 |
60495 | 57 |
ultimately have "set_mset K = {}" |
59813 | 58 |
by (induct rule: finite_induct) |
59 |
(simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans) |
|
60 |
with aux1 show False by simp |
|
61 |
qed |
|
62 |
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N" |
|
63 |
unfolding mult_def by (blast intro: trancl_trans) |
|
64 |
show "class.order ?le ?less" |
|
65 |
by default (auto simp add: le_multiset_def irrefl dest: trans) |
|
66 |
qed |
|
67 |
||
60500 | 68 |
text \<open>The Dershowitz--Manna ordering:\<close> |
59813 | 69 |
|
70 |
definition less_multiset\<^sub>D\<^sub>M where |
|
71 |
"less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow> |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
72 |
(\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))" |
59813 | 73 |
|
74 |
||
60500 | 75 |
text \<open>The Huet--Oppen ordering:\<close> |
59813 | 76 |
|
77 |
definition less_multiset\<^sub>H\<^sub>O where |
|
78 |
"less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))" |
|
79 |
||
80 |
lemma mult_imp_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
|
81 |
proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct) |
|
82 |
case (base P) |
|
83 |
then show ?case unfolding mult1_def by force |
|
84 |
next |
|
85 |
case (step N P) |
|
86 |
from step(2) obtain M0 a K where |
|
87 |
*: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a" |
|
88 |
unfolding mult1_def by blast |
|
89 |
then have count_K_a: "count K a = 0" by auto |
|
90 |
with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits) |
|
91 |
moreover |
|
92 |
{ assume "count P a \<le> count M a" |
|
93 |
with count_K_a have "count N a < count M a" unfolding *(1,2) by auto |
|
94 |
with step(3) obtain z where z: "z > a" "count M z < count N z" by blast |
|
95 |
with * have "count N z \<le> count P z" by force |
|
96 |
with z have "\<exists>z > a. count M z < count P z" by auto |
|
97 |
} note count_a = this |
|
98 |
{ fix y |
|
99 |
assume count_y: "count P y < count M y" |
|
100 |
have "\<exists>x>y. count M x < count P x" |
|
101 |
proof (cases "y = a") |
|
102 |
case True |
|
103 |
with count_y count_a show ?thesis by auto |
|
104 |
next |
|
105 |
case False |
|
106 |
show ?thesis |
|
107 |
proof (cases "y \<in># K") |
|
108 |
case True |
|
109 |
with *(3) have "y < a" by simp |
|
110 |
then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans) |
|
111 |
next |
|
112 |
case False |
|
60500 | 113 |
with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) by simp |
59813 | 114 |
with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto |
115 |
show ?thesis |
|
116 |
proof (cases "z \<in># K") |
|
117 |
case True |
|
118 |
with *(3) have "z < a" by simp |
|
119 |
with z(1) show ?thesis |
|
120 |
by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans) |
|
121 |
next |
|
122 |
case False |
|
123 |
with count_K_a have "count N z \<le> count P z" unfolding * by auto |
|
124 |
with z show ?thesis by auto |
|
125 |
qed |
|
126 |
qed |
|
127 |
qed |
|
128 |
} |
|
129 |
ultimately show ?case by blast |
|
130 |
qed |
|
131 |
||
132 |
lemma less_multiset\<^sub>D\<^sub>M_imp_mult: |
|
133 |
"less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}" |
|
134 |
proof - |
|
135 |
assume "less_multiset\<^sub>D\<^sub>M M N" |
|
136 |
then obtain X Y where |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
137 |
"X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)" |
59813 | 138 |
unfolding less_multiset\<^sub>D\<^sub>M_def by blast |
139 |
then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}" |
|
140 |
by (intro one_step_implies_mult) (auto simp: Bex_def trans_def) |
|
60500 | 141 |
with \<open>M = N - X + Y\<close> \<open>X \<le># N\<close> show "(M, N) \<in> mult {(x, y). x < y}" |
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
142 |
by (metis subset_mset.diff_add) |
59813 | 143 |
qed |
144 |
||
145 |
lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
|
146 |
unfolding less_multiset\<^sub>D\<^sub>M_def |
|
147 |
proof (intro iffI exI conjI) |
|
148 |
assume "less_multiset\<^sub>H\<^sub>O M N" |
|
149 |
then obtain z where z: "count M z < count N z" |
|
150 |
unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff) |
|
151 |
def X \<equiv> "N - M" |
|
152 |
def Y \<equiv> "M - N" |
|
153 |
from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq) |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
154 |
from z show "X \<le># N" unfolding X_def by auto |
59813 | 155 |
show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force |
156 |
show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)" |
|
157 |
proof (intro allI impI) |
|
158 |
fix k |
|
159 |
assume "k \<in># Y" |
|
160 |
then have "count N k < count M k" unfolding Y_def by auto |
|
60500 | 161 |
with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a" |
59813 | 162 |
unfolding less_multiset\<^sub>H\<^sub>O_def by blast |
163 |
then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto |
|
164 |
qed |
|
165 |
qed |
|
166 |
||
167 |
lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>D\<^sub>M M N" |
|
168 |
by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O) |
|
169 |
||
170 |
lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
|
171 |
by (metis less_multiset\<^sub>D\<^sub>M_imp_mult less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M mult_imp_less_multiset\<^sub>H\<^sub>O) |
|
172 |
||
173 |
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def] |
|
174 |
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def] |
|
175 |
||
176 |
end |
|
177 |
||
178 |
context linorder |
|
179 |
begin |
|
180 |
||
181 |
lemma total_le: "total {(a \<Colon> 'a, b). a \<le> b}" |
|
182 |
unfolding total_on_def by auto |
|
183 |
||
184 |
lemma total_less: "total {(a \<Colon> 'a, b). a < b}" |
|
185 |
unfolding total_on_def by auto |
|
186 |
||
187 |
lemma linorder_mult: "class.linorder |
|
188 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) |
|
189 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})" |
|
190 |
proof - |
|
191 |
interpret o: order |
|
192 |
"(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N)" |
|
193 |
"(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})" |
|
194 |
by (rule order_mult) |
|
195 |
show ?thesis by unfold_locales (auto 0 3 simp: mult\<^sub>H\<^sub>O not_less_iff_gr_or_eq) |
|
196 |
qed |
|
197 |
||
198 |
end |
|
199 |
||
200 |
lemma less_multiset_less_multiset\<^sub>H\<^sub>O: |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
201 |
"M #\<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
59813 | 202 |
unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def .. |
203 |
||
204 |
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def] |
|
205 |
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def] |
|
206 |
||
207 |
lemma le_multiset\<^sub>H\<^sub>O: |
|
208 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
209 |
shows "M #\<subseteq># N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))" |
59813 | 210 |
by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O) |
211 |
||
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
212 |
lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M #\<subset># N}" |
59813 | 213 |
unfolding less_multiset_def by (auto intro: wf_mult wf) |
214 |
||
215 |
lemma order_multiset: "class.order |
|
216 |
(le_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool) |
|
217 |
(less_multiset :: ('a \<Colon> order) multiset \<Rightarrow> ('a \<Colon> order) multiset \<Rightarrow> bool)" |
|
218 |
by unfold_locales |
|
219 |
||
220 |
lemma linorder_multiset: "class.linorder |
|
221 |
(le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool) |
|
222 |
(less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool)" |
|
223 |
by unfold_locales (fastforce simp add: less_multiset\<^sub>H\<^sub>O le_multiset_def not_less_iff_gr_or_eq) |
|
224 |
||
225 |
interpretation multiset_linorder: linorder |
|
226 |
"le_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool" |
|
227 |
"less_multiset :: ('a \<Colon> linorder) multiset \<Rightarrow> ('a \<Colon> linorder) multiset \<Rightarrow> bool" |
|
228 |
by (rule linorder_multiset) |
|
229 |
||
230 |
interpretation multiset_wellorder: wellorder |
|
231 |
"le_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool" |
|
232 |
"less_multiset :: ('a \<Colon> wellorder) multiset \<Rightarrow> ('a \<Colon> wellorder) multiset \<Rightarrow> bool" |
|
233 |
by unfold_locales (blast intro: wf_less_multiset[unfolded wf_def, rule_format]) |
|
234 |
||
235 |
lemma le_multiset_total: |
|
236 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
237 |
shows "\<not> M #\<subseteq># N \<Longrightarrow> N #\<subseteq># M" |
59813 | 238 |
by (metis multiset_linorder.le_cases) |
239 |
||
240 |
lemma less_eq_imp_le_multiset: |
|
241 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
242 |
shows "M \<le># N \<Longrightarrow> M #\<subseteq># N" |
59813 | 243 |
unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O |
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
244 |
by (simp add: less_le_not_le subseteq_mset_def) |
59813 | 245 |
|
246 |
lemma less_multiset_right_total: |
|
247 |
fixes M :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
248 |
shows "M #\<subset># M + {#undefined#}" |
59813 | 249 |
unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O by simp |
250 |
||
251 |
lemma le_multiset_empty_left[simp]: |
|
252 |
fixes M :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
253 |
shows "{#} #\<subseteq># M" |
59813 | 254 |
by (simp add: less_eq_imp_le_multiset) |
255 |
||
256 |
lemma le_multiset_empty_right[simp]: |
|
257 |
fixes M :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
258 |
shows "M \<noteq> {#} \<Longrightarrow> \<not> M #\<subseteq># {#}" |
59813 | 259 |
by (metis le_multiset_empty_left multiset_order.antisym) |
260 |
||
261 |
lemma less_multiset_empty_left[simp]: |
|
262 |
fixes M :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
263 |
shows "M \<noteq> {#} \<Longrightarrow> {#} #\<subset># M" |
59813 | 264 |
by (simp add: less_multiset\<^sub>H\<^sub>O) |
265 |
||
266 |
lemma less_multiset_empty_right[simp]: |
|
267 |
fixes M :: "('a \<Colon> linorder) multiset" |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
268 |
shows "\<not> M #\<subset># {#}" |
59813 | 269 |
using le_empty less_multiset\<^sub>D\<^sub>M by blast |
270 |
||
271 |
lemma |
|
272 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
273 |
shows |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
274 |
le_multiset_plus_left[simp]: "N #\<subseteq># (M + N)" and |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
275 |
le_multiset_plus_right[simp]: "M #\<subseteq># (M + N)" |
59813 | 276 |
using [[metis_verbose = false]] by (metis less_eq_imp_le_multiset mset_le_add_left add.commute)+ |
277 |
||
278 |
lemma |
|
279 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
280 |
shows |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
281 |
less_multiset_plus_plus_left_iff[simp]: "M + N #\<subset># M' + N \<longleftrightarrow> M #\<subset># M'" and |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
282 |
less_multiset_plus_plus_right_iff[simp]: "M + N #\<subset># M + N' \<longleftrightarrow> N #\<subset># N'" |
59813 | 283 |
unfolding less_multiset\<^sub>H\<^sub>O by auto |
284 |
||
285 |
lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}" |
|
286 |
by (metis add.commute add_diff_cancel_right' monoid_add_class.add.left_neutral) |
|
287 |
||
288 |
lemma |
|
289 |
fixes M N :: "('a \<Colon> linorder) multiset" |
|
290 |
shows |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
291 |
less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N #\<subset># M + N" and |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
292 |
less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M #\<subset># M + N" |
59813 | 293 |
using [[metis_verbose = false]] |
294 |
by (metis add.right_neutral less_multiset_empty_left less_multiset_plus_plus_right_iff |
|
295 |
add.commute)+ |
|
296 |
||
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
297 |
lemma ex_gt_imp_less_multiset: "(\<exists>y \<Colon> 'a \<Colon> linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N" |
59813 | 298 |
unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0) |
299 |
||
300 |
lemma ex_gt_count_imp_less_multiset: |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59817
diff
changeset
|
301 |
"(\<forall>y \<Colon> 'a \<Colon> linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N" |
59817 | 302 |
unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order |
303 |
less_not_sym mset_leD mset_le_add_left) |
|
59813 | 304 |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
305 |
lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M" |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
306 |
by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2) |
59813 | 307 |
|
308 |
end |