summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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