src/HOL/Library/Set_Algebras.thy
changeset 38622 86fc906dcd86
parent 35267 8dfd816713c6
child 39198 f967a16dfcdd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Set_Algebras.thy	Fri Aug 20 17:48:30 2010 +0200
     1.3 @@ -0,0 +1,357 @@
     1.4 +(*  Title:      HOL/Library/Set_Algebras.thy
     1.5 +    Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
     1.6 +*)
     1.7 +
     1.8 +header {* Algebraic operations on sets *}
     1.9 +
    1.10 +theory Set_Algebras
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +  This library lifts operations like addition and muliplication to
    1.16 +  sets.  It was designed to support asymptotic calculations. See the
    1.17 +  comments at the top of theory @{text BigO}.
    1.18 +*}
    1.19 +
    1.20 +definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<oplus>" 65) where
    1.21 +  "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
    1.22 +
    1.23 +definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<otimes>" 70) where
    1.24 +  "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
    1.25 +
    1.26 +definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70) where
    1.27 +  "a +o B = {c. \<exists>b\<in>B. c = a + b}"
    1.28 +
    1.29 +definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "*o" 80) where
    1.30 +  "a *o B = {c. \<exists>b\<in>B. c = a * b}"
    1.31 +
    1.32 +abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50) where
    1.33 +  "x =o A \<equiv> x \<in> A"
    1.34 +
    1.35 +interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.36 +qed (force simp add: set_plus_def add.assoc)
    1.37 +
    1.38 +interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.39 +qed (force simp add: set_plus_def add.commute)
    1.40 +
    1.41 +interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
    1.42 +qed (simp_all add: set_plus_def)
    1.43 +
    1.44 +interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
    1.45 +qed (simp add: set_plus_def)
    1.46 +
    1.47 +definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
    1.48 +  "listsum_set = monoid_add.listsum set_plus {0}"
    1.49 +
    1.50 +interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
    1.51 +  "monoid_add.listsum set_plus {0::'a} = listsum_set"
    1.52 +proof -
    1.53 +  show "class.monoid_add set_plus {0::'a}" proof
    1.54 +  qed (simp_all add: set_add.assoc)
    1.55 +  then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
    1.56 +  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
    1.57 +    by (simp only: listsum_set_def)
    1.58 +qed
    1.59 +
    1.60 +definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
    1.61 +  "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
    1.62 +
    1.63 +interpretation set_add!:
    1.64 +  comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set 
    1.65 +proof
    1.66 +qed (fact setsum_set_def)
    1.67 +
    1.68 +interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
    1.69 +  "monoid_add.listsum set_plus {0::'a} = listsum_set"
    1.70 +  and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
    1.71 +proof -
    1.72 +  show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
    1.73 +  qed (simp_all add: set_add.commute)
    1.74 +  then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
    1.75 +  show "monoid_add.listsum set_plus {0::'a} = listsum_set"
    1.76 +    by (simp only: listsum_set_def)
    1.77 +  show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
    1.78 +    by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
    1.79 +qed
    1.80 +
    1.81 +interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.82 +qed (force simp add: set_times_def mult.assoc)
    1.83 +
    1.84 +interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
    1.85 +qed (force simp add: set_times_def mult.commute)
    1.86 +
    1.87 +interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
    1.88 +qed (simp_all add: set_times_def)
    1.89 +
    1.90 +interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
    1.91 +qed (simp add: set_times_def)
    1.92 +
    1.93 +definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
    1.94 +  "power_set n A = power.power {1} set_times A n"
    1.95 +
    1.96 +interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.97 +  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
    1.98 +proof -
    1.99 +  show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
   1.100 +  qed (simp_all add: set_mult.assoc)
   1.101 +  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   1.102 +    by (simp add: power_set_def)
   1.103 +qed
   1.104 +
   1.105 +definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
   1.106 +  "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
   1.107 +
   1.108 +interpretation set_mult!:
   1.109 +  comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set 
   1.110 +proof
   1.111 +qed (fact setprod_set_def)
   1.112 +
   1.113 +interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
   1.114 +  "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   1.115 +  and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
   1.116 +proof -
   1.117 +  show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
   1.118 +  qed (simp_all add: set_mult.commute)
   1.119 +  then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
   1.120 +  show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   1.121 +    by (simp add: power_set_def)
   1.122 +  show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
   1.123 +    by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
   1.124 +qed
   1.125 +
   1.126 +lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   1.127 +  by (auto simp add: set_plus_def)
   1.128 +
   1.129 +lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   1.130 +  by (auto simp add: elt_set_plus_def)
   1.131 +
   1.132 +lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
   1.133 +    (b +o D) = (a + b) +o (C \<oplus> D)"
   1.134 +  apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   1.135 +   apply (rule_tac x = "ba + bb" in exI)
   1.136 +  apply (auto simp add: add_ac)
   1.137 +  apply (rule_tac x = "aa + a" in exI)
   1.138 +  apply (auto simp add: add_ac)
   1.139 +  done
   1.140 +
   1.141 +lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
   1.142 +    (a + b) +o C"
   1.143 +  by (auto simp add: elt_set_plus_def add_assoc)
   1.144 +
   1.145 +lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
   1.146 +    a +o (B \<oplus> C)"
   1.147 +  apply (auto simp add: elt_set_plus_def set_plus_def)
   1.148 +   apply (blast intro: add_ac)
   1.149 +  apply (rule_tac x = "a + aa" in exI)
   1.150 +  apply (rule conjI)
   1.151 +   apply (rule_tac x = "aa" in bexI)
   1.152 +    apply auto
   1.153 +  apply (rule_tac x = "ba" in bexI)
   1.154 +   apply (auto simp add: add_ac)
   1.155 +  done
   1.156 +
   1.157 +theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
   1.158 +    a +o (C \<oplus> D)"
   1.159 +  apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
   1.160 +   apply (rule_tac x = "aa + ba" in exI)
   1.161 +   apply (auto simp add: add_ac)
   1.162 +  done
   1.163 +
   1.164 +theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   1.165 +  set_plus_rearrange3 set_plus_rearrange4
   1.166 +
   1.167 +lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   1.168 +  by (auto simp add: elt_set_plus_def)
   1.169 +
   1.170 +lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   1.171 +    C \<oplus> E <= D \<oplus> F"
   1.172 +  by (auto simp add: set_plus_def)
   1.173 +
   1.174 +lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
   1.175 +  by (auto simp add: elt_set_plus_def set_plus_def)
   1.176 +
   1.177 +lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   1.178 +    a +o D <= D \<oplus> C"
   1.179 +  by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   1.180 +
   1.181 +lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   1.182 +  apply (subgoal_tac "a +o B <= a +o D")
   1.183 +   apply (erule order_trans)
   1.184 +   apply (erule set_plus_mono3)
   1.185 +  apply (erule set_plus_mono)
   1.186 +  done
   1.187 +
   1.188 +lemma set_plus_mono_b: "C <= D ==> x : a +o C
   1.189 +    ==> x : a +o D"
   1.190 +  apply (frule set_plus_mono)
   1.191 +  apply auto
   1.192 +  done
   1.193 +
   1.194 +lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
   1.195 +    x : D \<oplus> F"
   1.196 +  apply (frule set_plus_mono2)
   1.197 +   prefer 2
   1.198 +   apply force
   1.199 +  apply assumption
   1.200 +  done
   1.201 +
   1.202 +lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   1.203 +  apply (frule set_plus_mono3)
   1.204 +  apply auto
   1.205 +  done
   1.206 +
   1.207 +lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   1.208 +    x : a +o D ==> x : D \<oplus> C"
   1.209 +  apply (frule set_plus_mono4)
   1.210 +  apply auto
   1.211 +  done
   1.212 +
   1.213 +lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   1.214 +  by (auto simp add: elt_set_plus_def)
   1.215 +
   1.216 +lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
   1.217 +  apply (auto intro!: subsetI simp add: set_plus_def)
   1.218 +  apply (rule_tac x = 0 in bexI)
   1.219 +   apply (rule_tac x = x in bexI)
   1.220 +    apply (auto simp add: add_ac)
   1.221 +  done
   1.222 +
   1.223 +lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   1.224 +  by (auto simp add: elt_set_plus_def add_ac diff_minus)
   1.225 +
   1.226 +lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   1.227 +  apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   1.228 +  apply (subgoal_tac "a = (a + - b) + b")
   1.229 +   apply (rule bexI, assumption, assumption)
   1.230 +  apply (auto simp add: add_ac)
   1.231 +  done
   1.232 +
   1.233 +lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   1.234 +  by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   1.235 +    assumption)
   1.236 +
   1.237 +lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
   1.238 +  by (auto simp add: set_times_def)
   1.239 +
   1.240 +lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   1.241 +  by (auto simp add: elt_set_times_def)
   1.242 +
   1.243 +lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
   1.244 +    (b *o D) = (a * b) *o (C \<otimes> D)"
   1.245 +  apply (auto simp add: elt_set_times_def set_times_def)
   1.246 +   apply (rule_tac x = "ba * bb" in exI)
   1.247 +   apply (auto simp add: mult_ac)
   1.248 +  apply (rule_tac x = "aa * a" in exI)
   1.249 +  apply (auto simp add: mult_ac)
   1.250 +  done
   1.251 +
   1.252 +lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
   1.253 +    (a * b) *o C"
   1.254 +  by (auto simp add: elt_set_times_def mult_assoc)
   1.255 +
   1.256 +lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
   1.257 +    a *o (B \<otimes> C)"
   1.258 +  apply (auto simp add: elt_set_times_def set_times_def)
   1.259 +   apply (blast intro: mult_ac)
   1.260 +  apply (rule_tac x = "a * aa" in exI)
   1.261 +  apply (rule conjI)
   1.262 +   apply (rule_tac x = "aa" in bexI)
   1.263 +    apply auto
   1.264 +  apply (rule_tac x = "ba" in bexI)
   1.265 +   apply (auto simp add: mult_ac)
   1.266 +  done
   1.267 +
   1.268 +theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
   1.269 +    a *o (C \<otimes> D)"
   1.270 +  apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
   1.271 +    mult_ac)
   1.272 +   apply (rule_tac x = "aa * ba" in exI)
   1.273 +   apply (auto simp add: mult_ac)
   1.274 +  done
   1.275 +
   1.276 +theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   1.277 +  set_times_rearrange3 set_times_rearrange4
   1.278 +
   1.279 +lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   1.280 +  by (auto simp add: elt_set_times_def)
   1.281 +
   1.282 +lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   1.283 +    C \<otimes> E <= D \<otimes> F"
   1.284 +  by (auto simp add: set_times_def)
   1.285 +
   1.286 +lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
   1.287 +  by (auto simp add: elt_set_times_def set_times_def)
   1.288 +
   1.289 +lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   1.290 +    a *o D <= D \<otimes> C"
   1.291 +  by (auto simp add: elt_set_times_def set_times_def mult_ac)
   1.292 +
   1.293 +lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   1.294 +  apply (subgoal_tac "a *o B <= a *o D")
   1.295 +   apply (erule order_trans)
   1.296 +   apply (erule set_times_mono3)
   1.297 +  apply (erule set_times_mono)
   1.298 +  done
   1.299 +
   1.300 +lemma set_times_mono_b: "C <= D ==> x : a *o C
   1.301 +    ==> x : a *o D"
   1.302 +  apply (frule set_times_mono)
   1.303 +  apply auto
   1.304 +  done
   1.305 +
   1.306 +lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
   1.307 +    x : D \<otimes> F"
   1.308 +  apply (frule set_times_mono2)
   1.309 +   prefer 2
   1.310 +   apply force
   1.311 +  apply assumption
   1.312 +  done
   1.313 +
   1.314 +lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   1.315 +  apply (frule set_times_mono3)
   1.316 +  apply auto
   1.317 +  done
   1.318 +
   1.319 +lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   1.320 +    x : a *o D ==> x : D \<otimes> C"
   1.321 +  apply (frule set_times_mono4)
   1.322 +  apply auto
   1.323 +  done
   1.324 +
   1.325 +lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   1.326 +  by (auto simp add: elt_set_times_def)
   1.327 +
   1.328 +lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   1.329 +    (a * b) +o (a *o C)"
   1.330 +  by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   1.331 +
   1.332 +lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
   1.333 +    (a *o B) \<oplus> (a *o C)"
   1.334 +  apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   1.335 +   apply blast
   1.336 +  apply (rule_tac x = "b + bb" in exI)
   1.337 +  apply (auto simp add: ring_distribs)
   1.338 +  done
   1.339 +
   1.340 +lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
   1.341 +    a *o D \<oplus> C \<otimes> D"
   1.342 +  apply (auto intro!: subsetI simp add:
   1.343 +    elt_set_plus_def elt_set_times_def set_times_def
   1.344 +    set_plus_def ring_distribs)
   1.345 +  apply auto
   1.346 +  done
   1.347 +
   1.348 +theorems set_times_plus_distribs =
   1.349 +  set_times_plus_distrib
   1.350 +  set_times_plus_distrib2
   1.351 +
   1.352 +lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
   1.353 +    - a : C"
   1.354 +  by (auto simp add: elt_set_times_def)
   1.355 +
   1.356 +lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   1.357 +    - a : (- 1) *o C"
   1.358 +  by (auto simp add: elt_set_times_def)
   1.359 +
   1.360 +end