src/HOL/Library/Multiset_Order.thy
changeset 60495 d7ff0a1df90a
parent 60397 f8a513fedb31
child 60502 aa58872267ee
     1.1 --- a/src/HOL/Library/Multiset_Order.thy	Tue Jun 16 20:50:00 2015 +0100
     1.2 +++ b/src/HOL/Library/Multiset_Order.thy	Wed Jun 17 17:21:11 2015 +0200
     1.3 @@ -47,14 +47,14 @@
     1.4      moreover
     1.5      assume "(M, M) \<in> mult {(x, y). x < y}"
     1.6      ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
     1.7 -      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})"
     1.8 +      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
     1.9        by (rule mult_implies_one_step)
    1.10      then obtain I J K where "M = I + J" and "M = I + K"
    1.11 -      and "J \<noteq> {#}" and "(\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> {(x, y). x < y})" by blast
    1.12 -    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_of K. \<exists>j\<in>set_of K. k < j" by auto
    1.13 -    have "finite (set_of K)" by simp
    1.14 +      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
    1.15 +    then have aux1: "K \<noteq> {#}" and aux2: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
    1.16 +    have "finite (set_mset K)" by simp
    1.17      moreover note aux2
    1.18 -    ultimately have "set_of K = {}"
    1.19 +    ultimately have "set_mset K = {}"
    1.20        by (induct rule: finite_induct)
    1.21         (simp, metis (mono_tags) insert_absorb insert_iff insert_not_empty less_irrefl less_trans)
    1.22      with aux1 show False by simp