59813
|
1 |
(* Title: HOL/Library/Multiset_Order.thy
|
|
2 |
Author: Dmitriy Traytel, TU Muenchen
|
|
3 |
Author: Jasmin Blanchette, Inria, LORIA, MPII
|
|
4 |
*)
|
|
5 |
|
|
6 |
section {* More Theorems about the Multiset Order *}
|
|
7 |
|
|
8 |
theory Multiset_Order
|
|
9 |
imports Multiset
|
|
10 |
begin
|
|
11 |
|
|
12 |
subsubsection {* Alternative characterizations *}
|
|
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
|
|
50 |
\<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
|
|
51 |
by (rule mult_implies_one_step)
|
|
52 |
then obtain I J K where "M = I + J" and "M = I + K"
|
|
53 |
and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
|
|
54 |
then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
|
|
55 |
have "finite (set_of K)" by simp
|
|
56 |
moreover note aux2
|
|
57 |
ultimately have "set_of K = {}"
|
|
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 |
|
|
68 |
text {* The Dershowitz--Manna ordering: *}
|
|
69 |
|
|
70 |
definition less_multiset\<^sub>D\<^sub>M where
|
|
71 |
"less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
|
|
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)))"
|
|
73 |
|
|
74 |
|
|
75 |
text {* The Huet--Oppen ordering: *}
|
|
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
|
|
113 |
with `y \<noteq> a` have "count P y = count N y" unfolding *(1,2) by simp
|
|
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
|
|
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)"
|
|
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)
|
|
141 |
with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
|
|
142 |
by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
|
|
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)
|
|
154 |
from z show "X \<le> N" unfolding X_def by auto
|
|
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
|
|
161 |
with `less_multiset\<^sub>H\<^sub>O M N` obtain a where "k < a" and "count M a < count N a"
|
|
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:
|
|
201 |
"M \<subset># N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
|
|
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"
|
|
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))"
|
|
210 |
by (auto simp: le_multiset_def less_multiset\<^sub>H\<^sub>O)
|
|
211 |
|
|
212 |
lemma wf_less_multiset: "wf {(M \<Colon> ('a \<Colon> wellorder) multiset, N). M \<subset># N}"
|
|
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"
|
|
237 |
shows "\<not> M \<subseteq># N \<Longrightarrow> N \<subseteq># M"
|
|
238 |
by (metis multiset_linorder.le_cases)
|
|
239 |
|
|
240 |
lemma less_eq_imp_le_multiset:
|
|
241 |
fixes M N :: "('a \<Colon> linorder) multiset"
|
|
242 |
shows "M \<le> N \<Longrightarrow> M \<subseteq># N"
|
|
243 |
unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
|
|
244 |
by (auto dest: leD simp add: less_eq_multiset.rep_eq)
|
|
245 |
|
|
246 |
lemma less_multiset_right_total:
|
|
247 |
fixes M :: "('a \<Colon> linorder) multiset"
|
|
248 |
shows "M \<subset># M + {#undefined#}"
|
|
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"
|
|
253 |
shows "{#} \<subseteq># M"
|
|
254 |
by (simp add: less_eq_imp_le_multiset)
|
|
255 |
|
|
256 |
lemma le_multiset_empty_right[simp]:
|
|
257 |
fixes M :: "('a \<Colon> linorder) multiset"
|
|
258 |
shows "M \<noteq> {#} \<Longrightarrow> \<not> M \<subseteq># {#}"
|
|
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"
|
|
263 |
shows "M \<noteq> {#} \<Longrightarrow> {#} \<subset># M"
|
|
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"
|
|
268 |
shows "\<not> M \<subset># {#}"
|
|
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
|
|
274 |
le_multiset_plus_left[simp]: "N \<subseteq># (M + N)" and
|
|
275 |
le_multiset_plus_right[simp]: "M \<subseteq># (M + N)"
|
|
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
|
|
281 |
less_multiset_plus_plus_left_iff[simp]: "M + N \<subset># M' + N \<longleftrightarrow> M \<subset># M'" and
|
|
282 |
less_multiset_plus_plus_right_iff[simp]: "M + N \<subset># M + N' \<longleftrightarrow> N \<subset># N'"
|
|
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
|
|
291 |
less_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N \<subset># M + N" and
|
|
292 |
less_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M \<subset># M + N"
|
|
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 |
|
|
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"
|
|
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:
|
|
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 |
|
|
305 |
lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N \<subset># P \<Longrightarrow> M - P + N \<subset># M"
|
|
306 |
by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
|
|
307 |
|
|
308 |
end
|