src/HOL/Library/Set_Algebras.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (7 months ago)
changeset 69313 b021008c5397
parent 64267 b9a1486e79be
permissions -rw-r--r--
removed legacy input syntax
haftmann@38622
     1
(*  Title:      HOL/Library/Set_Algebras.thy
wenzelm@63473
     2
    Author:     Jeremy Avigad
wenzelm@63473
     3
    Author:     Kevin Donnelly
wenzelm@63473
     4
    Author:     Florian Haftmann, TUM
avigad@16908
     5
*)
avigad@16908
     6
wenzelm@60500
     7
section \<open>Algebraic operations on sets\<close>
avigad@16908
     8
haftmann@38622
     9
theory Set_Algebras
wenzelm@63485
    10
  imports Main
avigad@16908
    11
begin
avigad@16908
    12
wenzelm@60500
    13
text \<open>
wenzelm@63485
    14
  This library lifts operations like addition and multiplication to sets. It
wenzelm@63485
    15
  was designed to support asymptotic calculations. See the comments at the top
wenzelm@63680
    16
  of \<^file>\<open>BigO.thy\<close>.
wenzelm@60500
    17
\<close>
avigad@16908
    18
krauss@47443
    19
instantiation set :: (plus) plus
krauss@47443
    20
begin
krauss@47443
    21
wenzelm@63473
    22
definition plus_set :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"
wenzelm@63473
    23
  where set_plus_def: "A + B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
krauss@47443
    24
krauss@47443
    25
instance ..
krauss@47443
    26
krauss@47443
    27
end
krauss@47443
    28
krauss@47443
    29
instantiation set :: (times) times
krauss@47443
    30
begin
krauss@47443
    31
wenzelm@63473
    32
definition times_set :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"
wenzelm@63473
    33
  where set_times_def: "A * B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
krauss@47443
    34
krauss@47443
    35
instance ..
krauss@47443
    36
krauss@47443
    37
end
krauss@47443
    38
krauss@47443
    39
instantiation set :: (zero) zero
krauss@47443
    40
begin
krauss@47443
    41
wenzelm@63473
    42
definition set_zero[simp]: "(0::'a::zero set) = {0}"
krauss@47443
    43
krauss@47443
    44
instance ..
krauss@47443
    45
krauss@47443
    46
end
wenzelm@56899
    47
krauss@47443
    48
instantiation set :: (one) one
krauss@47443
    49
begin
krauss@47443
    50
wenzelm@63473
    51
definition set_one[simp]: "(1::'a::one set) = {1}"
krauss@47443
    52
krauss@47443
    53
instance ..
krauss@47443
    54
krauss@47443
    55
end
haftmann@25594
    56
wenzelm@63473
    57
definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70)
wenzelm@63473
    58
  where "a +o B = {c. \<exists>b\<in>B. c = a + b}"
avigad@16908
    59
wenzelm@63473
    60
definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "*o" 80)
wenzelm@63473
    61
  where "a *o B = {c. \<exists>b\<in>B. c = a * b}"
haftmann@25594
    62
wenzelm@63473
    63
abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50)
wenzelm@63473
    64
  where "x =o A \<equiv> x \<in> A"
haftmann@25594
    65
krauss@47443
    66
instance set :: (semigroup_add) semigroup_add
wenzelm@60679
    67
  by standard (force simp add: set_plus_def add.assoc)
haftmann@25594
    68
krauss@47443
    69
instance set :: (ab_semigroup_add) ab_semigroup_add
wenzelm@60679
    70
  by standard (force simp add: set_plus_def add.commute)
haftmann@25594
    71
krauss@47443
    72
instance set :: (monoid_add) monoid_add
wenzelm@60679
    73
  by standard (simp_all add: set_plus_def)
haftmann@25594
    74
krauss@47443
    75
instance set :: (comm_monoid_add) comm_monoid_add
wenzelm@60679
    76
  by standard (simp_all add: set_plus_def)
avigad@16908
    77
krauss@47443
    78
instance set :: (semigroup_mult) semigroup_mult
wenzelm@60679
    79
  by standard (force simp add: set_times_def mult.assoc)
avigad@16908
    80
krauss@47443
    81
