equal
deleted
inserted
replaced
246 lemma upper_plus_absorb: "xs +\<sharp> xs = xs" |
246 lemma upper_plus_absorb: "xs +\<sharp> xs = xs" |
247 apply (induct xs rule: upper_pd.principal_induct, simp) |
247 apply (induct xs rule: upper_pd.principal_induct, simp) |
248 apply (simp add: PDPlus_absorb) |
248 apply (simp add: PDPlus_absorb) |
249 done |
249 done |
250 |
250 |
251 interpretation aci_upper_plus!: ab_semigroup_idem_mult "op +\<sharp>" |
251 class_interpretation aci_upper_plus: ab_semigroup_idem_mult ["op +\<sharp>"] |
252 by unfold_locales |
252 by unfold_locales |
253 (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ |
253 (rule upper_plus_assoc upper_plus_commute upper_plus_absorb)+ |
254 |
254 |
255 lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)" |
255 lemma upper_plus_left_commute: "xs +\<sharp> (ys +\<sharp> zs) = ys +\<sharp> (xs +\<sharp> zs)" |
256 by (rule aci_upper_plus.mult_left_commute) |
256 by (rule aci_upper_plus.mult_left_commute) |