more symbols;
authorwenzelm
Wed May 07 14:44:07 2014 +0200 (2014-05-07)
changeset 568999b9f4abaaa7e
parent 56898 ba507cc96473
child 56900 beea3ee118af
more symbols;
tuned proofs;
src/HOL/Library/Set_Algebras.thy
     1.1 --- a/src/HOL/Library/Set_Algebras.thy	Wed May 07 14:05:17 2014 +0200
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Wed May 07 14:44:07 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  This library lifts operations like addition and muliplication to
     1.8 +  This library lifts operations like addition and multiplication to
     1.9    sets.  It was designed to support asymptotic calculations. See the
    1.10    comments at the top of theory @{text BigO}.
    1.11  *}
    1.12 @@ -38,17 +38,17 @@
    1.13  begin
    1.14  
    1.15  definition
    1.16 -  set_zero[simp]: "0::('a::zero)set == {0}"
    1.17 +  set_zero[simp]: "(0::'a::zero set) = {0}"
    1.18  
    1.19  instance ..
    1.20  
    1.21  end
    1.22 - 
    1.23 +
    1.24  instantiation set :: (one) one
    1.25  begin
    1.26  
    1.27  definition
    1.28 -  set_one[simp]: "1::('a::one)set == {1}"
    1.29 +  set_one[simp]: "(1::'a::one set) = {1}"
    1.30  
    1.31  instance ..
    1.32  
    1.33 @@ -64,30 +64,30 @@
    1.34    "x =o A \<equiv> x \<in> A"
    1.35  
    1.36  instance set :: (semigroup_add) semigroup_add
    1.37 -by default (force simp add: set_plus_def add.assoc)
    1.38 +  by default (force simp add: set_plus_def add.assoc)
    1.39  
    1.40  instance set :: (ab_semigroup_add) ab_semigroup_add
    1.41 -by default (force simp add: set_plus_def add.commute)
    1.42 +  by default (force simp add: set_plus_def add.commute)
    1.43  
    1.44  instance set :: (monoid_add) monoid_add
    1.45 -by default (simp_all add: set_plus_def)
    1.46 +  by default (simp_all add: set_plus_def)
    1.47  
    1.48  instance set :: (comm_monoid_add) comm_monoid_add
    1.49 -by default (simp_all add: set_plus_def)
    1.50 +  by default (simp_all add: set_plus_def)
    1.51  
    1.52  instance set :: (semigroup_mult) semigroup_mult
    1.53 -by default (force simp add: set_times_def mult.assoc)
    1.54 +  by default (force simp add: set_times_def mult.assoc)
    1.55  
    1.56  instance set :: (ab_semigroup_mult) ab_semigroup_mult
    1.57 -by default (force simp add: set_times_def mult.commute)
    1.58 +  by default (force simp add: set_times_def mult.commute)
    1.59  
    1.60  instance set :: (monoid_mult) monoid_mult
    1.61 -by default (simp_all add: set_times_def)
    1.62 +  by default (simp_all add: set_times_def)
    1.63  
    1.64  instance set :: (comm_monoid_mult) comm_monoid_mult
    1.65 -by default (simp_all add: set_times_def)
    1.66 +  by default (simp_all add: set_times_def)
    1.67  
    1.68 -lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C + D"
    1.69 +lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
    1.70    by (auto simp add: set_plus_def)
    1.71  
    1.72  lemma set_plus_elim:
    1.73 @@ -95,11 +95,11 @@
    1.74    obtains a b where "x = a + b" and "a \<in> A" and "b \<in> B"
    1.75    using assms unfolding set_plus_def by fast
    1.76  
    1.77 -lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
    1.78 +lemma set_plus_intro2 [intro]: "b \<in> C \<Longrightarrow> a + b \<in> a +o C"
    1.79    by (auto simp add: elt_set_plus_def)
    1.80  
    1.81 -lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) +
    1.82 -    (b +o D) = (a + b) +o (C + D)"
    1.83 +lemma set_plus_rearrange:
    1.84 +  "((a::'a::comm_monoid_add) +o C) + (b +o D) = (a + b) +o (C + D)"
    1.85    apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
    1.86     apply (rule_tac x = "ba + bb" in exI)
    1.87    apply (auto simp add: add_ac)
    1.88 @@ -107,12 +107,10 @@
    1.89    apply (auto simp add: add_ac)
    1.90    done
    1.91  
    1.92 -lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
    1.93 -    (a + b) +o C"
    1.94 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) = (a + b) +o C"
    1.95    by (auto simp add: elt_set_plus_def add_assoc)
    1.96  
    1.97 -lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C =
    1.98 -    a +o (B + C)"
    1.99 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) + C = a +o (B + C)"
   1.100    apply (auto simp add: elt_set_plus_def set_plus_def)
   1.101     apply (blast intro: add_ac)
   1.102    apply (rule_tac x = "a + aa" in exI)
   1.103 @@ -123,8 +121,7 @@
   1.104     apply (auto simp add: add_ac)
   1.105    done
   1.106  
   1.107 -theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) =
   1.108 -    a +o (C + D)"
   1.109 +theorem set_plus_rearrange4: "C + ((a::'a::comm_monoid_add) +o D) = a +o (C + D)"
   1.110    apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   1.111     apply (rule_tac x = "aa + ba" in exI)
   1.112     apply (auto simp add: add_ac)
   1.113 @@ -133,48 +130,43 @@
   1.114  theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   1.115    set_plus_rearrange3 set_plus_rearrange4
   1.116  
   1.117 -lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   1.118 +lemma set_plus_mono [intro!]: "C \<subseteq> D \<Longrightarrow> a +o C \<subseteq> a +o D"
   1.119    by (auto simp add: elt_set_plus_def)
   1.120  
   1.121 -lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   1.122 -    C + E <= D + F"
   1.123 +lemma set_plus_mono2 [intro]: "(C::'a::plus set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C + E \<subseteq> D + F"
   1.124    by (auto simp add: set_plus_def)
   1.125  
   1.126 -lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C + D"
   1.127 +lemma set_plus_mono3 [intro]: "a \<in> C \<Longrightarrow> a +o D \<subseteq> C + D"
   1.128    by (auto simp add: elt_set_plus_def set_plus_def)
   1.129  
   1.130 -lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   1.131 -    a +o D <= D + C"
   1.132 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) \<in> C \<Longrightarrow> a +o D \<subseteq> D + C"
   1.133    by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   1.134  
   1.135 -lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C + D"
   1.136 -  apply (subgoal_tac "a +o B <= a +o D")
   1.137 +lemma set_plus_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a +o B \<subseteq> C + D"
   1.138 +  apply (subgoal_tac "a +o B \<subseteq> a +o D")
   1.139     apply (erule order_trans)
   1.140     apply (erule set_plus_mono3)
   1.141    apply (erule set_plus_mono)
   1.142    done
   1.143  
   1.144 -lemma set_plus_mono_b: "C <= D ==> x : a +o C
   1.145 -    ==> x : a +o D"
   1.146 +lemma set_plus_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a +o C \<Longrightarrow> x \<in> a +o D"
   1.147    apply (frule set_plus_mono)
   1.148    apply auto
   1.149    done
   1.150  
   1.151 -lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C + E ==>
   1.152 -    x : D + F"
   1.153 +lemma set_plus_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C + E \<Longrightarrow> x \<in> D + F"
   1.154    apply (frule set_plus_mono2)
   1.155     prefer 2
   1.156     apply force
   1.157    apply assumption
   1.158    done
   1.159  
   1.160 -lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C + D"
   1.161 +lemma set_plus_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> C + D"
   1.162    apply (frule set_plus_mono3)
   1.163    apply auto
   1.164    done
   1.165  
   1.166 -lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   1.167 -    x : a +o D ==> x : D + C"
   1.168 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C \<Longrightarrow> x \<in> a +o D \<Longrightarrow> x \<in> D + C"
   1.169    apply (frule set_plus_mono4)
   1.170    apply auto
   1.171    done
   1.172 @@ -182,28 +174,27 @@
   1.173  lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   1.174    by (auto simp add: elt_set_plus_def)
   1.175  
   1.176 -lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A + B"
   1.177 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) \<in> A \<Longrightarrow> B \<subseteq> A + B"
   1.178    apply (auto simp add: set_plus_def)
   1.179    apply (rule_tac x = 0 in bexI)
   1.180     apply (rule_tac x = x in bexI)
   1.181      apply (auto simp add: add_ac)
   1.182    done
   1.183  
   1.184 -lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   1.185 +lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C \<Longrightarrow> (a - b) \<in> C"
   1.186    by (auto simp add: elt_set_plus_def add_ac)
   1.187  
   1.188 -lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   1.189 +lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C \<Longrightarrow> a \<in> b +o C"
   1.190    apply (auto simp add: elt_set_plus_def add_ac)
   1.191    apply (subgoal_tac "a = (a + - b) + b")
   1.192     apply (rule bexI, assumption)
   1.193    apply (auto simp add: add_ac)
   1.194    done
   1.195  
   1.196 -lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   1.197 -  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   1.198 -    assumption)
   1.199 +lemma set_minus_plus: "(a::'a::ab_group_add) - b \<in> C \<longleftrightarrow> a \<in> b +o C"
   1.200 +  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus)
   1.201  
   1.202 -lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C * D"
   1.203 +lemma set_times_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a * b \<in> C * D"
   1.204    by (auto simp add: set_times_def)
   1.205  
   1.206  lemma set_times_elim:
   1.207 @@ -211,11 +202,11 @@
   1.208    obtains a b where "x = a * b" and "a \<in> A" and "b \<in> B"
   1.209    using assms unfolding set_times_def by fast
   1.210  
   1.211 -lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   1.212 +lemma set_times_intro2 [intro!]: "b \<in> C \<Longrightarrow> a * b \<in> a *o C"
   1.213    by (auto simp add: elt_set_times_def)
   1.214  
   1.215 -lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) *
   1.216 -    (b *o D) = (a * b) *o (C * D)"
   1.217 +lemma set_times_rearrange:
   1.218 +  "((a::'a::comm_monoid_mult) *o C) * (b *o D) = (a * b) *o (C * D)"
   1.219    apply (auto simp add: elt_set_times_def set_times_def)
   1.220     apply (rule_tac x = "ba * bb" in exI)
   1.221     apply (auto simp add: mult_ac)
   1.222 @@ -223,12 +214,12 @@
   1.223    apply (auto simp add: mult_ac)
   1.224    done
   1.225  
   1.226 -lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
   1.227 -    (a * b) *o C"
   1.228 +lemma set_times_rearrange2:
   1.229 +  "(a::'a::semigroup_mult) *o (b *o C) = (a * b) *o C"
   1.230    by (auto simp add: elt_set_times_def mult_assoc)
   1.231  
   1.232 -lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) * C =
   1.233 -    a *o (B * C)"
   1.234 +lemma set_times_rearrange3:
   1.235 +  "((a::'a::semigroup_mult) *o B) * C = a *o (B * C)"
   1.236    apply (auto simp add: elt_set_times_def set_times_def)
   1.237     apply (blast intro: mult_ac)
   1.238    apply (rule_tac x = "a * aa" in exI)
   1.239 @@ -239,10 +230,9 @@
   1.240     apply (auto simp add: mult_ac)
   1.241    done
   1.242  
   1.243 -theorem set_times_rearrange4: "C * ((a::'a::comm_monoid_mult) *o D) =
   1.244 -    a *o (C * D)"
   1.245 -  apply (auto simp add: elt_set_times_def set_times_def
   1.246 -    mult_ac)
   1.247 +theorem set_times_rearrange4:
   1.248 +  "C * ((a::'a::comm_monoid_mult) *o D) = a *o (C * D)"
   1.249 +  apply (auto simp add: elt_set_times_def set_times_def mult_ac)
   1.250     apply (rule_tac x = "aa * ba" in exI)
   1.251     apply (auto simp add: mult_ac)
   1.252    done
   1.253 @@ -250,48 +240,43 @@
   1.254  theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   1.255    set_times_rearrange3 set_times_rearrange4
   1.256  
   1.257 -lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   1.258 +lemma set_times_mono [intro]: "C \<subseteq> D \<Longrightarrow> a *o C \<subseteq> a *o D"
   1.259    by (auto simp add: elt_set_times_def)
   1.260  
   1.261 -lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   1.262 -    C * E <= D * F"
   1.263 +lemma set_times_mono2 [intro]: "(C::'a::times set) \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> C * E \<subseteq> D * F"
   1.264    by (auto simp add: set_times_def)
   1.265  
   1.266 -lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C * D"
   1.267 +lemma set_times_mono3 [intro]: "a \<in> C \<Longrightarrow> a *o D \<subseteq> C * D"
   1.268    by (auto simp add: elt_set_times_def set_times_def)
   1.269  
   1.270 -lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   1.271 -    a *o D <= D * C"
   1.272 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C \<Longrightarrow> a *o D \<subseteq> D * C"
   1.273    by (auto simp add: elt_set_times_def set_times_def mult_ac)
   1.274  
   1.275 -lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C * D"
   1.276 -  apply (subgoal_tac "a *o B <= a *o D")
   1.277 +lemma set_times_mono5: "a \<in> C \<Longrightarrow> B \<subseteq> D \<Longrightarrow> a *o B \<subseteq> C * D"
   1.278 +  apply (subgoal_tac "a *o B \<subseteq> a *o D")
   1.279     apply (erule order_trans)
   1.280     apply (erule set_times_mono3)
   1.281    apply (erule set_times_mono)
   1.282    done
   1.283  
   1.284 -lemma set_times_mono_b: "C <= D ==> x : a *o C
   1.285 -    ==> x : a *o D"
   1.286 +lemma set_times_mono_b: "C \<subseteq> D \<Longrightarrow> x \<in> a *o C \<Longrightarrow> x \<in> a *o D"
   1.287    apply (frule set_times_mono)
   1.288    apply auto
   1.289    done
   1.290  
   1.291 -lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C * E ==>
   1.292 -    x : D * F"
   1.293 +lemma set_times_mono2_b: "C \<subseteq> D \<Longrightarrow> E \<subseteq> F \<Longrightarrow> x \<in> C * E \<Longrightarrow> x \<in> D * F"
   1.294    apply (frule set_times_mono2)
   1.295     prefer 2
   1.296     apply force
   1.297    apply assumption
   1.298    done
   1.299  
   1.300 -lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C * D"
   1.301 +lemma set_times_mono3_b: "a \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> C * D"
   1.302    apply (frule set_times_mono3)
   1.303    apply auto
   1.304    done
   1.305  
   1.306 -lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   1.307 -    x : a *o D ==> x : D * C"
   1.308 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) \<in> C \<Longrightarrow> x \<in> a *o D \<Longrightarrow> x \<in> D * C"
   1.309    apply (frule set_times_mono4)
   1.310    apply auto
   1.311    done
   1.312 @@ -299,20 +284,19 @@
   1.313  lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   1.314    by (auto simp add: elt_set_times_def)
   1.315  
   1.316 -lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   1.317 -    (a * b) +o (a *o C)"
   1.318 +lemma set_times_plus_distrib:
   1.319 +  "(a::'a::semiring) *o (b +o C) = (a * b) +o (a *o C)"
   1.320    by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   1.321  
   1.322 -lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B + C) =
   1.323 -    (a *o B) + (a *o C)"
   1.324 +lemma set_times_plus_distrib2:
   1.325 +  "(a::'a::semiring) *o (B + C) = (a *o B) + (a *o C)"
   1.326    apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   1.327     apply blast
   1.328    apply (rule_tac x = "b + bb" in exI)
   1.329    apply (auto simp add: ring_distribs)
   1.330    done
   1.331  
   1.332 -lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D <=
   1.333 -    a *o D + C * D"
   1.334 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) * D \<subseteq> a *o D + C * D"
   1.335    apply (auto simp add:
   1.336      elt_set_plus_def elt_set_times_def set_times_def
   1.337      set_plus_def ring_distribs)
   1.338 @@ -323,12 +307,10 @@
   1.339    set_times_plus_distrib
   1.340    set_times_plus_distrib2
   1.341  
   1.342 -lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
   1.343 -    - a : C"
   1.344 +lemma set_neg_intro: "(a::'a::ring_1) \<in> (- 1) *o C \<Longrightarrow> - a \<in> C"
   1.345    by (auto simp add: elt_set_times_def)
   1.346  
   1.347 -lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   1.348 -    - a : (- 1) *o C"
   1.349 +lemma set_neg_intro2: "(a::'a::ring_1) \<in> C \<Longrightarrow> - a \<in> (- 1) *o C"
   1.350    by (auto simp add: elt_set_times_def)
   1.351  
   1.352  lemma set_plus_image: "S + T = (\<lambda>(x, y). x + y) ` (S \<times> T)"
   1.353 @@ -337,53 +319,63 @@
   1.354  lemma set_times_image: "S * T = (\<lambda>(x, y). x * y) ` (S \<times> T)"
   1.355    unfolding set_times_def by (fastforce simp: image_iff)
   1.356  
   1.357 -lemma finite_set_plus:
   1.358 -  assumes "finite s" and "finite t" shows "finite (s + t)"
   1.359 -  using assms unfolding set_plus_image by simp
   1.360 +lemma finite_set_plus: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s + t)"
   1.361 +  unfolding set_plus_image by simp
   1.362  
   1.363 -lemma finite_set_times:
   1.364 -  assumes "finite s" and "finite t" shows "finite (s * t)"
   1.365 -  using assms unfolding set_times_image by simp
   1.366 +lemma finite_set_times: "finite s \<Longrightarrow> finite t \<Longrightarrow> finite (s * t)"
   1.367 +  unfolding set_times_image by simp
   1.368  
   1.369  lemma set_setsum_alt:
   1.370    assumes fin: "finite I"
   1.371    shows "setsum S I = {setsum s I |s. \<forall>i\<in>I. s i \<in> S i}"
   1.372      (is "_ = ?setsum I")
   1.373 -using fin proof induct
   1.374 +  using fin
   1.375 +proof induct
   1.376 +  case empty
   1.377 +  then show ?case by simp
   1.378 +next
   1.379    case (insert x F)
   1.380    have "setsum S (insert x F) = S x + ?setsum F"
   1.381      using insert.hyps by auto
   1.382 -  also have "...= {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
   1.383 +  also have "\<dots> = {s x + setsum s F |s. \<forall> i\<in>insert x F. s i \<in> S i}"
   1.384      unfolding set_plus_def
   1.385    proof safe
   1.386 -    fix y s assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
   1.387 +    fix y s
   1.388 +    assume "y \<in> S x" "\<forall>i\<in>F. s i \<in> S i"
   1.389      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)"
   1.390        using insert.hyps
   1.391        by (intro exI[of _ "\<lambda>i. if i \<in> F then s i else y"]) (auto simp add: set_plus_def)
   1.392    qed auto
   1.393    finally show ?case
   1.394      using insert.hyps by auto
   1.395 -qed auto
   1.396 +qed
   1.397  
   1.398  lemma setsum_set_cond_linear:
   1.399 -  fixes f :: "('a::comm_monoid_add) set \<Rightarrow> ('b::comm_monoid_add) set"
   1.400 +  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   1.401    assumes [intro!]: "\<And>A B. P A  \<Longrightarrow> P B  \<Longrightarrow> P (A + B)" "P {0}"
   1.402      and f: "\<And>A B. P A  \<Longrightarrow> P B \<Longrightarrow> f (A + B) = f A + f B" "f {0} = {0}"
   1.403    assumes all: "\<And>i. i \<in> I \<Longrightarrow> P (S i)"
   1.404    shows "f (setsum S I) = setsum (f \<circ> S) I"
   1.405 -proof cases
   1.406 -  assume "finite I" from this all show ?thesis
   1.407 +proof (cases "finite I")
   1.408 +  case True
   1.409 +  from this all show ?thesis
   1.410    proof induct
   1.411 +    case empty
   1.412 +    then show ?case by (auto intro!: f)
   1.413 +  next
   1.414      case (insert x F)
   1.415      from `finite F` `\<And>i. i \<in> insert x F \<Longrightarrow> P (S i)` have "P (setsum S F)"
   1.416        by induct auto
   1.417      with insert show ?case
   1.418        by (simp, subst f) auto
   1.419 -  qed (auto intro!: f)
   1.420 -qed (auto intro!: f)
   1.421 +  qed
   1.422 +next
   1.423 +  case False
   1.424 +  then show ?thesis by (auto intro!: f)
   1.425 +qed
   1.426  
   1.427  lemma setsum_set_linear:
   1.428 -  fixes f :: "('a::comm_monoid_add) set => ('b::comm_monoid_add) set"
   1.429 +  fixes f :: "'a::comm_monoid_add set \<Rightarrow> 'b::comm_monoid_add set"
   1.430    assumes "\<And>A B. f(A) + f(B) = f(A + B)" "f {0} = {0}"
   1.431    shows "f (setsum S I) = setsum (f \<circ> S) I"
   1.432    using setsum_set_cond_linear[of "\<lambda>x. True" f I S] assms by auto
   1.433 @@ -391,11 +383,11 @@
   1.434  lemma set_times_Un_distrib:
   1.435    "A * (B \<union> C) = A * B \<union> A * C"
   1.436    "(A \<union> B) * C = A * C \<union> B * C"
   1.437 -by (auto simp: set_times_def)
   1.438 +  by (auto simp: set_times_def)
   1.439  
   1.440  lemma set_times_UNION_distrib:
   1.441 -  "A * UNION I M = UNION I (%i. A * M i)"
   1.442 -  "UNION I M * A = UNION I (%i. M i * A)"
   1.443 -by (auto simp: set_times_def)
   1.444 +  "A * UNION I M = (\<Union>i\<in>I. A * M i)"
   1.445 +  "UNION I M * A = (\<Union>i\<in>I. M i * A)"
   1.446 +  by (auto simp: set_times_def)
   1.447  
   1.448  end