src/HOL/Library/Set_Algebras.thy
 author haftmann Fri Aug 27 19:34:23 2010 +0200 (2010-08-27 ago) changeset 38857 97775f3e8722 parent 38622 86fc906dcd86 child 39198 f967a16dfcdd permissions -rw-r--r--
renamed class/constant eq to equal; tuned some instantiations
```     1 (*  Title:      HOL/Library/Set_Algebras.thy
```
```     2     Author:     Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
```
```     3 *)
```
```     4
```
```     5 header {* Algebraic operations on sets *}
```
```     6
```
```     7 theory Set_Algebras
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text {*
```
```    12   This library lifts operations like addition and muliplication to
```
```    13   sets.  It was designed to support asymptotic calculations. See the
```
```    14   comments at the top of theory @{text BigO}.
```
```    15 *}
```
```    16
```
```    17 definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<oplus>" 65) where
```
```    18   "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
```
```    19
```
```    20 definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<otimes>" 70) where
```
```    21   "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
```
```    22
```
```    23 definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "+o" 70) where
```
```    24   "a +o B = {c. \<exists>b\<in>B. c = a + b}"
```
```    25
```
```    26 definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "*o" 80) where
```
```    27   "a *o B = {c. \<exists>b\<in>B. c = a * b}"
```
```    28
```
```    29 abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infix "=o" 50) where
```
```    30   "x =o A \<equiv> x \<in> A"
```
```    31
```
```    32 interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
```
```    33 qed (force simp add: set_plus_def add.assoc)
```
```    34
```
```    35 interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
```
```    36 qed (force simp add: set_plus_def add.commute)
```
```    37
```
```    38 interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
```
```    39 qed (simp_all add: set_plus_def)
```
```    40
```
```    41 interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
```
```    42 qed (simp add: set_plus_def)
```
```    43
```
```    44 definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
```
```    45   "listsum_set = monoid_add.listsum set_plus {0}"
```
```    46
```
```    47 interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
```
```    48   "monoid_add.listsum set_plus {0::'a} = listsum_set"
```
```    49 proof -
```
```    50   show "class.monoid_add set_plus {0::'a}" proof
```
```    51   qed (simp_all add: set_add.assoc)
```
```    52   then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
```
```    53   show "monoid_add.listsum set_plus {0::'a} = listsum_set"
```
```    54     by (simp only: listsum_set_def)
```
```    55 qed
```
```    56
```
```    57 definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
```
```    58   "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
```
```    59
```
```    60 interpretation set_add!:
```
```    61   comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set
```
```    62 proof
```
```    63 qed (fact setsum_set_def)
```
```    64
```
```    65 interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
```
```    66   "monoid_add.listsum set_plus {0::'a} = listsum_set"
```
```    67   and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
```
```    68 proof -
```
```    69   show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
```
```    70   qed (simp_all add: set_add.commute)
```
```    71   then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
```
```    72   show "monoid_add.listsum set_plus {0::'a} = listsum_set"
```
```    73     by (simp only: listsum_set_def)
```
```    74   show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
```
```    75     by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
```
```    76 qed
```
```    77
```
```    78 interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
```
```    79 qed (force simp add: set_times_def mult.assoc)
```
```    80
```
```    81 interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
```
```    82 qed (force simp add: set_times_def mult.commute)
```
```    83
```
```    84 interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
```
```    85 qed (simp_all add: set_times_def)
```
```    86
```
```    87 interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
```
```    88 qed (simp add: set_times_def)
```
```    89
```
```    90 definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
```
```    91   "power_set n A = power.power {1} set_times A n"
```
```    92
```
```    93 interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
```
```    94   "power.power {1} set_times = (\<lambda>A n. power_set n A)"
```
```    95 proof -
```
```    96   show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
```
```    97   qed (simp_all add: set_mult.assoc)
```
```    98   show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
```
```    99     by (simp add: power_set_def)
```
```   100 qed
```
```   101
```
```   102 definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
```
```   103   "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
```
```   104
```
```   105 interpretation set_mult!:
```
```   106   comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set
```
```   107 proof
```
```   108 qed (fact setprod_set_def)
```
```   109
```
```   110 interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
```
```   111   "power.power {1} set_times = (\<lambda>A n. power_set n A)"
```
```   112   and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
```
```   113 proof -
```
```   114   show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
```
```   115   qed (simp_all add: set_mult.commute)
```
```   116   then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
```
```   117   show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
```
```   118     by (simp add: power_set_def)
```
```   119   show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
```
```   120     by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
```
```   121 qed
```
```   122
```
```   123 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
```
```   124   by (auto simp add: set_plus_def)
```
```   125
```
```   126 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
```
```   127   by (auto simp add: elt_set_plus_def)
```
```   128
```
```   129 lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
```
```   130     (b +o D) = (a + b) +o (C \<oplus> D)"
```
```   131   apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
```
```   132    apply (rule_tac x = "ba + bb" in exI)
```
```   133   apply (auto simp add: add_ac)
```
```   134   apply (rule_tac x = "aa + a" in exI)
```
```   135   apply (auto simp add: add_ac)
```
```   136   done
```
```   137
```
```   138 lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
```
```   139     (a + b) +o C"
```
```   140   by (auto simp add: elt_set_plus_def add_assoc)
```
```   141
```
```   142 lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
```
```   143     a +o (B \<oplus> C)"
```
```   144   apply (auto simp add: elt_set_plus_def set_plus_def)
```
```   145    apply (blast intro: add_ac)
```
```   146   apply (rule_tac x = "a + aa" in exI)
```
```   147   apply (rule conjI)
```
```   148    apply (rule_tac x = "aa" in bexI)
```
```   149     apply auto
```
```   150   apply (rule_tac x = "ba" in bexI)
```
```   151    apply (auto simp add: add_ac)
```
```   152   done
```
```   153
```
```   154 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
```
```   155     a +o (C \<oplus> D)"
```
```   156   apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
```
```   157    apply (rule_tac x = "aa + ba" in exI)
```
```   158    apply (auto simp add: add_ac)
```
```   159   done
```
```   160
```
```   161 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
```
```   162   set_plus_rearrange3 set_plus_rearrange4
```
```   163
```
```   164 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
```
```   165   by (auto simp add: elt_set_plus_def)
```
```   166
```
```   167 lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
```
```   168     C \<oplus> E <= D \<oplus> F"
```
```   169   by (auto simp add: set_plus_def)
```
```   170
```
```   171 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
```
```   172   by (auto simp add: elt_set_plus_def set_plus_def)
```
```   173
```
```   174 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
```
```   175     a +o D <= D \<oplus> C"
```
```   176   by (auto simp add: elt_set_plus_def set_plus_def add_ac)
```
```   177
```
```   178 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
```
```   179   apply (subgoal_tac "a +o B <= a +o D")
```
```   180    apply (erule order_trans)
```
```   181    apply (erule set_plus_mono3)
```
```   182   apply (erule set_plus_mono)
```
```   183   done
```
```   184
```
```   185 lemma set_plus_mono_b: "C <= D ==> x : a +o C
```
```   186     ==> x : a +o D"
```
```   187   apply (frule set_plus_mono)
```
```   188   apply auto
```
```   189   done
```
```   190
```
```   191 lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
```
```   192     x : D \<oplus> F"
```
```   193   apply (frule set_plus_mono2)
```
```   194    prefer 2
```
```   195    apply force
```
```   196   apply assumption
```
```   197   done
```
```   198
```
```   199 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
```
```   200   apply (frule set_plus_mono3)
```
```   201   apply auto
```
```   202   done
```
```   203
```
```   204 lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
```
```   205     x : a +o D ==> x : D \<oplus> C"
```
```   206   apply (frule set_plus_mono4)
```
```   207   apply auto
```
```   208   done
```
```   209
```
```   210 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
```
```   211   by (auto simp add: elt_set_plus_def)
```
```   212
```
```   213 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
```
```   214   apply (auto intro!: subsetI simp add: set_plus_def)
```
```   215   apply (rule_tac x = 0 in bexI)
```
```   216    apply (rule_tac x = x in bexI)
```
```   217     apply (auto simp add: add_ac)
```
```   218   done
```
```   219
```
```   220 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
```
```   221   by (auto simp add: elt_set_plus_def add_ac diff_minus)
```
```   222
```
```   223 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
```
```   224   apply (auto simp add: elt_set_plus_def add_ac diff_minus)
```
```   225   apply (subgoal_tac "a = (a + - b) + b")
```
```   226    apply (rule bexI, assumption, assumption)
```
```   227   apply (auto simp add: add_ac)
```
```   228   done
```
```   229
```
```   230 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
```
```   231   by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
```
```   232     assumption)
```
```   233
```
```   234 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
```
```   235   by (auto simp add: set_times_def)
```
```   236
```
```   237 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
```
```   238   by (auto simp add: elt_set_times_def)
```
```   239
```
```   240 lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
```
```   241     (b *o D) = (a * b) *o (C \<otimes> D)"
```
```   242   apply (auto simp add: elt_set_times_def set_times_def)
```
```   243    apply (rule_tac x = "ba * bb" in exI)
```
```   244    apply (auto simp add: mult_ac)
```
```   245   apply (rule_tac x = "aa * a" in exI)
```
```   246   apply (auto simp add: mult_ac)
```
```   247   done
```
```   248
```
```   249 lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
```
```   250     (a * b) *o C"
```
```   251   by (auto simp add: elt_set_times_def mult_assoc)
```
```   252
```
```   253 lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
```
```   254     a *o (B \<otimes> C)"
```
```   255   apply (auto simp add: elt_set_times_def set_times_def)
```
```   256    apply (blast intro: mult_ac)
```
```   257   apply (rule_tac x = "a * aa" in exI)
```
```   258   apply (rule conjI)
```
```   259    apply (rule_tac x = "aa" in bexI)
```
```   260     apply auto
```
```   261   apply (rule_tac x = "ba" in bexI)
```
```   262    apply (auto simp add: mult_ac)
```
```   263   done
```
```   264
```
```   265 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
```
```   266     a *o (C \<otimes> D)"
```
```   267   apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
```
```   268     mult_ac)
```
```   269    apply (rule_tac x = "aa * ba" in exI)
```
```   270    apply (auto simp add: mult_ac)
```
```   271   done
```
```   272
```
```   273 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
```
```   274   set_times_rearrange3 set_times_rearrange4
```
```   275
```
```   276 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
```
```   277   by (auto simp add: elt_set_times_def)
```
```   278
```
```   279 lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
```
```   280     C \<otimes> E <= D \<otimes> F"
```
```   281   by (auto simp add: set_times_def)
```
```   282
```
```   283 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
```
```   284   by (auto simp add: elt_set_times_def set_times_def)
```
```   285
```
```   286 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
```
```   287     a *o D <= D \<otimes> C"
```
```   288   by (auto simp add: elt_set_times_def set_times_def mult_ac)
```
```   289
```
```   290 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
```
```   291   apply (subgoal_tac "a *o B <= a *o D")
```
```   292    apply (erule order_trans)
```
```   293    apply (erule set_times_mono3)
```
```   294   apply (erule set_times_mono)
```
```   295   done
```
```   296
```
```   297 lemma set_times_mono_b: "C <= D ==> x : a *o C
```
```   298     ==> x : a *o D"
```
```   299   apply (frule set_times_mono)
```
```   300   apply auto
```
```   301   done
```
```   302
```
```   303 lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
```
```   304     x : D \<otimes> F"
```
```   305   apply (frule set_times_mono2)
```
```   306    prefer 2
```
```   307    apply force
```
```   308   apply assumption
```
```   309   done
```
```   310
```
```   311 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
```
```   312   apply (frule set_times_mono3)
```
```   313   apply auto
```
```   314   done
```
```   315
```
```   316 lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
```
```   317     x : a *o D ==> x : D \<otimes> C"
```
```   318   apply (frule set_times_mono4)
```
```   319   apply auto
```
```   320   done
```
```   321
```
```   322 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
```
```   323   by (auto simp add: elt_set_times_def)
```
```   324
```
```   325 lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
```
```   326     (a * b) +o (a *o C)"
```
```   327   by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
```
```   328
```
```   329 lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
```
```   330     (a *o B) \<oplus> (a *o C)"
```
```   331   apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
```
```   332    apply blast
```
```   333   apply (rule_tac x = "b + bb" in exI)
```
```   334   apply (auto simp add: ring_distribs)
```
```   335   done
```
```   336
```
```   337 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
```
```   338     a *o D \<oplus> C \<otimes> D"
```
```   339   apply (auto intro!: subsetI simp add:
```
```   340     elt_set_plus_def elt_set_times_def set_times_def
```
```   341     set_plus_def ring_distribs)
```
```   342   apply auto
```
```   343   done
```
```   344
```
```   345 theorems set_times_plus_distribs =
```
```   346   set_times_plus_distrib
```
```   347   set_times_plus_distrib2
```
```   348
```
```   349 lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
```
```   350     - a : C"
```
```   351   by (auto simp add: elt_set_times_def)
```
```   352
```
```   353 lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
```
```   354     - a : (- 1) *o C"
```
```   355   by (auto simp add: elt_set_times_def)
```
```   356
```
```   357 end
```