812 show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#" |
812 show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#" |
813 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
813 by standard (auto simp add: sup_subset_mset_def subseteq_mset_def) |
814 qed |
814 qed |
815 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
815 \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close> |
816 |
816 |
|
817 interpretation subset_mset: bounded_lattice_bot "op #\<inter>" "op \<subseteq>#" "op \<subset>#" |
|
818 "op #\<union>" "{#}" |
|
819 by standard auto |
|
820 |
817 lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close> |
821 lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close> |
818 "count (A #\<union> B) x = max (count A x) (count B x)" |
822 "count (A #\<union> B) x = max (count A x) (count B x)" |
819 by (simp add: sup_subset_mset_def) |
823 by (simp add: sup_subset_mset_def) |
820 |
824 |
821 lemma set_mset_sup [simp]: |
825 lemma set_mset_sup [simp]: |
822 "set_mset (A #\<union> B) = set_mset A \<union> set_mset B" |
826 "set_mset (A #\<union> B) = set_mset A \<union> set_mset B" |
823 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count) |
827 by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count) |
824 (auto simp add: not_in_iff elim: mset_add) |
828 (auto simp add: not_in_iff elim: mset_add) |
825 |
829 |
826 lemma empty_sup [simp]: "{#} #\<union> M = M" |
830 lemma empty_sup: "{#} #\<union> M = M" |
827 by (simp add: multiset_eq_iff) |
831 by (fact subset_mset.sup_bot.left_neutral) |
828 |
832 |
829 lemma sup_empty [simp]: "M #\<union> {#} = M" |
833 lemma sup_empty: "M #\<union> {#} = M" |
830 by (simp add: multiset_eq_iff) |
834 by (fact subset_mset.sup_bot.right_neutral) |
831 |
835 |
832 lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> N)" |
836 lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> N)" |
833 by (simp add: multiset_eq_iff not_in_iff) |
837 by (simp add: multiset_eq_iff not_in_iff) |
834 |
838 |
835 lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> (N - {#x#}))" |
839 lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> (N - {#x#}))" |
2527 |
2540 |
2528 subsubsection \<open>Closure-free presentation\<close> |
2541 subsubsection \<open>Closure-free presentation\<close> |
2529 |
2542 |
2530 text \<open>One direction.\<close> |
2543 text \<open>One direction.\<close> |
2531 lemma mult_implies_one_step: |
2544 lemma mult_implies_one_step: |
2532 "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow> |
2545 assumes |
2533 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> |
2546 trans: "trans r" and |
2534 (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)" |
2547 MN: "(M, N) \<in> mult r" |
2535 apply (unfold mult_def mult1_def) |
2548 shows "\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)" |
2536 apply (erule converse_trancl_induct, clarify) |
2549 using MN unfolding mult_def mult1_def |
2537 apply (rule_tac x = M0 in exI, simp) |
2550 proof (induction rule: converse_trancl_induct) |
2538 apply clarify |
2551 case (base y) |
2539 apply (case_tac "a \<in># K") |
2552 then show ?case by force |
2540 apply (rule_tac x = I in exI) |
2553 next |
2541 apply (simp (no_asm)) |
2554 case (step y z) note yz = this(1) and zN = this(2) and N_decomp = this(3) |
2542 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
2555 obtain I J K where |
2543 apply (simp (no_asm_simp) add: add.assoc [symmetric]) |
2556 N: "N = I + J" "z = I + K" "J \<noteq> {#}" "\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> r" |
2544 apply (drule union_single_eq_diff) |
2557 using N_decomp by blast |
2545 apply (auto simp: subset_mset.add_diff_assoc dest: in_diffD)[] |
2558 obtain a M0 K' where |
2546 apply (meson transD) |
2559 z: "z = add_mset a M0" and y: "y = M0 + K'" and K: "\<forall>b. b \<in># K' \<longrightarrow> (b, a) \<in> r" |
2547 apply (subgoal_tac "a \<in># I") |
2560 using yz by blast |
2548 apply (rule_tac x = "I - {#a#}" in exI) |
2561 show ?case |
2549 apply (rule_tac x = "add_mset a J" in exI) |
2562 proof (cases "a \<in># K") |
2550 apply (rule_tac x = "K + Ka" in exI) |
2563 case True |
2551 apply (rule conjI) |
2564 moreover have "\<exists>j\<in>#J. (k, j) \<in> r" if "k \<in># K'" for k |
2552 apply (simp add: multiset_eq_iff union_single_eq_diff split: nat_diff_split) |
2565 using K N trans True by (meson that transE) |
2553 apply (rule conjI) |
2566 ultimately show ?thesis |
2554 apply (drule union_single_eq_diff) |
2567 by (rule_tac x = I in exI, rule_tac x = J in exI, rule_tac x = "(K - {#a#}) + K'" in exI) |
2555 apply (simp add: add.assoc subset_mset.add_diff_assoc2) |
2568 (use z y N in \<open>auto simp: subset_mset.add_diff_assoc dest: in_diffD\<close>) |
2556 apply (simp) |
2569 next |
2557 apply (simp add: multiset_eq_iff split: nat_diff_split) |
2570 case False |
2558 apply (simp (no_asm_use) add: trans_def) |
2571 then have "a \<in># I" by (metis N(2) union_iff union_single_eq_member z) |
2559 apply (subgoal_tac "a \<in># add_mset a M0") |
2572 moreover have "M0 = I + K - {#a#}" |
2560 apply (simp_all add: not_in_iff) |
2573 using N(2) z by force |
2561 apply blast |
2574 ultimately show ?thesis |
2562 by (metis (no_types, lifting) not_in_iff union_iff union_single_eq_member) |
2575 by (rule_tac x = "I - {#a#}" in exI, rule_tac x = "add_mset a J" in exI, |
2563 |
2576 rule_tac x = "K + K'" in exI) |
2564 lemma one_step_implies_mult_aux: |
2577 (use z y N False K in \<open>auto simp: subset_mset.diff_add_assoc2\<close>) |
2565 "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r) |
2578 qed |
2566 \<longrightarrow> (I + K, I + J) \<in> mult r" |
2579 qed |
2567 apply (induct n) |
|
2568 apply auto |
|
2569 apply (frule size_eq_Suc_imp_eq_union, clarify) |
|
2570 apply (rename_tac "J'", simp) |
|
2571 apply (case_tac "J' = {#}") |
|
2572 apply (simp add: mult_def) |
|
2573 apply (rule r_into_trancl) |
|
2574 apply (simp add: mult1_def, blast) |
|
2575 txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close> |
|
2576 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) |
|
2577 apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp) |
|
2578 apply (simp add: Ball_def, auto) |
|
2579 apply (subgoal_tac |
|
2580 "((I + {# x \<in># K. (x, a) \<in> r #}) + {# x \<in># K. (x, a) \<notin> r #}, |
|
2581 (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r") |
|
2582 prefer 2 |
|
2583 apply (drule_tac x = "I + {# x \<in># K. (x, a) \<in> r#}" in spec) |
|
2584 apply (drule_tac x = "J'" in spec) |
|
2585 apply (drule_tac x = "{# x \<in># K. (x, a) \<notin> r#}" in spec) |
|
2586 apply auto[] |
|
2587 apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def) |
|
2588 apply (subst (asm)(1) add.assoc) |
|
2589 apply (subst (asm)(2) multiset_partition[symmetric]) |
|
2590 apply (erule trancl_trans) |
|
2591 apply (rule r_into_trancl) |
|
2592 apply (simp add: mult1_def) |
|
2593 apply (rule_tac x = a in exI) |
|
2594 apply (rule_tac x = "I + J'" in exI) |
|
2595 apply simp |
|
2596 done |
|
2597 |
2580 |
2598 lemma one_step_implies_mult: |
2581 lemma one_step_implies_mult: |
2599 "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r |
2582 assumes |
2600 \<Longrightarrow> (I + K, I + J) \<in> mult r" |
2583 "J \<noteq> {#}" and |
2601 using one_step_implies_mult_aux by blast |
2584 "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r" |
|
2585 shows "(I + K, I + J) \<in> mult r" |
|
2586 using assms |
|
2587 proof (induction "size J" arbitrary: I J K) |
|
2588 case 0 |
|
2589 then show ?case by auto |
|
2590 next |
|
2591 case (Suc n) note IH = this(1) and size_J = this(2)[THEN sym] |
|
2592 obtain J' a where J: "J = add_mset a J'" |
|
2593 using size_J by (blast dest: size_eq_Suc_imp_eq_union) |
|
2594 show ?case |
|
2595 proof (cases "J' = {#}") |
|
2596 case True |
|
2597 then show ?thesis |
|
2598 using J Suc by (fastforce simp add: mult_def mult1_def) |
|
2599 next |
|
2600 case [simp]: False |
|
2601 have K: "K = {#x \<in># K. (x, a) \<in> r#} + {#x \<in># K. (x, a) \<notin> r#}" |
|
2602 by (rule multiset_partition) |
|
2603 have "(I + K, (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r" |
|
2604 using IH[of J' "{# x \<in># K. (x, a) \<notin> r#}" "I + {# x \<in># K. (x, a) \<in> r#}"] |
|
2605 J Suc.prems K size_J by (auto simp: ac_simps) |
|
2606 moreover have "(I + {#x \<in># K. (x, a) \<in> r#} + J', I + J) \<in> mult r" |
|
2607 by (fastforce simp: J mult1_def mult_def) |
|
2608 ultimately show ?thesis |
|
2609 unfolding mult_def by simp |
|
2610 qed |
|
2611 qed |
2602 |
2612 |
2603 |
2613 |
2604 subsection \<open>The multiset extension is cancellative for multiset union\<close> |
2614 subsection \<open>The multiset extension is cancellative for multiset union\<close> |
2605 |
2615 |
2606 lemma mult_cancel: |
2616 lemma mult_cancel: |