equal
deleted
inserted
replaced
294 lemma convex_plus_absorb: "xs +\<natural> xs = xs" |
294 lemma convex_plus_absorb: "xs +\<natural> xs = xs" |
295 apply (induct xs rule: convex_pd.principal_induct, simp) |
295 apply (induct xs rule: convex_pd.principal_induct, simp) |
296 apply (simp add: PDPlus_absorb) |
296 apply (simp add: PDPlus_absorb) |
297 done |
297 done |
298 |
298 |
299 class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"] |
299 interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>" |
300 by unfold_locales |
300 proof qed (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ |
301 (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+ |
|
302 |
301 |
303 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)" |
302 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)" |
304 by (rule aci_convex_plus.mult_left_commute) |
303 by (rule aci_convex_plus.mult_left_commute) |
305 |
304 |
306 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys" |
305 lemma convex_plus_left_absorb: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys" |