instance set :: (ab_semigroup_mult) ab_semigroup_mult
wenzelm@60679
    82
  by standard (force simp add: set_times_def mult.commute)
avigad@16908
    83
krauss@47443
    84
instance set :: (monoid_mult) monoid_mult
wenzelm@60679
    85
  by standard (simp_all add: set_times_def)
avigad@16908
    86
krauss@47443
    87
instance set :: (comm_monoid_mult) comm_monoid_mult
wenzelm@60679
    88
  by standard (simp_all add: set_times_def)
avigad@16908
    89
wenzelm@56899
    90
lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
berghofe@26814
    91
  by (auto simp add: set_plus_def)
avigad@16908
    92
huffman@53596
    93
lemma set_plus_elim:
huffman@53596
    94
  assumes "x \<in> A + B"
huffman@53596
    95
  obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
huffman@53596
    96
  using assms unfolding set_plus_def by fast
huffman@53596
    97
wenzelm@56899
    98
lemma set_plus_intro2 [intro]: "b \<in> C \<Longrightarrow> a + b \<in> a +o C"
wenzelm@19736
    99
  by (auto simp add: elt_set_plus_def)
avigad@16908
   100
wenzelm@63473
   101
lemma set_plus_rearrange: "(a +o C) + (b +o D) = (a + b) +o (C + D)"
wenzelm@63473
   102
  for a b :: "'a::comm_monoid_add"
haftmann@57514
   103
  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
wenzelm@19736
   104
   apply (rule_tac x = "ba + bb" in exI)
wenzelm@63473
   105
   apply (auto simp add: ac_simps)
avigad@16908
   106
  apply (rule_tac x = "aa + a" in exI)
haftmann@57514
   107
  apply (auto simp add: ac_simps)
wenzelm@19736
   108
  done
avigad@16908
   109
wenzelm@63473
   110
lemma set_plus_rearrange2: "a +o (b +o C) = (a + b) +o C"
wenzelm@63473
   111
  for a b :: "'a::semigroup_add"
haftmann@57512
   112
  by (auto simp add: elt_set_plus_def add.assoc)
avigad@16908
   113
wenzelm@63473
   114
lemma set_plus_rearrange3: "(a +o B) + C = a +o (B + C)"
wenzelm@63473
   115
  for a :: "'a::semigroup_add"
berghofe@26814
   116
  apply (auto simp add: elt_set_plus_def set_plus_def)
haftmann@57514
   117
   apply (blast intro: ac_simps)
avigad@16908
   118
  apply (rule_tac x = "a + aa" in exI)
avigad@16908
   119
  apply (rule conjI)
wenzelm@19736
   120
   apply (rule_tac x = "aa" in bexI)
wenzelm@19736
   121
    apply auto
avigad@16908
   122
  apply (rule_tac x = "ba" in bexI)
haftmann@57514
   123
   apply (auto simp add: ac_simps)
wenzelm@19736
   124
  done
avigad@16908
   125
wenzelm@63473
   126
theorem set_plus_rearrange4: "C + (a +o D) = a +o (C + D)"
wenzelm@63473
   127
  for a :: "'a::comm_monoid_add"
haftmann@57514
   128
  apply (auto simp add: elt_set_plus_def set_plus_def ac_simps)
wenzelm@19736
   129
   apply (rule_tac x = "aa + ba" in exI)
haftmann@57514
   130
   apply (auto simp add: ac_simps)
wenzelm@19736
   131
  done
avigad@16908
   132
wenzelm@61337
   133
lemmas set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
avigad@16908
   134
  set_plus_rearrange3 set_plus_rearrange4
avigad@16908
   135
wenzelm@56899
   136
lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
wenzelm@19736
   137
  by (auto simp add: elt_set_plus_def)
avigad@16908
   138
wenzelm@63473
   139
lemma set_plus_mono2 [intro]: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C + E \<subseteq> D + F"
wenzelm@63473
   140
  for C D E F :: "'a::plus set"
berghofe@26814
   141
  by (auto simp add: set_plus_def)
avigad@16908
   142
wenzelm@56899
   143
lemma set_plus_mono3 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> C + D"
berghofe@26814
   144
  by (auto simp add: elt_set_plus_def set_plus_def)
