2394 lemma one_step_implies_mult: |
2402 lemma one_step_implies_mult: |
2395 "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r |
2403 "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r |
2396 \<Longrightarrow> (I + K, I + J) \<in> mult r" |
2404 \<Longrightarrow> (I + K, I + J) \<in> mult r" |
2397 using one_step_implies_mult_aux by blast |
2405 using one_step_implies_mult_aux by blast |
2398 |
2406 |
2399 subsection \<open>A quasi-executable characterization\<close> |
2407 |
|
2408 subsection \<open>The multiset extension is cancellative for multiset union\<close> |
|
2409 |
|
2410 lemma mult_cancel: |
|
2411 assumes "trans s" and "irrefl s" |
|
2412 shows "(X + Z, Y + Z) \<in> mult s \<longleftrightarrow> (X, Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R") |
|
2413 proof |
|
2414 assume ?L thus ?R |
|
2415 proof (induct Z) |
|
2416 case (add Z z) |
|
2417 obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \<noteq> {#}" |
|
2418 "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s" |
|
2419 using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast |
|
2420 consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}" |
|
2421 using *(1,2) by (metis mset_add union_iff union_single_eq_member) |
|
2422 thus ?case |
|
2423 proof (cases) |
|
2424 case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2] |
|
2425 by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1)) |
|
2426 next |
|
2427 case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) `irrefl s` |
|
2428 by (auto simp: irrefl_def) |
|
2429 moreover from this transD[OF `trans s` _ this(2)] |
|
2430 have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x' |
|
2431 using 2 *(4)[rule_format, of x'] by auto |
|
2432 ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2 |
|
2433 by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1)) |
|
2434 qed |
|
2435 qed auto |
|
2436 next |
|
2437 assume ?R then obtain I J K |
|
2438 where "Y = I + J" "X = I + K" "J \<noteq> {#}" "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> s" |
|
2439 using mult_implies_one_step[OF `trans s`] by blast |
|
2440 thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps) |
|
2441 qed |
|
2442 |
|
2443 lemma mult_cancel_max: |
|
2444 assumes "trans s" and "irrefl s" |
|
2445 shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X #\<inter> Y, Y - X #\<inter> Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R") |
|
2446 proof - |
|
2447 have "X - X #\<inter> Y + X #\<inter> Y = X" "Y - X #\<inter> Y + X #\<inter> Y = Y" by (auto simp: count_inject[symmetric]) |
|
2448 thus ?thesis using mult_cancel[OF assms, of "X - X #\<inter> Y" "X #\<inter> Y" "Y - X #\<inter> Y"] by auto |
|
2449 qed |
|
2450 |
|
2451 |
|
2452 subsection \<open>Quasi-executable version of the multiset extension\<close> |
2400 |
2453 |
2401 text \<open> |
2454 text \<open> |
2402 The decreasing parts \<open>A\<close> and \<open>B\<close> of multisets in a multiset-comparison |
2455 Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are |
2403 \<open>(I + B, I + A) \<in> mult r\<close>, can always be made disjoint. |
2456 executable whenever the given predicate \<open>P\<close> is. Together with the standard |
|
2457 code equations for \<open>op #\<inter>\<close> and \<open>op -\<close> this should yield quadratic |
|
2458 (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>. |
2404 \<close> |
2459 \<close> |
2405 lemma decreasing_parts_disj: |
2460 |
2406 assumes "irrefl r" and "trans r" |
2461 definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
2407 and "A \<noteq> {#}" and *: "\<forall>b\<in>#B. \<exists>a\<in>#A. (b, a) \<in> r" |
2462 "multp P N M = |
2408 defines "Z \<equiv> A #\<inter> B" |
2463 (let Z = M #\<inter> N; X = M - Z in |
2409 defines "X \<equiv> A - Z" |
2464 X \<noteq> {#} \<and> (let Y = N - Z in (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x)))" |
2410 defines "Y \<equiv> B - Z" |
2465 |
2411 shows "X \<noteq> {#} \<and> X #\<inter> Y = {#} \<and> |
|
2412 A = X + Z \<and> B = Y + Z \<and> (\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r)" |
|
2413 proof - |
|
2414 define D |
|
2415 where "D = set_mset A \<union> set_mset B" |
|
2416 let ?r = "r \<inter> D \<times> D" |
|
2417 have "irrefl ?r" and "trans ?r" and "finite ?r" |
|
2418 using \<open>irrefl r\<close> and \<open>trans r\<close> by (auto simp: D_def irrefl_def trans_Restr) |
|
2419 note wf_converse_induct = wf_induct [OF wf_converse [OF this]] |
|
2420 { fix b assume "b \<in># B" |
|
2421 then have "\<exists>x. x \<in># X \<and> (b, x) \<in> r" |
|
2422 proof (induction rule: wf_converse_induct) |
|
2423 case (1 b) |
|
2424 then obtain a where "b \<in># B" and "a \<in># A" and "(b, a) \<in> r" |
|
2425 using * by blast |
|
2426 then show ?case |
|
2427 proof (cases "a \<in># X") |
|
2428 case False |
|
2429 then have "a \<in># B" using \<open>a \<in># A\<close> |
|
2430 by (simp add: X_def Z_def not_in_iff) |
|
2431 (metis le_zero_eq not_in_iff) |
|
2432 moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>" |
|
2433 using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close> |
|
2434 by (auto simp: D_def) |
|
2435 ultimately obtain x where x: "x \<in># X" "(a, x) \<in> r" |
|
2436 using "1.IH" by blast |
|
2437 then have "(b, x) \<in> r" |
|
2438 using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD) |
|
2439 with x show ?thesis by blast |
|
2440 qed blast |
|
2441 qed } |
|
2442 note B_less = this |
|
2443 then have "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> r" |
|
2444 by (auto simp: Y_def Z_def dest: in_diffD) |
|
2445 moreover have "X \<noteq> {#}" |
|
2446 proof - |
|
2447 obtain a where "a \<in># A" using \<open>A \<noteq> {#}\<close> |
|
2448 by (auto simp: multiset_eq_iff) |
|
2449 show ?thesis |
|
2450 proof (cases "a \<in># X") |
|
2451 case False |
|
2452 then have "a \<in># B" using \<open>a \<in># A\<close> |
|
2453 by (simp add: X_def Z_def not_in_iff) |
|
2454 (metis le_zero_eq not_in_iff) |
|
2455 then show ?thesis by (auto dest: B_less) |
|
2456 qed auto |
|
2457 qed |
|
2458 moreover have "A = X + Z" and "B = Y + Z" and "X #\<inter> Y = {#}" |
|
2459 by (auto simp: X_def Y_def Z_def multiset_eq_iff) |
|
2460 ultimately show ?thesis by blast |
|
2461 qed |
|
2462 |
|
2463 text \<open> |
|
2464 A predicate variant of the reflexive closure of \<open>mult\<close>, which is |
|
2465 executable whenever the given predicate \<open>P\<close> is. Together with the |
|
2466 standard code equations for \<open>op #\<inter>\<close> and \<open>op -\<close> this should yield |
|
2467 a quadratic (with respect to calls to \<open>P\<close>) implementation of \<open>multeqp\<close>. |
|
2468 \<close> |
|
2469 definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
2466 definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where |
2470 "multeqp P N M = |
2467 "multeqp P N M = |
2471 (let Z = M #\<inter> N; X = M - Z; Y = N - Z in |
2468 (let Z = M #\<inter> N; X = M - Z; Y = N - Z in |
2472 (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))" |
2469 (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))" |
2473 |
2470 |
|
2471 lemma multp_iff: |
|
2472 assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R" |
|
2473 shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R") |
|
2474 proof - |
|
2475 have *: "M #\<inter> N + (N - M #\<inter> N) = N" "M #\<inter> N + (M - M #\<inter> N) = M" |
|
2476 "(M - M #\<inter> N) #\<inter> (N - M #\<inter> N) = {#}" by (auto simp: count_inject[symmetric]) |
|
2477 show ?thesis |
|
2478 proof |
|
2479 assume ?L thus ?R |
|
2480 using one_step_implies_mult[of "M - M #\<inter> N" "N - M #\<inter> N" R "M #\<inter> N"] * |
|
2481 by (auto simp: multp_def Let_def) |
|
2482 next |
|
2483 { fix I J K :: "'a multiset" assume "(I + J) #\<inter> (I + K) = {#}" |
|
2484 then have "I = {#}" by (metis inter_union_distrib_right union_eq_empty) |
|
2485 } note [dest!] = this |
|
2486 assume ?R thus ?L |
|
2487 using mult_implies_one_step[OF assms(2), of "N - M #\<inter> N" "M - M #\<inter> N"] |
|
2488 mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def ac_simps) |
|
2489 qed |
|
2490 qed |
|
2491 |
2474 lemma multeqp_iff: |
2492 lemma multeqp_iff: |
2475 assumes "irrefl R" and "trans R" |
2493 assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R" |
2476 and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R" |
|
2477 shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>=" |
2494 shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>=" |
2478 proof |
2495 proof - |
2479 assume "(N, M) \<in> (mult R)\<^sup>=" |
2496 { assume "N \<noteq> M" "M - M #\<inter> N = {#}" |
2480 then show "multeqp P N M" |
2497 then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric]) |
2481 proof |
2498 then have "\<exists>y. count M y < count N y" using `M - M #\<inter> N = {#}` |
2482 assume "(N, M) \<in> mult R" |
2499 by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y]) |
2483 from mult_implies_one_step [OF \<open>trans R\<close> this] obtain I J K |
2500 } |
2484 where *: "I \<noteq> {#}" "\<forall>j\<in>#J. \<exists>i\<in>#I. (j, i) \<in> R" |
2501 then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M" |
2485 and [simp]: "M = K + I" "N = K + J" by blast |
2502 by (auto simp: multeqp_def multp_def Let_def in_diff_count) |
2486 from decreasing_parts_disj [OF \<open>irrefl R\<close> \<open>trans R\<close> *] |
2503 thus ?thesis using multp_iff[OF assms] by simp |
2487 show "multeqp P N M" |
|
2488 by (auto simp: multeqp_def split: if_splits) |
|
2489 next |
|
2490 assume "(N, M) \<in> Id" then show "multeqp P N M" by (auto simp: multeqp_def) |
|
2491 qed |
|
2492 next |
|
2493 assume "multeqp P N M" |
|
2494 then obtain X Y Z where *: "Z = M #\<inter> N" "X = M - Z" "Y = N - Z" |
|
2495 and **: "\<forall>y\<in>#Y. \<exists>x\<in>#X. (y, x) \<in> R" by (auto simp: multeqp_def Let_def) |
|
2496 then have M: "M = Z + X" and N: "N = Z + Y" by (auto simp: multiset_eq_iff) |
|
2497 show "(N, M) \<in> (mult R)\<^sup>=" |
|
2498 proof (cases "X \<noteq> {#}") |
|
2499 case True |
|
2500 with * and ** have "(Z + Y, Z + X) \<in> mult R" |
|
2501 by (auto intro: one_step_implies_mult) |
|
2502 then show ?thesis by (simp add: M N) |
|
2503 next |
|
2504 case False |
|
2505 then show ?thesis using ** |
|
2506 by (cases "Y = {#}") (auto simp: M N) |
|
2507 qed |
|
2508 qed |
2504 qed |
2509 |
2505 |
2510 |
2506 |
2511 subsubsection \<open>Partial-order properties\<close> |
2507 subsubsection \<open>Partial-order properties\<close> |
2512 |
2508 |