src/HOL/Library/Multiset_Order.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 67020 c32254ab1901 permissions -rw-r--r--
improved code equations taken over from AFP
 blanchet@59813 ` 1` ```(* Title: HOL/Library/Multiset_Order.thy ``` blanchet@59813 ` 2` ``` Author: Dmitriy Traytel, TU Muenchen ``` blanchet@59813 ` 3` ``` Author: Jasmin Blanchette, Inria, LORIA, MPII ``` blanchet@59813 ` 4` ```*) ``` blanchet@59813 ` 5` wenzelm@60500 ` 6` ```section \More Theorems about the Multiset Order\ ``` blanchet@59813 ` 7` blanchet@59813 ` 8` ```theory Multiset_Order ``` blanchet@59813 ` 9` ```imports Multiset ``` blanchet@59813 ` 10` ```begin ``` blanchet@59813 ` 11` blanchet@65546 ` 12` ```subsection \Alternative Characterizations\ ``` blanchet@59813 ` 13` Mathias@63410 ` 14` ```context preorder ``` blanchet@59813 ` 15` ```begin ``` blanchet@59813 ` 16` blanchet@59813 ` 17` ```lemma order_mult: "class.order ``` blanchet@59813 ` 18` ``` (\M N. (M, N) \ mult {(x, y). x < y} \ M = N) ``` blanchet@59813 ` 19` ``` (\M N. (M, N) \ mult {(x, y). x < y})" ``` blanchet@59813 ` 20` ``` (is "class.order ?le ?less") ``` blanchet@59813 ` 21` ```proof - ``` blanchet@59813 ` 22` ``` have irrefl: "\M :: 'a multiset. \ ?less M M" ``` blanchet@59813 ` 23` ``` proof ``` blanchet@59813 ` 24` ``` fix M :: "'a multiset" ``` blanchet@59813 ` 25` ``` have "trans {(x'::'a, x). x' < x}" ``` Mathias@63410 ` 26` ``` by (rule transI) (blast intro: less_trans) ``` blanchet@59813 ` 27` ``` moreover ``` blanchet@59813 ` 28` ``` assume "(M, M) \ mult {(x, y). x < y}" ``` blanchet@59813 ` 29` ``` ultimately have "\I J K. M = I + J \ M = I + K ``` nipkow@60495 ` 30` ``` \ J \ {#} \ (\k\set_mset K. \j\set_mset J. (k, j) \ {(x, y). x < y})" ``` blanchet@59813 ` 31` ``` by (rule mult_implies_one_step) ``` blanchet@59813 ` 32` ``` then obtain I J K where "M = I + J" and "M = I + K" ``` nipkow@60495 ` 33` ``` and "J \ {#}" and "(\k\set_mset K. \j\set_mset J. (k, j) \ {(x, y). x < y})" by blast ``` nipkow@60495 ` 34` ``` then have aux1: "K \ {#}" and aux2: "\k\set_mset K. \j\set_mset K. k < j" by auto ``` nipkow@60495 ` 35` ``` have "finite (set_mset K)" by simp ``` blanchet@59813 ` 36` ``` moreover note aux2 ``` nipkow@60495 ` 37` ``` ultimately have "set_mset K = {}" ``` blanchet@59813 ` 38` ``` by (induct rule: finite_induct) ``` blanchet@59813 ` 39` ``` (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans) ``` blanchet@59813 ` 40` ``` with aux1 show False by simp ``` blanchet@59813 ` 41` ``` qed ``` blanchet@59813 ` 42` ``` have trans: "\K M N :: 'a multiset. ?less K M \ ?less M N \ ?less K N" ``` blanchet@59813 ` 43` ``` unfolding mult_def by (blast intro: trancl_trans) ``` blanchet@59813 ` 44` ``` show "class.order ?le ?less" ``` Mathias@63388 ` 45` ``` by standard (auto simp add: less_eq_multiset_def irrefl dest: trans) ``` blanchet@59813 ` 46` ```qed ``` blanchet@59813 ` 47` wenzelm@60500 ` 48` ```text \The Dershowitz--Manna ordering:\ ``` blanchet@59813 ` 49` blanchet@59813 ` 50` ```definition less_multiset\<^sub>D\<^sub>M where ``` blanchet@59813 ` 51` ``` "less_multiset\<^sub>D\<^sub>M M N \ ``` haftmann@64587 ` 52` ``` (\X Y. X \ {#} \ X \# N \ M = (N - X) + Y \ (\k. k \# Y \ (\a. a \# X \ k < a)))" ``` blanchet@59813 ` 53` blanchet@59813 ` 54` wenzelm@60500 ` 55` ```text \The Huet--Oppen ordering:\ ``` blanchet@59813 ` 56` blanchet@59813 ` 57` ```definition less_multiset\<^sub>H\<^sub>O where ``` blanchet@59813 ` 58` ``` "less_multiset\<^sub>H\<^sub>O M N \ M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))" ``` blanchet@59813 ` 59` haftmann@62430 ` 60` ```lemma mult_imp_less_multiset\<^sub>H\<^sub>O: ``` haftmann@62430 ` 61` ``` "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>H\<^sub>O M N" ``` haftmann@62430 ` 62` ```proof (unfold mult_def, induct rule: trancl_induct) ``` blanchet@59813 ` 63` ``` case (base P) ``` haftmann@62430 ` 64` ``` then show ?case ``` haftmann@62430 ` 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) ``` blanchet@59813 ` 66` ```next ``` blanchet@59813 ` 67` ``` case (step N P) ``` haftmann@62430 ` 68` ``` from step(3) have "M \ N" and ``` haftmann@62430 ` 69` ``` **: "\y. count N y < count M y \ (\x>y. count M x < count N x)" ``` haftmann@62430 ` 70` ``` by (simp_all add: less_multiset\<^sub>H\<^sub>O_def) ``` blanchet@59813 ` 71` ``` from step(2) obtain M0 a K where ``` Mathias@63793 ` 72` ``` *: "P = add_mset a M0" "N = M0 + K" "a \# K" "\b. b \# K \ b < a" ``` haftmann@62430 ` 73` ``` by (blast elim: mult1_lessE) ``` Mathias@63410 ` 74` ``` from \M \ N\ ** *(1,2,3) have "M \ P" by (force dest: *(4) elim!: less_asym split: if_splits ) ``` blanchet@59813 ` 75` ``` moreover ``` blanchet@59813 ` 76` ``` { assume "count P a \ count M a" ``` haftmann@62430 ` 77` ``` with \a \# K\ have "count N a < count M a" unfolding *(1,2) ``` haftmann@62430 ` 78` ``` by (auto simp add: not_in_iff) ``` haftmann@62430 ` 79` ``` with ** obtain z where z: "z > a" "count M z < count N z" ``` haftmann@62430 ` 80` ``` by blast ``` haftmann@62430 ` 81` ``` with * have "count N z \ count P z" ``` Mathias@63410 ` 82` ``` by (auto elim: less_asym intro: count_inI) ``` blanchet@59813 ` 83` ``` with z have "\z > a. count M z < count P z" by auto ``` blanchet@59813 ` 84` ``` } note count_a = this ``` blanchet@59813 ` 85` ``` { fix y ``` blanchet@59813 ` 86` ``` assume count_y: "count P y < count M y" ``` blanchet@59813 ` 87` ``` have "\x>y. count M x < count P x" ``` blanchet@59813 ` 88` ``` proof (cases "y = a") ``` blanchet@59813 ` 89` ``` case True ``` blanchet@59813 ` 90` ``` with count_y count_a show ?thesis by auto ``` blanchet@59813 ` 91` ``` next ``` blanchet@59813 ` 92` ``` case False ``` blanchet@59813 ` 93` ``` show ?thesis ``` blanchet@59813 ` 94` ``` proof (cases "y \# K") ``` blanchet@59813 ` 95` ``` case True ``` haftmann@62430 ` 96` ``` with *(4) have "y < a" by simp ``` blanchet@59813 ` 97` ``` then show ?thesis by (cases "count P a \ count M a") (auto dest: count_a intro: less_trans) ``` blanchet@59813 ` 98` ``` next ``` blanchet@59813 ` 99` ``` case False ``` haftmann@62430 ` 100` ``` with \y \ a\ have "count P y = count N y" unfolding *(1,2) ``` haftmann@62430 ` 101` ``` by (simp add: not_in_iff) ``` haftmann@62430 ` 102` ``` with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto ``` blanchet@59813 ` 103` ``` show ?thesis ``` blanchet@59813 ` 104` ``` proof (cases "z \# K") ``` blanchet@59813 ` 105` ``` case True ``` haftmann@62430 ` 106` ``` with *(4) have "z < a" by simp ``` blanchet@59813 ` 107` ``` with z(1) show ?thesis ``` blanchet@59813 ` 108` ``` by (cases "count P a \ count M a") (auto dest!: count_a intro: less_trans) ``` blanchet@59813 ` 109` ``` next ``` blanchet@59813 ` 110` ``` case False ``` haftmann@62430 ` 111` ``` with \a \# K\ have "count N z \ count P z" unfolding * ``` haftmann@62430 ` 112` ``` by (auto simp add: not_in_iff) ``` blanchet@59813 ` 113` ``` with z show ?thesis by auto ``` blanchet@59813 ` 114` ``` qed ``` blanchet@59813 ` 115` ``` qed ``` blanchet@59813 ` 116` ``` qed ``` blanchet@59813 ` 117` ``` } ``` haftmann@62430 ` 118` ``` ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast ``` blanchet@59813 ` 119` ```qed ``` blanchet@59813 ` 120` blanchet@59813 ` 121` ```lemma less_multiset\<^sub>D\<^sub>M_imp_mult: ``` blanchet@59813 ` 122` ``` "less_multiset\<^sub>D\<^sub>M M N \ (M, N) \ mult {(x, y). x < y}" ``` blanchet@59813 ` 123` ```proof - ``` blanchet@59813 ` 124` ``` assume "less_multiset\<^sub>D\<^sub>M M N" ``` blanchet@59813 ` 125` ``` then obtain X Y where ``` haftmann@64587 ` 126` ``` "X \ {#}" and "X \# N" and "M = N - X + Y" and "\k. k \# Y \ (\a. a \# X \ k < a)" ``` blanchet@59813 ` 127` ``` unfolding less_multiset\<^sub>D\<^sub>M_def by blast ``` blanchet@59813 ` 128` ``` then have "(N - X + Y, N - X + X) \ mult {(x, y). x < y}" ``` blanchet@59813 ` 129` ``` by (intro one_step_implies_mult) (auto simp: Bex_def trans_def) ``` haftmann@64587 ` 130` ``` with \M = N - X + Y\ \X \# N\ show "(M, N) \ mult {(x, y). x < y}" ``` Mathias@60397 ` 131` ``` by (metis subset_mset.diff_add) ``` blanchet@59813 ` 132` ```qed ``` blanchet@59813 ` 133` blanchet@59813 ` 134` ```lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \ less_multiset\<^sub>D\<^sub>M M N" ``` blanchet@59813 ` 135` ```unfolding less_multiset\<^sub>D\<^sub>M_def ``` blanchet@59813 ` 136` ```proof (intro iffI exI conjI) ``` blanchet@59813 ` 137` ``` assume "less_multiset\<^sub>H\<^sub>O M N" ``` blanchet@59813 ` 138` ``` then obtain z where z: "count M z < count N z" ``` blanchet@59813 ` 139` ``` unfolding less_multiset\<^sub>H\<^sub>O_def by (auto simp: multiset_eq_iff nat_neq_iff) ``` wenzelm@63040 ` 140` ``` define X where "X = N - M" ``` wenzelm@63040 ` 141` ``` define Y where "Y = M - N" ``` blanchet@59813 ` 142` ``` from z show "X \ {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq) ``` haftmann@64587 ` 143` ``` from z show "X \# N" unfolding X_def by auto ``` blanchet@59813 ` 144` ``` show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force ``` blanchet@59813 ` 145` ``` show "\k. k \# Y \ (\a. a \# X \ k < a)" ``` blanchet@59813 ` 146` ``` proof (intro allI impI) ``` blanchet@59813 ` 147` ``` fix k ``` blanchet@59813 ` 148` ``` assume "k \# Y" ``` haftmann@62430 ` 149` ``` then have "count N k < count M k" unfolding Y_def ``` haftmann@62430 ` 150` ``` by (auto simp add: in_diff_count) ``` wenzelm@60500 ` 151` ``` with \less_multiset\<^sub>H\<^sub>O M N\ obtain a where "k < a" and "count M a < count N a" ``` blanchet@59813 ` 152` ``` unfolding less_multiset\<^sub>H\<^sub>O_def by blast ``` haftmann@62430 ` 153` ``` then show "\a. a \# X \ k < a" unfolding X_def ``` haftmann@62430 ` 154` ``` by (auto simp add: in_diff_count) ``` blanchet@59813 ` 155` ``` qed ``` blanchet@59813 ` 156` ```qed ``` blanchet@59813 ` 157` blanchet@59813 ` 158` ```lemma mult_less_multiset\<^sub>D\<^sub>M: "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>D\<^sub>M M N" ``` blanchet@59813 ` 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) ``` blanchet@59813 ` 160` blanchet@59813 ` 161` ```lemma mult_less_multiset\<^sub>H\<^sub>O: "(M, N) \ mult {(x, y). x < y} \ less_multiset\<^sub>H\<^sub>O M N" ``` blanchet@59813 ` 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) ``` blanchet@59813 ` 163` blanchet@59813 ` 164` ```lemmas mult\<^sub>D\<^sub>M = mult_less_multiset\<^sub>D\<^sub>M[unfolded less_multiset\<^sub>D\<^sub>M_def] ``` blanchet@59813 ` 165` ```lemmas mult\<^sub>H\<^sub>O = mult_less_multiset\<^sub>H\<^sub>O[unfolded less_multiset\<^sub>H\<^sub>O_def] ``` blanchet@59813 ` 166` blanchet@59813 ` 167` ```end ``` blanchet@59813 ` 168` blanchet@67020 ` 169` ```lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \ less_multiset\<^sub>H\<^sub>O M N" ``` blanchet@59813 ` 170` ``` unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def .. ``` blanchet@59813 ` 171` blanchet@59813 ` 172` ```lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def] ``` blanchet@59813 ` 173` ```lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def] ``` blanchet@59813 ` 174` Mathias@63388 ` 175` ```lemma subset_eq_imp_le_multiset: ``` haftmann@64587 ` 176` ``` shows "M \# N \ M \ N" ``` Mathias@63388 ` 177` ``` unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O ``` Mathias@60397 ` 178` ``` by (simp add: less_le_not_le subseteq_mset_def) ``` blanchet@59813 ` 179` blanchet@67020 ` 180` ```(* FIXME: "le" should be "less" in this and other names *) ``` blanchet@67020 ` 181` ```lemma le_multiset_right_total: "M < add_mset x M" ``` Mathias@63388 ` 182` ``` unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp ``` Mathias@63388 ` 183` Mathias@63388 ` 184` ```lemma less_eq_multiset_empty_left[simp]: ``` Mathias@63388 ` 185` ``` shows "{#} \ M" ``` Mathias@63388 ` 186` ``` by (simp add: subset_eq_imp_le_multiset) ``` Mathias@63388 ` 187` blanchet@63409 ` 188` ```lemma ex_gt_imp_less_multiset: "(\y. y \# N \ (\x. x \# M \ x < y)) \ M < N" ``` blanchet@63409 ` 189` ``` unfolding less_multiset\<^sub>H\<^sub>O ``` blanchet@63409 ` 190` ``` by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le) ``` blanchet@63409 ` 191` blanchet@67020 ` 192` ```lemma less_eq_multiset_empty_right[simp]: "M \ {#} \ \ M \ {#}" ``` Mathias@63388 ` 193` ``` by (metis less_eq_multiset_empty_left antisym) ``` blanchet@59813 ` 194` blanchet@67020 ` 195` ```(* FIXME: "le" should be "less" in this and other names *) ``` blanchet@63409 ` 196` ```lemma le_multiset_empty_left[simp]: "M \ {#} \ {#} < M" ``` Mathias@63388 ` 197` ``` by (simp add: less_multiset\<^sub>H\<^sub>O) ``` blanchet@59813 ` 198` blanchet@67020 ` 199` ```(* FIXME: "le" should be "less" in this and other names *) ``` blanchet@63409 ` 200` ```lemma le_multiset_empty_right[simp]: "\ M < {#}" ``` Mathias@64076 ` 201` ``` using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast ``` blanchet@59813 ` 202` blanchet@67020 ` 203` ```(* FIXME: "le" should be "less" in this and other names *) ``` haftmann@64587 ` 204` ```lemma union_le_diff_plus: "P \# M \ N < P \ M - P + N < M" ``` blanchet@63409 ` 205` ``` by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2) ``` blanchet@63409 ` 206` Mathias@63525 ` 207` ```instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le ``` blanchet@63409 ` 208` ```begin ``` blanchet@63409 ` 209` blanchet@63409 ` 210` ```lemma less_eq_multiset\<^sub>H\<^sub>O: ``` blanchet@63409 ` 211` ``` "M \ N \ (\y. count N y < count M y \ (\x. y < x \ count M x < count N x))" ``` blanchet@63409 ` 212` ``` by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O) ``` blanchet@63409 ` 213` Mathias@63410 ` 214` ```instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O) ``` blanchet@63409 ` 215` blanchet@59813 ` 216` ```lemma ``` blanchet@63409 ` 217` ``` fixes M N :: "'a multiset" ``` blanchet@59813 ` 218` ``` shows ``` Mathias@63525 ` 219` ``` less_eq_multiset_plus_left: "N \ (M + N)" and ``` Mathias@63525 ` 220` ``` less_eq_multiset_plus_right: "M \ (M + N)" ``` Mathias@63410 ` 221` ``` by simp_all ``` blanchet@59813 ` 222` blanchet@59813 ` 223` ```lemma ``` blanchet@63409 ` 224` ``` fixes M N :: "'a multiset" ``` blanchet@59813 ` 225` ``` shows ``` Mathias@63525 ` 226` ``` le_multiset_plus_left_nonempty: "M \ {#} \ N < M + N" and ``` Mathias@63525 ` 227` ``` le_multiset_plus_right_nonempty: "N \ {#} \ M < M + N" ``` Mathias@63525 ` 228` ``` by simp_all ``` Mathias@63388 ` 229` Mathias@63410 ` 230` ```end ``` Mathias@63410 ` 231` blanchet@65546 ` 232` ```lemma all_lt_Max_imp_lt_mset: "N \ {#} \ (\a \# M. a < Max (set_mset N)) \ M < N" ``` blanchet@65546 ` 233` ``` by (meson Max_in[OF finite_set_mset] ex_gt_imp_less_multiset set_mset_eq_empty_iff) ``` blanchet@65546 ` 234` blanchet@65546 ` 235` ```lemma lt_imp_ex_count_lt: "M < N \ \y. count M y < count N y" ``` blanchet@65546 ` 236` ``` by (meson less_eq_multiset\<^sub>H\<^sub>O less_le_not_le) ``` blanchet@65546 ` 237` blanchet@65546 ` 238` ```lemma subset_imp_less_mset: "A \# B \ A < B" ``` blanchet@65546 ` 239` ``` by (simp add: order.not_eq_order_implies_strict subset_eq_imp_le_multiset) ``` blanchet@65546 ` 240` blanchet@65546 ` 241` ```lemma image_mset_strict_mono: ``` blanchet@65546 ` 242` ``` assumes ``` blanchet@65546 ` 243` ``` mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y" and ``` blanchet@65546 ` 244` ``` less: "M < N" ``` blanchet@65546 ` 245` ``` shows "image_mset f M < image_mset f N" ``` blanchet@65546 ` 246` ```proof - ``` blanchet@65546 ` 247` ``` obtain Y X where ``` blanchet@65546 ` 248` ``` y_nemp: "Y \ {#}" and y_sub_N: "Y \# N" and M_eq: "M = N - Y + X" and ``` blanchet@65546 ` 249` ``` ex_y: "\x. x \# X \ (\y. y \# Y \ x < y)" ``` blanchet@65546 ` 250` ``` using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast ``` blanchet@65546 ` 251` blanchet@65546 ` 252` ``` have x_sub_M: "X \# M" ``` blanchet@65546 ` 253` ``` using M_eq by simp ``` blanchet@65546 ` 254` blanchet@65546 ` 255` ``` let ?fY = "image_mset f Y" ``` blanchet@65546 ` 256` ``` let ?fX = "image_mset f X" ``` blanchet@65546 ` 257` blanchet@65546 ` 258` ``` show ?thesis ``` blanchet@65546 ` 259` ``` unfolding less_multiset\<^sub>D\<^sub>M ``` blanchet@65546 ` 260` ``` proof (intro exI conjI) ``` blanchet@65546 ` 261` ``` show "image_mset f M = image_mset f N - ?fY + ?fX" ``` blanchet@65546 ` 262` ``` using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N ``` blanchet@65546 ` 263` ``` by (metis image_mset_Diff image_mset_union) ``` blanchet@65546 ` 264` ``` next ``` blanchet@65546 ` 265` ``` obtain y where y: "\x. x \# X \ y x \# Y \ x < y x" ``` blanchet@65546 ` 266` ``` using ex_y by moura ``` blanchet@65546 ` 267` blanchet@65546 ` 268` ``` show "\fx. fx \# ?fX \ (\fy. fy \# ?fY \ fx < fy)" ``` blanchet@65546 ` 269` ``` proof (intro allI impI) ``` blanchet@65546 ` 270` ``` fix fx ``` blanchet@65546 ` 271` ``` assume "fx \# ?fX" ``` blanchet@65546 ` 272` ``` then obtain x where fx: "fx = f x" and x_in: "x \# X" ``` blanchet@65546 ` 273` ``` by auto ``` blanchet@65546 ` 274` ``` hence y_in: "y x \# Y" and y_gt: "x < y x" ``` blanchet@65546 ` 275` ``` using y[rule_format, OF x_in] by blast+ ``` blanchet@65546 ` 276` ``` hence "f (y x) \# ?fY \ f x < f (y x)" ``` blanchet@65546 ` 277` ``` using mono_f y_sub_N x_sub_M x_in ``` blanchet@65546 ` 278` ``` by (metis image_eqI in_image_mset mset_subset_eqD) ``` blanchet@65546 ` 279` ``` thus "\fy. fy \# ?fY \ fx < fy" ``` blanchet@65546 ` 280` ``` unfolding fx by auto ``` blanchet@65546 ` 281` ``` qed ``` blanchet@65546 ` 282` ``` qed (auto simp: y_nemp y_sub_N image_mset_subseteq_mono) ``` blanchet@65546 ` 283` ```qed ``` blanchet@65546 ` 284` blanchet@65546 ` 285` ```lemma image_mset_mono: ``` blanchet@65546 ` 286` ``` assumes ``` blanchet@65546 ` 287` ``` mono_f: "\x \ set_mset M. \y \ set_mset N. x < y \ f x < f y" and ``` blanchet@65546 ` 288` ``` less: "M \ N" ``` blanchet@65546 ` 289` ``` shows "image_mset f M \ image_mset f N" ``` blanchet@65546 ` 290` ``` by (metis eq_iff image_mset_strict_mono less less_imp_le mono_f order.not_eq_order_implies_strict) ``` blanchet@65546 ` 291` blanchet@65546 ` 292` ```lemma mset_lt_single_right_iff[simp]: "M < {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder" ``` blanchet@65546 ` 293` ```proof (rule iffI) ``` blanchet@65546 ` 294` ``` assume M_lt_y: "M < {#y#}" ``` blanchet@65546 ` 295` ``` show "\x \# M. x < y" ``` blanchet@65546 ` 296` ``` proof ``` blanchet@65546 ` 297` ``` fix x ``` blanchet@65546 ` 298` ``` assume x_in: "x \# M" ``` blanchet@65546 ` 299` ``` hence M: "M - {#x#} + {#x#} = M" ``` blanchet@65546 ` 300` ``` by (meson insert_DiffM2) ``` blanchet@65546 ` 301` ``` hence "\ {#x#} < {#y#} \ x < y" ``` blanchet@65546 ` 302` ``` using x_in M_lt_y ``` blanchet@65546 ` 303` ``` by (metis diff_single_eq_union le_multiset_empty_left less_add_same_cancel2 mset_le_trans) ``` blanchet@65546 ` 304` ``` also have "\ {#y#} < M" ``` blanchet@65546 ` 305` ``` using M_lt_y mset_le_not_sym by blast ``` blanchet@65546 ` 306` ``` ultimately show "x < y" ``` blanchet@65546 ` 307` ``` by (metis (no_types) Max_ge all_lt_Max_imp_lt_mset empty_iff finite_set_mset insertE ``` blanchet@65546 ` 308` ``` less_le_trans linorder_less_linear mset_le_not_sym set_mset_add_mset_insert ``` blanchet@65546 ` 309` ``` set_mset_eq_empty_iff x_in) ``` blanchet@65546 ` 310` ``` qed ``` blanchet@65546 ` 311` ```next ``` blanchet@65546 ` 312` ``` assume y_max: "\x \# M. x < y" ``` blanchet@65546 ` 313` ``` show "M < {#y#}" ``` blanchet@65546 ` 314` ``` by (rule all_lt_Max_imp_lt_mset) (auto intro!: y_max) ``` blanchet@65546 ` 315` ```qed ``` blanchet@65546 ` 316` blanchet@65546 ` 317` ```lemma mset_le_single_right_iff[simp]: ``` blanchet@65546 ` 318` ``` "M \ {#y#} \ M = {#y#} \ (\x \# M. x < y)" for y :: "'a::linorder" ``` blanchet@65546 ` 319` ``` by (meson less_eq_multiset_def mset_lt_single_right_iff) ``` blanchet@65546 ` 320` Mathias@63793 ` 321` Mathias@63793 ` 322` ```subsection \Simprocs\ ``` Mathias@63793 ` 323` Mathias@63793 ` 324` ```lemma mset_le_add_iff1: ``` Mathias@63793 ` 325` ``` "j \ (i::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (repeat_mset (i-j) u + m \ n)" ``` Mathias@63793 ` 326` ```proof - ``` Mathias@63793 ` 327` ``` assume "j \ i" ``` Mathias@63793 ` 328` ``` then have "j + (i - j) = i" ``` Mathias@63793 ` 329` ``` using le_add_diff_inverse by blast ``` Mathias@63793 ` 330` ``` then show ?thesis ``` Mathias@63793 ` 331` ``` by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset) ``` Mathias@63793 ` 332` ```qed ``` Mathias@63793 ` 333` Mathias@63793 ` 334` ```lemma mset_le_add_iff2: ``` Mathias@63793 ` 335` ``` "i \ (j::nat) \ (repeat_mset i u + m \ repeat_mset j u + n) = (m \ repeat_mset (j-i) u + n)" ``` Mathias@63793 ` 336` ```proof - ``` Mathias@63793 ` 337` ``` assume "i \ j" ``` Mathias@63793 ` 338` ``` then have "i + (j - i) = j" ``` Mathias@63793 ` 339` ``` using le_add_diff_inverse by blast ``` Mathias@63793 ` 340` ``` then show ?thesis ``` Mathias@63793 ` 341` ``` by (metis (no_types) add_le_cancel_left left_add_mult_distrib_mset) ``` Mathias@63793 ` 342` ```qed ``` Mathias@63793 ` 343` Mathias@65027 ` 344` ```simproc_setup msetless_cancel ``` Mathias@63793 ` 345` ``` ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" | ``` Mathias@65028 ` 346` ``` "add_mset a m < n" | "m < add_mset a n" | ``` Mathias@65028 ` 347` ``` "replicate_mset p a < n" | "m < replicate_mset p a" | ``` Mathias@65028 ` 348` ``` "repeat_mset p m < n" | "m < repeat_mset p n") = ``` Mathias@65031 ` 349` ``` \fn phi => Cancel_Simprocs.less_cancel\ ``` Mathias@63793 ` 350` Mathias@65027 ` 351` ```simproc_setup msetle_cancel ``` Mathias@63793 ` 352` ``` ("(l::'a::preorder multiset) + m \ n" | "(l::'a multiset) \ m + n" | ``` Mathias@65028 ` 353` ``` "add_mset a m \ n" | "m \ add_mset a n" | ``` Mathias@65028 ` 354` ``` "replicate_mset p a \ n" | "m \ replicate_mset p a" | ``` Mathias@65028 ` 355` ``` "repeat_mset p m \ n" | "m \ repeat_mset p n") = ``` Mathias@65031 ` 356` ``` \fn phi => Cancel_Simprocs.less_eq_cancel\ ``` Mathias@63793 ` 357` Mathias@63793 ` 358` Mathias@63793 ` 359` ```subsection \Additional facts and instantiations\ ``` Mathias@63793 ` 360` Mathias@63388 ` 361` ```lemma ex_gt_count_imp_le_multiset: ``` Mathias@63410 ` 362` ``` "(\y :: 'a :: order. y \# M + N \ y \ x) \ count M x < count N x \ M < N" ``` haftmann@62430 ` 363` ``` unfolding less_multiset\<^sub>H\<^sub>O ``` Mathias@63410 ` 364` ``` by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff) ``` Mathias@63410 ` 365` Mathias@64418 ` 366` ```lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \ x < y" ``` Mathias@64418 ` 367` ``` unfolding less_multiset\<^sub>H\<^sub>O by simp ``` Mathias@64418 ` 368` Mathias@64418 ` 369` ```lemma mset_le_single_iff[iff]: "{#x#} \ {#y#} \ x \ y" for x y :: "'a::order" ``` Mathias@64418 ` 370` ``` unfolding less_eq_multiset\<^sub>H\<^sub>O by force ``` Mathias@64418 ` 371` Mathias@63410 ` 372` ```instance multiset :: (linorder) linordered_cancel_ab_semigroup_add ``` Mathias@63410 ` 373` ``` by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq) ``` Mathias@63410 ` 374` Mathias@63410 ` 375` ```lemma less_eq_multiset_total: ``` Mathias@63410 ` 376` ``` fixes M N :: "'a :: linorder multiset" ``` Mathias@63410 ` 377` ``` shows "\ M \ N \ N \ M" ``` Mathias@63410 ` 378` ``` by simp ``` blanchet@63409 ` 379` blanchet@63409 ` 380` ```instantiation multiset :: (wellorder) wellorder ``` blanchet@63409 ` 381` ```begin ``` blanchet@63409 ` 382` blanchet@63409 ` 383` ```lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}" ``` blanchet@63409 ` 384` ``` unfolding less_multiset_def by (auto intro: wf_mult wf) ``` blanchet@63409 ` 385` blanchet@63409 ` 386` ```instance by standard (metis less_multiset_def wf wf_def wf_mult) ``` blanchet@59813 ` 387` blanchet@59813 ` 388` ```end ``` blanchet@63409 ` 389` Mathias@63410 ` 390` ```instantiation multiset :: (preorder) order_bot ``` Mathias@63410 ` 391` ```begin ``` Mathias@63410 ` 392` Mathias@63410 ` 393` ```definition bot_multiset :: "'a multiset" where "bot_multiset = {#}" ``` Mathias@63410 ` 394` Mathias@63410 ` 395` ```instance by standard (simp add: bot_multiset_def) ``` Mathias@63410 ` 396` blanchet@63409 ` 397` ```end ``` Mathias@63410 ` 398` Mathias@63410 ` 399` ```instance multiset :: (preorder) no_top ``` Mathias@63410 ` 400` ```proof standard ``` Mathias@63410 ` 401` ``` fix x :: "'a multiset" ``` Mathias@63410 ` 402` ``` obtain a :: 'a where True by simp ``` Mathias@63410 ` 403` ``` have "x < x + (x + {#a#})" ``` Mathias@63410 ` 404` ``` by simp ``` Mathias@63410 ` 405` ``` then show "\y. x < y" ``` Mathias@63410 ` 406` ``` by blast ``` Mathias@63410 ` 407` ```qed ``` Mathias@63410 ` 408` Mathias@63410 ` 409` ```instance multiset :: (preorder) ordered_cancel_comm_monoid_add ``` Mathias@63410 ` 410` ``` by standard ``` Mathias@63410 ` 411` blanchet@65546 ` 412` ```instantiation multiset :: (linorder) distrib_lattice ``` blanchet@65546 ` 413` ```begin ``` blanchet@65546 ` 414` blanchet@65546 ` 415` ```definition inf_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where ``` blanchet@65546 ` 416` ``` "inf_multiset A B = (if A < B then A else B)" ``` blanchet@65546 ` 417` blanchet@65546 ` 418` ```definition sup_multiset :: "'a multiset \ 'a multiset \ 'a multiset" where ``` blanchet@65546 ` 419` ``` "sup_multiset A B = (if B > A then B else A)" ``` blanchet@65546 ` 420` blanchet@65546 ` 421` ```instance ``` blanchet@65546 ` 422` ``` by intro_classes (auto simp: inf_multiset_def sup_multiset_def) ``` blanchet@65546 ` 423` Mathias@63410 ` 424` ```end ``` blanchet@65546 ` 425` blanchet@65546 ` 426` ```end ```