author wenzelm Wed May 07 14:44:07 2014 +0200 (2014-05-07) changeset 56899 9b9f4abaaa7e parent 56898 ba507cc96473 child 56900 beea3ee118af
more symbols;
tuned proofs;
```     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.39
1.43
1.45 -by default (simp_all add: set_plus_def)
1.46 +  by default (simp_all add: set_plus_def)
1.47
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.86     apply (rule_tac x = "ba + bb" in exI)
1.88 @@ -107,12 +107,10 @@
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.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.102    apply (rule_tac x = "a + aa" in exI)
1.103 @@ -123,8 +121,7 @@
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.111     apply (rule_tac x = "aa + ba" in exI)
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.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.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.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.191    apply (subgoal_tac "a = (a + - b) + b")
1.192     apply (rule bexI, assumption)
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.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.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.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
```