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