author | nipkow |
Fri, 05 Aug 2016 10:05:50 +0200 | |
changeset 63598 | 025d6e52d86f |
parent 63525 | f01d1e393f3f |
child 63793 | e68a0b651eb5 |
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 |
||
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
12 |
subsection \<open>Alternative characterizations\<close> |
59813 | 13 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
14 |
context preorder |
59813 | 15 |
begin |
16 |
||
17 |
lemma order_mult: "class.order |
|
18 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y} \<or> M = N) |
|
19 |
(\<lambda>M N. (M, N) \<in> mult {(x, y). x < y})" |
|
20 |
(is "class.order ?le ?less") |
|
21 |
proof - |
|
22 |
have irrefl: "\<And>M :: 'a multiset. \<not> ?less M M" |
|
23 |
proof |
|
24 |
fix M :: "'a multiset" |
|
25 |
have "trans {(x'::'a, x). x' < x}" |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
26 |
by (rule transI) (blast intro: less_trans) |
59813 | 27 |
moreover |
28 |
assume "(M, M) \<in> mult {(x, y). x < y}" |
|
29 |
ultimately have "\<exists>I J K. M = I + J \<and> M = I + K |
|
60495 | 30 |
\<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" |
59813 | 31 |
by (rule mult_implies_one_step) |
32 |
then obtain I J K where "M = I + J" and "M = I + K" |
|
60495 | 33 |
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 |
34 |
then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto |
|
35 |
have "finite (set_mset K)" by simp |
|
59813 | 36 |
moreover note aux2 |
60495 | 37 |
ultimately have "set_mset K = {}" |
59813 | 38 |
by (induct rule: finite_induct) |
39 |
(simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans) |
|
40 |
with aux1 show False by simp |
|
41 |
qed |
|
42 |
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N" |
|
43 |
unfolding mult_def by (blast intro: trancl_trans) |
|
44 |
show "class.order ?le ?less" |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
45 |
by standard (auto simp add: less_eq_multiset_def irrefl dest: trans) |
59813 | 46 |
qed |
47 |
||
60500 | 48 |
text \<open>The Dershowitz--Manna ordering:\<close> |
59813 | 49 |
|
50 |
definition less_multiset\<^sub>D\<^sub>M where |
|
51 |
"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
|
52 |
(\<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 | 53 |
|
54 |
||
60500 | 55 |
text \<open>The Huet--Oppen ordering:\<close> |
59813 | 56 |
|
57 |
definition less_multiset\<^sub>H\<^sub>O where |
|
58 |
"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))" |
|
59 |
||
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
60 |
lemma mult_imp_less_multiset\<^sub>H\<^sub>O: |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
61 |
"(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
62 |
proof (unfold mult_def, induct rule: trancl_induct) |
59813 | 63 |
case (base P) |
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
64 |
then show ?case |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
65 |
by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD) |
59813 | 66 |
next |
67 |
case (step N P) |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
68 |
from step(3) have "M \<noteq> N" and |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
69 |
**: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)" |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
70 |
by (simp_all add: less_multiset\<^sub>H\<^sub>O_def) |
59813 | 71 |
from step(2) obtain M0 a K where |
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
72 |
*: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a" |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
73 |
by (blast elim: mult1_lessE) |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
74 |
from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) elim!: less_asym split: if_splits ) |
59813 | 75 |
moreover |
76 |
{ assume "count P a \<le> count M a" |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
77 |
with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2) |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
78 |
by (auto simp add: not_in_iff) |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
79 |
with ** obtain z where z: "z > a" "count M z < count N z" |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
80 |
by blast |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
81 |
with * have "count N z \<le> count P z" |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
82 |
by (auto elim: less_asym intro: count_inI) |
59813 | 83 |
with z have "\<exists>z > a. count M z < count P z" by auto |
84 |
} note count_a = this |
|
85 |
{ fix y |
|
86 |
assume count_y: "count P y < count M y" |
|
87 |
have "\<exists>x>y. count M x < count P x" |
|
88 |
proof (cases "y = a") |
|
89 |
case True |
|
90 |
with count_y count_a show ?thesis by auto |
|
91 |
next |
|
92 |
case False |
|
93 |
show ?thesis |
|
94 |
proof (cases "y \<in># K") |
|
95 |
case True |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
96 |
with *(4) have "y < a" by simp |
59813 | 97 |
then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans) |
98 |
next |
|
99 |
case False |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
100 |
with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
101 |
by (simp add: not_in_iff) |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
102 |
with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto |
59813 | 103 |
show ?thesis |
104 |
proof (cases "z \<in># K") |
|
105 |
case True |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
106 |
with *(4) have "z < a" by simp |
59813 | 107 |
with z(1) show ?thesis |
108 |
by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans) |
|
109 |
next |
|
110 |
case False |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
111 |
with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding * |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
112 |
by (auto simp add: not_in_iff) |
59813 | 113 |
with z show ?thesis by auto |
114 |
qed |
|
115 |
qed |
|
116 |
qed |
|
117 |
} |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
118 |
ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast |
59813 | 119 |
qed |
120 |
||
121 |
lemma less_multiset\<^sub>D\<^sub>M_imp_mult: |
|
122 |
"less_multiset\<^sub>D\<^sub>M M N \<Longrightarrow> (M, N) \<in> mult {(x, y). x < y}" |
|
123 |
proof - |
|
124 |
assume "less_multiset\<^sub>D\<^sub>M M N" |
|
125 |
then obtain X Y where |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59958
diff
changeset
|
126 |
"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 | 127 |
unfolding less_multiset\<^sub>D\<^sub>M_def by blast |
128 |
then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}" |
|
129 |
by (intro one_step_implies_mult) (auto simp: Bex_def trans_def) |
|
60500 | 130 |
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
|
131 |
by (metis subset_mset.diff_add) |
59813 | 132 |
qed |
133 |
||
134 |
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" |
|
135 |
unfolding less_multiset\<^sub>D\<^sub>M_def |
|
136 |
proof (intro iffI exI conjI) |
|
137 |
assume "less_multiset\<^sub>H\<^sub>O M N" |
|
138 |
then obtain z where z: "count M z < count N z" |
|
139 |
unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff) |
|
63040 | 140 |
define X where "X = N - M" |
141 |
define Y where "Y = M - N" |
|
59813 | 142 |
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
|
143 |
from z show "X \<le># N" unfolding X_def by auto |
59813 | 144 |
show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force |
145 |
show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)" |
|
146 |
proof (intro allI impI) |
|
147 |
fix k |
|
148 |
assume "k \<in># Y" |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
149 |
then have "count N k < count M k" unfolding Y_def |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
150 |
by (auto simp add: in_diff_count) |
60500 | 151 |
with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a" |
59813 | 152 |
unfolding less_multiset\<^sub>H\<^sub>O_def by blast |
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
153 |
then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
154 |
by (auto simp add: in_diff_count) |
59813 | 155 |
qed |
156 |
qed |
|
157 |
||
158 |
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" |
|
159 |
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) |
|
160 |
||
161 |
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" |
|
162 |
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) |
|
163 |
||
164 |
lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def] |
|
165 |
lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def] |
|
166 |
||
167 |
end |
|
168 |
||
169 |
||
170 |
lemma less_multiset_less_multiset\<^sub>H\<^sub>O: |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
171 |
"M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N" |
59813 | 172 |
unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def .. |
173 |
||
174 |
lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def] |
|
175 |
lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def] |
|
176 |
||
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
177 |
lemma subset_eq_imp_le_multiset: |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
178 |
shows "M \<le># N \<Longrightarrow> M \<le> N" |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
179 |
unfolding less_eq_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
|
180 |
by (simp add: less_le_not_le subseteq_mset_def) |
59813 | 181 |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
182 |
lemma le_multiset_right_total: |
63407
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset
|
183 |
shows "M < M + {#x#}" |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
184 |
unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
185 |
|
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
186 |
lemma less_eq_multiset_empty_left[simp]: |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
187 |
shows "{#} \<le> M" |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
188 |
by (simp add: subset_eq_imp_le_multiset) |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
189 |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
190 |
lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N" |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
191 |
unfolding less_multiset\<^sub>H\<^sub>O |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
192 |
by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le) |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
193 |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
194 |
lemma less_eq_multiset_empty_right[simp]: |
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
195 |
"M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}" |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
196 |
by (metis less_eq_multiset_empty_left antisym) |
59813 | 197 |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
198 |
lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M" |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
199 |
by (simp add: less_multiset\<^sub>H\<^sub>O) |
59813 | 200 |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
201 |
lemma le_multiset_empty_right[simp]: "\<not> M < {#}" |
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63040
diff
changeset
|
202 |
using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast |
59813 | 203 |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
204 |
lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M" |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
205 |
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2) |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
206 |
|
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
207 |
instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le |
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
208 |
begin |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
209 |
|
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
210 |
lemma less_eq_multiset\<^sub>H\<^sub>O: |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
211 |
"M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))" |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
212 |
by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O) |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
213 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
214 |
instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O) |
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
215 |
|
59813 | 216 |
lemma |
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
217 |
fixes M N :: "'a multiset" |
59813 | 218 |
shows |
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
219 |
less_eq_multiset_plus_left: "N \<le> (M + N)" and |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
220 |
less_eq_multiset_plus_right: "M \<le> (M + N)" |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
221 |
by simp_all |
59813 | 222 |
|
223 |
lemma |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
224 |
fixes M N :: "'a multiset" |
59813 | 225 |
shows |
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
226 |
le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
227 |
le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N" |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63410
diff
changeset
|
228 |
by simp_all |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
229 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
230 |
end |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
231 |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63310
diff
changeset
|
232 |
lemma ex_gt_count_imp_le_multiset: |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
233 |
"(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N" |
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
61424
diff
changeset
|
234 |
unfolding less_multiset\<^sub>H\<^sub>O |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
235 |
by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff) |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
236 |
|
59813 | 237 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
238 |
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
239 |
by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq) |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
240 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
241 |
lemma less_eq_multiset_total: |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
242 |
fixes M N :: "'a :: linorder multiset" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
243 |
shows "\<not> M \<le> N \<Longrightarrow> N \<le> M" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
244 |
by simp |
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
245 |
|
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
246 |
instantiation multiset :: (wellorder) wellorder |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
247 |
begin |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
248 |
|
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
249 |
lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}" |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
250 |
unfolding less_multiset_def by (auto intro: wf_mult wf) |
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
251 |
|
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
252 |
instance by standard (metis less_multiset_def wf wf_def wf_mult) |
59813 | 253 |
|
254 |
end |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
255 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
256 |
instantiation multiset :: (preorder) order_bot |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
257 |
begin |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
258 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
259 |
definition bot_multiset :: "'a multiset" where "bot_multiset = {#}" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
260 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
261 |
instance by standard (simp add: bot_multiset_def) |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
262 |
|
63409
3f3223b90239
moved lemmas and locales around (with minor incompatibilities)
blanchet
parents:
63407
diff
changeset
|
263 |
end |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
264 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
265 |
instance multiset :: (preorder) no_top |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
266 |
proof standard |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
267 |
fix x :: "'a multiset" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
268 |
obtain a :: 'a where True by simp |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
269 |
have "x < x + (x + {#a#})" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
270 |
by simp |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
271 |
then show "\<exists>y. x < y" |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
272 |
by blast |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
273 |
qed |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
274 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
275 |
instance multiset :: (preorder) ordered_cancel_comm_monoid_add |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
276 |
by standard |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
277 |
|
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63409
diff
changeset
|
278 |
end |