352 |
352 |
353 lemma set_neg_intro2: "(a::'a::ring_1) : C ==> |
353 lemma set_neg_intro2: "(a::'a::ring_1) : C ==> |
354 - a : (- 1) *o C" |
354 - a : (- 1) *o C" |
355 by (auto simp add: elt_set_times_def) |
355 by (auto simp add: elt_set_times_def) |
356 |
356 |
|
357 lemma set_plus_image: |
|
358 fixes S T :: "'n::semigroup_add set" shows "S \<oplus> T = (\<lambda>(x, y). x + y) ` (S \<times> T)" |
|
359 unfolding set_plus_def by (fastsimp simp: image_iff) |
|
360 |
|
361 lemma set_setsum_alt: |
|
362 assumes fin: "finite I" |
|
363 shows "setsum_set S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}" |
|
364 (is "_ = ?setsum I") |
|
365 using fin proof induct |
|
366 case (insert x F) |
|
367 have "setsum_set S (insert x F) = S x \<oplus> ?setsum F" |
|
368 using insert.hyps by auto |
|
369 also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}" |
|
370 unfolding set_plus_def |
|
371 proof safe |
|
372 fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i" |
|
373 then show "\<exists>s'. y + setsum s F = s' x + setsum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)" |
|
374 using insert.hyps |
|
375 by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def) |
|
376 qed auto |
|
377 finally show ?case |
|
378 using insert.hyps by auto |
|
379 qed auto |
|
380 |
|
381 lemma setsum_set_cond_linear: |
|
382 fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set" |
|
383 assumes [intro!]: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> P (A \<oplus> B)" "P {0}" |
|
384 and f: "\<And>A B. P A \<Longrightarrow> P B \<Longrightarrow> f (A \<oplus> B) = f A \<oplus> f B" "f {0} = {0}" |
|
385 assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)" |
|
386 shows "f (setsum_set S I) = setsum_set (f \<circ> S) I" |
|
387 proof cases |
|
388 assume "finite I" from this all show ?thesis |
|
389 proof induct |
|
390 case (insert x F) |
|
391 from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum_set S F)" |
|
392 by induct auto |
|
393 with insert show ?case |
|
394 by (simp, subst f) auto |
|
395 qed (auto intro!: f) |
|
396 qed (auto intro!: f) |
|
397 |
|
398 lemma setsum_set_linear: |
|
399 fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set" |
|
400 assumes "\<And>A B. f(A) \<oplus> f(B) = f(A \<oplus> B)" "f {0} = {0}" |
|
401 shows "f (setsum_set S I) = setsum_set (f \<circ> S) I" |
|
402 using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto |
|
403 |
357 end |
404 end |