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