avigad@16908
   145
wenzelm@63473
   146
lemma set_plus_mono4 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
wenzelm@63473
   147
  for a :: "'a::comm_monoid_add"
haftmann@57514
   148
  by (auto simp add: elt_set_plus_def set_plus_def ac_simps)
avigad@16908
   149
wenzelm@56899
   150
lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
wenzelm@56899
   151
  apply (subgoal_tac "a +o B \<subseteq> a +o D")
wenzelm@19736
   152
   apply (erule order_trans)
wenzelm@19736
   153
   apply (erule set_plus_mono3)
avigad@16908
   154
  apply (erule set_plus_mono)
wenzelm@19736
   155
  done
avigad@16908
   156
wenzelm@56899
   157
lemma set_plus_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a +o C \<Longrightarrow> x \<in> a +o D"
avigad@16908
   158
  apply (frule set_plus_mono)
avigad@16908
   159
  apply auto
wenzelm@19736
   160
  done
avigad@16908
   161
wenzelm@56899
   162
lemma set_plus_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C + E \<Longrightarrow> x \<in> D + F"
avigad@16908
   163
  apply (frule set_plus_mono2)
wenzelm@19736
   164
   prefer 2
wenzelm@19736
   165
   apply force
avigad@16908
   166
  apply assumption
wenzelm@19736
   167
  done
avigad@16908
   168
wenzelm@56899
   169
lemma set_plus_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> C + D"
avigad@16908
   170
  apply (frule set_plus_mono3)
avigad@16908
   171
  apply auto
wenzelm@19736
   172
  done
avigad@16908
   173
wenzelm@63473
   174
lemma set_plus_mono4_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> D + C"
wenzelm@63473
   175
  for a x :: "'a::comm_monoid_add"
avigad@16908
   176
  apply (frule set_plus_mono4)
avigad@16908
   177
  apply auto
wenzelm@19736
   178
  done
avigad@16908
   179
wenzelm@63473
   180
lemma set_zero_plus [simp]: "0 +o C = C"
wenzelm@63473
   181
  for C :: "'a::comm_monoid_add set"
wenzelm@19736
   182
  by (auto simp add: elt_set_plus_def)
avigad@16908
   183
wenzelm@63473
   184
lemma set_zero_plus2: "0 \<in> A \<Longrightarrow> B \<subseteq> A + B"
wenzelm@63473
   185
  for A B :: "'a::comm_monoid_add set"
huffman@44142
   186
  apply (auto simp add: set_plus_def)
avigad@16908
   187
  apply (rule_tac x = 0 in bexI)
wenzelm@19736
   188
   apply (rule_tac x = x in bexI)
haftmann@57514
   189
    apply (auto simp add: ac_simps)
wenzelm@19736
   190
  done
avigad@16908
   191
wenzelm@63473
   192
lemma set_plus_imp_minus: "a \<in> b +o C \<Longrightarrow> a - b \<in> C"
wenzelm@63473
   193
  for a b :: "'a::ab_group_add"
haftmann@57514
   194
  by (auto simp add: elt_set_plus_def ac_simps)
avigad@16908
   195
wenzelm@63473
   196
lemma set_minus_imp_plus: "a - b \<in> C \<Longrightarrow> a \<in> b +o C"
wenzelm@63473
   197
  for a b :: "'a::ab_group_add"
haftmann@57514
   198
  apply (auto simp add: elt_set_plus_def ac_simps)
avigad@16908
   199
  apply (subgoal_tac "a = (a + - b) + b")
wenzelm@63473
   200
   apply (rule bexI)
wenzelm@63473
   201
    apply assumption
wenzelm@63473
   202
   apply (auto simp add: ac_simps)
wenzelm@19736
   203
  done
avigad@16908
   204
wenzelm@63473
   205
lemma set_minus_plus: "a - b \<in> C \<longleftrightarrow> a \<in> b +o C"
wenzelm@63473
   206
  for a b :: "'a::ab_group_add"
wenzelm@63473
   207
  apply (rule iffI)
wenzelm@63473
   208
   apply (rule set_minus_imp_plus)
wenzelm@63473
   209
   apply assumption
