equal
deleted
inserted
replaced
106 apply (rule union_commute [THEN arg_cong]) |
106 apply (rule union_commute [THEN arg_cong]) |
107 done |
107 done |
108 |
108 |
109 theorems union_ac = union_assoc union_commute union_lcomm |
109 theorems union_ac = union_assoc union_commute union_lcomm |
110 |
110 |
111 instance multiset :: (type) plus_ac0 |
111 instance multiset :: (type) comm_monoid_add |
112 proof |
112 proof |
113 fix a b c :: "'a multiset" |
113 fix a b c :: "'a multiset" |
114 show "(a + b) + c = a + (b + c)" by (rule union_assoc) |
114 show "(a + b) + c = a + (b + c)" by (rule union_assoc) |
115 show "a + b = b + a" by (rule union_commute) |
115 show "a + b = b + a" by (rule union_commute) |
116 show "0 + a = a" by simp |
116 show "0 + a = a" by simp |