src/HOL/Library/SetsAndFunctions.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 30741 9e23e3ea7edd
child 35267 8dfd816713c6
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Library/SetsAndFunctions.thy
     2     Author:     Jeremy Avigad and Kevin Donnelly
     3 *)
     4 
     5 header {* Operations on sets and functions *}
     6 
     7 theory SetsAndFunctions
     8 imports Main
     9 begin
    10 
    11 text {*
    12 This library lifts operations like addition and muliplication to sets and
    13 functions of appropriate types. It was designed to support asymptotic
    14 calculations. See the comments at the top of theory @{text BigO}.
    15 *}
    16 
    17 subsection {* Basic definitions *}
    18 
    19 definition
    20   set_plus :: "('a::plus) set => 'a set => 'a set"  (infixl "\<oplus>" 65) where
    21   "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
    22 
    23 instantiation "fun" :: (type, plus) plus
    24 begin
    25 
    26 definition
    27   func_plus: "f + g == (%x. f x + g x)"
    28 
    29 instance ..
    30 
    31 end
    32 
    33 definition
    34   set_times :: "('a::times) set => 'a set => 'a set"  (infixl "\<otimes>" 70) where
    35   "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
    36 
    37 instantiation "fun" :: (type, times) times
    38 begin
    39 
    40 definition
    41   func_times: "f * g == (%x. f x * g x)"
    42 
    43 instance ..
    44 
    45 end
    46 
    47 
    48 instantiation "fun" :: (type, zero) zero
    49 begin
    50 
    51 definition
    52   func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
    53 
    54 instance ..
    55 
    56 end
    57 
    58 instantiation "fun" :: (type, one) one
    59 begin
    60 
    61 definition
    62   func_one: "1::(('a::type) => ('b::one)) == %x. 1"
    63 
    64 instance ..
    65 
    66 end
    67 
    68 definition
    69   elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
    70   "a +o B = {c. EX b:B. c = a + b}"
    71 
    72 definition
    73   elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80) where
    74   "a *o B = {c. EX b:B. c = a * b}"
    75 
    76 abbreviation (input)
    77   elt_set_eq :: "'a => 'a set => bool"  (infix "=o" 50) where
    78   "x =o A == x : A"
    79 
    80 instance "fun" :: (type,semigroup_add)semigroup_add
    81   by default (auto simp add: func_plus add_assoc)
    82 
    83 instance "fun" :: (type,comm_monoid_add)comm_monoid_add
    84   by default (auto simp add: func_zero func_plus add_ac)
    85 
    86 instance "fun" :: (type,ab_group_add)ab_group_add
    87   apply default
    88    apply (simp add: fun_Compl_def func_plus func_zero)
    89   apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
    90   done
    91 
    92 instance "fun" :: (type,semigroup_mult)semigroup_mult
    93   apply default
    94   apply (auto simp add: func_times mult_assoc)
    95   done
    96 
    97 instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
    98   apply default
    99    apply (auto simp add: func_one func_times mult_ac)
   100   done
   101 
   102 instance "fun" :: (type,comm_ring_1)comm_ring_1
   103   apply default
   104    apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def
   105      func_one func_zero algebra_simps)
   106   apply (drule fun_cong)
   107   apply simp
   108   done
   109 
   110 interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
   111   apply default
   112   apply (unfold set_plus_def)
   113   apply (force simp add: add_assoc)
   114   done
   115 
   116 interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
   117   apply default
   118   apply (unfold set_times_def)
   119   apply (force simp add: mult_assoc)
   120   done
   121 
   122 interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
   123   apply default
   124    apply (unfold set_plus_def)
   125    apply (force simp add: add_ac)
   126   apply force
   127   done
   128 
   129 interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
   130   apply default
   131    apply (unfold set_times_def)
   132    apply (force simp add: mult_ac)
   133   apply force
   134   done
   135 
   136 
   137 subsection {* Basic properties *}
   138 
   139 lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
   140   by (auto simp add: set_plus_def)
   141 
   142 lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
   143   by (auto simp add: elt_set_plus_def)
   144 
   145 lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
   146     (b +o D) = (a + b) +o (C \<oplus> D)"
   147   apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
   148    apply (rule_tac x = "ba + bb" in exI)
   149   apply (auto simp add: add_ac)
   150   apply (rule_tac x = "aa + a" in exI)
   151   apply (auto simp add: add_ac)
   152   done
   153 
   154 lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
   155     (a + b) +o C"
   156   by (auto simp add: elt_set_plus_def add_assoc)
   157 
   158 lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
   159     a +o (B \<oplus> C)"
   160   apply (auto simp add: elt_set_plus_def set_plus_def)
   161    apply (blast intro: add_ac)
   162   apply (rule_tac x = "a + aa" in exI)
   163   apply (rule conjI)
   164    apply (rule_tac x = "aa" in bexI)
   165     apply auto
   166   apply (rule_tac x = "ba" in bexI)
   167    apply (auto simp add: add_ac)
   168   done
   169 
   170 theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
   171     a +o (C \<oplus> D)"
   172   apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
   173    apply (rule_tac x = "aa + ba" in exI)
   174    apply (auto simp add: add_ac)
   175   done
   176 
   177 theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
   178   set_plus_rearrange3 set_plus_rearrange4
   179 
   180 lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
   181   by (auto simp add: elt_set_plus_def)
   182 
   183 lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
   184     C \<oplus> E <= D \<oplus> F"
   185   by (auto simp add: set_plus_def)
   186 
   187 lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
   188   by (auto simp add: elt_set_plus_def set_plus_def)
   189 
   190 lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
   191     a +o D <= D \<oplus> C"
   192   by (auto simp add: elt_set_plus_def set_plus_def add_ac)
   193 
   194 lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
   195   apply (subgoal_tac "a +o B <= a +o D")
   196    apply (erule order_trans)
   197    apply (erule set_plus_mono3)
   198   apply (erule set_plus_mono)
   199   done
   200 
   201 lemma set_plus_mono_b: "C <= D ==> x : a +o C
   202     ==> x : a +o D"
   203   apply (frule set_plus_mono)
   204   apply auto
   205   done
   206 
   207 lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
   208     x : D \<oplus> F"
   209   apply (frule set_plus_mono2)
   210    prefer 2
   211    apply force
   212   apply assumption
   213   done
   214 
   215 lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
   216   apply (frule set_plus_mono3)
   217   apply auto
   218   done
   219 
   220 lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
   221     x : a +o D ==> x : D \<oplus> C"
   222   apply (frule set_plus_mono4)
   223   apply auto
   224   done
   225 
   226 lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
   227   by (auto simp add: elt_set_plus_def)
   228 
   229 lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
   230   apply (auto intro!: subsetI simp add: set_plus_def)
   231   apply (rule_tac x = 0 in bexI)
   232    apply (rule_tac x = x in bexI)
   233     apply (auto simp add: add_ac)
   234   done
   235 
   236 lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
   237   by (auto simp add: elt_set_plus_def add_ac diff_minus)
   238 
   239 lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
   240   apply (auto simp add: elt_set_plus_def add_ac diff_minus)
   241   apply (subgoal_tac "a = (a + - b) + b")
   242    apply (rule bexI, assumption, assumption)
   243   apply (auto simp add: add_ac)
   244   done
   245 
   246 lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
   247   by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
   248     assumption)
   249 
   250 lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
   251   by (auto simp add: set_times_def)
   252 
   253 lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
   254   by (auto simp add: elt_set_times_def)
   255 
   256 lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
   257     (b *o D) = (a * b) *o (C \<otimes> D)"
   258   apply (auto simp add: elt_set_times_def set_times_def)
   259    apply (rule_tac x = "ba * bb" in exI)
   260    apply (auto simp add: mult_ac)
   261   apply (rule_tac x = "aa * a" in exI)
   262   apply (auto simp add: mult_ac)
   263   done
   264 
   265 lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
   266     (a * b) *o C"
   267   by (auto simp add: elt_set_times_def mult_assoc)
   268 
   269 lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
   270     a *o (B \<otimes> C)"
   271   apply (auto simp add: elt_set_times_def set_times_def)
   272    apply (blast intro: mult_ac)
   273   apply (rule_tac x = "a * aa" in exI)
   274   apply (rule conjI)
   275    apply (rule_tac x = "aa" in bexI)
   276     apply auto
   277   apply (rule_tac x = "ba" in bexI)
   278    apply (auto simp add: mult_ac)
   279   done
   280 
   281 theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
   282     a *o (C \<otimes> D)"
   283   apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
   284     mult_ac)
   285    apply (rule_tac x = "aa * ba" in exI)
   286    apply (auto simp add: mult_ac)
   287   done
   288 
   289 theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
   290   set_times_rearrange3 set_times_rearrange4
   291 
   292 lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
   293   by (auto simp add: elt_set_times_def)
   294 
   295 lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
   296     C \<otimes> E <= D \<otimes> F"
   297   by (auto simp add: set_times_def)
   298 
   299 lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
   300   by (auto simp add: elt_set_times_def set_times_def)
   301 
   302 lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
   303     a *o D <= D \<otimes> C"
   304   by (auto simp add: elt_set_times_def set_times_def mult_ac)
   305 
   306 lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
   307   apply (subgoal_tac "a *o B <= a *o D")
   308    apply (erule order_trans)
   309    apply (erule set_times_mono3)
   310   apply (erule set_times_mono)
   311   done
   312 
   313 lemma set_times_mono_b: "C <= D ==> x : a *o C
   314     ==> x : a *o D"
   315   apply (frule set_times_mono)
   316   apply auto
   317   done
   318 
   319 lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
   320     x : D \<otimes> F"
   321   apply (frule set_times_mono2)
   322    prefer 2
   323    apply force
   324   apply assumption
   325   done
   326 
   327 lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
   328   apply (frule set_times_mono3)
   329   apply auto
   330   done
   331 
   332 lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
   333     x : a *o D ==> x : D \<otimes> C"
   334   apply (frule set_times_mono4)
   335   apply auto
   336   done
   337 
   338 lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
   339   by (auto simp add: elt_set_times_def)
   340 
   341 lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
   342     (a * b) +o (a *o C)"
   343   by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
   344 
   345 lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
   346     (a *o B) \<oplus> (a *o C)"
   347   apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
   348    apply blast
   349   apply (rule_tac x = "b + bb" in exI)
   350   apply (auto simp add: ring_distribs)
   351   done
   352 
   353 lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
   354     a *o D \<oplus> C \<otimes> D"
   355   apply (auto intro!: subsetI simp add:
   356     elt_set_plus_def elt_set_times_def set_times_def
   357     set_plus_def ring_distribs)
   358   apply auto
   359   done
   360 
   361 theorems set_times_plus_distribs =
   362   set_times_plus_distrib
   363   set_times_plus_distrib2
   364 
   365 lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
   366     - a : C"
   367   by (auto simp add: elt_set_times_def)
   368 
   369 lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
   370     - a : (- 1) *o C"
   371   by (auto simp add: elt_set_times_def)
   372 
   373 end