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