wenzelm@63473
   210
  apply (rule set_plus_imp_minus)
wenzelm@63473
   211
  apply assumption
wenzelm@63473
   212
  done
avigad@16908
   213
wenzelm@56899
   214
lemma set_times_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a * b \<in> C * D"
berghofe@26814
   215
  by (auto simp add: set_times_def)
avigad@16908
   216
huffman@53596
   217
lemma set_times_elim:
huffman@53596
   218
  assumes "x \<in> A * B"
huffman@53596
   219
  obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
huffman@53596
   220
  using assms unfolding set_times_def by fast
huffman@53596
   221
wenzelm@56899
   222
lemma set_times_intro2 [intro!]: "b \<in> C \<Longrightarrow> a * b \<in> a *o C"
wenzelm@19736
   223
  by (auto simp add: elt_set_times_def)
avigad@16908
   224
wenzelm@63473
   225
lemma set_times_rearrange: "(a *o C) * (b *o D) = (a * b) *o (C * D)"
wenzelm@63473
   226
  for a b :: "'a::comm_monoid_mult"
berghofe@26814
   227
  apply (auto simp add: elt_set_times_def set_times_def)
wenzelm@19736
   228
   apply (rule_tac x = "ba * bb" in exI)
haftmann@57514
   229
   apply (auto simp add: ac_simps)
avigad@16908
   230
  apply (rule_tac x = "aa * a" in exI)
haftmann@57514
   231
  apply (auto simp add: ac_simps)
wenzelm@19736
   232
  done
avigad@16908
   233
wenzelm@63473
   234
lemma set_times_rearrange2: "a *o (b *o C) = (a * b) *o C"
wenzelm@63473
   235
  for a b :: "'a::semigroup_mult"
haftmann@57512
   236
  by (auto simp add: elt_set_times_def mult.assoc)
avigad@16908
   237
wenzelm@63473
   238
lemma set_times_rearrange3: "(a *o B) * C = a *o (B * C)"
wenzelm@63473
   239
  for a :: "'a::semigroup_mult"
berghofe@26814
   240
  apply (auto simp add: elt_set_times_def set_times_def)
haftmann@57514
   241
   apply (blast intro: ac_simps)
avigad@16908
   242
  apply (rule_tac x = "a * aa" in exI)
avigad@16908
   243
  apply (rule conjI)
wenzelm@19736
   244
   apply (rule_tac x = "aa" in bexI)
wenzelm@19736
   245
    apply auto
avigad@16908
   246
  apply (rule_tac x = "ba" in bexI)
haftmann@57514
   247
   apply (auto simp add: ac_simps)
wenzelm@19736
   248
  done
avigad@16908
   249
wenzelm@63473
   250
theorem set_times_rearrange4: "C * (a *o D) = a *o (C * D)"
wenzelm@63473
   251
  for a :: "'a::comm_monoid_mult"
haftmann@57514
   252
  apply (auto simp add: elt_set_times_def set_times_def ac_simps)
wenzelm@19736
   253
   apply (rule_tac x = "aa * ba" in exI)
haftmann@57514
   254
   apply (auto simp add: ac_simps)
wenzelm@19736
   255
  done
avigad@16908
   256
wenzelm@61337
   257
lemmas set_times_rearranges = set_times_rearrange set_times_rearrange2
avigad@16908
   258
  set_times_rearrange3 set_times_rearrange4
avigad@16908
   259
wenzelm@56899
   260
lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
wenzelm@19736
   261
  by (auto simp add: elt_set_times_def)
avigad@16908
   262
wenzelm@63473
   263
lemma set_times_mono2 [intro]: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C * E \<subseteq> D * F"
wenzelm@63473
   264
  for C D E F :: "'a::times set"
berghofe@26814
   265
  by (auto simp add: set_times_def)
avigad@16908
   266
wenzelm@56899
   267
lemma set_times_mono3 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> C * D"
berghofe@26814
   268
  by (auto simp add: elt_set_times_def set_times_def)
avigad@16908
   269
wenzelm@63473
   270
lemma set_times_mono4 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> D * C"
wenzelm@63473
   271
  for a :: "'a::comm_monoid_mult"
