277 |
277 |
278 lemma approx_convex_plus [simp]: |
278 lemma approx_convex_plus [simp]: |
279 "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys" |
279 "approx n\<cdot>(xs +\<natural> ys) = approx n\<cdot>xs +\<natural> approx n\<cdot>ys" |
280 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) |
280 by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp) |
281 |
281 |
282 lemma convex_plus_assoc: |
282 interpretation convex_add!: semilattice convex_add proof |
283 "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)" |
283 fix xs ys zs :: "'a convex_pd" |
284 apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp) |
284 show "(xs +\<natural> ys) +\<natural> zs = xs +\<natural> (ys +\<natural> zs)" |
285 apply (rule_tac x=zs in convex_pd.principal_induct, simp) |
285 apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp) |
286 apply (simp add: PDPlus_assoc) |
286 apply (rule_tac x=zs in convex_pd.principal_induct, simp) |
287 done |
287 apply (simp add: PDPlus_assoc) |
288 |
288 done |
289 lemma convex_plus_commute: "xs +\<natural> ys = ys +\<natural> xs" |
289 show "xs +\<natural> ys = ys +\<natural> xs" |
290 apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp) |
290 apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp) |
291 apply (simp add: PDPlus_commute) |
291 apply (simp add: PDPlus_commute) |
292 done |
292 done |
293 |
293 show "xs +\<natural> xs = xs" |
294 lemma convex_plus_absorb [simp]: "xs +\<natural> xs = xs" |
294 apply (induct xs rule: convex_pd.principal_induct, simp) |
295 apply (induct xs rule: convex_pd.principal_induct, simp) |
295 apply (simp add: PDPlus_absorb) |
296 apply (simp add: PDPlus_absorb) |
296 done |
297 done |
297 qed |
298 |
298 |
299 lemma convex_plus_left_commute: "xs +\<natural> (ys +\<natural> zs) = ys +\<natural> (xs +\<natural> zs)" |
299 lemmas convex_plus_assoc = convex_add.assoc |
300 by (rule mk_left_commute |
300 lemmas convex_plus_commute = convex_add.commute |
301 [of "op +\<natural>", OF convex_plus_assoc convex_plus_commute]) |
301 lemmas convex_plus_absorb = convex_add.idem |
302 |
302 lemmas convex_plus_left_commute = convex_add.left_commute |
303 lemma convex_plus_left_absorb [simp]: "xs +\<natural> (xs +\<natural> ys) = xs +\<natural> ys" |
303 lemmas convex_plus_left_absorb = convex_add.left_idem |
304 by (simp only: convex_plus_assoc [symmetric] convex_plus_absorb) |
|
305 |
304 |
306 text {* Useful for @{text "simp add: convex_plus_ac"} *} |
305 text {* Useful for @{text "simp add: convex_plus_ac"} *} |
307 lemmas convex_plus_ac = |
306 lemmas convex_plus_ac = |
308 convex_plus_assoc convex_plus_commute convex_plus_left_commute |
307 convex_plus_assoc convex_plus_commute convex_plus_left_commute |
309 |
308 |