2803 assume ?L thus ?R |
2803 assume ?L thus ?R |
2804 proof (induct Z) |
2804 proof (induct Z) |
2805 case (add z Z) |
2805 case (add z Z) |
2806 obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}" |
2806 obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}" |
2807 "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s" |
2807 "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s" |
2808 using mult_implies_one_step[OF `trans s` add(2)] by auto |
2808 using mult_implies_one_step[OF \<open>trans s\<close> add(2)] by auto |
2809 consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2" |
2809 consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2" |
2810 using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff) |
2810 using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff) |
2811 thus ?case |
2811 thus ?case |
2812 proof (cases) |
2812 proof (cases) |
2813 case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2] |
2813 case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2] |
2814 by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1)) |
2814 by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1)) |
2815 next |
2815 next |
2816 case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) `irrefl s` |
2816 case 2 then obtain y where "y \<in> set_mset Y2" "(z, y) \<in> s" using *(4) \<open>irrefl s\<close> |
2817 by (auto simp: irrefl_def) |
2817 by (auto simp: irrefl_def) |
2818 moreover from this transD[OF `trans s` _ this(2)] |
2818 moreover from this transD[OF \<open>trans s\<close> _ this(2)] |
2819 have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x' |
2819 have "x' \<in> set_mset X2 \<Longrightarrow> \<exists>y \<in> set_mset Y2. (x', y) \<in> s" for x' |
2820 using 2 *(4)[rule_format, of x'] by auto |
2820 using 2 *(4)[rule_format, of x'] by auto |
2821 ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2 |
2821 ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2 |
2822 by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1)) |
2822 by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1)) |
2823 qed |
2823 qed |
2824 qed auto |
2824 qed auto |
2825 next |
2825 next |
2826 assume ?R then obtain I J K |
2826 assume ?R then obtain I J K |
2827 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" |
2827 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" |
2828 using mult_implies_one_step[OF `trans s`] by blast |
2828 using mult_implies_one_step[OF \<open>trans s\<close>] by blast |
2829 thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps) |
2829 thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps) |
2830 qed |
2830 qed |
2831 |
2831 |
2832 lemmas mult_cancel_add_mset = |
2832 lemmas mult_cancel_add_mset = |
2833 mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral] |
2833 mult_cancel[of _ _ "{#_#}", unfolded union_mset_add_mset_right add.comm_neutral] |
2885 assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R" |
2885 assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R" |
2886 shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>=" |
2886 shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>=" |
2887 proof - |
2887 proof - |
2888 { assume "N \<noteq> M" "M - M \<inter># N = {#}" |
2888 { assume "N \<noteq> M" "M - M \<inter># N = {#}" |
2889 then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric]) |
2889 then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric]) |
2890 then have "\<exists>y. count M y < count N y" using `M - M \<inter># N = {#}` |
2890 then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close> |
2891 by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y]) |
2891 by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y]) |
2892 } |
2892 } |
2893 then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M" |
2893 then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M" |
2894 by (auto simp: multeqp_def multp_def Let_def in_diff_count) |
2894 by (auto simp: multeqp_def multp_def Let_def in_diff_count) |
2895 thus ?thesis using multp_iff[OF assms] by simp |
2895 thus ?thesis using multp_iff[OF assms] by simp |