haftmann@57514
   272
  by (auto simp add: elt_set_times_def set_times_def ac_simps)
avigad@16908
   273
wenzelm@56899
   274
lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
wenzelm@56899
   275
  apply (subgoal_tac "a *o B \<subseteq> a *o D")
wenzelm@19736
   276
   apply (erule order_trans)
wenzelm@19736
   277
   apply (erule set_times_mono3)
avigad@16908
   278
  apply (erule set_times_mono)
wenzelm@19736
   279
  done
avigad@16908
   280
wenzelm@56899
   281
lemma set_times_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a *o C \<Longrightarrow> x \<in> a *o D"
avigad@16908
   282
  apply (frule set_times_mono)
avigad@16908
   283
  apply auto
wenzelm@19736
   284
  done
avigad@16908
   285
wenzelm@56899
   286
lemma set_times_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C * E \<Longrightarrow> x \<in> D * F"
avigad@16908
   287
  apply (frule set_times_mono2)
wenzelm@19736
   288
   prefer 2
wenzelm@19736
   289
   apply force
avigad@16908
   290
  apply assumption
wenzelm@19736
   291
  done
avigad@16908
   292
wenzelm@56899
   293
lemma set_times_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> C * D"
avigad@16908
   294
  apply (frule set_times_mono3)
avigad@16908
   295
  apply auto
wenzelm@19736
   296
  done
avigad@16908
   297
wenzelm@63473
   298
lemma set_times_mono4_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> D * C"
wenzelm@63473
   299
  for a x :: "'a::comm_monoid_mult"
avigad@16908
   300
  apply (frule set_times_mono4)
avigad@16908
   301
  apply auto
wenzelm@19736
   302
  done
avigad@16908
   303
wenzelm@63473
   304
lemma set_one_times [simp]: "1 *o C = C"
wenzelm@63473
   305
  for C :: "'a::comm_monoid_mult set"
wenzelm@19736
   306
  by (auto simp add: elt_set_times_def)
avigad@16908
   307
wenzelm@63473
   308
lemma set_times_plus_distrib: "a *o (b +o C) = (a * b) +o (a *o C)"
wenzelm@63473
   309
  for a b :: "'a::semiring"
nipkow@23477
   310
  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
avigad@16908
   311
wenzelm@63473
   312
lemma set_times_plus_distrib2: "a *o (B + C) = (a *o B) + (a *o C)"
wenzelm@63473
   313
  for a :: "'a::semiring"
berghofe@26814
   314
  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
wenzelm@19736
   315
   apply blast
avigad@16908
   316
  apply (rule_tac x = "b + bb" in exI)
nipkow@23477
   317
  apply (auto simp add: ring_distribs)
wenzelm@19736
   318
  done
avigad@16908
   319
wenzelm@63473
   320
lemma set_times_plus_distrib3: "(a +o C) * D \<subseteq> a *o D + C * D"
wenzelm@63473
   321
  for a :: "'a::semiring"
wenzelm@63473
   322
  apply (auto simp: elt_set_plus_def elt_set_times_def set_times_def set_plus_def ring_distribs)
avigad@16908
   323
  apply auto
wenzelm@19736
   324
  done
avigad@16908
   325
wenzelm@61337
   326
lemmas set_times_plus_distribs =
wenzelm@19380
   327
  set_times_plus_distrib
avigad@16908
   328
  set_times_plus_distrib2
avigad@16908
   329
wenzelm@63473
   330
lemma set_neg_intro: "a \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
wenzelm@63473
   331
  for a :: "'a::ring_1"
wenzelm@19736
   332
  by (auto simp add: elt_set_times_def)
avigad@16908
   333
wenzelm@63473
   334
lemma set_neg_intro2: "a \<in> C \<Longrightarrow> - a \<in> (- 1) *o C"
wenzelm@63473
   335
  for a :: "'a::ring_1"
wenzelm@19736
   336
  by (auto simp add: elt_set_times_def)
wenzelm@19736
   337
huffman@53596
   338
lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
wenzelm@63473
   339
  by (fastforce simp: set_plus_def image_iff)
hoelzl@40887
   340
huffman@53596
   341
lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
wenzelm@63473
   342
  by (fastforce simp: set_times_def image_iff)
