1656 apply (case_tac "a :# K") |
1656 apply (case_tac "a :# K") |
1657 apply (rule_tac x = I in exI) |
1657 apply (rule_tac x = I in exI) |
1658 apply (simp (no_asm)) |
1658 apply (simp (no_asm)) |
1659 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
1659 apply (rule_tac x = "(K - {#a#}) + Ka" in exI) |
1660 apply (simp (no_asm_simp) add: add.assoc [symmetric]) |
1660 apply (simp (no_asm_simp) add: add.assoc [symmetric]) |
1661 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong) |
1661 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong) |
1662 apply (simp add: diff_union_single_conv) |
1662 apply (simp add: diff_union_single_conv) |
1663 apply (simp (no_asm_use) add: trans_def) |
1663 apply (simp (no_asm_use) add: trans_def) |
1664 apply blast |
1664 apply blast |
1665 apply (subgoal_tac "a :# I") |
1665 apply (subgoal_tac "a :# I") |
1666 apply (rule_tac x = "I - {#a#}" in exI) |
1666 apply (rule_tac x = "I - {#a#}" in exI) |
1667 apply (rule_tac x = "J + {#a#}" in exI) |
1667 apply (rule_tac x = "J + {#a#}" in exI) |
1668 apply (rule_tac x = "K + Ka" in exI) |
1668 apply (rule_tac x = "K + Ka" in exI) |
1669 apply (rule conjI) |
1669 apply (rule conjI) |
1670 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1670 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1671 apply (rule conjI) |
1671 apply (rule conjI) |
1672 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp) |
1672 apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp) |
1673 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1673 apply (simp add: multiset_eq_iff split: nat_diff_split) |
1674 apply (simp (no_asm_use) add: trans_def) |
1674 apply (simp (no_asm_use) add: trans_def) |
1675 apply blast |
1675 apply blast |
1676 apply (subgoal_tac "a :# (M0 + {#a#})") |
1676 apply (subgoal_tac "a :# (M0 + {#a#})") |
1677 apply simp |
1677 apply simp |
1690 apply (simp add: mult_def) |
1690 apply (simp add: mult_def) |
1691 apply (rule r_into_trancl) |
1691 apply (rule r_into_trancl) |
1692 apply (simp add: mult1_def set_of_def, blast) |
1692 apply (simp add: mult1_def set_of_def, blast) |
1693 txt {* Now we know @{term "J' \<noteq> {#}"}. *} |
1693 txt {* Now we know @{term "J' \<noteq> {#}"}. *} |
1694 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) |
1694 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) |
1695 apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) |
1695 apply (erule_tac P = "\<forall>k \<in> set_of K. P k" for P in rev_mp) |
1696 apply (erule ssubst) |
1696 apply (erule ssubst) |
1697 apply (simp add: Ball_def, auto) |
1697 apply (simp add: Ball_def, auto) |
1698 apply (subgoal_tac |
1698 apply (subgoal_tac |
1699 "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #}, |
1699 "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #}, |
1700 (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r") |
1700 (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r") |