equal
deleted
inserted
replaced
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) plus_ac0 |
112 apply intro_classes |
112 proof |
113 apply (rule union_commute) |
113 fix a b c :: "'a multiset" |
114 apply (rule union_assoc) |
114 show "(a + b) + c = a + (b + c)" by (rule union_assoc) |
115 apply simp |
115 show "a + b = b + a" by (rule union_commute) |
116 done |
116 show "0 + a = a" by simp |
|
117 qed |
117 |
118 |
118 |
119 |
119 subsubsection {* Difference *} |
120 subsubsection {* Difference *} |
120 |
121 |
121 theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |
122 theorem diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}" |