huffman@53596
   343
wenzelm@56899
   344
lemma finite_set_plus: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s + t)"
wenzelm@63473
   345
  by (simp add: set_plus_image)
huffman@53596
   346
wenzelm@56899
   347
lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
wenzelm@63473
   348
  by (simp add: set_times_image)
huffman@53596
   349
nipkow@64267
   350
lemma set_sum_alt:
hoelzl@40887
   351
  assumes fin: "finite I"
nipkow@64267
   352
  shows "sum S I = {sum s I |s. \<forall>i\<in>I. s i \<in> S i}"
nipkow@64267
   353
    (is "_ = ?sum I")
wenzelm@56899
   354
  using fin
wenzelm@56899
   355
proof induct
wenzelm@56899
   356
  case empty
wenzelm@56899
   357
  then show ?case by simp
wenzelm@56899
   358
next
hoelzl@40887
   359
  case (insert x F)
nipkow@64267
   360
  have "sum S (insert x F) = S x + ?sum F"
hoelzl@40887
   361
    using insert.hyps by auto
nipkow@64267
   362
  also have "\<dots> = {s x + sum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
hoelzl@40887
   363
    unfolding set_plus_def
hoelzl@40887
   364
  proof safe
wenzelm@56899
   365
    fix y s
wenzelm@56899
   366
    assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
nipkow@64267
   367
    then show "\<exists>s'. y + sum s F = s' x + sum s' F \<and> (\<forall>i\<in>insert x F. s' i \<in> S i)"
hoelzl@40887
   368
      using insert.hyps
hoelzl@40887
   369
      by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
hoelzl@40887
   370
  qed auto
hoelzl@40887
   371
  finally show ?case
hoelzl@40887
   372
    using insert.hyps by auto
wenzelm@56899
   373
qed
hoelzl@40887
   374
nipkow@64267
   375
lemma sum_set_cond_linear:
wenzelm@56899
   376
  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
krauss@47445
   377
  assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A + B)" "P {0}"
krauss@47445
   378
    and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
hoelzl@40887
   379
  assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
nipkow@64267
   380
  shows "f (sum S I) = sum (f \<circ> S) I"
wenzelm@56899
   381
proof (cases "finite I")
wenzelm@56899
   382
  case True
wenzelm@56899
   383
  from this all show ?thesis
hoelzl@40887
   384
  proof induct
wenzelm@56899
   385
    case empty
wenzelm@56899
   386
    then show ?case by (auto intro!: f)
wenzelm@56899
   387
  next
hoelzl@40887
   388
    case (insert x F)
nipkow@64267
   389
    from \<open>finite F\<close> \<open>\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)\<close> have "P (sum S F)"
hoelzl@40887
   390
      by induct auto
hoelzl@40887
   391
    with insert show ?case
hoelzl@40887
   392
      by (simp, subst f) auto
wenzelm@56899
   393
  qed
wenzelm@56899
   394
next
wenzelm@56899
   395
  case False
wenzelm@56899
   396
  then show ?thesis by (auto intro!: f)
wenzelm@56899
   397
qed
hoelzl@40887
   398
nipkow@64267
   399
lemma sum_set_linear:
wenzelm@56899
   400
  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
krauss@47445
   401
  assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
nipkow@64267
   402
  shows "f (sum S I) = sum (f \<circ> S) I"
nipkow@64267
   403
  using sum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
hoelzl@40887
   404
krauss@47446
   405
lemma set_times_Un_distrib:
krauss@47446
   406
  "A * (B \<union> C) = A * B \<union> A * C"
krauss@47446
   407
  "(A \<union> B) * C = A * C \<union> B * C"
wenzelm@56899
   408
  by (auto simp: set_times_def)
krauss@47446
   409
krauss@47446
   410
lemma set_times_UNION_distrib:
haftmann@69313
   411
  "A * \<Union>(M ` I) = (\<Union>i\<in>I. A * M i)"
haftmann@69313
   412
  "\<Union>(M ` I) * A = (\<Union>i\<in>I. M i * A)"
wenzelm@56899
   413
  by (auto simp: set_times_def)
krauss@47446
   414
avigad@16908
   415
end