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