src/HOL/Import/HOL/HOL4Real.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17694 b7870c2bd7df
child 20485 3078fd2eec7b
permissions -rw-r--r--
adaptions to codegen_package
skalberg@15647
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
skalberg@15647
     2
wenzelm@17566
     3
theory HOL4Real imports HOL4Base begin
skalberg@14516
     4
skalberg@14516
     5
;setup_theory realax
skalberg@14516
     6
obua@17644
     7
lemma HREAL_RDISTRIB: "ALL (x::hreal) (y::hreal) z::hreal.
skalberg@14516
     8
   hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"
skalberg@14516
     9
  by (import realax HREAL_RDISTRIB)
skalberg@14516
    10
obua@17644
    11
lemma HREAL_EQ_ADDL: "ALL (x::hreal) y::hreal. x ~= hreal_add x y"
skalberg@14516
    12
  by (import realax HREAL_EQ_ADDL)
skalberg@14516
    13
obua@17644
    14
lemma HREAL_EQ_LADD: "ALL (x::hreal) (y::hreal) z::hreal.
obua@17644
    15
   (hreal_add x y = hreal_add x z) = (y = z)"
skalberg@14516
    16
  by (import realax HREAL_EQ_LADD)
skalberg@14516
    17
obua@17644
    18
lemma HREAL_LT_REFL: "ALL x::hreal. ~ hreal_lt x x"
skalberg@14516
    19
  by (import realax HREAL_LT_REFL)
skalberg@14516
    20
obua@17644
    21
lemma HREAL_LT_ADDL: "ALL (x::hreal) y::hreal. hreal_lt x (hreal_add x y)"
skalberg@14516
    22
  by (import realax HREAL_LT_ADDL)
skalberg@14516
    23
obua@17644
    24
lemma HREAL_LT_NE: "ALL (x::hreal) y::hreal. hreal_lt x y --> x ~= y"
skalberg@14516
    25
  by (import realax HREAL_LT_NE)
skalberg@14516
    26
obua@17644
    27
lemma HREAL_LT_ADDR: "ALL (x::hreal) y::hreal. ~ hreal_lt (hreal_add x y) x"
skalberg@14516
    28
  by (import realax HREAL_LT_ADDR)
skalberg@14516
    29
obua@17644
    30
lemma HREAL_LT_GT: "ALL (x::hreal) y::hreal. hreal_lt x y --> ~ hreal_lt y x"
skalberg@14516
    31
  by (import realax HREAL_LT_GT)
skalberg@14516
    32
obua@17644
    33
lemma HREAL_LT_ADD2: "ALL (x1::hreal) (x2::hreal) (y1::hreal) y2::hreal.
skalberg@14516
    34
   hreal_lt x1 y1 & hreal_lt x2 y2 -->
skalberg@14516
    35
   hreal_lt (hreal_add x1 x2) (hreal_add y1 y2)"
skalberg@14516
    36
  by (import realax HREAL_LT_ADD2)
skalberg@14516
    37
obua@17644
    38
lemma HREAL_LT_LADD: "ALL (x::hreal) (y::hreal) z::hreal.
obua@17644
    39
   hreal_lt (hreal_add x y) (hreal_add x z) = hreal_lt y z"
skalberg@14516
    40
  by (import realax HREAL_LT_LADD)
skalberg@14516
    41
skalberg@14516
    42
constdefs
skalberg@14516
    43
  treal_0 :: "hreal * hreal" 
skalberg@14516
    44
  "treal_0 == (hreal_1, hreal_1)"
skalberg@14516
    45
skalberg@14516
    46
lemma treal_0: "treal_0 = (hreal_1, hreal_1)"
skalberg@14516
    47
  by (import realax treal_0)
skalberg@14516
    48
skalberg@14516
    49
constdefs
skalberg@14516
    50
  treal_1 :: "hreal * hreal" 
skalberg@14516
    51
  "treal_1 == (hreal_add hreal_1 hreal_1, hreal_1)"
skalberg@14516
    52
skalberg@14516
    53
lemma treal_1: "treal_1 = (hreal_add hreal_1 hreal_1, hreal_1)"
skalberg@14516
    54
  by (import realax treal_1)
skalberg@14516
    55
skalberg@14516
    56
constdefs
skalberg@14516
    57
  treal_neg :: "hreal * hreal => hreal * hreal" 
obua@17644
    58
  "treal_neg == %(x::hreal, y::hreal). (y, x)"
obua@17644
    59
obua@17644
    60
lemma treal_neg: "ALL (x::hreal) y::hreal. treal_neg (x, y) = (y, x)"
skalberg@14516
    61
  by (import realax treal_neg)
skalberg@14516
    62
skalberg@14516
    63
constdefs
skalberg@14516
    64
  treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" 
obua@17644
    65
  "treal_add ==
obua@17644
    66
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
obua@17644
    67
   (hreal_add x1 x2, hreal_add y1 y2)"
obua@17644
    68
obua@17644
    69
lemma treal_add: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
skalberg@14516
    70
   treal_add (x1, y1) (x2, y2) = (hreal_add x1 x2, hreal_add y1 y2)"
skalberg@14516
    71
  by (import realax treal_add)
skalberg@14516
    72
skalberg@14516
    73
constdefs
skalberg@14516
    74
  treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" 
skalberg@14516
    75
  "treal_mul ==
obua@17644
    76
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
skalberg@14516
    77
   (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
skalberg@14516
    78
    hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
skalberg@14516
    79
obua@17644
    80
lemma treal_mul: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
skalberg@14516
    81
   treal_mul (x1, y1) (x2, y2) =
skalberg@14516
    82
   (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
skalberg@14516
    83
    hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
skalberg@14516
    84
  by (import realax treal_mul)
skalberg@14516
    85
skalberg@14516
    86
constdefs
skalberg@14516
    87
  treal_lt :: "hreal * hreal => hreal * hreal => bool" 
obua@17644
    88
  "treal_lt ==
obua@17644
    89
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
obua@17644
    90
   hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
obua@17644
    91
obua@17644
    92
lemma treal_lt: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
skalberg@14516
    93
   treal_lt (x1, y1) (x2, y2) = hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
skalberg@14516
    94
  by (import realax treal_lt)
skalberg@14516
    95
skalberg@14516
    96
constdefs
skalberg@14516
    97
  treal_inv :: "hreal * hreal => hreal * hreal" 
skalberg@14516
    98
  "treal_inv ==
obua@17644
    99
%(x::hreal, y::hreal).
skalberg@14516
   100
   if x = y then treal_0
skalberg@14516
   101
   else if hreal_lt y x
skalberg@14516
   102
        then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
skalberg@14516
   103
        else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1)"
skalberg@14516
   104
obua@17644
   105
lemma treal_inv: "ALL (x::hreal) y::hreal.
skalberg@14516
   106
   treal_inv (x, y) =
skalberg@14516
   107
   (if x = y then treal_0
skalberg@14516
   108
    else if hreal_lt y x
skalberg@14516
   109
         then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
skalberg@14516
   110
         else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1))"
skalberg@14516
   111
  by (import realax treal_inv)
skalberg@14516
   112
skalberg@14516
   113
constdefs
skalberg@14516
   114
  treal_eq :: "hreal * hreal => hreal * hreal => bool" 
obua@17644
   115
  "treal_eq ==
obua@17644
   116
%(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
obua@17644
   117
   hreal_add x1 y2 = hreal_add x2 y1"
obua@17644
   118
obua@17644
   119
lemma treal_eq: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
skalberg@14516
   120
   treal_eq (x1, y1) (x2, y2) = (hreal_add x1 y2 = hreal_add x2 y1)"
skalberg@14516
   121
  by (import realax treal_eq)
skalberg@14516
   122
obua@17644
   123
lemma TREAL_EQ_REFL: "ALL x::hreal * hreal. treal_eq x x"
skalberg@14516
   124
  by (import realax TREAL_EQ_REFL)
skalberg@14516
   125
obua@17644
   126
lemma TREAL_EQ_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_eq x y = treal_eq y x"
skalberg@14516
   127
  by (import realax TREAL_EQ_SYM)
skalberg@14516
   128
obua@17644
   129
lemma TREAL_EQ_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
obua@17644
   130
   treal_eq x y & treal_eq y z --> treal_eq x z"
skalberg@14516
   131
  by (import realax TREAL_EQ_TRANS)
skalberg@14516
   132
obua@17644
   133
lemma TREAL_EQ_EQUIV: "ALL (p::hreal * hreal) q::hreal * hreal.
obua@17644
   134
   treal_eq p q = (treal_eq p = treal_eq q)"
skalberg@14516
   135
  by (import realax TREAL_EQ_EQUIV)
skalberg@14516
   136
obua@17644
   137
lemma TREAL_EQ_AP: "ALL (p::hreal * hreal) q::hreal * hreal. p = q --> treal_eq p q"
skalberg@14516
   138
  by (import realax TREAL_EQ_AP)
skalberg@14516
   139
skalberg@14516
   140
lemma TREAL_10: "~ treal_eq treal_1 treal_0"
skalberg@14516
   141
  by (import realax TREAL_10)
skalberg@14516
   142
obua@17644
   143
lemma TREAL_ADD_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_add x y = treal_add y x"
skalberg@14516
   144
  by (import realax TREAL_ADD_SYM)
skalberg@14516
   145
obua@17644
   146
lemma TREAL_MUL_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_mul x y = treal_mul y x"
skalberg@14516
   147
  by (import realax TREAL_MUL_SYM)
skalberg@14516
   148
obua@17644
   149
lemma TREAL_ADD_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
obua@17644
   150
   treal_add x (treal_add y z) = treal_add (treal_add x y) z"
skalberg@14516
   151
  by (import realax TREAL_ADD_ASSOC)
skalberg@14516
   152
obua@17644
   153
lemma TREAL_MUL_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
obua@17644
   154
   treal_mul x (treal_mul y z) = treal_mul (treal_mul x y) z"
skalberg@14516
   155
  by (import realax TREAL_MUL_ASSOC)
skalberg@14516
   156
obua@17644
   157
lemma TREAL_LDISTRIB: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
skalberg@14516
   158
   treal_mul x (treal_add y z) = treal_add (treal_mul x y) (treal_mul x z)"
skalberg@14516
   159
  by (import realax TREAL_LDISTRIB)
skalberg@14516
   160
obua@17644
   161
lemma TREAL_ADD_LID: "ALL x::hreal * hreal. treal_eq (treal_add treal_0 x) x"
skalberg@14516
   162
  by (import realax TREAL_ADD_LID)
skalberg@14516
   163
obua@17644
   164
lemma TREAL_MUL_LID: "ALL x::hreal * hreal. treal_eq (treal_mul treal_1 x) x"
skalberg@14516
   165
  by (import realax TREAL_MUL_LID)
skalberg@14516
   166
obua@17644
   167
lemma TREAL_ADD_LINV: "ALL x::hreal * hreal. treal_eq (treal_add (treal_neg x) x) treal_0"
skalberg@14516
   168
  by (import realax TREAL_ADD_LINV)
skalberg@14516
   169
skalberg@14516
   170
lemma TREAL_INV_0: "treal_eq (treal_inv treal_0) treal_0"
skalberg@14516
   171
  by (import realax TREAL_INV_0)
skalberg@14516
   172
obua@17644
   173
lemma TREAL_MUL_LINV: "ALL x::hreal * hreal.
obua@17644
   174
   ~ treal_eq x treal_0 --> treal_eq (treal_mul (treal_inv x) x) treal_1"
skalberg@14516
   175
  by (import realax TREAL_MUL_LINV)
skalberg@14516
   176
obua@17644
   177
lemma TREAL_LT_TOTAL: "ALL (x::hreal * hreal) y::hreal * hreal.
obua@17644
   178
   treal_eq x y | treal_lt x y | treal_lt y x"
skalberg@14516
   179
  by (import realax TREAL_LT_TOTAL)
skalberg@14516
   180
obua@17644
   181
lemma TREAL_LT_REFL: "ALL x::hreal * hreal. ~ treal_lt x x"
skalberg@14516
   182
  by (import realax TREAL_LT_REFL)
skalberg@14516
   183
obua@17644
   184
lemma TREAL_LT_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
obua@17644
   185
   treal_lt x y & treal_lt y z --> treal_lt x z"
skalberg@14516
   186
  by (import realax TREAL_LT_TRANS)
skalberg@14516
   187
obua@17644
   188
lemma TREAL_LT_ADD: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
obua@17644
   189
   treal_lt y z --> treal_lt (treal_add x y) (treal_add x z)"
skalberg@14516
   190
  by (import realax TREAL_LT_ADD)
skalberg@14516
   191
obua@17644
   192
lemma TREAL_LT_MUL: "ALL (x::hreal * hreal) y::hreal * hreal.
skalberg@14516
   193
   treal_lt treal_0 x & treal_lt treal_0 y -->
skalberg@14516
   194
   treal_lt treal_0 (treal_mul x y)"
skalberg@14516
   195
  by (import realax TREAL_LT_MUL)
skalberg@14516
   196
skalberg@14516
   197
constdefs
skalberg@14516
   198
  treal_of_hreal :: "hreal => hreal * hreal" 
obua@17644
   199
  "treal_of_hreal == %x::hreal. (hreal_add x hreal_1, hreal_1)"
obua@17644
   200
obua@17644
   201
lemma treal_of_hreal: "ALL x::hreal. treal_of_hreal x = (hreal_add x hreal_1, hreal_1)"
skalberg@14516
   202
  by (import realax treal_of_hreal)
skalberg@14516
   203
skalberg@14516
   204
constdefs
skalberg@14516
   205
  hreal_of_treal :: "hreal * hreal => hreal" 
obua@17644
   206
  "hreal_of_treal == %(x::hreal, y::hreal). SOME d::hreal. x = hreal_add y d"
obua@17644
   207
obua@17644
   208
lemma hreal_of_treal: "ALL (x::hreal) y::hreal.
obua@17644
   209
   hreal_of_treal (x, y) = (SOME d::hreal. x = hreal_add y d)"
skalberg@14516
   210
  by (import realax hreal_of_treal)
skalberg@14516
   211
obua@17644
   212
lemma TREAL_BIJ: "(ALL h::hreal. hreal_of_treal (treal_of_hreal h) = h) &
obua@17644
   213
(ALL r::hreal * hreal.
obua@17644
   214
    treal_lt treal_0 r = treal_eq (treal_of_hreal (hreal_of_treal r)) r)"
skalberg@14516
   215
  by (import realax TREAL_BIJ)
skalberg@14516
   216
obua@17644
   217
lemma TREAL_ISO: "ALL (h::hreal) i::hreal.
obua@17644
   218
   hreal_lt h i --> treal_lt (treal_of_hreal h) (treal_of_hreal i)"
skalberg@14516
   219
  by (import realax TREAL_ISO)
skalberg@14516
   220
obua@17644
   221
lemma TREAL_BIJ_WELLDEF: "ALL (h::hreal * hreal) i::hreal * hreal.
obua@17644
   222
   treal_eq h i --> hreal_of_treal h = hreal_of_treal i"
skalberg@14516
   223
  by (import realax TREAL_BIJ_WELLDEF)
skalberg@14516
   224
obua@17644
   225
lemma TREAL_NEG_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal.
obua@17644
   226
   treal_eq x1 x2 --> treal_eq (treal_neg x1) (treal_neg x2)"
skalberg@14516
   227
  by (import realax TREAL_NEG_WELLDEF)
skalberg@14516
   228
obua@17644
   229
lemma TREAL_ADD_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
obua@17644
   230
   treal_eq x1 x2 --> treal_eq (treal_add x1 y) (treal_add x2 y)"
skalberg@14516
   231
  by (import realax TREAL_ADD_WELLDEFR)
skalberg@14516
   232
obua@17644
   233
lemma TREAL_ADD_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
obua@17644
   234
   y2::hreal * hreal.
skalberg@14516
   235
   treal_eq x1 x2 & treal_eq y1 y2 -->
skalberg@14516
   236
   treal_eq (treal_add x1 y1) (treal_add x2 y2)"
skalberg@14516
   237
  by (import realax TREAL_ADD_WELLDEF)
skalberg@14516
   238
obua@17644
   239
lemma TREAL_MUL_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
obua@17644
   240
   treal_eq x1 x2 --> treal_eq (treal_mul x1 y) (treal_mul x2 y)"
skalberg@14516
   241
  by (import realax TREAL_MUL_WELLDEFR)
skalberg@14516
   242
obua@17644
   243
lemma TREAL_MUL_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
obua@17644
   244
   y2::hreal * hreal.
skalberg@14516
   245
   treal_eq x1 x2 & treal_eq y1 y2 -->
skalberg@14516
   246
   treal_eq (treal_mul x1 y1) (treal_mul x2 y2)"
skalberg@14516
   247
  by (import realax TREAL_MUL_WELLDEF)
skalberg@14516
   248
obua@17644
   249
lemma TREAL_LT_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
obua@17644
   250
   treal_eq x1 x2 --> treal_lt x1 y = treal_lt x2 y"
skalberg@14516
   251
  by (import realax TREAL_LT_WELLDEFR)
skalberg@14516
   252
obua@17644
   253
lemma TREAL_LT_WELLDEFL: "ALL (x::hreal * hreal) (y1::hreal * hreal) y2::hreal * hreal.
obua@17644
   254
   treal_eq y1 y2 --> treal_lt x y1 = treal_lt x y2"
skalberg@14516
   255
  by (import realax TREAL_LT_WELLDEFL)
skalberg@14516
   256
obua@17644
   257
lemma TREAL_LT_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
obua@17644
   258
   y2::hreal * hreal.
skalberg@14516
   259
   treal_eq x1 x2 & treal_eq y1 y2 --> treal_lt x1 y1 = treal_lt x2 y2"
skalberg@14516
   260
  by (import realax TREAL_LT_WELLDEF)
skalberg@14516
   261
obua@17644
   262
lemma TREAL_INV_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal.
obua@17644
   263
   treal_eq x1 x2 --> treal_eq (treal_inv x1) (treal_inv x2)"
skalberg@14516
   264
  by (import realax TREAL_INV_WELLDEF)
skalberg@14516
   265
skalberg@14516
   266
;end_setup
skalberg@14516
   267
skalberg@14516
   268
;setup_theory real
skalberg@14516
   269
obua@17652
   270
lemma REAL_0: "(op =::real => real => bool) (0::real) (0::real)"
skalberg@14516
   271
  by (import real REAL_0)
skalberg@14516
   272
obua@17652
   273
lemma REAL_1: "(op =::real => real => bool) (1::real) (1::real)"
skalberg@14516
   274
  by (import real REAL_1)
skalberg@14516
   275
obua@17652
   276
lemma REAL_ADD_LID_UNIQ: "ALL (x::real) y::real. (x + y = y) = (x = 0)"
skalberg@14516
   277
  by (import real REAL_ADD_LID_UNIQ)
skalberg@14516
   278
obua@17652
   279
lemma REAL_ADD_RID_UNIQ: "ALL (x::real) y::real. (x + y = x) = (y = 0)"
skalberg@14516
   280
  by (import real REAL_ADD_RID_UNIQ)
skalberg@14516
   281
obua@17652
   282
lemma REAL_LNEG_UNIQ: "ALL (x::real) y::real. (x + y = 0) = (x = - y)"
skalberg@14516
   283
  by (import real REAL_LNEG_UNIQ)
skalberg@14516
   284
skalberg@14516
   285
lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)"
skalberg@14516
   286
  by (import real REAL_LT_ANTISYM)
skalberg@14516
   287
skalberg@14516
   288
lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x"
skalberg@14516
   289
  by (import real REAL_LTE_TOTAL)
skalberg@14516
   290
skalberg@14516
   291
lemma REAL_LET_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y <= x)"
skalberg@14516
   292
  by (import real REAL_LET_ANTISYM)
skalberg@14516
   293
skalberg@14516
   294
lemma REAL_LTE_ANTSYM: "ALL (x::real) y::real. ~ (x <= y & y < x)"
skalberg@14516
   295
  by (import real REAL_LTE_ANTSYM)
skalberg@14516
   296
obua@17652
   297
lemma REAL_LT_NEGTOTAL: "ALL x::real. x = 0 | 0 < x | 0 < - x"
skalberg@14516
   298
  by (import real REAL_LT_NEGTOTAL)
skalberg@14516
   299
obua@17652
   300
lemma REAL_LE_NEGTOTAL: "ALL x::real. 0 <= x | 0 <= - x"
skalberg@14516
   301
  by (import real REAL_LE_NEGTOTAL)
skalberg@14516
   302
skalberg@14516
   303
lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)"
skalberg@14516
   304
  by (import real REAL_LT_ADDNEG)
skalberg@14516
   305
skalberg@14516
   306
lemma REAL_LT_ADDNEG2: "ALL (x::real) (y::real) z::real. (x + - y < z) = (x < z + y)"
skalberg@14516
   307
  by (import real REAL_LT_ADDNEG2)
skalberg@14516
   308
obua@17652
   309
lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + 1"
skalberg@14516
   310
  by (import real REAL_LT_ADD1)
skalberg@14516
   311
wenzelm@14796
   312
lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x"
wenzelm@14796
   313
  by (import real REAL_SUB_ADD2)
wenzelm@14796
   314
obua@17652
   315
lemma REAL_SUB_LT: "ALL (x::real) y::real. (0 < x - y) = (y < x)"
skalberg@15647
   316
  by (import real REAL_SUB_LT)
skalberg@15647
   317
obua@17652
   318
lemma REAL_SUB_LE: "ALL (x::real) y::real. (0 <= x - y) = (y <= x)"
skalberg@15647
   319
  by (import real REAL_SUB_LE)
skalberg@15647
   320
wenzelm@14796
   321
lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y"
wenzelm@14796
   322
  by (import real REAL_ADD_SUB)
skalberg@14516
   323
skalberg@14516
   324
lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)"
skalberg@14516
   325
  by (import real REAL_NEG_EQ)
skalberg@14516
   326
obua@17652
   327
lemma REAL_NEG_MINUS1: "ALL x::real. - x = - 1 * x"
skalberg@14516
   328
  by (import real REAL_NEG_MINUS1)
skalberg@14516
   329
obua@17652
   330
lemma REAL_LT_LMUL_0: "ALL (x::real) y::real. 0 < x --> (0 < x * y) = (0 < y)"
skalberg@14516
   331
  by (import real REAL_LT_LMUL_0)
skalberg@14516
   332
obua@17652
   333
lemma REAL_LT_RMUL_0: "ALL (x::real) y::real. 0 < y --> (0 < x * y) = (0 < x)"
skalberg@14516
   334
  by (import real REAL_LT_RMUL_0)
skalberg@14516
   335
obua@17652
   336
lemma REAL_LT_LMUL: "ALL (x::real) (y::real) z::real. 0 < x --> (x * y < x * z) = (y < z)"
skalberg@14516
   337
  by (import real REAL_LT_LMUL)
skalberg@14516
   338
obua@17652
   339
lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = 1 --> x = inverse y"
skalberg@14516
   340
  by (import real REAL_LINV_UNIQ)
skalberg@14516
   341
obua@17652
   342
lemma REAL_LE_INV: "(All::(real => bool) => bool)
obua@17652
   343
 (%x::real.
obua@17652
   344
     (op -->::bool => bool => bool)
obua@17652
   345
      ((op <=::real => real => bool) (0::real) x)
obua@17652
   346
      ((op <=::real => real => bool) (0::real) ((inverse::real => real) x)))"
skalberg@14516
   347
  by (import real REAL_LE_INV)
skalberg@14516
   348
obua@17652
   349
lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = (0 <= y)"
skalberg@14516
   350
  by (import real REAL_LE_ADDR)
skalberg@14516
   351
obua@17652
   352
lemma REAL_LE_ADDL: "ALL (x::real) y::real. (y <= x + y) = (0 <= x)"
skalberg@14516
   353
  by (import real REAL_LE_ADDL)
skalberg@14516
   354
obua@17652
   355
lemma REAL_LT_ADDR: "ALL (x::real) y::real. (x < x + y) = (0 < y)"
skalberg@14516
   356
  by (import real REAL_LT_ADDR)
skalberg@14516
   357
obua@17652
   358
lemma REAL_LT_ADDL: "ALL (x::real) y::real. (y < x + y) = (0 < x)"
skalberg@14516
   359
  by (import real REAL_LT_ADDL)
skalberg@14516
   360
obua@17652
   361
lemma REAL_LT_NZ: "ALL n::nat. (real n ~= 0) = (0 < real n)"
skalberg@14516
   362
  by (import real REAL_LT_NZ)
skalberg@14516
   363
obua@17652
   364
lemma REAL_NZ_IMP_LT: "ALL n::nat. n ~= 0 --> 0 < real n"
skalberg@14516
   365
  by (import real REAL_NZ_IMP_LT)
skalberg@14516
   366
obua@17652
   367
lemma REAL_LT_RDIV_0: "ALL (y::real) z::real. 0 < z --> (0 < y / z) = (0 < y)"
skalberg@14516
   368
  by (import real REAL_LT_RDIV_0)
skalberg@14516
   369
obua@17652
   370
lemma REAL_LT_RDIV: "ALL (x::real) (y::real) z::real. 0 < z --> (x / z < y / z) = (x < y)"
skalberg@14516
   371
  by (import real REAL_LT_RDIV)
skalberg@14516
   372
obua@17652
   373
lemma REAL_LT_FRACTION_0: "ALL (n::nat) d::real. n ~= 0 --> (0 < d / real n) = (0 < d)"
skalberg@14516
   374
  by (import real REAL_LT_FRACTION_0)
skalberg@14516
   375
obua@17652
   376
lemma REAL_LT_MULTIPLE: "ALL (x::nat) xa::real. 1 < x --> (xa < real x * xa) = (0 < xa)"
skalberg@14516
   377
  by (import real REAL_LT_MULTIPLE)
skalberg@14516
   378
obua@17652
   379
lemma REAL_LT_FRACTION: "ALL (n::nat) d::real. 1 < n --> (d / real n < d) = (0 < d)"
skalberg@14516
   380
  by (import real REAL_LT_FRACTION)
skalberg@14516
   381
obua@17652
   382
lemma REAL_LT_HALF2: "ALL d::real. (d / 2 < d) = (0 < d)"
skalberg@14516
   383
  by (import real REAL_LT_HALF2)
skalberg@14516
   384
obua@17652
   385
lemma REAL_DIV_LMUL: "ALL (x::real) y::real. y ~= 0 --> y * (x / y) = x"
skalberg@14516
   386
  by (import real REAL_DIV_LMUL)
skalberg@14516
   387
obua@17652
   388
lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= 0 --> x / y * y = x"
skalberg@14516
   389
  by (import real REAL_DIV_RMUL)
skalberg@14516
   390
obua@17652
   391
lemma REAL_DOWN: "(All::(real => bool) => bool)
obua@17652
   392
 (%x::real.
obua@17652
   393
     (op -->::bool => bool => bool)
obua@17652
   394
      ((op <::real => real => bool) (0::real) x)
obua@17652
   395
      ((Ex::(real => bool) => bool)
obua@17652
   396
        (%xa::real.
obua@17652
   397
            (op &::bool => bool => bool)
obua@17652
   398
             ((op <::real => real => bool) (0::real) xa)
obua@17652
   399
             ((op <::real => real => bool) xa x))))"
skalberg@14516
   400
  by (import real REAL_DOWN)
skalberg@14516
   401
skalberg@14516
   402
lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y"
skalberg@14516
   403
  by (import real REAL_SUB_SUB)
skalberg@14516
   404
skalberg@14516
   405
lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b - (c + d) = a - c + (b - d)"
skalberg@14516
   406
  by (import real REAL_ADD2_SUB2)
skalberg@14516
   407
skalberg@14516
   408
lemma REAL_SUB_LNEG: "ALL (x::real) y::real. - x - y = - (x + y)"
skalberg@14516
   409
  by (import real REAL_SUB_LNEG)
skalberg@14516
   410
skalberg@14516
   411
lemma REAL_SUB_NEG2: "ALL (x::real) y::real. - x - - y = y - x"
skalberg@14516
   412
  by (import real REAL_SUB_NEG2)
skalberg@14516
   413
skalberg@14516
   414
lemma REAL_SUB_TRIANGLE: "ALL (a::real) (b::real) c::real. a - b + (b - c) = a - c"
skalberg@14516
   415
  by (import real REAL_SUB_TRIANGLE)
skalberg@14516
   416
skalberg@14516
   417
lemma REAL_INV_MUL: "ALL (x::real) y::real.
obua@17652
   418
   x ~= 0 & y ~= 0 --> inverse (x * y) = inverse x * inverse y"
skalberg@14516
   419
  by (import real REAL_INV_MUL)
skalberg@14516
   420
skalberg@14516
   421
lemma REAL_SUB_INV2: "ALL (x::real) y::real.
obua@17652
   422
   x ~= 0 & y ~= 0 --> inverse x - inverse y = (y - x) / (x * y)"
skalberg@14516
   423
  by (import real REAL_SUB_INV2)
skalberg@14516
   424
skalberg@14516
   425
lemma REAL_SUB_SUB2: "ALL (x::real) y::real. x - (x - y) = y"
skalberg@14516
   426
  by (import real REAL_SUB_SUB2)
skalberg@14516
   427
skalberg@14516
   428
lemma REAL_ADD_SUB2: "ALL (x::real) y::real. x - (x + y) = - y"
skalberg@14516
   429
  by (import real REAL_ADD_SUB2)
skalberg@14516
   430
skalberg@14516
   431
lemma REAL_LE_MUL2: "ALL (x1::real) (x2::real) (y1::real) y2::real.
obua@17652
   432
   0 <= x1 & 0 <= y1 & x1 <= x2 & y1 <= y2 --> x1 * y1 <= x2 * y2"
skalberg@14516
   433
  by (import real REAL_LE_MUL2)
skalberg@14516
   434
obua@17652
   435
lemma REAL_LE_DIV: "ALL (x::real) xa::real. 0 <= x & 0 <= xa --> 0 <= x / xa"
skalberg@14516
   436
  by (import real REAL_LE_DIV)
skalberg@14516
   437
obua@17652
   438
lemma REAL_LT_1: "ALL (x::real) y::real. 0 <= x & x < y --> x / y < 1"
skalberg@14516
   439
  by (import real REAL_LT_1)
skalberg@14516
   440
obua@17652
   441
lemma REAL_POS_NZ: "(All::(real => bool) => bool)
obua@17652
   442
 (%x::real.
obua@17652
   443
     (op -->::bool => bool => bool)
obua@17652
   444
      ((op <::real => real => bool) (0::real) x)
obua@17652
   445
      ((Not::bool => bool) ((op =::real => real => bool) x (0::real))))"
skalberg@14516
   446
  by (import real REAL_POS_NZ)
skalberg@14516
   447
obua@17652
   448
lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real. x ~= 0 & x * xa = x * xb --> xa = xb"
skalberg@14516
   449
  by (import real REAL_EQ_LMUL_IMP)
skalberg@14516
   450
obua@17652
   451
lemma REAL_FACT_NZ: "ALL n::nat. real (FACT n) ~= 0"
skalberg@14516
   452
  by (import real REAL_FACT_NZ)
skalberg@14516
   453
skalberg@14516
   454
lemma REAL_DIFFSQ: "ALL (x::real) y::real. (x + y) * (x - y) = x * x - y * y"
skalberg@14516
   455
  by (import real REAL_DIFFSQ)
skalberg@14516
   456
obua@17652
   457
lemma REAL_POASQ: "ALL x::real. (0 < x * x) = (x ~= 0)"
skalberg@14516
   458
  by (import real REAL_POASQ)
skalberg@14516
   459
obua@17652
   460
lemma REAL_SUMSQ: "ALL (x::real) y::real. (x * x + y * y = 0) = (x = 0 & y = 0)"
skalberg@14516
   461
  by (import real REAL_SUMSQ)
skalberg@14516
   462
obua@17188
   463
lemma REAL_DIV_MUL2: "ALL (x::real) z::real.
obua@17652
   464
   x ~= 0 & z ~= 0 --> (ALL y::real. y / z = x * y / (x * z))"
obua@17188
   465
  by (import real REAL_DIV_MUL2)
obua@17188
   466
obua@17652
   467
lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b --> a <= (a + b) / 2"
skalberg@14516
   468
  by (import real REAL_MIDDLE1)
skalberg@14516
   469
obua@17652
   470
lemma REAL_MIDDLE2: "ALL (a::real) b::real. a <= b --> (a + b) / 2 <= b"
skalberg@14516
   471
  by (import real REAL_MIDDLE2)
skalberg@14516
   472
skalberg@14516
   473
lemma ABS_LT_MUL2: "ALL (w::real) (x::real) (y::real) z::real.
skalberg@14516
   474
   abs w < y & abs x < z --> abs (w * x) < y * z"
skalberg@14516
   475
  by (import real ABS_LT_MUL2)
skalberg@14516
   476
obua@17652
   477
lemma ABS_REFL: "ALL x::real. (abs x = x) = (0 <= x)"
skalberg@14516
   478
  by (import real ABS_REFL)
skalberg@14516
   479
skalberg@14516
   480
lemma ABS_BETWEEN: "ALL (x::real) (y::real) d::real.
obua@17652
   481
   (0 < d & x - d < y & y < x + d) = (abs (y - x) < d)"
skalberg@14516
   482
  by (import real ABS_BETWEEN)
skalberg@14516
   483
skalberg@14516
   484
lemma ABS_BOUND: "ALL (x::real) (y::real) d::real. abs (x - y) < d --> y < x + d"
skalberg@14516
   485
  by (import real ABS_BOUND)
skalberg@14516
   486
obua@17652
   487
lemma ABS_STILLNZ: "ALL (x::real) y::real. abs (x - y) < abs y --> x ~= 0"
skalberg@14516
   488
  by (import real ABS_STILLNZ)
skalberg@14516
   489
obua@17652
   490
lemma ABS_CASES: "ALL x::real. x = 0 | 0 < abs x"
skalberg@14516
   491
  by (import real ABS_CASES)
skalberg@14516
   492
skalberg@14516
   493
lemma ABS_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & abs (y - x) < z - x --> y < z"
skalberg@14516
   494
  by (import real ABS_BETWEEN1)
skalberg@14516
   495
obua@17652
   496
lemma ABS_SIGN: "ALL (x::real) y::real. abs (x - y) < y --> 0 < x"
skalberg@14516
   497
  by (import real ABS_SIGN)
skalberg@14516
   498
obua@17652
   499
lemma ABS_SIGN2: "ALL (x::real) y::real. abs (x - y) < - y --> x < 0"
skalberg@14516
   500
  by (import real ABS_SIGN2)
skalberg@14516
   501
skalberg@14516
   502
lemma ABS_CIRCLE: "ALL (x::real) (y::real) h::real.
skalberg@14516
   503
   abs h < abs y - abs x --> abs (x + h) < abs y"
skalberg@14516
   504
  by (import real ABS_CIRCLE)
skalberg@14516
   505
skalberg@14516
   506
lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real.
obua@17652
   507
   x0 < y0 & abs (x - x0) < (y0 - x0) / 2 & abs (y - y0) < (y0 - x0) / 2 -->
skalberg@14516
   508
   x < y"
skalberg@14516
   509
  by (import real ABS_BETWEEN2)
skalberg@14516
   510
obua@17652
   511
lemma POW_PLUS1: "ALL e>0. ALL n::nat. 1 + real n * e <= (1 + e) ^ n"
skalberg@14516
   512
  by (import real POW_PLUS1)
skalberg@14516
   513
obua@17652
   514
lemma POW_M1: "(All::(nat => bool) => bool)
obua@17652
   515
 (%n::nat.
obua@17652
   516
     (op =::real => real => bool)
obua@17652
   517
      ((abs::real => real)
obua@17652
   518
        ((op ^::real => nat => real) ((uminus::real => real) (1::real)) n))
obua@17652
   519
      (1::real))"
skalberg@14516
   520
  by (import real POW_M1)
skalberg@14516
   521
obua@17652
   522
lemma REAL_LE1_POW2: "(All::(real => bool) => bool)
obua@17652
   523
 (%x::real.
obua@17652
   524
     (op -->::bool => bool => bool)
obua@17652
   525
      ((op <=::real => real => bool) (1::real) x)
obua@17652
   526
      ((op <=::real => real => bool) (1::real)
obua@17652
   527
        ((op ^::real => nat => real) x
obua@17652
   528
          ((number_of::bin => nat)
obua@17652
   529
            ((op BIT::bin => bit => bin)
obua@17652
   530
              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
obua@17652
   531
              (bit.B0::bit))))))"
skalberg@14516
   532
  by (import real REAL_LE1_POW2)
skalberg@14516
   533
obua@17652
   534
lemma REAL_LT1_POW2: "(All::(real => bool) => bool)
obua@17652
   535
 (%x::real.
obua@17652
   536
     (op -->::bool => bool => bool)
obua@17652
   537
      ((op <::real => real => bool) (1::real) x)
obua@17652
   538
      ((op <::real => real => bool) (1::real)
obua@17652
   539
        ((op ^::real => nat => real) x
obua@17652
   540
          ((number_of::bin => nat)
obua@17652
   541
            ((op BIT::bin => bit => bin)
obua@17652
   542
              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
obua@17652
   543
              (bit.B0::bit))))))"
skalberg@14516
   544
  by (import real REAL_LT1_POW2)
skalberg@14516
   545
obua@17652
   546
lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n"
skalberg@14516
   547
  by (import real POW_POS_LT)
skalberg@14516
   548
obua@17652
   549
lemma POW_LT: "ALL (n::nat) (x::real) y::real. 0 <= x & x < y --> x ^ Suc n < y ^ Suc n"
skalberg@14516
   550
  by (import real POW_LT)
skalberg@14516
   551
obua@17652
   552
lemma POW_ZERO_EQ: "ALL (n::nat) x::real. (x ^ Suc n = 0) = (x = 0)"
skalberg@14516
   553
  by (import real POW_ZERO_EQ)
skalberg@14516
   554
obua@17652
   555
lemma REAL_POW_LT2: "ALL (n::nat) (x::real) y::real. n ~= 0 & 0 <= x & x < y --> x ^ n < y ^ n"
skalberg@14516
   556
  by (import real REAL_POW_LT2)
skalberg@14516
   557
obua@17652
   558
lemma REAL_POW_MONO_LT: "ALL (m::nat) (n::nat) x::real. 1 < x & m < n --> x ^ m < x ^ n"
obua@17188
   559
  by (import real REAL_POW_MONO_LT)
obua@17188
   560
skalberg@14516
   561
lemma REAL_SUP_SOMEPOS: "ALL P::real => bool.
obua@17652
   562
   (EX x::real. P x & 0 < x) & (EX z::real. ALL x::real. P x --> x < z) -->
skalberg@14516
   563
   (EX s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
skalberg@14516
   564
  by (import real REAL_SUP_SOMEPOS)
skalberg@14516
   565
skalberg@14516
   566
lemma SUP_LEMMA1: "ALL (P::real => bool) (s::real) d::real.
skalberg@14516
   567
   (ALL y::real. (EX x::real. P (x + d) & y < x) = (y < s)) -->
skalberg@14516
   568
   (ALL y::real. (EX x::real. P x & y < x) = (y < s + d))"
skalberg@14516
   569
  by (import real SUP_LEMMA1)
skalberg@14516
   570
obua@17652
   571
lemma SUP_LEMMA2: "ALL P::real => bool. Ex P --> (EX (d::real) x::real. P (x + d) & 0 < x)"
skalberg@14516
   572
  by (import real SUP_LEMMA2)
skalberg@14516
   573
skalberg@14516
   574
lemma SUP_LEMMA3: "ALL d::real.
skalberg@14516
   575
   (EX z::real. ALL x::real. (P::real => bool) x --> x < z) -->
skalberg@14516
   576
   (EX x::real. ALL xa::real. P (xa + d) --> xa < x)"
skalberg@14516
   577
  by (import real SUP_LEMMA3)
skalberg@14516
   578
skalberg@14516
   579
lemma REAL_SUP_EXISTS: "ALL P::real => bool.
skalberg@14516
   580
   Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
skalberg@14516
   581
   (EX x::real. ALL y::real. (EX x::real. P x & y < x) = (y < x))"
skalberg@14516
   582
  by (import real REAL_SUP_EXISTS)
skalberg@14516
   583
skalberg@14516
   584
constdefs
skalberg@14516
   585
  sup :: "(real => bool) => real" 
obua@17644
   586
  "sup ==
obua@17644
   587
%P::real => bool.
obua@17644
   588
   SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s)"
obua@17644
   589
obua@17644
   590
lemma sup: "ALL P::real => bool.
obua@17644
   591
   sup P = (SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
skalberg@14516
   592
  by (import real sup)
skalberg@14516
   593
obua@17644
   594
lemma REAL_SUP: "ALL P::real => bool.
obua@17644
   595
   Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
obua@17644
   596
   (ALL y::real. (EX x::real. P x & y < x) = (y < sup P))"
skalberg@14516
   597
  by (import real REAL_SUP)
skalberg@14516
   598
obua@17644
   599
lemma REAL_SUP_UBOUND: "ALL P::real => bool.
obua@17644
   600
   Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
obua@17644
   601
   (ALL y::real. P y --> y <= sup P)"
skalberg@14516
   602
  by (import real REAL_SUP_UBOUND)
skalberg@14516
   603
skalberg@14516
   604
lemma SETOK_LE_LT: "ALL P::real => bool.
skalberg@14516
   605
   (Ex P & (EX z::real. ALL x::real. P x --> x <= z)) =
skalberg@14516
   606
   (Ex P & (EX z::real. ALL x::real. P x --> x < z))"
skalberg@14516
   607
  by (import real SETOK_LE_LT)
skalberg@14516
   608
obua@17644
   609
lemma REAL_SUP_LE: "ALL P::real => bool.
obua@17644
   610
   Ex P & (EX z::real. ALL x::real. P x --> x <= z) -->
obua@17644
   611
   (ALL y::real. (EX x::real. P x & y < x) = (y < sup P))"
skalberg@14516
   612
  by (import real REAL_SUP_LE)
skalberg@14516
   613
obua@17644
   614
lemma REAL_SUP_UBOUND_LE: "ALL P::real => bool.
obua@17644
   615
   Ex P & (EX z::real. ALL x::real. P x --> x <= z) -->
obua@17644
   616
   (ALL y::real. P y --> y <= sup P)"
skalberg@14516
   617
  by (import real REAL_SUP_UBOUND_LE)
skalberg@14516
   618
obua@17652
   619
lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n::nat. real n * y <= x & x < real (Suc n) * y"
skalberg@14516
   620
  by (import real REAL_ARCH_LEAST)
skalberg@14516
   621
skalberg@14516
   622
consts
skalberg@14516
   623
  sumc :: "nat => nat => (nat => real) => real" 
skalberg@14516
   624
obua@17652
   625
specification (sumc) sumc: "(ALL (n::nat) f::nat => real. sumc n 0 f = 0) &
obua@17644
   626
(ALL (n::nat) (m::nat) f::nat => real.
obua@17644
   627
    sumc n (Suc m) f = sumc n m f + f (n + m))"
skalberg@14516
   628
  by (import real sumc)
skalberg@14516
   629
wenzelm@14694
   630
consts
skalberg@14516
   631
  sum :: "nat * nat => (nat => real) => real" 
wenzelm@14694
   632
wenzelm@14694
   633
defs
skalberg@15647
   634
  sum_def: "(op ==::(nat * nat => (nat => real) => real)
skalberg@15647
   635
        => (nat * nat => (nat => real) => real) => prop)
skalberg@15647
   636
 (real.sum::nat * nat => (nat => real) => real)
skalberg@15647
   637
 ((split::(nat => nat => (nat => real) => real)
skalberg@15647
   638
          => nat * nat => (nat => real) => real)
skalberg@15647
   639
   (sumc::nat => nat => (nat => real) => real))"
skalberg@14516
   640
obua@17644
   641
lemma SUM_DEF: "ALL (m::nat) (n::nat) f::nat => real. real.sum (m, n) f = sumc m n f"
skalberg@14516
   642
  by (import real SUM_DEF)
skalberg@14516
   643
obua@17644
   644
lemma sum: "ALL (x::nat => real) (xa::nat) xb::nat.
obua@17652
   645
   real.sum (xa, 0) x = 0 &
skalberg@14516
   646
   real.sum (xa, Suc xb) x = real.sum (xa, xb) x + x (xa + xb)"
skalberg@14516
   647
  by (import real sum)
skalberg@14516
   648
obua@17644
   649
lemma SUM_TWO: "ALL (f::nat => real) (n::nat) p::nat.
obua@17652
   650
   real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f"
skalberg@14516
   651
  by (import real SUM_TWO)
skalberg@14516
   652
obua@17644
   653
lemma SUM_DIFF: "ALL (f::nat => real) (m::nat) n::nat.
obua@17652
   654
   real.sum (m, n) f = real.sum (0, m + n) f - real.sum (0, m) f"
skalberg@14516
   655
  by (import real SUM_DIFF)
skalberg@14516
   656
obua@17644
   657
lemma ABS_SUM: "ALL (f::nat => real) (m::nat) n::nat.
obua@17644
   658
   abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))"
skalberg@14516
   659
  by (import real ABS_SUM)
skalberg@14516
   660
obua@17644
   661
lemma SUM_LE: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
obua@17644
   662
   (ALL r::nat. m <= r & r < n + m --> f r <= g r) -->
skalberg@14516
   663
   real.sum (m, n) f <= real.sum (m, n) g"
skalberg@14516
   664
  by (import real SUM_LE)
skalberg@14516
   665
obua@17644
   666
lemma SUM_EQ: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
obua@17644
   667
   (ALL r::nat. m <= r & r < n + m --> f r = g r) -->
skalberg@14516
   668
   real.sum (m, n) f = real.sum (m, n) g"
skalberg@14516
   669
  by (import real SUM_EQ)
skalberg@14516
   670
obua@17644
   671
lemma SUM_POS: "ALL f::nat => real.
obua@17652
   672
   (ALL n::nat. 0 <= f n) --> (ALL (m::nat) n::nat. 0 <= real.sum (m, n) f)"
skalberg@14516
   673
  by (import real SUM_POS)
skalberg@14516
   674
obua@17644
   675
lemma SUM_POS_GEN: "ALL (f::nat => real) m::nat.
obua@17652
   676
   (ALL n::nat. m <= n --> 0 <= f n) -->
obua@17652
   677
   (ALL n::nat. 0 <= real.sum (m, n) f)"
skalberg@14516
   678
  by (import real SUM_POS_GEN)
skalberg@14516
   679
obua@17644
   680
lemma SUM_ABS: "ALL (f::nat => real) (m::nat) x::nat.
obua@17644
   681
   abs (real.sum (m, x) (%m::nat. abs (f m))) =
obua@17644
   682
   real.sum (m, x) (%m::nat. abs (f m))"
skalberg@14516
   683
  by (import real SUM_ABS)
skalberg@14516
   684
obua@17644
   685
lemma SUM_ABS_LE: "ALL (f::nat => real) (m::nat) n::nat.
obua@17644
   686
   abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))"
skalberg@14516
   687
  by (import real SUM_ABS_LE)
skalberg@14516
   688
obua@17644
   689
lemma SUM_ZERO: "ALL (f::nat => real) N::nat.
obua@17652
   690
   (ALL n::nat. N <= n --> f n = 0) -->
obua@17652
   691
   (ALL (m::nat) n::nat. N <= m --> real.sum (m, n) f = 0)"
skalberg@14516
   692
  by (import real SUM_ZERO)
skalberg@14516
   693
obua@17644
   694
lemma SUM_ADD: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
obua@17644
   695
   real.sum (m, n) (%n::nat. f n + g n) =
obua@17644
   696
   real.sum (m, n) f + real.sum (m, n) g"
skalberg@14516
   697
  by (import real SUM_ADD)
skalberg@14516
   698
obua@17644
   699
lemma SUM_CMUL: "ALL (f::nat => real) (c::real) (m::nat) n::nat.
obua@17644
   700
   real.sum (m, n) (%n::nat. c * f n) = c * real.sum (m, n) f"
skalberg@14516
   701
  by (import real SUM_CMUL)
skalberg@14516
   702
obua@17644
   703
lemma SUM_NEG: "ALL (f::nat => real) (n::nat) d::nat.
obua@17644
   704
   real.sum (n, d) (%n::nat. - f n) = - real.sum (n, d) f"
skalberg@14516
   705
  by (import real SUM_NEG)
skalberg@14516
   706
obua@17644
   707
lemma SUM_SUB: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
obua@17644
   708
   real.sum (m, n) (%x::nat. f x - g x) =
obua@17644
   709
   real.sum (m, n) f - real.sum (m, n) g"
skalberg@14516
   710
  by (import real SUM_SUB)
skalberg@14516
   711
obua@17644
   712
lemma SUM_SUBST: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
obua@17644
   713
   (ALL p::nat. m <= p & p < m + n --> f p = g p) -->
skalberg@14516
   714
   real.sum (m, n) f = real.sum (m, n) g"
skalberg@14516
   715
  by (import real SUM_SUBST)
skalberg@14516
   716
obua@17644
   717
lemma SUM_NSUB: "ALL (n::nat) (f::nat => real) c::real.
obua@17652
   718
   real.sum (0, n) f - real n * c = real.sum (0, n) (%p::nat. f p - c)"
skalberg@14516
   719
  by (import real SUM_NSUB)
skalberg@14516
   720
obua@17644
   721
lemma SUM_BOUND: "ALL (f::nat => real) (k::real) (m::nat) n::nat.
obua@17644
   722
   (ALL p::nat. m <= p & p < m + n --> f p <= k) -->
skalberg@14516
   723
   real.sum (m, n) f <= real n * k"
skalberg@14516
   724
  by (import real SUM_BOUND)
skalberg@14516
   725
obua@17644
   726
lemma SUM_GROUP: "ALL (n::nat) (k::nat) f::nat => real.
obua@17652
   727
   real.sum (0, n) (%m::nat. real.sum (m * k, k) f) = real.sum (0, n * k) f"
skalberg@14516
   728
  by (import real SUM_GROUP)
skalberg@14516
   729
obua@17652
   730
lemma SUM_1: "ALL (f::nat => real) n::nat. real.sum (n, 1) f = f n"
skalberg@14516
   731
  by (import real SUM_1)
skalberg@14516
   732
obua@17652
   733
lemma SUM_2: "ALL (f::nat => real) n::nat. real.sum (n, 2) f = f n + f (n + 1)"
skalberg@14516
   734
  by (import real SUM_2)
skalberg@14516
   735
obua@17644
   736
lemma SUM_OFFSET: "ALL (f::nat => real) (n::nat) k::nat.
obua@17652
   737
   real.sum (0, n) (%m::nat. f (m + k)) =
obua@17652
   738
   real.sum (0, n + k) f - real.sum (0, k) f"
skalberg@14516
   739
  by (import real SUM_OFFSET)
skalberg@14516
   740
obua@17644
   741
lemma SUM_REINDEX: "ALL (f::nat => real) (m::nat) (k::nat) n::nat.
obua@17644
   742
   real.sum (m + k, n) f = real.sum (m, n) (%r::nat. f (r + k))"
skalberg@14516
   743
  by (import real SUM_REINDEX)
skalberg@14516
   744
obua@17652
   745
lemma SUM_0: "ALL (m::nat) n::nat. real.sum (m, n) (%r::nat. 0) = 0"
skalberg@14516
   746
  by (import real SUM_0)
skalberg@14516
   747
wenzelm@14847
   748
lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool)
wenzelm@14847
   749
 (%n::nat.
wenzelm@14847
   750
     (All::((nat => nat) => bool) => bool)
wenzelm@14847
   751
      (%p::nat => nat.
wenzelm@14847
   752
          (op -->::bool => bool => bool)
wenzelm@14847
   753
           ((All::(nat => bool) => bool)
wenzelm@14847
   754
             (%y::nat.
wenzelm@14847
   755
                 (op -->::bool => bool => bool)
wenzelm@14847
   756
                  ((op <::nat => nat => bool) y n)
wenzelm@14847
   757
                  ((Ex1::(nat => bool) => bool)
wenzelm@14847
   758
                    (%x::nat.
wenzelm@14847
   759
                        (op &::bool => bool => bool)
wenzelm@14847
   760
                         ((op <::nat => nat => bool) x n)
wenzelm@14847
   761
                         ((op =::nat => nat => bool) (p x) y)))))
wenzelm@14847
   762
           ((All::((nat => real) => bool) => bool)
wenzelm@14847
   763
             (%f::nat => real.
wenzelm@14847
   764
                 (op =::real => real => bool)
wenzelm@14847
   765
                  ((real.sum::nat * nat => (nat => real) => real)
wenzelm@14847
   766
                    ((Pair::nat => nat => nat * nat) (0::nat) n)
wenzelm@14847
   767
                    (%n::nat. f (p n)))
wenzelm@14847
   768
                  ((real.sum::nat * nat => (nat => real) => real)
wenzelm@14847
   769
                    ((Pair::nat => nat => nat * nat) (0::nat) n) f)))))"
skalberg@14516
   770
  by (import real SUM_PERMUTE_0)
skalberg@14516
   771
obua@17644
   772
lemma SUM_CANCEL: "ALL (f::nat => real) (n::nat) d::nat.
obua@17644
   773
   real.sum (n, d) (%n::nat. f (Suc n) - f n) = f (n + d) - f n"
skalberg@14516
   774
  by (import real SUM_CANCEL)
skalberg@14516
   775
obua@17652
   776
lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x = xa / xb) = (x * xb = xa)"
skalberg@14516
   777
  by (import real REAL_EQ_RDIV_EQ)
skalberg@14516
   778
obua@17652
   779
lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x / xb = xa) = (x = xa * xb)"
skalberg@14516
   780
  by (import real REAL_EQ_LDIV_EQ)
skalberg@14516
   781
skalberg@14516
   782
;end_setup
skalberg@14516
   783
skalberg@14516
   784
;setup_theory topology
skalberg@14516
   785
skalberg@14516
   786
constdefs
obua@17652
   787
  re_Union :: "(('a => bool) => bool) => 'a => bool" 
obua@17644
   788
  "re_Union ==
obua@17644
   789
%(P::('a::type => bool) => bool) x::'a::type.
obua@17644
   790
   EX s::'a::type => bool. P s & s x"
obua@17644
   791
obua@17644
   792
lemma re_Union: "ALL P::('a::type => bool) => bool.
obua@17644
   793
   re_Union P = (%x::'a::type. EX s::'a::type => bool. P s & s x)"
skalberg@14516
   794
  by (import topology re_Union)
skalberg@14516
   795
skalberg@14516
   796
constdefs
obua@17652
   797
  re_union :: "('a => bool) => ('a => bool) => 'a => bool" 
obua@17644
   798
  "re_union ==
obua@17644
   799
%(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x | Q x"
obua@17644
   800
obua@17644
   801
lemma re_union: "ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
   802
   re_union P Q = (%x::'a::type. P x | Q x)"
skalberg@14516
   803
  by (import topology re_union)
skalberg@14516
   804
skalberg@14516
   805
constdefs
obua@17652
   806
  re_intersect :: "('a => bool) => ('a => bool) => 'a => bool" 
obua@17644
   807
  "re_intersect ==
obua@17644
   808
%(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x & Q x"
obua@17644
   809
obua@17644
   810
lemma re_intersect: "ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
   811
   re_intersect P Q = (%x::'a::type. P x & Q x)"
skalberg@14516
   812
  by (import topology re_intersect)
skalberg@14516
   813
skalberg@14516
   814
constdefs
obua@17652
   815
  re_null :: "'a => bool" 
obua@17644
   816
  "re_null == %x::'a::type. False"
obua@17644
   817
obua@17644
   818
lemma re_null: "re_null = (%x::'a::type. False)"
skalberg@14516
   819
  by (import topology re_null)
skalberg@14516
   820
skalberg@14516
   821
constdefs
obua@17652
   822
  re_universe :: "'a => bool" 
obua@17644
   823
  "re_universe == %x::'a::type. True"
obua@17644
   824
obua@17644
   825
lemma re_universe: "re_universe = (%x::'a::type. True)"
skalberg@14516
   826
  by (import topology re_universe)
skalberg@14516
   827
skalberg@14516
   828
constdefs
obua@17652
   829
  re_subset :: "('a => bool) => ('a => bool) => bool" 
obua@17644
   830
  "re_subset ==
obua@17644
   831
%(P::'a::type => bool) Q::'a::type => bool. ALL x::'a::type. P x --> Q x"
obua@17644
   832
obua@17644
   833
lemma re_subset: "ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
   834
   re_subset P Q = (ALL x::'a::type. P x --> Q x)"
skalberg@14516
   835
  by (import topology re_subset)
skalberg@14516
   836
skalberg@14516
   837
constdefs
obua@17652
   838
  re_compl :: "('a => bool) => 'a => bool" 
obua@17644
   839
  "re_compl == %(P::'a::type => bool) x::'a::type. ~ P x"
obua@17644
   840
obua@17644
   841
lemma re_compl: "ALL P::'a::type => bool. re_compl P = (%x::'a::type. ~ P x)"
skalberg@14516
   842
  by (import topology re_compl)
skalberg@14516
   843
obua@17644
   844
lemma SUBSET_REFL: "ALL P::'a::type => bool. re_subset P P"
skalberg@14516
   845
  by (import topology SUBSET_REFL)
skalberg@14516
   846
obua@17644
   847
lemma COMPL_MEM: "ALL (P::'a::type => bool) x::'a::type. P x = (~ re_compl P x)"
skalberg@14516
   848
  by (import topology COMPL_MEM)
skalberg@14516
   849
obua@17644
   850
lemma SUBSET_ANTISYM: "ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
   851
   (re_subset P Q & re_subset Q P) = (P = Q)"
skalberg@14516
   852
  by (import topology SUBSET_ANTISYM)
skalberg@14516
   853
obua@17644
   854
lemma SUBSET_TRANS: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
obua@17644
   855
   re_subset P Q & re_subset Q R --> re_subset P R"
skalberg@14516
   856
  by (import topology SUBSET_TRANS)
skalberg@14516
   857
skalberg@14516
   858
constdefs
obua@17652
   859
  istopology :: "(('a => bool) => bool) => bool" 
skalberg@14516
   860
  "istopology ==
obua@17644
   861
%L::('a::type => bool) => bool.
obua@17644
   862
   L re_null &
obua@17644
   863
   L re_universe &
obua@17644
   864
   (ALL (a::'a::type => bool) b::'a::type => bool.
obua@17644
   865
       L a & L b --> L (re_intersect a b)) &
obua@17644
   866
   (ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P))"
obua@17644
   867
obua@17644
   868
lemma istopology: "ALL L::('a::type => bool) => bool.
skalberg@14516
   869
   istopology L =
skalberg@14516
   870
   (L re_null &
skalberg@14516
   871
    L re_universe &
obua@17644
   872
    (ALL (a::'a::type => bool) b::'a::type => bool.
obua@17644
   873
        L a & L b --> L (re_intersect a b)) &
obua@17644
   874
    (ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P)))"
skalberg@14516
   875
  by (import topology istopology)
skalberg@14516
   876
obua@17644
   877
typedef (open) ('a) topology = "(Collect::((('a::type => bool) => bool) => bool)
obua@17644
   878
          => (('a::type => bool) => bool) set)
obua@17644
   879
 (istopology::(('a::type => bool) => bool) => bool)" 
skalberg@14516
   880
  by (rule typedef_helper,import topology topology_TY_DEF)
skalberg@14516
   881
skalberg@14516
   882
lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology]
skalberg@14516
   883
skalberg@14516
   884
consts
obua@17652
   885
  topology :: "(('a => bool) => bool) => 'a topology" 
obua@17652
   886
  "open" :: "'a topology => ('a => bool) => bool" 
obua@17644
   887
obua@17644
   888
specification ("open" topology) topology_tybij: "(ALL a::'a::type topology. topology (open a) = a) &
obua@17644
   889
(ALL r::('a::type => bool) => bool. istopology r = (open (topology r) = r))"
skalberg@14516
   890
  by (import topology topology_tybij)
skalberg@14516
   891
obua@17644
   892
lemma TOPOLOGY: "ALL L::'a::type topology.
skalberg@14516
   893
   open L re_null &
skalberg@14516
   894
   open L re_universe &
obua@17644
   895
   (ALL (a::'a::type => bool) b::'a::type => bool.
obua@17644
   896
       open L a & open L b --> open L (re_intersect a b)) &
obua@17644
   897
   (ALL P::('a::type => bool) => bool.
obua@17644
   898
       re_subset P (open L) --> open L (re_Union P))"
skalberg@14516
   899
  by (import topology TOPOLOGY)
skalberg@14516
   900
obua@17644
   901
lemma TOPOLOGY_UNION: "ALL (x::'a::type topology) xa::('a::type => bool) => bool.
obua@17644
   902
   re_subset xa (open x) --> open x (re_Union xa)"
skalberg@14516
   903
  by (import topology TOPOLOGY_UNION)
skalberg@14516
   904
skalberg@14516
   905
constdefs
obua@17652
   906
  neigh :: "'a topology => ('a => bool) * 'a => bool" 
obua@17644
   907
  "neigh ==
obua@17644
   908
%(top::'a::type topology) (N::'a::type => bool, x::'a::type).
obua@17644
   909
   EX P::'a::type => bool. open top P & re_subset P N & P x"
obua@17644
   910
obua@17644
   911
lemma neigh: "ALL (top::'a::type topology) (N::'a::type => bool) x::'a::type.
obua@17644
   912
   neigh top (N, x) =
obua@17644
   913
   (EX P::'a::type => bool. open top P & re_subset P N & P x)"
skalberg@14516
   914
  by (import topology neigh)
skalberg@14516
   915
obua@17644
   916
lemma OPEN_OWN_NEIGH: "ALL (S'::'a::type => bool) (top::'a::type topology) x::'a::type.
obua@17644
   917
   open top S' & S' x --> neigh top (S', x)"
skalberg@14516
   918
  by (import topology OPEN_OWN_NEIGH)
skalberg@14516
   919
obua@17644
   920
lemma OPEN_UNOPEN: "ALL (S'::'a::type => bool) top::'a::type topology.
obua@17644
   921
   open top S' =
obua@17644
   922
   (re_Union (%P::'a::type => bool. open top P & re_subset P S') = S')"
skalberg@14516
   923
  by (import topology OPEN_UNOPEN)
skalberg@14516
   924
obua@17644
   925
lemma OPEN_SUBOPEN: "ALL (S'::'a::type => bool) top::'a::type topology.
obua@17644
   926
   open top S' =
obua@17644
   927
   (ALL x::'a::type.
obua@17644
   928
       S' x --> (EX P::'a::type => bool. P x & open top P & re_subset P S'))"
skalberg@14516
   929
  by (import topology OPEN_SUBOPEN)
skalberg@14516
   930
obua@17644
   931
lemma OPEN_NEIGH: "ALL (S'::'a::type => bool) top::'a::type topology.
obua@17644
   932
   open top S' =
obua@17644
   933
   (ALL x::'a::type.
obua@17644
   934
       S' x --> (EX N::'a::type => bool. neigh top (N, x) & re_subset N S'))"
skalberg@14516
   935
  by (import topology OPEN_NEIGH)
skalberg@14516
   936
skalberg@14516
   937
constdefs
obua@17652
   938
  closed :: "'a topology => ('a => bool) => bool" 
obua@17644
   939
  "closed == %(L::'a::type topology) S'::'a::type => bool. open L (re_compl S')"
obua@17644
   940
obua@17644
   941
lemma closed: "ALL (L::'a::type topology) S'::'a::type => bool.
obua@17644
   942
   closed L S' = open L (re_compl S')"
skalberg@14516
   943
  by (import topology closed)
skalberg@14516
   944
skalberg@14516
   945
constdefs
obua@17652
   946
  limpt :: "'a topology => 'a => ('a => bool) => bool" 
obua@17644
   947
  "limpt ==
obua@17644
   948
%(top::'a::type topology) (x::'a::type) S'::'a::type => bool.
obua@17644
   949
   ALL N::'a::type => bool.
obua@17644
   950
      neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y)"
obua@17644
   951
obua@17644
   952
lemma limpt: "ALL (top::'a::type topology) (x::'a::type) S'::'a::type => bool.
skalberg@14516
   953
   limpt top x S' =
obua@17644
   954
   (ALL N::'a::type => bool.
obua@17644
   955
       neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y))"
skalberg@14516
   956
  by (import topology limpt)
skalberg@14516
   957
obua@17644
   958
lemma CLOSED_LIMPT: "ALL (top::'a::type topology) S'::'a::type => bool.
obua@17644
   959
   closed top S' = (ALL x::'a::type. limpt top x S' --> S' x)"
skalberg@14516
   960
  by (import topology CLOSED_LIMPT)
skalberg@14516
   961
skalberg@14516
   962
constdefs
obua@17652
   963
  ismet :: "('a * 'a => real) => bool" 
skalberg@14516
   964
  "ismet ==
obua@17644
   965
%m::'a::type * 'a::type => real.
obua@17652
   966
   (ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) &
obua@17644
   967
   (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   968
       m (y, z) <= m (x, y) + m (x, z))"
obua@17644
   969
obua@17644
   970
lemma ismet: "ALL m::'a::type * 'a::type => real.
skalberg@14516
   971
   ismet m =
obua@17652
   972
   ((ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) &
obua@17644
   973
    (ALL (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
   974
        m (y, z) <= m (x, y) + m (x, z)))"
skalberg@14516
   975
  by (import topology ismet)
skalberg@14516
   976
obua@17644
   977
typedef (open) ('a) metric = "(Collect::(('a::type * 'a::type => real) => bool)
obua@17644
   978
          => ('a::type * 'a::type => real) set)
obua@17644
   979
 (ismet::('a::type * 'a::type => real) => bool)" 
skalberg@14516
   980
  by (rule typedef_helper,import topology metric_TY_DEF)
skalberg@14516
   981
skalberg@14516
   982
lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric]
skalberg@14516
   983
skalberg@14516
   984
consts
obua@17652
   985
  metric :: "('a * 'a => real) => 'a metric" 
obua@17652
   986
  dist :: "'a metric => 'a * 'a => real" 
obua@17644
   987
obua@17644
   988
specification (dist metric) metric_tybij: "(ALL a::'a::type metric. metric (dist a) = a) &
obua@17644
   989
(ALL r::'a::type * 'a::type => real. ismet r = (dist (metric r) = r))"
skalberg@14516
   990
  by (import topology metric_tybij)
skalberg@14516
   991
obua@17644
   992
lemma METRIC_ISMET: "ALL m::'a::type metric. ismet (dist m)"
skalberg@14516
   993
  by (import topology METRIC_ISMET)
skalberg@14516
   994
obua@17644
   995
lemma METRIC_ZERO: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
obua@17652
   996
   (dist m (x, y) = 0) = (x = y)"
skalberg@14516
   997
  by (import topology METRIC_ZERO)
skalberg@14516
   998
obua@17652
   999
lemma METRIC_SAME: "ALL (m::'a::type metric) x::'a::type. dist m (x, x) = 0"
skalberg@14516
  1000
  by (import topology METRIC_SAME)
skalberg@14516
  1001
obua@17652
  1002
lemma METRIC_POS: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. 0 <= dist m (x, y)"
skalberg@14516
  1003
  by (import topology METRIC_POS)
skalberg@14516
  1004
obua@17644
  1005
lemma METRIC_SYM: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
obua@17644
  1006
   dist m (x, y) = dist m (y, x)"
skalberg@14516
  1007
  by (import topology METRIC_SYM)
skalberg@14516
  1008
obua@17644
  1009
lemma METRIC_TRIANGLE: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type.
obua@17644
  1010
   dist m (x, z) <= dist m (x, y) + dist m (y, z)"
skalberg@14516
  1011
  by (import topology METRIC_TRIANGLE)
skalberg@14516
  1012
obua@17644
  1013
lemma METRIC_NZ: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
obua@17652
  1014
   x ~= y --> 0 < dist m (x, y)"
skalberg@14516
  1015
  by (import topology METRIC_NZ)
skalberg@14516
  1016
skalberg@14516
  1017
constdefs
obua@17652
  1018
  mtop :: "'a metric => 'a topology" 
skalberg@14516
  1019
  "mtop ==
obua@17644
  1020
%m::'a::type metric.
obua@17644
  1021
   topology
obua@17644
  1022
    (%S'::'a::type => bool.
obua@17644
  1023
        ALL x::'a::type.
obua@17652
  1024
           S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
obua@17644
  1025
obua@17644
  1026
lemma mtop: "ALL m::'a::type metric.
skalberg@14516
  1027
   mtop m =
skalberg@14516
  1028
   topology
obua@17644
  1029
    (%S'::'a::type => bool.
obua@17644
  1030
        ALL x::'a::type.
obua@17652
  1031
           S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
skalberg@14516
  1032
  by (import topology mtop)
skalberg@14516
  1033
obua@17644
  1034
lemma mtop_istopology: "ALL m::'a::type metric.
skalberg@14516
  1035
   istopology
obua@17644
  1036
    (%S'::'a::type => bool.
obua@17644
  1037
        ALL x::'a::type.
obua@17652
  1038
           S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
skalberg@14516
  1039
  by (import topology mtop_istopology)
skalberg@14516
  1040
obua@17644
  1041
lemma MTOP_OPEN: "ALL (S'::'a::type => bool) x::'a::type metric.
skalberg@14516
  1042
   open (mtop x) S' =
obua@17644
  1043
   (ALL xa::'a::type.
obua@17652
  1044
       S' xa --> (EX e>0. ALL y::'a::type. dist x (xa, y) < e --> S' y))"
skalberg@14516
  1045
  by (import topology MTOP_OPEN)
skalberg@14516
  1046
skalberg@14516
  1047
constdefs
obua@17652
  1048
  B :: "'a metric => 'a * real => 'a => bool" 
obua@17644
  1049
  "B ==
obua@17644
  1050
%(m::'a::type metric) (x::'a::type, e::real) y::'a::type. dist m (x, y) < e"
obua@17644
  1051
obua@17644
  1052
lemma ball: "ALL (m::'a::type metric) (x::'a::type) e::real.
obua@17644
  1053
   B m (x, e) = (%y::'a::type. dist m (x, y) < e)"
skalberg@14516
  1054
  by (import topology ball)
skalberg@14516
  1055
obua@17644
  1056
lemma BALL_OPEN: "ALL (m::'a::type metric) (x::'a::type) e::real.
obua@17652
  1057
   0 < e --> open (mtop m) (B m (x, e))"
skalberg@14516
  1058
  by (import topology BALL_OPEN)
skalberg@14516
  1059
obua@17644
  1060
lemma BALL_NEIGH: "ALL (m::'a::type metric) (x::'a::type) e::real.
obua@17652
  1061
   0 < e --> neigh (mtop m) (B m (x, e), x)"
skalberg@14516
  1062
  by (import topology BALL_NEIGH)
skalberg@14516
  1063
obua@17644
  1064
lemma MTOP_LIMPT: "ALL (m::'a::type metric) (x::'a::type) S'::'a::type => bool.
obua@17644
  1065
   limpt (mtop m) x S' =
obua@17652
  1066
   (ALL e>0. EX y::'a::type. x ~= y & S' y & dist m (x, y) < e)"
skalberg@14516
  1067
  by (import topology MTOP_LIMPT)
skalberg@14516
  1068
obua@17644
  1069
lemma ISMET_R1: "ismet (%(x::real, y::real). abs (y - x))"
skalberg@14516
  1070
  by (import topology ISMET_R1)
skalberg@14516
  1071
skalberg@14516
  1072
constdefs
skalberg@14516
  1073
  mr1 :: "real metric" 
obua@17644
  1074
  "mr1 == metric (%(x::real, y::real). abs (y - x))"
obua@17644
  1075
obua@17644
  1076
lemma mr1: "mr1 = metric (%(x::real, y::real). abs (y - x))"
skalberg@14516
  1077
  by (import topology mr1)
skalberg@14516
  1078
obua@17644
  1079
lemma MR1_DEF: "ALL (x::real) y::real. dist mr1 (x, y) = abs (y - x)"
skalberg@14516
  1080
  by (import topology MR1_DEF)
skalberg@14516
  1081
obua@17644
  1082
lemma MR1_ADD: "ALL (x::real) d::real. dist mr1 (x, x + d) = abs d"
skalberg@14516
  1083
  by (import topology MR1_ADD)
skalberg@14516
  1084
obua@17644
  1085
lemma MR1_SUB: "ALL (x::real) d::real. dist mr1 (x, x - d) = abs d"
skalberg@14516
  1086
  by (import topology MR1_SUB)
skalberg@14516
  1087
obua@17652
  1088
lemma MR1_ADD_POS: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x + d) = d"
skalberg@14516
  1089
  by (import topology MR1_ADD_POS)
skalberg@14516
  1090
obua@17652
  1091
lemma MR1_SUB_LE: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x - d) = d"
skalberg@14516
  1092
  by (import topology MR1_SUB_LE)
skalberg@14516
  1093
obua@17652
  1094
lemma MR1_ADD_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x + d) = d"
skalberg@14516
  1095
  by (import topology MR1_ADD_LT)
skalberg@14516
  1096
obua@17652
  1097
lemma MR1_SUB_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x - d) = d"
skalberg@14516
  1098
  by (import topology MR1_SUB_LT)
skalberg@14516
  1099
obua@17644
  1100
lemma MR1_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & dist mr1 (x, y) < z - x --> y < z"
skalberg@14516
  1101
  by (import topology MR1_BETWEEN1)
skalberg@14516
  1102
obua@17644
  1103
lemma MR1_LIMPT: "ALL x::real. limpt (mtop mr1) x re_universe"
skalberg@14516
  1104
  by (import topology MR1_LIMPT)
skalberg@14516
  1105
skalberg@14516
  1106
;end_setup
skalberg@14516
  1107
skalberg@14516
  1108
;setup_theory nets
skalberg@14516
  1109
skalberg@14516
  1110
constdefs
obua@17652
  1111
  dorder :: "('a => 'a => bool) => bool" 
skalberg@14516
  1112
  "dorder ==
obua@17644
  1113
%g::'a::type => 'a::type => bool.
obua@17644
  1114
   ALL (x::'a::type) y::'a::type.
obua@17644
  1115
      g x x & g y y -->
obua@17644
  1116
      (EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y))"
obua@17644
  1117
obua@17644
  1118
lemma dorder: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1119
   dorder g =
obua@17644
  1120
   (ALL (x::'a::type) y::'a::type.
obua@17644
  1121
       g x x & g y y -->
obua@17644
  1122
       (EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y)))"
skalberg@14516
  1123
  by (import nets dorder)
skalberg@14516
  1124
skalberg@14516
  1125
constdefs
obua@17652
  1126
  tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool" 
skalberg@14516
  1127
  "tends ==
obua@17644
  1128
%(s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology,
obua@17644
  1129
   g::'b::type => 'b::type => bool).
obua@17644
  1130
   ALL N::'a::type => bool.
skalberg@14516
  1131
      neigh top (N, l) -->
obua@17644
  1132
      (EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m)))"
obua@17644
  1133
obua@17644
  1134
lemma tends: "ALL (s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology)
obua@17644
  1135
   g::'b::type => 'b::type => bool.
skalberg@14516
  1136
   tends s l (top, g) =
obua@17644
  1137
   (ALL N::'a::type => bool.
skalberg@14516
  1138
       neigh top (N, l) -->
obua@17644
  1139
       (EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m))))"
skalberg@14516
  1140
  by (import nets tends)
skalberg@14516
  1141
skalberg@14516
  1142
constdefs
obua@17652
  1143
  bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool" 
skalberg@14516
  1144
  "bounded ==
obua@17644
  1145
%(m::'a::type metric, g::'b::type => 'b::type => bool)
obua@17644
  1146
   f::'b::type => 'a::type.
obua@17644
  1147
   EX (k::real) (x::'a::type) N::'b::type.
obua@17644
  1148
      g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k)"
obua@17644
  1149
obua@17644
  1150
lemma bounded: "ALL (m::'a::type metric) (g::'b::type => 'b::type => bool)
obua@17644
  1151
   f::'b::type => 'a::type.
skalberg@14516
  1152
   bounded (m, g) f =
obua@17644
  1153
   (EX (k::real) (x::'a::type) N::'b::type.
obua@17644
  1154
       g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k))"
skalberg@14516
  1155
  by (import nets bounded)
skalberg@14516
  1156
skalberg@14516
  1157
constdefs
obua@17652
  1158
  tendsto :: "'a metric * 'a => 'a => 'a => bool" 
obua@17644
  1159
  "tendsto ==
obua@17644
  1160
%(m::'a::type metric, x::'a::type) (y::'a::type) z::'a::type.
obua@17652
  1161
   0 < dist m (x, y) & dist m (x, y) <= dist m (x, z)"
obua@17644
  1162
obua@17644
  1163
lemma tendsto: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type.
obua@17652
  1164
   tendsto (m, x) y z = (0 < dist m (x, y) & dist m (x, y) <= dist m (x, z))"
skalberg@14516
  1165
  by (import nets tendsto)
skalberg@14516
  1166
obua@17644
  1167
lemma DORDER_LEMMA: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1168
   dorder g -->
obua@17644
  1169
   (ALL (P::'a::type => bool) Q::'a::type => bool.
obua@17644
  1170
       (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m)) &
obua@17644
  1171
       (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> Q m)) -->
obua@17644
  1172
       (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m & Q m)))"
skalberg@14516
  1173
  by (import nets DORDER_LEMMA)
skalberg@14516
  1174
skalberg@14516
  1175
lemma DORDER_NGE: "dorder nat_ge"
skalberg@14516
  1176
  by (import nets DORDER_NGE)
skalberg@14516
  1177
obua@17644
  1178
lemma DORDER_TENDSTO: "ALL (m::'a::type metric) x::'a::type. dorder (tendsto (m, x))"
skalberg@14516
  1179
  by (import nets DORDER_TENDSTO)
skalberg@14516
  1180
obua@17644
  1181
lemma MTOP_TENDS: "ALL (d::'a::type metric) (g::'b::type => 'b::type => bool)
obua@17644
  1182
   (x::'b::type => 'a::type) x0::'a::type.
skalberg@14516
  1183
   tends x x0 (mtop d, g) =
obua@17652
  1184
   (ALL e>0.
obua@17644
  1185
       EX n::'b::type.
obua@17644
  1186
          g n n & (ALL m::'b::type. g m n --> dist d (x m, x0) < e))"
skalberg@14516
  1187
  by (import nets MTOP_TENDS)
skalberg@14516
  1188
obua@17644
  1189
lemma MTOP_TENDS_UNIQ: "ALL (g::'b::type => 'b::type => bool) d::'a::type metric.
skalberg@14516
  1190
   dorder g -->
obua@17644
  1191
   tends (x::'b::type => 'a::type) (x0::'a::type) (mtop d, g) &
obua@17644
  1192
   tends x (x1::'a::type) (mtop d, g) -->
skalberg@14516
  1193
   x0 = x1"
skalberg@14516
  1194
  by (import nets MTOP_TENDS_UNIQ)
skalberg@14516
  1195
obua@17644
  1196
lemma SEQ_TENDS: "ALL (d::'a::type metric) (x::nat => 'a::type) x0::'a::type.
skalberg@14516
  1197
   tends x x0 (mtop d, nat_ge) =
obua@17652
  1198
   (ALL xa>0. EX xb::nat. ALL xc::nat. xb <= xc --> dist d (x xc, x0) < xa)"
skalberg@14516
  1199
  by (import nets SEQ_TENDS)
skalberg@14516
  1200
obua@17644
  1201
lemma LIM_TENDS: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type)
obua@17644
  1202
   (x0::'a::type) y0::'b::type.
skalberg@14516
  1203
   limpt (mtop m1) x0 re_universe -->
skalberg@14516
  1204
   tends f y0 (mtop m2, tendsto (m1, x0)) =
obua@17652
  1205
   (ALL e>0.
obua@17652
  1206
       EX d>0.
obua@17644
  1207
          ALL x::'a::type.
obua@17652
  1208
             0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
skalberg@15647
  1209
             dist m2 (f x, y0) < e)"
skalberg@14516
  1210
  by (import nets LIM_TENDS)
skalberg@14516
  1211
obua@17644
  1212
lemma LIM_TENDS2: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type)
obua@17644
  1213
   (x0::'a::type) y0::'b::type.
skalberg@14516
  1214
   limpt (mtop m1) x0 re_universe -->
skalberg@14516
  1215
   tends f y0 (mtop m2, tendsto (m1, x0)) =
obua@17652
  1216
   (ALL e>0.
obua@17652
  1217
       EX d>0.
obua@17644
  1218
          ALL x::'a::type.
obua@17652
  1219
             0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
skalberg@15647
  1220
             dist m2 (f x, y0) < e)"
skalberg@14516
  1221
  by (import nets LIM_TENDS2)
skalberg@14516
  1222
obua@17644
  1223
lemma MR1_BOUNDED: "ALL (g::'a::type => 'a::type => bool) f::'a::type => real.
obua@17644
  1224
   bounded (mr1, g) f =
obua@17644
  1225
   (EX (k::real) N::'a::type.
obua@17644
  1226
       g N N & (ALL n::'a::type. g n N --> abs (f n) < k))"
skalberg@14516
  1227
  by (import nets MR1_BOUNDED)
skalberg@14516
  1228
obua@17644
  1229
lemma NET_NULL: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
obua@17652
  1230
   tends x x0 (mtop mr1, g) = tends (%n::'a::type. x n - x0) 0 (mtop mr1, g)"
skalberg@14516
  1231
  by (import nets NET_NULL)
skalberg@14516
  1232
obua@17644
  1233
lemma NET_CONV_BOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
obua@17644
  1234
   tends x x0 (mtop mr1, g) --> bounded (mr1, g) x"
skalberg@14516
  1235
  by (import nets NET_CONV_BOUNDED)
skalberg@14516
  1236
obua@17644
  1237
lemma NET_CONV_NZ: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
obua@17652
  1238
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
obua@17652
  1239
   (EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n ~= 0))"
skalberg@14516
  1240
  by (import nets NET_CONV_NZ)
skalberg@14516
  1241
obua@17644
  1242
lemma NET_CONV_IBOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
obua@17652
  1243
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
obua@17644
  1244
   bounded (mr1, g) (%n::'a::type. inverse (x n))"
skalberg@14516
  1245
  by (import nets NET_CONV_IBOUNDED)
skalberg@14516
  1246
obua@17644
  1247
lemma NET_NULL_ADD: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1248
   dorder g -->
obua@17644
  1249
   (ALL (x::'a::type => real) y::'a::type => real.
obua@17652
  1250
       tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) -->
obua@17652
  1251
       tends (%n::'a::type. x n + y n) 0 (mtop mr1, g))"
skalberg@14516
  1252
  by (import nets NET_NULL_ADD)
skalberg@14516
  1253
obua@17644
  1254
lemma NET_NULL_MUL: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1255
   dorder g -->
obua@17644
  1256
   (ALL (x::'a::type => real) y::'a::type => real.
obua@17652
  1257
       bounded (mr1, g) x & tends y 0 (mtop mr1, g) -->
obua@17652
  1258
       tends (%n::'a::type. x n * y n) 0 (mtop mr1, g))"
skalberg@14516
  1259
  by (import nets NET_NULL_MUL)
skalberg@14516
  1260
obua@17644
  1261
lemma NET_NULL_CMUL: "ALL (g::'a::type => 'a::type => bool) (k::real) x::'a::type => real.
obua@17652
  1262
   tends x 0 (mtop mr1, g) --> tends (%n::'a::type. k * x n) 0 (mtop mr1, g)"
skalberg@14516
  1263
  by (import nets NET_NULL_CMUL)
skalberg@14516
  1264
obua@17644
  1265
lemma NET_ADD: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1266
   dorder g -->
obua@17644
  1267
   (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
skalberg@14516
  1268
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
obua@17644
  1269
       tends (%n::'a::type. x n + y n) (x0 + y0) (mtop mr1, g))"
skalberg@14516
  1270
  by (import nets NET_ADD)
skalberg@14516
  1271
obua@17644
  1272
lemma NET_NEG: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1273
   dorder g -->
obua@17644
  1274
   (ALL (x::'a::type => real) x0::real.
obua@17644
  1275
       tends x x0 (mtop mr1, g) =
obua@17644
  1276
       tends (%n::'a::type. - x n) (- x0) (mtop mr1, g))"
skalberg@14516
  1277
  by (import nets NET_NEG)
skalberg@14516
  1278
obua@17644
  1279
lemma NET_SUB: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1280
   dorder g -->
obua@17644
  1281
   (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
skalberg@14516
  1282
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
obua@17644
  1283
       tends (%xa::'a::type. x xa - y xa) (x0 - y0) (mtop mr1, g))"
skalberg@14516
  1284
  by (import nets NET_SUB)
skalberg@14516
  1285
obua@17644
  1286
lemma NET_MUL: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1287
   dorder g -->
obua@17644
  1288
   (ALL (x::'a::type => real) (y::'a::type => real) (x0::real) y0::real.
skalberg@14516
  1289
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
obua@17644
  1290
       tends (%n::'a::type. x n * y n) (x0 * y0) (mtop mr1, g))"
skalberg@14516
  1291
  by (import nets NET_MUL)
skalberg@14516
  1292
obua@17644
  1293
lemma NET_INV: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1294
   dorder g -->
obua@17644
  1295
   (ALL (x::'a::type => real) x0::real.
obua@17652
  1296
       tends x x0 (mtop mr1, g) & x0 ~= 0 -->
obua@17644
  1297
       tends (%n::'a::type. inverse (x n)) (inverse x0) (mtop mr1, g))"
skalberg@14516
  1298
  by (import nets NET_INV)
skalberg@14516
  1299
obua@17644
  1300
lemma NET_DIV: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1301
   dorder g -->
obua@17644
  1302
   (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
obua@17652
  1303
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 -->
obua@17644
  1304
       tends (%xa::'a::type. x xa / y xa) (x0 / y0) (mtop mr1, g))"
skalberg@14516
  1305
  by (import nets NET_DIV)
skalberg@14516
  1306
obua@17644
  1307
lemma NET_ABS: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
obua@17644
  1308
   tends x x0 (mtop mr1, g) -->
obua@17644
  1309
   tends (%n::'a::type. abs (x n)) (abs x0) (mtop mr1, g)"
skalberg@14516
  1310
  by (import nets NET_ABS)
skalberg@14516
  1311
obua@17644
  1312
lemma NET_LE: "ALL g::'a::type => 'a::type => bool.
skalberg@14516
  1313
   dorder g -->
obua@17644
  1314
   (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
skalberg@14516
  1315
       tends x x0 (mtop mr1, g) &
skalberg@14516
  1316
       tends y y0 (mtop mr1, g) &
obua@17644
  1317
       (EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n <= y n)) -->
skalberg@14516
  1318
       x0 <= y0)"
skalberg@14516
  1319
  by (import nets NET_LE)
skalberg@14516
  1320
skalberg@14516
  1321
;end_setup
skalberg@14516
  1322
skalberg@14516
  1323
;setup_theory seq
skalberg@14516
  1324
wenzelm@14694
  1325
consts
obua@17694
  1326
  "hol4-->" :: "(nat => real) => real => bool" ("hol4-->")
wenzelm@14694
  1327
wenzelm@14694
  1328
defs
obua@17694
  1329
  "hol4-->_def": "hol4--> == %(x::nat => real) x0::real. tends x x0 (mtop mr1, nat_ge)"
obua@17694
  1330
obua@17694
  1331
lemma tends_num_real: "ALL (x::nat => real) x0::real. hol4--> x x0 = tends x x0 (mtop mr1, nat_ge)"
skalberg@14516
  1332
  by (import seq tends_num_real)
skalberg@14516
  1333
obua@17694
  1334
lemma SEQ: "ALL (x::nat => real) x0::real.
obua@17694
  1335
   hol4--> x x0 =
obua@17694
  1336
   (ALL e>0. EX N::nat. ALL n::nat. N <= n --> abs (x n - x0) < e)"
skalberg@14516
  1337
  by (import seq SEQ)
skalberg@14516
  1338
obua@17694
  1339
lemma SEQ_CONST: "ALL k::real. hol4--> (%x::nat. k) k"
skalberg@14516
  1340
  by (import seq SEQ_CONST)
skalberg@14516
  1341
obua@17694
  1342
lemma SEQ_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1343
   hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n + y n) (x0 + y0)"
skalberg@14516
  1344
  by (import seq SEQ_ADD)
skalberg@14516
  1345
obua@17694
  1346
lemma SEQ_MUL: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1347
   hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n * y n) (x0 * y0)"
skalberg@14516
  1348
  by (import seq SEQ_MUL)
skalberg@14516
  1349
obua@17694
  1350
lemma SEQ_NEG: "ALL (x::nat => real) x0::real.
obua@17694
  1351
   hol4--> x x0 = hol4--> (%n::nat. - x n) (- x0)"
skalberg@14516
  1352
  by (import seq SEQ_NEG)
skalberg@14516
  1353
obua@17694
  1354
lemma SEQ_INV: "ALL (x::nat => real) x0::real.
obua@17694
  1355
   hol4--> x x0 & x0 ~= 0 --> hol4--> (%n::nat. inverse (x n)) (inverse x0)"
skalberg@14516
  1356
  by (import seq SEQ_INV)
skalberg@14516
  1357
obua@17694
  1358
lemma SEQ_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1359
   hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n - y n) (x0 - y0)"
skalberg@14516
  1360
  by (import seq SEQ_SUB)
skalberg@14516
  1361
obua@17694
  1362
lemma SEQ_DIV: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1363
   hol4--> x x0 & hol4--> y y0 & y0 ~= 0 -->
obua@17694
  1364
   hol4--> (%n::nat. x n / y n) (x0 / y0)"
skalberg@14516
  1365
  by (import seq SEQ_DIV)
skalberg@14516
  1366
obua@17694
  1367
lemma SEQ_UNIQ: "ALL (x::nat => real) (x1::real) x2::real.
obua@17694
  1368
   hol4--> x x1 & hol4--> x x2 --> x1 = x2"
skalberg@14516
  1369
  by (import seq SEQ_UNIQ)
skalberg@14516
  1370
skalberg@14516
  1371
constdefs
skalberg@14516
  1372
  convergent :: "(nat => real) => bool" 
obua@17694
  1373
  "convergent == %f::nat => real. Ex (hol4--> f)"
obua@17694
  1374
obua@17694
  1375
lemma convergent: "ALL f::nat => real. convergent f = Ex (hol4--> f)"
skalberg@14516
  1376
  by (import seq convergent)
skalberg@14516
  1377
skalberg@14516
  1378
constdefs
skalberg@14516
  1379
  cauchy :: "(nat => real) => bool" 
obua@17694
  1380
  "cauchy ==
obua@17694
  1381
%f::nat => real.
obua@17694
  1382
   ALL e>0.
obua@17694
  1383
      EX N::nat.
obua@17694
  1384
         ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e"
obua@17694
  1385
obua@17694
  1386
lemma cauchy: "ALL f::nat => real.
obua@17694
  1387
   cauchy f =
obua@17694
  1388
   (ALL e>0.
obua@17694
  1389
       EX N::nat.
obua@17694
  1390
          ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e)"
skalberg@14516
  1391
  by (import seq cauchy)
skalberg@14516
  1392
skalberg@14516
  1393
constdefs
skalberg@14516
  1394
  lim :: "(nat => real) => real" 
obua@17694
  1395
  "lim == %f::nat => real. Eps (hol4--> f)"
obua@17694
  1396
obua@17694
  1397
lemma lim: "ALL f::nat => real. lim f = Eps (hol4--> f)"
skalberg@14516
  1398
  by (import seq lim)
skalberg@14516
  1399
obua@17694
  1400
lemma SEQ_LIM: "ALL f::nat => real. convergent f = hol4--> f (lim f)"
skalberg@14516
  1401
  by (import seq SEQ_LIM)
skalberg@14516
  1402
skalberg@14516
  1403
constdefs
skalberg@14516
  1404
  subseq :: "(nat => nat) => bool" 
obua@17694
  1405
  "subseq == %f::nat => nat. ALL (m::nat) n::nat. m < n --> f m < f n"
obua@17694
  1406
obua@17694
  1407
lemma subseq: "ALL f::nat => nat. subseq f = (ALL (m::nat) n::nat. m < n --> f m < f n)"
skalberg@14516
  1408
  by (import seq subseq)
skalberg@14516
  1409
obua@17644
  1410
lemma SUBSEQ_SUC: "ALL f::nat => nat. subseq f = (ALL n::nat. f n < f (Suc n))"
skalberg@14516
  1411
  by (import seq SUBSEQ_SUC)
skalberg@14516
  1412
wenzelm@14694
  1413
consts
skalberg@14516
  1414
  mono :: "(nat => real) => bool" 
wenzelm@14694
  1415
wenzelm@14694
  1416
defs
obua@17694
  1417
  mono_def: "seq.mono ==
obua@17694
  1418
%f::nat => real.
obua@17694
  1419
   (ALL (m::nat) n::nat. m <= n --> f m <= f n) |
obua@17694
  1420
   (ALL (m::nat) n::nat. m <= n --> f n <= f m)"
obua@17694
  1421
obua@17694
  1422
lemma mono: "ALL f::nat => real.
obua@17694
  1423
   seq.mono f =
obua@17694
  1424
   ((ALL (m::nat) n::nat. m <= n --> f m <= f n) |
obua@17694
  1425
    (ALL (m::nat) n::nat. m <= n --> f n <= f m))"
skalberg@14516
  1426
  by (import seq mono)
skalberg@14516
  1427
obua@17644
  1428
lemma MONO_SUC: "ALL f::nat => real.
obua@17644
  1429
   seq.mono f =
obua@17644
  1430
   ((ALL x::nat. f x <= f (Suc x)) | (ALL n::nat. f (Suc n) <= f n))"
skalberg@14516
  1431
  by (import seq MONO_SUC)
skalberg@14516
  1432
wenzelm@14847
  1433
lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool)
wenzelm@14847
  1434
 (%s::nat => real.
wenzelm@14847
  1435
     (All::(nat => bool) => bool)
wenzelm@14847
  1436
      (%N::nat.
wenzelm@14847
  1437
          (Ex::(real => bool) => bool)
wenzelm@14847
  1438
           (%k::real.
wenzelm@14847
  1439
               (All::(nat => bool) => bool)
wenzelm@14847
  1440
                (%n::nat.
wenzelm@14847
  1441
                    (op -->::bool => bool => bool)
wenzelm@14847
  1442
                     ((op <::nat => nat => bool) n N)
wenzelm@14847
  1443
                     ((op <::real => real => bool)
wenzelm@14847
  1444
                       ((abs::real => real) (s n)) k)))))"
skalberg@14516
  1445
  by (import seq MAX_LEMMA)
skalberg@14516
  1446
obua@17644
  1447
lemma SEQ_BOUNDED: "ALL s::nat => real.
obua@17644
  1448
   bounded (mr1, nat_ge) s = (EX k::real. ALL n::nat. abs (s n) < k)"
skalberg@14516
  1449
  by (import seq SEQ_BOUNDED)
skalberg@14516
  1450
obua@17694
  1451
lemma SEQ_BOUNDED_2: "ALL (f::nat => real) (k::real) k'::real.
obua@17694
  1452
   (ALL n::nat. k <= f n & f n <= k') --> bounded (mr1, nat_ge) f"
skalberg@14516
  1453
  by (import seq SEQ_BOUNDED_2)
skalberg@14516
  1454
obua@17694
  1455
lemma SEQ_CBOUNDED: "ALL f::nat => real. cauchy f --> bounded (mr1, nat_ge) f"
skalberg@14516
  1456
  by (import seq SEQ_CBOUNDED)
skalberg@14516
  1457
obua@17694
  1458
lemma SEQ_ICONV: "ALL f::nat => real.
obua@17694
  1459
   bounded (mr1, nat_ge) f &
obua@17694
  1460
   (ALL (m::nat) n::nat. n <= m --> f n <= f m) -->
obua@17694
  1461
   convergent f"
skalberg@14516
  1462
  by (import seq SEQ_ICONV)
skalberg@14516
  1463
obua@17644
  1464
lemma SEQ_NEG_CONV: "ALL f::nat => real. convergent f = convergent (%n::nat. - f n)"
skalberg@14516
  1465
  by (import seq SEQ_NEG_CONV)
skalberg@14516
  1466
obua@17644
  1467
lemma SEQ_NEG_BOUNDED: "ALL f::nat => real.
obua@17644
  1468
   bounded (mr1, nat_ge) (%n::nat. - f n) = bounded (mr1, nat_ge) f"
skalberg@14516
  1469
  by (import seq SEQ_NEG_BOUNDED)
skalberg@14516
  1470
obua@17694
  1471
lemma SEQ_BCONV: "ALL f::nat => real. bounded (mr1, nat_ge) f & seq.mono f --> convergent f"
skalberg@14516
  1472
  by (import seq SEQ_BCONV)
skalberg@14516
  1473
obua@17644
  1474
lemma SEQ_MONOSUB: "ALL s::nat => real. EX f::nat => nat. subseq f & seq.mono (%n::nat. s (f n))"
skalberg@14516
  1475
  by (import seq SEQ_MONOSUB)
skalberg@14516
  1476
obua@17694
  1477
lemma SEQ_SBOUNDED: "ALL (s::nat => real) f::nat => nat.
obua@17694
  1478
   bounded (mr1, nat_ge) s --> bounded (mr1, nat_ge) (%n::nat. s (f n))"
skalberg@14516
  1479
  by (import seq SEQ_SBOUNDED)
skalberg@14516
  1480
obua@17694
  1481
lemma SEQ_SUBLE: "ALL f::nat => nat. subseq f --> (ALL n::nat. n <= f n)"
skalberg@14516
  1482
  by (import seq SEQ_SUBLE)
skalberg@14516
  1483
obua@17694
  1484
lemma SEQ_DIRECT: "ALL f::nat => nat.
obua@17694
  1485
   subseq f --> (ALL (N1::nat) N2::nat. EX x::nat. N1 <= x & N2 <= f x)"
skalberg@14516
  1486
  by (import seq SEQ_DIRECT)
skalberg@14516
  1487
obua@17644
  1488
lemma SEQ_CAUCHY: "ALL f::nat => real. cauchy f = convergent f"
skalberg@14516
  1489
  by (import seq SEQ_CAUCHY)
skalberg@14516
  1490
obua@17694
  1491
lemma SEQ_LE: "ALL (f::nat => real) (g::nat => real) (l::real) m::real.
obua@17694
  1492
   hol4--> f l &
obua@17694
  1493
   hol4--> g m & (EX x::nat. ALL xa::nat. x <= xa --> f xa <= g xa) -->
obua@17694
  1494
   l <= m"
skalberg@14516
  1495
  by (import seq SEQ_LE)
skalberg@14516
  1496
obua@17694
  1497
lemma SEQ_SUC: "ALL (f::nat => real) l::real. hol4--> f l = hol4--> (%n::nat. f (Suc n)) l"
skalberg@14516
  1498
  by (import seq SEQ_SUC)
skalberg@14516
  1499
obua@17694
  1500
lemma SEQ_ABS: "ALL f::nat => real. hol4--> (%n::nat. abs (f n)) 0 = hol4--> f 0"
skalberg@14516
  1501
  by (import seq SEQ_ABS)
skalberg@14516
  1502
obua@17694
  1503
lemma SEQ_ABS_IMP: "ALL (f::nat => real) l::real.
obua@17694
  1504
   hol4--> f l --> hol4--> (%n::nat. abs (f n)) (abs l)"
skalberg@14516
  1505
  by (import seq SEQ_ABS_IMP)
skalberg@14516
  1506
obua@17694
  1507
lemma SEQ_INV0: "ALL f::nat => real.
obua@17694
  1508
   (ALL y::real. EX N::nat. ALL n::nat. N <= n --> y < f n) -->
obua@17694
  1509
   hol4--> (%n::nat. inverse (f n)) 0"
skalberg@14516
  1510
  by (import seq SEQ_INV0)
skalberg@14516
  1511
obua@17694
  1512
lemma SEQ_POWER_ABS: "ALL c::real. abs c < 1 --> hol4--> (op ^ (abs c)) 0"
skalberg@14516
  1513
  by (import seq SEQ_POWER_ABS)
skalberg@14516
  1514
obua@17694
  1515
lemma SEQ_POWER: "ALL c::real. abs c < 1 --> hol4--> (op ^ c) 0"
skalberg@14516
  1516
  by (import seq SEQ_POWER)
skalberg@14516
  1517
obua@17694
  1518
lemma NEST_LEMMA: "ALL (f::nat => real) g::nat => real.
obua@17694
  1519
   (ALL n::nat. f n <= f (Suc n)) &
obua@17694
  1520
   (ALL n::nat. g (Suc n) <= g n) & (ALL n::nat. f n <= g n) -->
obua@17694
  1521
   (EX (l::real) m::real.
obua@17694
  1522
       l <= m &
obua@17694
  1523
       ((ALL n::nat. f n <= l) & hol4--> f l) &
obua@17694
  1524
       (ALL n::nat. m <= g n) & hol4--> g m)"
skalberg@14516
  1525
  by (import seq NEST_LEMMA)
skalberg@14516
  1526
obua@17694
  1527
lemma NEST_LEMMA_UNIQ: "ALL (f::nat => real) g::nat => real.
obua@17694
  1528
   (ALL n::nat. f n <= f (Suc n)) &
obua@17694
  1529
   (ALL n::nat. g (Suc n) <= g n) &
obua@17694
  1530
   (ALL n::nat. f n <= g n) & hol4--> (%n::nat. f n - g n) 0 -->
obua@17694
  1531
   (EX x::real.
obua@17694
  1532
       ((ALL n::nat. f n <= x) & hol4--> f x) &
obua@17694
  1533
       (ALL n::nat. x <= g n) & hol4--> g x)"
skalberg@14516
  1534
  by (import seq NEST_LEMMA_UNIQ)
skalberg@14516
  1535
obua@17694
  1536
lemma BOLZANO_LEMMA: "ALL P::real * real => bool.
obua@17694
  1537
   (ALL (a::real) (b::real) c::real.
obua@17694
  1538
       a <= b & b <= c & P (a, b) & P (b, c) --> P (a, c)) &
obua@17694
  1539
   (ALL x::real.
obua@17694
  1540
       EX d>0.
obua@17694
  1541
          ALL (a::real) b::real.
obua@17694
  1542
             a <= x & x <= b & b - a < d --> P (a, b)) -->
obua@17694
  1543
   (ALL (a::real) b::real. a <= b --> P (a, b))"
skalberg@14516
  1544
  by (import seq BOLZANO_LEMMA)
skalberg@14516
  1545
skalberg@14516
  1546
constdefs
skalberg@14516
  1547
  sums :: "(nat => real) => real => bool" 
obua@17694
  1548
  "sums == %f::nat => real. hol4--> (%n::nat. real.sum (0, n) f)"
obua@17694
  1549
obua@17694
  1550
lemma sums: "ALL (f::nat => real) s::real.
obua@17694
  1551
   sums f s = hol4--> (%n::nat. real.sum (0, n) f) s"
skalberg@14516
  1552
  by (import seq sums)
skalberg@14516
  1553
skalberg@14516
  1554
constdefs
skalberg@14516
  1555
  summable :: "(nat => real) => bool" 
obua@17644
  1556
  "summable == %f::nat => real. Ex (sums f)"
obua@17644
  1557
obua@17644
  1558
lemma summable: "ALL f::nat => real. summable f = Ex (sums f)"
skalberg@14516
  1559
  by (import seq summable)
skalberg@14516
  1560
skalberg@14516
  1561
constdefs
skalberg@14516
  1562
  suminf :: "(nat => real) => real" 
obua@17644
  1563
  "suminf == %f::nat => real. Eps (sums f)"
obua@17644
  1564
obua@17644
  1565
lemma suminf: "ALL f::nat => real. suminf f = Eps (sums f)"
skalberg@14516
  1566
  by (import seq suminf)
skalberg@14516
  1567
obua@17694
  1568
lemma SUM_SUMMABLE: "ALL (f::nat => real) l::real. sums f l --> summable f"
skalberg@14516
  1569
  by (import seq SUM_SUMMABLE)
skalberg@14516
  1570
obua@17694
  1571
lemma SUMMABLE_SUM: "ALL f::nat => real. summable f --> sums f (suminf f)"
skalberg@14516
  1572
  by (import seq SUMMABLE_SUM)
skalberg@14516
  1573
obua@17694
  1574
lemma SUM_UNIQ: "ALL (f::nat => real) x::real. sums f x --> x = suminf f"
skalberg@14516
  1575
  by (import seq SUM_UNIQ)
skalberg@14516
  1576
obua@17694
  1577
lemma SER_0: "ALL (f::nat => real) n::nat.
obua@17694
  1578
   (ALL m::nat. n <= m --> f m = 0) --> sums f (real.sum (0, n) f)"
skalberg@14516
  1579
  by (import seq SER_0)
skalberg@14516
  1580
obua@17694
  1581
lemma SER_POS_LE: "ALL (f::nat => real) n::nat.
obua@17694
  1582
   summable f & (ALL m::nat. n <= m --> 0 <= f m) -->
obua@17694
  1583
   real.sum (0, n) f <= suminf f"
skalberg@14516
  1584
  by (import seq SER_POS_LE)
skalberg@14516
  1585
obua@17694
  1586
lemma SER_POS_LT: "ALL (f::nat => real) n::nat.
obua@17694
  1587
   summable f & (ALL m::nat. n <= m --> 0 < f m) -->
obua@17694
  1588
   real.sum (0, n) f < suminf f"
skalberg@14516
  1589
  by (import seq SER_POS_LT)
skalberg@14516
  1590
obua@17694
  1591
lemma SER_GROUP: "ALL (f::nat => real) k::nat.
obua@17694
  1592
   summable f & 0 < k --> sums (%n::nat. real.sum (n * k, k) f) (suminf f)"
skalberg@14516
  1593
  by (import seq SER_GROUP)
skalberg@14516
  1594
obua@17694
  1595
lemma SER_PAIR: "ALL f::nat => real.
obua@17694
  1596
   summable f --> sums (%n::nat. real.sum (2 * n, 2) f) (suminf f)"
skalberg@14516
  1597
  by (import seq SER_PAIR)
skalberg@14516
  1598
obua@17694
  1599
lemma SER_OFFSET: "ALL f::nat => real.
obua@17694
  1600
   summable f -->
obua@17694
  1601
   (ALL k::nat. sums (%n::nat. f (n + k)) (suminf f - real.sum (0, k) f))"
skalberg@14516
  1602
  by (import seq SER_OFFSET)
skalberg@14516
  1603
obua@17694
  1604
lemma SER_POS_LT_PAIR: "ALL (f::nat => real) n::nat.
obua@17694
  1605
   summable f & (ALL d::nat. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) -->
obua@17694
  1606
   real.sum (0, n) f < suminf f"
skalberg@14516
  1607
  by (import seq SER_POS_LT_PAIR)
skalberg@14516
  1608
obua@17694
  1609
lemma SER_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1610
   sums x x0 & sums y y0 --> sums (%n::nat. x n + y n) (x0 + y0)"
skalberg@14516
  1611
  by (import seq SER_ADD)
skalberg@14516
  1612
obua@17694
  1613
lemma SER_CMUL: "ALL (x::nat => real) (x0::real) c::real.
obua@17694
  1614
   sums x x0 --> sums (%n::nat. c * x n) (c * x0)"
skalberg@14516
  1615
  by (import seq SER_CMUL)
skalberg@14516
  1616
obua@17694
  1617
lemma SER_NEG: "ALL (x::nat => real) x0::real. sums x x0 --> sums (%xa::nat. - x xa) (- x0)"
skalberg@14516
  1618
  by (import seq SER_NEG)
skalberg@14516
  1619
obua@17694
  1620
lemma SER_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
obua@17694
  1621
   sums x x0 & sums y y0 --> sums (%xa::nat. x xa - y xa) (x0 - y0)"
skalberg@14516
  1622
  by (import seq SER_SUB)
skalberg@14516
  1623
obua@17694
  1624
lemma SER_CDIV: "ALL (x::nat => real) (x0::real) c::real.
obua@17694
  1625
   sums x x0 --> sums (%xa::nat. x xa / c) (x0 / c)"
skalberg@14516
  1626
  by (import seq SER_CDIV)
skalberg@14516
  1627
obua@17694
  1628
lemma SER_CAUCHY: "ALL f::nat => real.
obua@17694
  1629
   summable f =
obua@17694
  1630
   (ALL e>0.
obua@17694
  1631
       EX N::nat.
obua@17694
  1632
          ALL (m::nat) n::nat. N <= m --> abs (real.sum (m, n) f) < e)"
skalberg@14516
  1633
  by (import seq SER_CAUCHY)
skalberg@14516
  1634
obua@17694
  1635
lemma SER_ZERO: "ALL f::nat => real. summable f --> hol4--> f 0"
skalberg@14516
  1636
  by (import seq SER_ZERO)
skalberg@14516
  1637
obua@17694
  1638
lemma SER_COMPAR: "ALL (f::nat => real) g::nat => real.
obua@17694
  1639
   (EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g -->
obua@17694
  1640
   summable f"
skalberg@14516
  1641
  by (import seq SER_COMPAR)
skalberg@14516
  1642
obua@17694
  1643
lemma SER_COMPARA: "ALL (f::nat => real) g::nat => real.
obua@17694
  1644
   (EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g -->
obua@17694
  1645
   summable (%k::nat. abs (f k))"
skalberg@14516
  1646
  by (import seq SER_COMPARA)
skalberg@14516
  1647
obua@17694
  1648
lemma SER_LE: "ALL (f::nat => real) g::nat => real.
obua@17694
  1649
   (ALL n::nat. f n <= g n) & summable f & summable g -->
obua@17694
  1650
   suminf f <= suminf g"
skalberg@14516
  1651
  by (import seq SER_LE)
skalberg@14516
  1652
obua@17694
  1653
lemma SER_LE2: "ALL (f::nat => real) g::nat => real.
obua@17694
  1654
   (ALL n::nat. abs (f n) <= g n) & summable g -->
obua@17694
  1655
   summable f & suminf f <= suminf g"
skalberg@14516
  1656
  by (import seq SER_LE2)
skalberg@14516
  1657
obua@17694
  1658
lemma SER_ACONV: "ALL f::nat => real. summable (%n::nat. abs (f n)) --> summable f"
skalberg@14516
  1659
  by (import seq SER_ACONV)
skalberg@14516
  1660
obua@17694
  1661
lemma SER_ABS: "ALL f::nat => real.
obua@17694
  1662
   summable (%n::nat. abs (f n)) -->
obua@17694
  1663
   abs (suminf f) <= suminf (%n::nat. abs (f n))"
skalberg@14516
  1664
  by (import seq SER_ABS)
skalberg@14516
  1665
obua@17694
  1666
lemma GP_FINITE: "ALL x::real.
obua@17694
  1667
   x ~= 1 --> (ALL n::nat. real.sum (0, n) (op ^ x) = (x ^ n - 1) / (x - 1))"
skalberg@14516
  1668
  by (import seq GP_FINITE)
skalberg@14516
  1669
obua@17694
  1670
lemma GP: "ALL x::real. abs x < 1 --> sums (op ^ x) (inverse (1 - x))"
skalberg@14516
  1671
  by (import seq GP)
skalberg@14516
  1672
skalberg@14516
  1673
lemma ABS_NEG_LEMMA: "(All::(real => bool) => bool)
skalberg@14516
  1674
 (%c::real.
skalberg@14516
  1675
     (op -->::bool => bool => bool)
skalberg@14516
  1676
      ((op <=::real => real => bool) c (0::real))
skalberg@14516
  1677
      ((All::(real => bool) => bool)
skalberg@14516
  1678
        (%x::real.
skalberg@14516
  1679
            (All::(real => bool) => bool)
skalberg@14516
  1680
             (%y::real.
skalberg@14516
  1681
                 (op -->::bool => bool => bool)
skalberg@14516
  1682
                  ((op <=::real => real => bool) ((abs::real => real) x)
skalberg@14516
  1683
                    ((op *::real => real => real) c
skalberg@14516
  1684
                      ((abs::real => real) y)))
skalberg@14516
  1685
                  ((op =::real => real => bool) x (0::real))))))"
skalberg@14516
  1686
  by (import seq ABS_NEG_LEMMA)
skalberg@14516
  1687
obua@17694
  1688
lemma SER_RATIO: "ALL (f::nat => real) (c::real) N::nat.
obua@17694
  1689
   c < 1 & (ALL n::nat. N <= n --> abs (f (Suc n)) <= c * abs (f n)) -->
obua@17694
  1690
   summable f"
skalberg@14516
  1691
  by (import seq SER_RATIO)
skalberg@14516
  1692
skalberg@14516
  1693
;end_setup
skalberg@14516
  1694
skalberg@14516
  1695
;setup_theory lim
skalberg@14516
  1696
skalberg@14516
  1697
constdefs
skalberg@14516
  1698
  tends_real_real :: "(real => real) => real => real => bool" 
obua@17644
  1699
  "tends_real_real ==
obua@17644
  1700
%(f::real => real) (l::real) x0::real.
obua@17644
  1701
   tends f l (mtop mr1, tendsto (mr1, x0))"
obua@17644
  1702
obua@17644
  1703
lemma tends_real_real: "ALL (f::real => real) (l::real) x0::real.
obua@17644
  1704
   tends_real_real f l x0 = tends f l (mtop mr1, tendsto (mr1, x0))"
skalberg@14516
  1705
  by (import lim tends_real_real)
skalberg@14516
  1706
obua@17694
  1707
lemma LIM: "ALL (f::real => real) (y0::real) x0::real.
obua@17694
  1708
   tends_real_real f y0 x0 =
obua@17694
  1709
   (ALL e>0.
obua@17694
  1710
       EX d>0.
obua@17694
  1711
          ALL x::real.
obua@17694
  1712
             0 < abs (x - x0) & abs (x - x0) < d --> abs (f x - y0) < e)"
skalberg@14516
  1713
  by (import lim LIM)
skalberg@14516
  1714
obua@17644
  1715
lemma LIM_CONST: "ALL k::real. All (tends_real_real (%x::real. k) k)"
skalberg@14516
  1716
  by (import lim LIM_CONST)
skalberg@14516
  1717
obua@17694
  1718
lemma LIM_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1719
   tends_real_real f l x & tends_real_real g m x -->
obua@17694
  1720
   tends_real_real (%x::real. f x + g x) (l + m) x"
skalberg@14516
  1721
  by (import lim LIM_ADD)
skalberg@14516
  1722
obua@17694
  1723
lemma LIM_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1724
   tends_real_real f l x & tends_real_real g m x -->
obua@17694
  1725
   tends_real_real (%x::real. f x * g x) (l * m) x"
skalberg@14516
  1726
  by (import lim LIM_MUL)
skalberg@14516
  1727
obua@17644
  1728
lemma LIM_NEG: "ALL (f::real => real) (l::real) x::real.
obua@17644
  1729
   tends_real_real f l x = tends_real_real (%x::real. - f x) (- l) x"
skalberg@14516
  1730
  by (import lim LIM_NEG)
skalberg@14516
  1731
obua@17694
  1732
lemma LIM_INV: "ALL (f::real => real) (l::real) x::real.
obua@17694
  1733
   tends_real_real f l x & l ~= 0 -->
obua@17694
  1734
   tends_real_real (%x::real. inverse (f x)) (inverse l) x"
skalberg@14516
  1735
  by (import lim LIM_INV)
skalberg@14516
  1736
obua@17694
  1737
lemma LIM_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1738
   tends_real_real f l x & tends_real_real g m x -->
obua@17694
  1739
   tends_real_real (%x::real. f x - g x) (l - m) x"
skalberg@14516
  1740
  by (import lim LIM_SUB)
skalberg@14516
  1741
obua@17694
  1742
lemma LIM_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1743
   tends_real_real f l x & tends_real_real g m x & m ~= 0 -->
obua@17694
  1744
   tends_real_real (%x::real. f x / g x) (l / m) x"
skalberg@14516
  1745
  by (import lim LIM_DIV)
skalberg@14516
  1746
obua@17644
  1747
lemma LIM_NULL: "ALL (f::real => real) (l::real) x::real.
obua@17652
  1748
   tends_real_real f l x = tends_real_real (%x::real. f x - l) 0 x"
skalberg@14516
  1749
  by (import lim LIM_NULL)
skalberg@14516
  1750
obua@17644
  1751
lemma LIM_X: "ALL x0::real. tends_real_real (%x::real. x) x0 x0"
skalberg@14516
  1752
  by (import lim LIM_X)
skalberg@14516
  1753
obua@17694
  1754
lemma LIM_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real.
obua@17694
  1755
   tends_real_real f l x & tends_real_real f m x --> l = m"
skalberg@14516
  1756
  by (import lim LIM_UNIQ)
skalberg@14516
  1757
obua@17694
  1758
lemma LIM_EQUAL: "ALL (f::real => real) (g::real => real) (l::real) x0::real.
obua@17694
  1759
   (ALL x::real. x ~= x0 --> f x = g x) -->
obua@17694
  1760
   tends_real_real f l x0 = tends_real_real g l x0"
skalberg@14516
  1761
  by (import lim LIM_EQUAL)
skalberg@14516
  1762
obua@17694
  1763
lemma LIM_TRANSFORM: "ALL (f::real => real) (g::real => real) (x0::real) l::real.
obua@17694
  1764
   tends_real_real (%x::real. f x - g x) 0 x0 & tends_real_real g l x0 -->
obua@17694
  1765
   tends_real_real f l x0"
skalberg@14516
  1766
  by (import lim LIM_TRANSFORM)
skalberg@14516
  1767
skalberg@14516
  1768
constdefs
skalberg@14516
  1769
  diffl :: "(real => real) => real => real => bool" 
obua@17644
  1770
  "diffl ==
obua@17644
  1771
%(f::real => real) (l::real) x::real.
obua@17652
  1772
   tends_real_real (%h::real. (f (x + h) - f x) / h) l 0"
obua@17644
  1773
obua@17644
  1774
lemma diffl: "ALL (f::real => real) (l::real) x::real.
obua@17652
  1775
   diffl f l x = tends_real_real (%h::real. (f (x + h) - f x) / h) l 0"
skalberg@14516
  1776
  by (import lim diffl)
skalberg@14516
  1777
skalberg@14516
  1778
constdefs
skalberg@14516
  1779
  contl :: "(real => real) => real => bool" 
obua@17644
  1780
  "contl ==
obua@17652
  1781
%(f::real => real) x::real. tends_real_real (%h::real. f (x + h)) (f x) 0"
obua@17644
  1782
obua@17644
  1783
lemma contl: "ALL (f::real => real) x::real.
obua@17652
  1784
   contl f x = tends_real_real (%h::real. f (x + h)) (f x) 0"
skalberg@14516
  1785
  by (import lim contl)
skalberg@14516
  1786
skalberg@14516
  1787
constdefs
skalberg@14516
  1788
  differentiable :: "(real => real) => real => bool" 
obua@17644
  1789
  "differentiable == %(f::real => real) x::real. EX l::real. diffl f l x"
obua@17644
  1790
obua@17644
  1791
lemma differentiable: "ALL (f::real => real) x::real.
obua@17644
  1792
   differentiable f x = (EX l::real. diffl f l x)"
skalberg@14516
  1793
  by (import lim differentiable)
skalberg@14516
  1794
obua@17694
  1795
lemma DIFF_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real.
obua@17694
  1796
   diffl f l x & diffl f m x --> l = m"
skalberg@14516
  1797
  by (import lim DIFF_UNIQ)
skalberg@14516
  1798
obua@17694
  1799
lemma DIFF_CONT: "ALL (f::real => real) (l::real) x::real. diffl f l x --> contl f x"
skalberg@14516
  1800
  by (import lim DIFF_CONT)
skalberg@14516
  1801
obua@17644
  1802
lemma CONTL_LIM: "ALL (f::real => real) x::real. contl f x = tends_real_real f (f x) x"
skalberg@14516
  1803
  by (import lim CONTL_LIM)
skalberg@14516
  1804
obua@17644
  1805
lemma DIFF_CARAT: "ALL (f::real => real) (l::real) x::real.
skalberg@14516
  1806
   diffl f l x =
obua@17644
  1807
   (EX g::real => real.
obua@17644
  1808
       (ALL z::real. f z - f x = g z * (z - x)) & contl g x & g x = l)"
skalberg@14516
  1809
  by (import lim DIFF_CARAT)
skalberg@14516
  1810
obua@17644
  1811
lemma CONT_CONST: "ALL k::real. All (contl (%x::real. k))"
skalberg@14516
  1812
  by (import lim CONT_CONST)
skalberg@14516
  1813
obua@17694
  1814
lemma CONT_ADD: "ALL (f::real => real) (g::real => real) x::real.
obua@17694
  1815
   contl f x & contl g x --> contl (%x::real. f x + g x) x"
skalberg@14516
  1816
  by (import lim CONT_ADD)
skalberg@14516
  1817
obua@17694
  1818
lemma CONT_MUL: "ALL (f::real => real) (g::real => real) x::real.
obua@17694
  1819
   contl f x & contl g x --> contl (%x::real. f x * g x) x"
skalberg@14516
  1820
  by (import lim CONT_MUL)
skalberg@14516
  1821
obua@17694
  1822
lemma CONT_NEG: "ALL (f::real => real) x::real. contl f x --> contl (%x::real. - f x) x"
skalberg@14516
  1823
  by (import lim CONT_NEG)
skalberg@14516
  1824
obua@17694
  1825
lemma CONT_INV: "ALL (f::real => real) x::real.
obua@17694
  1826
   contl f x & f x ~= 0 --> contl (%x::real. inverse (f x)) x"
skalberg@14516
  1827
  by (import lim CONT_INV)
skalberg@14516
  1828
obua@17694
  1829
lemma CONT_SUB: "ALL (f::real => real) (g::real => real) x::real.
obua@17694
  1830
   contl f x & contl g x --> contl (%x::real. f x - g x) x"
skalberg@14516
  1831
  by (import lim CONT_SUB)
skalberg@14516
  1832
obua@17694
  1833
lemma CONT_DIV: "ALL (f::real => real) (g::real => real) x::real.
obua@17694
  1834
   contl f x & contl g x & g x ~= 0 --> contl (%x::real. f x / g x) x"
skalberg@14516
  1835
  by (import lim CONT_DIV)
skalberg@14516
  1836
obua@17694
  1837
lemma CONT_COMPOSE: "ALL (f::real => real) (g::real => real) x::real.
obua@17694
  1838
   contl f x & contl g (f x) --> contl (%x::real. g (f x)) x"
skalberg@14516
  1839
  by (import lim CONT_COMPOSE)
skalberg@14516
  1840
obua@17694
  1841
lemma IVT: "ALL (f::real => real) (a::real) (b::real) y::real.
obua@17694
  1842
   a <= b &
obua@17694
  1843
   (f a <= y & y <= f b) & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1844
   (EX x::real. a <= x & x <= b & f x = y)"
skalberg@14516
  1845
  by (import lim IVT)
skalberg@14516
  1846
obua@17694
  1847
lemma IVT2: "ALL (f::real => real) (a::real) (b::real) y::real.
obua@17694
  1848
   a <= b &
obua@17694
  1849
   (f b <= y & y <= f a) & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1850
   (EX x::real. a <= x & x <= b & f x = y)"
skalberg@14516
  1851
  by (import lim IVT2)
skalberg@14516
  1852
obua@17652
  1853
lemma DIFF_CONST: "ALL k::real. All (diffl (%x::real. k) 0)"
skalberg@14516
  1854
  by (import lim DIFF_CONST)
skalberg@14516
  1855
obua@17694
  1856
lemma DIFF_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1857
   diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x"
skalberg@14516
  1858
  by (import lim DIFF_ADD)
skalberg@14516
  1859
obua@17694
  1860
lemma DIFF_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1861
   diffl f l x & diffl g m x -->
obua@17694
  1862
   diffl (%x::real. f x * g x) (l * g x + m * f x) x"
skalberg@14516
  1863
  by (import lim DIFF_MUL)
skalberg@14516
  1864
obua@17694
  1865
lemma DIFF_CMUL: "ALL (f::real => real) (c::real) (l::real) x::real.
obua@17694
  1866
   diffl f l x --> diffl (%x::real. c * f x) (c * l) x"
skalberg@14516
  1867
  by (import lim DIFF_CMUL)
skalberg@14516
  1868
obua@17694
  1869
lemma DIFF_NEG: "ALL (f::real => real) (l::real) x::real.
obua@17694
  1870
   diffl f l x --> diffl (%x::real. - f x) (- l) x"
skalberg@14516
  1871
  by (import lim DIFF_NEG)
skalberg@14516
  1872
obua@17694
  1873
lemma DIFF_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1874
   diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x"
skalberg@14516
  1875
  by (import lim DIFF_SUB)
skalberg@14516
  1876
obua@17694
  1877
lemma DIFF_CHAIN: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1878
   diffl f l (g x) & diffl g m x --> diffl (%x::real. f (g x)) (l * m) x"
skalberg@14516
  1879
  by (import lim DIFF_CHAIN)
skalberg@14516
  1880
obua@17652
  1881
lemma DIFF_X: "All (diffl (%x::real. x) 1)"
skalberg@14516
  1882
  by (import lim DIFF_X)
skalberg@14516
  1883
obua@17652
  1884
lemma DIFF_POW: "ALL (n::nat) x::real. diffl (%x::real. x ^ n) (real n * x ^ (n - 1)) x"
skalberg@14516
  1885
  by (import lim DIFF_POW)
skalberg@14516
  1886
obua@17694
  1887
lemma DIFF_XM1: "ALL x::real. x ~= 0 --> diffl inverse (- (inverse x ^ 2)) x"
skalberg@14516
  1888
  by (import lim DIFF_XM1)
skalberg@14516
  1889
obua@17694
  1890
lemma DIFF_INV: "ALL (f::real => real) (l::real) x::real.
obua@17694
  1891
   diffl f l x & f x ~= 0 -->
obua@17694
  1892
   diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x"
skalberg@14516
  1893
  by (import lim DIFF_INV)
skalberg@14516
  1894
obua@17694
  1895
lemma DIFF_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
obua@17694
  1896
   diffl f l x & diffl g m x & g x ~= 0 -->
obua@17694
  1897
   diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x"
skalberg@14516
  1898
  by (import lim DIFF_DIV)
skalberg@14516
  1899
obua@17694
  1900
lemma DIFF_SUM: "ALL (f::nat => real => real) (f'::nat => real => real) (m::nat) (n::nat)
obua@17694
  1901
   x::real.
obua@17694
  1902
   (ALL r::nat. m <= r & r < m + n --> diffl (f r) (f' r x) x) -->
obua@17694
  1903
   diffl (%x::real. real.sum (m, n) (%n::nat. f n x))
obua@17694
  1904
    (real.sum (m, n) (%r::nat. f' r x)) x"
skalberg@14516
  1905
  by (import lim DIFF_SUM)
skalberg@14516
  1906
obua@17694
  1907
lemma CONT_BOUNDED: "ALL (f::real => real) (a::real) b::real.
obua@17694
  1908
   a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1909
   (EX M::real. ALL x::real. a <= x & x <= b --> f x <= M)"
skalberg@14516
  1910
  by (import lim CONT_BOUNDED)
skalberg@14516
  1911
skalberg@14516
  1912
lemma CONT_HASSUP: "(All::((real => real) => bool) => bool)
skalberg@14516
  1913
 (%f::real => real.
skalberg@14516
  1914
     (All::(real => bool) => bool)
skalberg@14516
  1915
      (%a::real.
skalberg@14516
  1916
          (All::(real => bool) => bool)
skalberg@14516
  1917
           (%b::real.
skalberg@14516
  1918
               (op -->::bool => bool => bool)
skalberg@14516
  1919
                ((op &::bool => bool => bool)
skalberg@14516
  1920
                  ((op <=::real => real => bool) a b)
skalberg@14516
  1921
                  ((All::(real => bool) => bool)
skalberg@14516
  1922
                    (%x::real.
skalberg@14516
  1923
                        (op -->::bool => bool => bool)
skalberg@14516
  1924
                         ((op &::bool => bool => bool)
skalberg@14516
  1925
                           ((op <=::real => real => bool) a x)
skalberg@14516
  1926
                           ((op <=::real => real => bool) x b))
skalberg@14516
  1927
                         ((contl::(real => real) => real => bool) f x))))
skalberg@14516
  1928
                ((Ex::(real => bool) => bool)
skalberg@14516
  1929
                  (%M::real.
skalberg@14516
  1930
                      (op &::bool => bool => bool)
skalberg@14516
  1931
                       ((All::(real => bool) => bool)
skalberg@14516
  1932
                         (%x::real.
skalberg@14516
  1933
                             (op -->::bool => bool => bool)
skalberg@14516
  1934
                              ((op &::bool => bool => bool)
skalberg@14516
  1935
                                ((op <=::real => real => bool) a x)
skalberg@14516
  1936
                                ((op <=::real => real => bool) x b))
skalberg@14516
  1937
                              ((op <=::real => real => bool) (f x) M)))
skalberg@14516
  1938
                       ((All::(real => bool) => bool)
skalberg@14516
  1939
                         (%N::real.
skalberg@14516
  1940
                             (op -->::bool => bool => bool)
skalberg@14516
  1941
                              ((op <::real => real => bool) N M)
skalberg@14516
  1942
                              ((Ex::(real => bool) => bool)
skalberg@14516
  1943
                                (%x::real.
skalberg@14516
  1944
                                    (op &::bool => bool => bool)
skalberg@14516
  1945
                                     ((op <=::real => real => bool) a x)
skalberg@14516
  1946
                                     ((op &::bool => bool => bool)
skalberg@14516
  1947
 ((op <=::real => real => bool) x b)
skalberg@14516
  1948
 ((op <::real => real => bool) N (f x))))))))))))"
skalberg@14516
  1949
  by (import lim CONT_HASSUP)
skalberg@14516
  1950
obua@17694
  1951
lemma CONT_ATTAINS: "ALL (f::real => real) (a::real) b::real.
obua@17694
  1952
   a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1953
   (EX x::real.
obua@17694
  1954
       (ALL xa::real. a <= xa & xa <= b --> f xa <= x) &
obua@17694
  1955
       (EX xa::real. a <= xa & xa <= b & f xa = x))"
skalberg@14516
  1956
  by (import lim CONT_ATTAINS)
skalberg@14516
  1957
obua@17694
  1958
lemma CONT_ATTAINS2: "ALL (f::real => real) (a::real) b::real.
obua@17694
  1959
   a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1960
   (EX x::real.
obua@17694
  1961
       (ALL xa::real. a <= xa & xa <= b --> x <= f xa) &
obua@17694
  1962
       (EX xa::real. a <= xa & xa <= b & f xa = x))"
skalberg@14516
  1963
  by (import lim CONT_ATTAINS2)
skalberg@14516
  1964
obua@17694
  1965
lemma CONT_ATTAINS_ALL: "ALL (f::real => real) (a::real) b::real.
obua@17694
  1966
   a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
obua@17694
  1967
   (EX (x::real) M::real.
obua@17694
  1968
       x <= M &
obua@17694
  1969
       (ALL y::real.
obua@17694
  1970
           x <= y & y <= M --> (EX x::real. a <= x & x <= b & f x = y)) &
obua@17694
  1971
       (ALL xa::real. a <= xa & xa <= b --> x <= f xa & f xa <= M))"
skalberg@14516
  1972
  by (import lim CONT_ATTAINS_ALL)
skalberg@14516
  1973
obua@17694
  1974
lemma DIFF_LINC: "ALL (f::real => real) (x::real) l::real.
obua@17694
  1975
   diffl f l x & 0 < l -->
obua@17694
  1976
   (EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x + h))"
skalberg@14516
  1977
  by (import lim DIFF_LINC)
skalberg@14516
  1978
obua@17694
  1979
lemma DIFF_LDEC: "ALL (f::real => real) (x::real) l::real.
obua@17694
  1980
   diffl f l x & l < 0 -->
obua@17694
  1981
   (EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x - h))"
skalberg@14516
  1982
  by (import lim DIFF_LDEC)
skalberg@14516
  1983
obua@17694
  1984
lemma DIFF_LMAX: "ALL (f::real => real) (x::real) l::real.
obua@17694
  1985
   diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y <= f x) -->
obua@17694
  1986
   l = 0"
skalberg@14516
  1987
  by (import lim DIFF_LMAX)
skalberg@14516
  1988
obua@17694
  1989
lemma DIFF_LMIN: "ALL (f::real => real) (x::real) l::real.
obua@17694
  1990
   diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f x <= f y) -->
obua@17694
  1991
   l = 0"
skalberg@14516
  1992
  by (import lim DIFF_LMIN)
skalberg@14516
  1993
obua@17694
  1994
lemma DIFF_LCONST: "ALL (f::real => real) (x::real) l::real.
obua@17694
  1995
   diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y = f x) -->
obua@17694
  1996
   l = 0"
skalberg@14516
  1997
  by (import lim DIFF_LCONST)
skalberg@14516
  1998
obua@17694
  1999
lemma INTERVAL_LEMMA: "ALL (a::real) (b::real) x::real.
obua@17694
  2000
   a < x & x < b -->
obua@17694
  2001
   (EX d>0. ALL y::real. abs (x - y) < d --> a <= y & y <= b)"
skalberg@14516
  2002
  by (import lim INTERVAL_LEMMA)
skalberg@14516
  2003
obua@17694
  2004
lemma ROLLE: "ALL (f::real => real) (a::real) b::real.
obua@17694
  2005
   a < b &
obua@17694
  2006
   f a = f b &
obua@17694
  2007
   (ALL x::real. a <= x & x <= b --> contl f x) &
obua@17694
  2008
   (ALL x::real. a < x & x < b --> differentiable f x) -->
obua@17694
  2009
   (EX z::real. a < z & z < b & diffl f 0 z)"
skalberg@14516
  2010
  by (import lim ROLLE)
skalberg@14516
  2011
skalberg@14516
  2012
lemma MVT_LEMMA: "ALL (f::real => real) (a::real) b::real.
skalberg@14516
  2013
   f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b"
skalberg@14516
  2014
  by (import lim MVT_LEMMA)
skalberg@14516
  2015
obua@17694
  2016
lemma MVT: "ALL (f::real => real) (a::real) b::real.
obua@17694
  2017
   a < b &
obua@17694
  2018
   (ALL x::real. a <= x & x <= b --> contl f x) &
obua@17694
  2019
   (ALL x::real. a < x & x < b --> differentiable f x) -->
obua@17694
  2020
   (EX (l::real) z::real.
obua@17694
  2021
       a < z & z < b & diffl f l z & f b - f a = (b - a) * l)"
skalberg@14516
  2022
  by (import lim MVT)
skalberg@14516
  2023
obua@17694
  2024
lemma DIFF_ISCONST_END: "ALL (f::real => real) (a::real) b::real.
obua@17694
  2025
   a < b &
obua@17694
  2026
   (ALL x::real. a <= x & x <= b --> contl f x) &
obua@17694
  2027
   (ALL x::real. a < x & x < b --> diffl f 0 x) -->
obua@17694
  2028
   f b = f a"
skalberg@14516
  2029
  by (import lim DIFF_ISCONST_END)
skalberg@14516
  2030
obua@17694
  2031
lemma DIFF_ISCONST: "ALL (f::real => real) (a::real) b::real.
obua@17694
  2032
   a < b &
obua@17694
  2033
   (ALL x::real. a <= x & x <= b --> contl f x) &
obua@17694
  2034
   (ALL x::real. a < x & x < b --> diffl f 0 x) -->
obua@17694
  2035
   (ALL x::real. a <= x & x <= b --> f x = f a)"
skalberg@14516
  2036
  by (import lim DIFF_ISCONST)
skalberg@14516
  2037
obua@17694
  2038
lemma DIFF_ISCONST_ALL: "ALL f::real => real. All (diffl f 0) --> (ALL (x::real) y::real. f x = f y)"
skalberg@14516
  2039
  by (import lim DIFF_ISCONST_ALL)
skalberg@14516
  2040
skalberg@14516
  2041
lemma INTERVAL_ABS: "ALL (x::real) (z::real) d::real.
skalberg@14516
  2042
   (x - d <= z & z <= x + d) = (abs (z - x) <= d)"
skalberg@14516
  2043
  by (import lim INTERVAL_ABS)
skalberg@14516
  2044
obua@17694
  2045
lemma CONT_INJ_LEMMA: "ALL (f::real => real) (g::real => real) (x::real) d::real.
obua@17694
  2046
   0 < d &
obua@17694
  2047
   (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
obua@17694
  2048
   (ALL z::real. abs (z - x) <= d --> contl f z) -->
obua@17694
  2049
   ~ (ALL z::real. abs (z - x) <= d --> f z <= f x)"
skalberg@14516
  2050
  by (import lim CONT_INJ_LEMMA)
skalberg@14516
  2051
obua@17694
  2052
lemma CONT_INJ_LEMMA2: "ALL (f::real => real) (g::real => real) (x::real) d::real.
obua@17694
  2053
   0 < d &
obua@17694
  2054
   (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
obua@17694
  2055
   (ALL z::real. abs (z - x) <= d --> contl f z) -->
obua@17694
  2056
   ~ (ALL z::real. abs (z - x) <= d --> f x <= f z)"
skalberg@14516
  2057
  by (import lim CONT_INJ_LEMMA2)
skalberg@14516
  2058
obua@17694
  2059
lemma CONT_INJ_RANGE: "ALL (f::real => real) (g::real => real) (x::real) d::real.
obua@17694
  2060
   0 < d &
obua@17694
  2061
   (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
obua@17694
  2062
   (ALL z::real. abs (z - x) <= d --> contl f z) -->
obua@17694
  2063
   (EX e>0.
obua@17694
  2064
       ALL y::real.
obua@17694
  2065
          abs (y - f x) <= e --> (EX z::real. abs (z - x) <= d & f z = y))"
skalberg@14516
  2066
  by (import lim CONT_INJ_RANGE)
skalberg@14516
  2067
obua@17694
  2068
lemma CONT_INVERSE: "ALL (f::real => real) (g::real => real) (x::real) d::real.
obua@17694
  2069
   0 < d &
obua@17694
  2070
   (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
obua@17694
  2071
   (ALL z::real. abs (z - x) <= d --> contl f z) -->
obua@17694
  2072
   contl g (f x)"
skalberg@14516
  2073
  by (import lim CONT_INVERSE)
skalberg@14516
  2074
obua@17694
  2075
lemma DIFF_INVERSE: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real.
obua@17694
  2076
   0 < d &
obua@17694
  2077
   (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
obua@17694
  2078
   (ALL z::real. abs (z - x) <= d --> contl f z) & diffl f l x & l ~= 0 -->
obua@17694
  2079
   diffl g (inverse l) (f x)"
skalberg@14516
  2080
  by (import lim DIFF_INVERSE)
skalberg@14516
  2081
obua@17694
  2082
lemma DIFF_INVERSE_LT: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real.
obua@17694
  2083
   0 < d &
obua@17694
  2084
   (ALL z::real. abs (z - x) < d --> g (f z) = z) &
obua@17694
  2085
   (ALL z::real. abs (z - x) < d --> contl f z) & diffl f l x & l ~= 0 -->
obua@17694
  2086
   diffl g (inverse l) (f x)"
skalberg@14516
  2087
  by (import lim DIFF_INVERSE_LT)
skalberg@14516
  2088
obua@17694
  2089
lemma INTERVAL_CLEMMA: "ALL (a::real) (b::real) x::real.
obua@17694
  2090
   a < x & x < b -->
obua@17694
  2091
   (EX d>0. ALL y::real. abs (y - x) <= d --> a < y & y < b)"
skalberg@14516
  2092
  by (import lim INTERVAL_CLEMMA)
skalberg@14516
  2093
obua@17694
  2094
lemma DIFF_INVERSE_OPEN: "ALL (f::real => real) (g::real => real) (l::real) (a::real) (x::real)
obua@17694
  2095
   b::real.
obua@17694
  2096
   a < x &
obua@17694
  2097
   x < b &
obua@17694
  2098
   (ALL z::real. a < z & z < b --> g (f z) = z & contl f z) &
obua@17694
  2099
   diffl f l x & l ~= 0 -->
obua@17694
  2100
   diffl g (inverse l) (f x)"
skalberg@14516
  2101
  by (import lim DIFF_INVERSE_OPEN)
skalberg@14516
  2102
skalberg@14516
  2103
;end_setup
skalberg@14516
  2104
skalberg@14516
  2105
;setup_theory powser
skalberg@14516
  2106
obua@17644
  2107
lemma POWDIFF_LEMMA: "ALL (n::nat) (x::real) y::real.
obua@17652
  2108
   real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (Suc n - p)) =
obua@17652
  2109
   y * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))"
skalberg@14516
  2110
  by (import powser POWDIFF_LEMMA)
skalberg@14516
  2111
obua@17644
  2112
lemma POWDIFF: "ALL (n::nat) (x::real) y::real.
skalberg@14516
  2113
   x ^ Suc n - y ^ Suc n =
obua@17652
  2114
   (x - y) * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))"
skalberg@14516
  2115
  by (import powser POWDIFF)
skalberg@14516
  2116
obua@17644
  2117
lemma POWREV: "ALL (n::nat) (x::real) y::real.
obua@17652
  2118
   real.sum (0, Suc n) (%xa::nat. x ^ xa * y ^ (n - xa)) =
obua@17652
  2119
   real.sum (0, Suc n) (%xa::nat. x ^ (n - xa) * y ^ xa)"
skalberg@14516
  2120
  by (import powser POWREV)
skalberg@14516
  2121
obua@17694
  2122
lemma POWSER_INSIDEA: "ALL (f::nat => real) (x::real) z::real.
obua@17694
  2123
   summable (%n::nat. f n * x ^ n) & abs z < abs x -->
obua@17694
  2124
   summable (%n::nat. abs (f n) * z ^ n)"
skalberg@14516
  2125
  by (import powser POWSER_INSIDEA)
skalberg@14516
  2126
obua@17694
  2127
lemma POWSER_INSIDE: "ALL (f::nat => real) (x::real) z::real.
obua@17694
  2128
   summable (%n::nat. f n * x ^ n) & abs z < abs x -->
obua@17694
  2129
   summable (%n::nat. f n * z ^ n)"
skalberg@14516
  2130
  by (import powser POWSER_INSIDE)
skalberg@14516
  2131
skalberg@14516
  2132
constdefs
skalberg@14516
  2133
  diffs :: "(nat => real) => nat => real" 
obua@17644
  2134
  "diffs == %(c::nat => real) n::nat. real (Suc n) * c (Suc n)"
obua@17644
  2135
obua@17644
  2136
lemma diffs: "ALL c::nat => real. diffs c = (%n::nat. real (Suc n) * c (Suc n))"
skalberg@14516
  2137
  by (import powser diffs)
skalberg@14516
  2138
obua@17644
  2139
lemma DIFFS_NEG: "ALL c::nat => real. diffs (%n::nat. - c n) = (%x::nat. - diffs c x)"
skalberg@14516
  2140
  by (import powser DIFFS_NEG)
skalberg@14516
  2141
obua@17644
  2142
lemma DIFFS_LEMMA: "ALL (n::nat) (c::nat => real) x::real.
obua@17652
  2143
   real.sum (0, n) (%n::nat. diffs c n * x ^ n) =
obua@17652
  2144
   real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) +
obua@17652
  2145
   real n * (c n * x ^ (n - 1))"
skalberg@14516
  2146
  by (import powser DIFFS_LEMMA)
skalberg@14516
  2147
obua@17644
  2148
lemma DIFFS_LEMMA2: "ALL (n::nat) (c::nat => real) x::real.
obua@17652
  2149
   real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) =
obua@17652
  2150
   real.sum (0, n) (%n::nat. diffs c n * x ^ n) -
obua@17652
  2151
   real n * (c n * x ^ (n - 1))"
skalberg@14516
  2152
  by (import powser DIFFS_LEMMA2)
skalberg@14516
  2153
obua@17694
  2154
lemma DIFFS_EQUIV: "ALL (c::nat => real) x::real.
obua@17694
  2155
   summable (%n::nat. diffs c n * x ^ n) -->
obua@17694
  2156
   sums (%n::nat. real n * (c n * x ^ (n - 1)))
obua@17694
  2157
    (suminf (%n::nat. diffs c n * x ^ n))"
skalberg@14516
  2158
  by (import powser DIFFS_EQUIV)
skalberg@14516
  2159
obua@17644
  2160
lemma TERMDIFF_LEMMA1: "ALL (m::nat) (z::real) h::real.
obua@17652
  2161
   real.sum (0, m) (%p::nat. (z + h) ^ (m - p) * z ^ p - z ^ m) =
obua@17652
  2162
   real.sum (0, m) (%p::nat. z ^ p * ((z + h) ^ (m - p) - z ^ (m - p)))"
skalberg@14516
  2163
  by (import powser TERMDIFF_LEMMA1)
skalberg@14516
  2164
obua@17694
  2165
lemma TERMDIFF_LEMMA2: "ALL (z::real) (h::real) n::nat.
obua@17694
  2166
   h ~= 0 -->
obua@17694
  2167
   ((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1) =
obua@17694
  2168
   h *
obua@17694
  2169
   real.sum (0, n - 1)
obua@17694
  2170
    (%p::nat.
obua@17694
  2171
        z ^ p *
obua@17694
  2172
        real.sum (0, n - 1 - p)
obua@17694
  2173
         (%q::nat. (z + h) ^ q * z ^ (n - 2 - p - q)))"
skalberg@14516
  2174
  by (import powser TERMDIFF_LEMMA2)
skalberg@14516
  2175
obua@17694
  2176
lemma TERMDIFF_LEMMA3: "ALL (z::real) (h::real) (n::nat) k'::real.
obua@17694
  2177
   h ~= 0 & abs z <= k' & abs (z + h) <= k' -->
obua@17694
  2178
   abs (((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1))
obua@17694
  2179
   <= real n * (real (n - 1) * (k' ^ (n - 2) * abs h))"
skalberg@14516
  2180
  by (import powser TERMDIFF_LEMMA3)
skalberg@14516
  2181
obua@17694
  2182
lemma TERMDIFF_LEMMA4: "ALL (f::real => real) (k'::real) k::real.
obua@17694
  2183
   0 < k &
obua@17694
  2184
   (ALL h::real. 0 < abs h & abs h < k --> abs (f h) <= k' * abs h) -->
obua@17694
  2185
   tends_real_real f 0 0"
skalberg@14516
  2186
  by (import powser TERMDIFF_LEMMA4)
skalberg@14516
  2187
obua@17694
  2188
lemma TERMDIFF_LEMMA5: "ALL (f::nat => real) (g::real => nat => real) k::real.
obua@17694
  2189
   0 < k &
obua@17694
  2190
   summable f &
obua@17694
  2191
   (ALL h::real.
obua@17694
  2192
       0 < abs h & abs h < k -->
obua@17694
  2193
       (ALL n::nat. abs (g h n) <= f n * abs h)) -->
obua@17694
  2194
   tends_real_real (%h::real. suminf (g h)) 0 0"
skalberg@14516
  2195
  by (import powser TERMDIFF_LEMMA5)
skalberg@14516
  2196
obua@17694
  2197
lemma TERMDIFF: "ALL (c::nat => real) (k'::real) x::real.
obua@17694
  2198
   summable (%n::nat. c n * k' ^ n) &
obua@17694
  2199
   summable (%n::nat. diffs c n * k' ^ n) &
obua@17694
  2200
   summable (%n::nat. diffs (diffs c) n * k' ^ n) & abs x < abs k' -->
obua@17694
  2201
   diffl (%x::real. suminf (%n::nat. c n * x ^ n))
obua@17694
  2202
    (suminf (%n::nat. diffs c n * x ^ n)) x"
skalberg@14516
  2203
  by (import powser TERMDIFF)
skalberg@14516
  2204
skalberg@14516
  2205
;end_setup
skalberg@14516
  2206
skalberg@14516
  2207
;setup_theory transc
skalberg@14516
  2208
skalberg@14516
  2209
constdefs
skalberg@14516
  2210
  exp :: "real => real" 
obua@17644
  2211
  "exp == %x::real. suminf (%n::nat. inverse (real (FACT n)) * x ^ n)"
obua@17644
  2212
obua@17644
  2213
lemma exp: "ALL x::real. exp x = suminf (%n::nat. inverse (real (FACT n)) * x ^ n)"
skalberg@14516
  2214
  by (import transc exp)
skalberg@14516
  2215
skalberg@14516
  2216
constdefs
skalberg@14516
  2217
  cos :: "real => real" 
obua@17652
  2218
  "cos ==
obua@17652
  2219
%x::real.
obua@17652
  2220
   suminf
obua@17652
  2221
    (%n::nat.
obua@17652
  2222
        (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)"
obua@17652
  2223
obua@17652
  2224
lemma cos: "ALL x::real.
obua@17652
  2225
   cos x =
obua@17652
  2226
   suminf
obua@17652
  2227
    (%n::nat.
obua@17652
  2228
        (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)"
skalberg@14516
  2229
  by (import transc cos)
skalberg@14516
  2230
skalberg@14516
  2231
constdefs
skalberg@14516
  2232
  sin :: "real => real" 
skalberg@14516
  2233
  "sin ==
obua@17644
  2234
%x::real.
obua@17644
  2235
   suminf
obua@17644
  2236
    (%n::nat.
obua@17652
  2237
        (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
obua@17644
  2238
        x ^ n)"
obua@17644
  2239
obua@17644
  2240
lemma sin: "ALL x::real.
skalberg@14516
  2241
   sin x =
skalberg@14516
  2242
   suminf
obua@17644
  2243
    (%n::nat.
obua@17652
  2244
        (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
obua@17644
  2245
        x ^ n)"
skalberg@14516
  2246
  by (import transc sin)
skalberg@14516
  2247
obua@17644
  2248
lemma EXP_CONVERGES: "ALL x::real. sums (%n::nat. inverse (real (FACT n)) * x ^ n) (exp x)"
skalberg@14516
  2249
  by (import transc EXP_CONVERGES)
skalberg@14516
  2250
obua@17644
  2251
lemma SIN_CONVERGES: "ALL x::real.
skalberg@14516
  2252
   sums
obua@17644
  2253
    (%n::nat.
obua@17652
  2254
        (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
obua@17644
  2255
        x ^ n)
skalberg@14516
  2256
    (sin x)"
skalberg@14516
  2257
  by (import transc SIN_CONVERGES)
skalberg@14516
  2258
obua@17652
  2259
lemma COS_CONVERGES: "ALL x::real.
obua@17652
  2260
   sums
obua@17652
  2261
    (%n::nat.
obua@17652
  2262
        (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)
obua@17652
  2263
    (cos x)"
skalberg@14516
  2264
  by (import transc COS_CONVERGES)
skalberg@14516
  2265
obua@17644
  2266
lemma EXP_FDIFF: "diffs (%n::nat. inverse (real (FACT n))) =
obua@17644
  2267
(%n::nat. inverse (real (FACT n)))"
skalberg@14516
  2268
  by (import transc EXP_FDIFF)
skalberg@14516
  2269
obua@17652
  2270
lemma SIN_FDIFF: "diffs
obua@17652
  2271
 (%n::nat. if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) =
obua@17652
  2272
(%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0)"
skalberg@14516
  2273
  by (import transc SIN_FDIFF)
skalberg@14516
  2274
obua@17652
  2275
lemma COS_FDIFF: "diffs (%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) =
obua@17652
  2276
(%n::nat. - (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)))"
skalberg@14516
  2277
  by (import transc COS_FDIFF)
skalberg@14516
  2278
obua@17644
  2279
lemma SIN_NEGLEMMA: "ALL x::real.
skalberg@14516
  2280
   - sin x =
skalberg@14516
  2281
   suminf
obua@17644
  2282
    (%n::nat.
obua@17652
  2283
        - ((if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
obua@17644
  2284
           x ^ n))"
skalberg@14516
  2285
  by (import transc SIN_NEGLEMMA)
skalberg@14516
  2286
obua@17644
  2287
lemma DIFF_EXP: "ALL x::real. diffl exp (exp x) x"
skalberg@14516
  2288
  by (import transc DIFF_EXP)
skalberg@14516
  2289
obua@17644
  2290
lemma DIFF_SIN: "ALL x::real. diffl sin (cos x) x"
skalberg@14516
  2291
  by (import transc DIFF_SIN)
skalberg@14516
  2292
obua@17644
  2293
lemma DIFF_COS: "ALL x::real. diffl cos (- sin x) x"
skalberg@14516
  2294
  by (import transc DIFF_COS)
skalberg@14516
  2295
obua@17694
  2296
lemma DIFF_COMPOSITE: "(diffl (f::real => real) (l::real) (x::real) & f x ~= 0 -->
obua@17694
  2297
 diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x) &
obua@17694
  2298
(diffl f l x & diffl (g::real => real) (m::real) x & g x ~= 0 -->
obua@17694
  2299
 diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x) &
obua@17694
  2300
(diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x) &
obua@17694
  2301
(diffl f l x & diffl g m x -->
obua@17694
  2302
 diffl (%x::real. f x * g x) (l * g x + m * f x) x) &
obua@17694
  2303
(diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x) &
obua@17694
  2304
(diffl f l x --> diffl (%x::real. - f x) (- l) x) &
obua@17694
  2305
(diffl g m x -->
obua@17694
  2306
 diffl (%x::real. g x ^ (n::nat)) (real n * g x ^ (n - 1) * m) x) &
obua@17694
  2307
(diffl g m x --> diffl (%x::real. exp (g x)) (exp (g x) * m) x) &
obua@17694
  2308
(diffl g m x --> diffl (%x::real. sin (g x)) (cos (g x) * m) x) &
obua@17694
  2309
(diffl g m x --> diffl (%x::real. cos (g x)) (- sin (g x) * m) x)"
skalberg@14516
  2310
  by (import transc DIFF_COMPOSITE)
skalberg@14516
  2311
obua@17652
  2312
lemma EXP_0: "exp 0 = 1"
skalberg@14516
  2313
  by (import transc EXP_0)
skalberg@14516
  2314
obua@17652
  2315
lemma EXP_LE_X: "ALL x>=0. 1 + x <= exp x"
skalberg@14516
  2316
  by (import transc EXP_LE_X)
skalberg@14516
  2317
obua@17652
  2318
lemma EXP_LT_1: "ALL x>0. 1 < exp x"
skalberg@14516
  2319
  by (import transc EXP_LT_1)
skalberg@14516
  2320
obua@17644
  2321
lemma EXP_ADD_MUL: "ALL (x::real) y::real. exp (x + y) * exp (- x) = exp y"
skalberg@14516
  2322
  by (import transc EXP_ADD_MUL)
skalberg@14516
  2323
obua@17652
  2324
lemma EXP_NEG_MUL: "ALL x::real. exp x * exp (- x) = 1"
skalberg@14516
  2325
  by (import transc EXP_NEG_MUL)
skalberg@14516
  2326
obua@17652
  2327
lemma EXP_NEG_MUL2: "ALL x::real. exp (- x) * exp x = 1"
skalberg@14516
  2328
  by (import transc EXP_NEG_MUL2)
skalberg@14516
  2329
obua@17644
  2330
lemma EXP_NEG: "ALL x::real. exp (- x) = inverse (exp x)"
skalberg@14516
  2331
  by (import transc EXP_NEG)
skalberg@14516
  2332
obua@17644
  2333
lemma EXP_ADD: "ALL (x::real) y::real. exp (x + y) = exp x * exp y"
skalberg@14516
  2334
  by (import transc EXP_ADD)
skalberg@14516
  2335
obua@17652
  2336
lemma EXP_POS_LE: "ALL x::real. 0 <= exp x"
skalberg@14516
  2337
  by (import transc EXP_POS_LE)
skalberg@14516
  2338
obua@17652
  2339
lemma EXP_NZ: "ALL x::real. exp x ~= 0"
skalberg@14516
  2340
  by (import transc EXP_NZ)
skalberg@14516
  2341
obua@17652
  2342
lemma EXP_POS_LT: "ALL x::real. 0 < exp x"
skalberg@14516
  2343
  by (import transc EXP_POS_LT)
skalberg@14516
  2344
obua@17644
  2345
lemma EXP_N: "ALL (n::nat) x::real. exp (real n * x) = exp x ^ n"
skalberg@14516
  2346
  by (import transc EXP_N)
skalberg@14516
  2347
obua@17644
  2348
lemma EXP_SUB: "ALL (x::real) y::real. exp (x - y) = exp x / exp y"
skalberg@14516
  2349
  by (import transc EXP_SUB)
skalberg@14516
  2350
obua@17694
  2351
lemma EXP_MONO_IMP: "ALL (x::real) y::real. x < y --> exp x < exp y"
skalberg@14516
  2352
  by (import transc EXP_MONO_IMP)
skalberg@14516
  2353
obua@17644
  2354
lemma EXP_MONO_LT: "ALL (x::real) y::real. (exp x < exp y) = (x < y)"
skalberg@14516
  2355
  by (import transc EXP_MONO_LT)
skalberg@14516
  2356
obua@17644
  2357
lemma EXP_MONO_LE: "ALL (x::real) y::real. (exp x <= exp y) = (x <= y)"
skalberg@14516
  2358
  by (import transc EXP_MONO_LE)
skalberg@14516
  2359
obua@17644
  2360
lemma EXP_INJ: "ALL (x::real) y::real. (exp x = exp y) = (x = y)"
skalberg@14516
  2361
  by (import transc EXP_INJ)
skalberg@14516
  2362
obua@17652
  2363
lemma EXP_TOTAL_LEMMA: "ALL y>=1. EX x>=0. x <= y - 1 & exp x = y"
skalberg@14516
  2364
  by (import transc EXP_TOTAL_LEMMA)
skalberg@14516
  2365
obua@17652
  2366
lemma EXP_TOTAL: "ALL y>0. EX x::real. exp x = y"
skalberg@14516
  2367
  by (import transc EXP_TOTAL)
skalberg@14516
  2368
skalberg@14516
  2369
constdefs
skalberg@14516
  2370
  ln :: "real => real" 
obua@17644
  2371
  "ln == %x::real. SOME u::real. exp u = x"
obua@17644
  2372
obua@17644
  2373
lemma ln: "ALL x::real. ln x = (SOME u::real. exp u = x)"
skalberg@14516
  2374
  by (import transc ln)
skalberg@14516
  2375
obua@17644
  2376
lemma LN_EXP: "ALL x::real. ln (exp x) = x"
skalberg@14516
  2377
  by (import transc LN_EXP)
skalberg@14516
  2378
obua@17652
  2379
lemma EXP_LN: "ALL x::real. (exp (ln x) = x) = (0 < x)"
skalberg@14516
  2380
  by (import transc EXP_LN)
skalberg@14516
  2381
obua@17694
  2382
lemma LN_MUL: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x * y) = ln x + ln y"
skalberg@14516
  2383
  by (import transc LN_MUL)
skalberg@14516
  2384
obua@17694
  2385
lemma LN_INJ: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x = ln y) = (x = y)"
skalberg@14516
  2386
  by (import transc LN_INJ)
skalberg@14516
  2387
obua@17652
  2388
lemma LN_1: "ln 1 = 0"
skalberg@14516
  2389
  by (import transc LN_1)
skalberg@14516
  2390
obua@17652
  2391
lemma LN_INV: "ALL x>0. ln (inverse x) = - ln x"
skalberg@14516
  2392
  by (import transc LN_INV)
skalberg@14516
  2393
obua@17694
  2394
lemma LN_DIV: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x / y) = ln x - ln y"
skalberg@14516
  2395
  by (import transc LN_DIV)
skalberg@14516
  2396
obua@17694
  2397
lemma LN_MONO_LT: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x < ln y) = (x < y)"
skalberg@14516
  2398
  by (import transc LN_MONO_LT)
skalberg@14516
  2399
obua@17694
  2400
lemma LN_MONO_LE: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x <= ln y) = (x <= y)"
skalberg@14516
  2401
  by (import transc LN_MONO_LE)
skalberg@14516
  2402
obua@17694
  2403
lemma LN_POW: "ALL (n::nat) x::real. 0 < x --> ln (x ^ n) = real n * ln x"
skalberg@14516
  2404
  by (import transc LN_POW)
skalberg@14516
  2405
obua@17652
  2406
lemma LN_LE: "ALL x>=0. ln (1 + x) <= x"
skalberg@14516
  2407
  by (import transc LN_LE)
skalberg@14516
  2408
obua@17652
  2409
lemma LN_LT_X: "ALL x>0. ln x < x"
skalberg@14516
  2410
  by (import transc LN_LT_X)
skalberg@14516
  2411
obua@17652
  2412
lemma LN_POS: "ALL x>=1. 0 <= ln x"
skalberg@14516
  2413
  by (import transc LN_POS)
skalberg@14516
  2414
skalberg@14516
  2415
constdefs
skalberg@14516
  2416
  root :: "nat => real => real" 
obua@17694
  2417
  "root == %(n::nat) x::real. SOME u::real. (0 < x --> 0 < u) & u ^ n = x"
obua@17694
  2418
obua@17694
  2419
lemma root: "ALL (n::nat) x::real.
obua@17694
  2420
   root n x = (SOME u::real. (0 < x --> 0 < u) & u ^ n = x)"
skalberg@14516
  2421
  by (import transc root)
skalberg@14516
  2422
skalberg@14516
  2423
constdefs
skalberg@14516
  2424
  sqrt :: "real => real" 
obua@17652
  2425
  "sqrt == root 2"
obua@17652
  2426
obua@17652
  2427
lemma sqrt: "ALL x::real. sqrt x = root 2 x"
skalberg@14516
  2428
  by (import transc sqrt)
skalberg@14516
  2429
obua@17694
  2430
lemma ROOT_LT_LEMMA: "ALL (n::nat) x::real. 0 < x --> exp (ln x / real (Suc n)) ^ Suc n = x"
skalberg@14516
  2431
  by (import transc ROOT_LT_LEMMA)
skalberg@14516
  2432
obua@17694
  2433
lemma ROOT_LN: "ALL (n::nat) x::real. 0 < x --> root (Suc n) x = exp (ln x / real (Suc n))"
skalberg@14516
  2434
  by (import transc ROOT_LN)
skalberg@14516
  2435
obua@17652
  2436
lemma ROOT_0: "ALL n::nat. root (Suc n) 0 = 0"
skalberg@14516
  2437
  by (import transc ROOT_0)
skalberg@14516
  2438
obua@17652
  2439
lemma ROOT_1: "ALL n::nat. root (Suc n) 1 = 1"
skalberg@14516
  2440
  by (import transc ROOT_1)
skalberg@14516
  2441
obua@17694
  2442
lemma ROOT_POS_LT: "ALL (n::nat) x::real. 0 < x --> 0 < root (Suc n) x"
skalberg@14516
  2443
  by (import transc ROOT_POS_LT)
skalberg@14516
  2444
obua@17694
  2445
lemma ROOT_POW_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) x ^ Suc n = x"
skalberg@14516
  2446
  by (import transc ROOT_POW_POS)
skalberg@14516
  2447
obua@17694
  2448
lemma POW_ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) (x ^ Suc n) = x"
skalberg@14516
  2449
  by (import transc POW_ROOT_POS)
skalberg@14516
  2450
obua@17694
  2451
lemma ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> 0 <= root (Suc n) x"
skalberg@14516
  2452
  by (import transc ROOT_POS)
skalberg@14516
  2453
obua@17694
  2454
lemma ROOT_POS_UNIQ: "ALL (n::nat) (x::real) y::real.
obua@17694
  2455
   0 <= x & 0 <= y & y ^ Suc n = x --> root (Suc n) x = y"
skalberg@14516
  2456
  by (import transc ROOT_POS_UNIQ)
skalberg@14516
  2457
obua@17694
  2458
lemma ROOT_MUL: "ALL (n::nat) (x::real) y::real.
obua@17694
  2459
   0 <= x & 0 <= y -->
obua@17694
  2460
   root (Suc n) (x * y) = root (Suc n) x * root (Suc n) y"
skalberg@14516
  2461
  by (import transc ROOT_MUL)
skalberg@14516
  2462
obua@17694
  2463
lemma ROOT_INV: "ALL (n::nat) x::real.
obua@17694
  2464
   0 <= x --> root (Suc n) (inverse x) = inverse (root (Suc n) x)"
skalberg@14516
  2465
  by (import transc ROOT_INV)
skalberg@14516
  2466
obua@17694
  2467
lemma ROOT_DIV: "ALL (x::nat) (xa::real) xb::real.
obua@17694
  2468
   0 <= xa & 0 <= xb -->
obua@17694
  2469
   root (Suc x) (xa / xb) = root (Suc x) xa / root (Suc x) xb"
skalberg@14516
  2470
  by (import transc ROOT_DIV)
skalberg@14516
  2471
obua@17694
  2472
lemma ROOT_MONO_LE: "ALL (x::real) y::real.
obua@17694
  2473
   0 <= x & x <= y --> root (Suc (n::nat)) x <= root (Suc n) y"
skalberg@14516
  2474
  by (import transc ROOT_MONO_LE)
skalberg@14516
  2475
obua@17652
  2476
lemma SQRT_0: "sqrt 0 = 0"
skalberg@14516
  2477
  by (import transc SQRT_0)
skalberg@14516
  2478
obua@17652
  2479
lemma SQRT_1: "sqrt 1 = 1"
skalberg@14516
  2480
  by (import transc SQRT_1)
skalberg@14516
  2481
obua@17652
  2482
lemma SQRT_POS_LT: "ALL x>0. 0 < sqrt x"
skalberg@14516
  2483
  by (import transc SQRT_POS_LT)
skalberg@14516
  2484
obua@17652
  2485
lemma SQRT_POS_LE: "ALL x>=0. 0 <= sqrt x"
skalberg@14516
  2486
  by (import transc SQRT_POS_LE)
skalberg@14516
  2487
obua@17652
  2488
lemma SQRT_POW2: "ALL x::real. (sqrt x ^ 2 = x) = (0 <= x)"
skalberg@14516
  2489
  by (import transc SQRT_POW2)
skalberg@14516
  2490
obua@17652
  2491
lemma SQRT_POW_2: "ALL x>=0. sqrt x ^ 2 = x"
skalberg@14516
  2492
  by (import transc SQRT_POW_2)
skalberg@14516
  2493
obua@17694
  2494
lemma POW_2_SQRT: "0 <= (x::real) --> sqrt (x ^ 2) = x"
skalberg@14516
  2495
  by (import transc POW_2_SQRT)
skalberg@14516
  2496
obua@17694
  2497
lemma SQRT_POS_UNIQ: "ALL (x::real) xa::real. 0 <= x & 0 <= xa & xa ^ 2 = x --> sqrt x = xa"
skalberg@14516
  2498
  by (import transc SQRT_POS_UNIQ)
skalberg@14516
  2499
obua@17694
  2500
lemma SQRT_MUL: "ALL (x::real) xa::real.
obua@17694
  2501
   0 <= x & 0 <= xa --> sqrt (x * xa) = sqrt x * sqrt xa"
skalberg@14516
  2502
  by (import transc SQRT_MUL)
skalberg@14516
  2503
obua@17652
  2504
lemma SQRT_INV: "ALL x>=0. sqrt (inverse x) = inverse (sqrt x)"
skalberg@14516
  2505
  by (import transc SQRT_INV)
skalberg@14516
  2506
obua@17694
  2507
lemma SQRT_DIV: "ALL (x::real) xa::real.
obua@17694
  2508
   0 <= x & 0 <= xa --> sqrt (x / xa) = sqrt x / sqrt xa"
skalberg@14516
  2509
  by (import transc SQRT_DIV)
skalberg@14516
  2510
obua@17694
  2511
lemma SQRT_MONO_LE: "ALL (x::real) xa::real. 0 <= x & x <= xa --> sqrt x <= sqrt xa"
skalberg@14516
  2512
  by (import transc SQRT_MONO_LE)
skalberg@14516
  2513
obua@17694
  2514
lemma SQRT_EVEN_POW2: "ALL n::nat. EVEN n --> sqrt (2 ^ n) = 2 ^ (n div 2)"
skalberg@14516
  2515
  by (import transc SQRT_EVEN_POW2)
skalberg@14516
  2516
obua@17652
  2517
lemma REAL_DIV_SQRT: "ALL x>=0. x / sqrt x = sqrt x"
skalberg@14516
  2518
  by (import transc REAL_DIV_SQRT)
skalberg@14516
  2519
obua@17694
  2520
lemma SQRT_EQ: "ALL (x::real) y::real. x ^ 2 = y & 0 <= x --> x = sqrt y"
skalberg@14516
  2521
  by (import transc SQRT_EQ)
skalberg@14516
  2522
obua@17652
  2523
lemma SIN_0: "sin 0 = 0"
skalberg@14516
  2524
  by (import transc SIN_0)
skalberg@14516
  2525
obua@17652
  2526
lemma COS_0: "cos 0 = 1"
skalberg@14516
  2527
  by (import transc COS_0)
skalberg@14516
  2528
obua@17652
  2529
lemma SIN_CIRCLE: "ALL x::real. sin x ^ 2 + cos x ^ 2 = 1"
skalberg@14516
  2530
  by (import transc SIN_CIRCLE)
skalberg@14516
  2531
obua@17652
  2532
lemma SIN_BOUND: "ALL x::real. abs (sin x) <= 1"
skalberg@14516
  2533
  by (import transc SIN_BOUND)
skalberg@14516
  2534
obua@17652
  2535
lemma SIN_BOUNDS: "ALL x::real. - 1 <= sin x & sin x <= 1"
skalberg@14516
  2536
  by (import transc SIN_BOUNDS)
skalberg@14516
  2537
obua@17652
  2538
lemma COS_BOUND: "ALL x::real. abs (cos x) <= 1"
skalberg@14516
  2539
  by (import transc COS_BOUND)
skalberg@14516
  2540
obua@17652
  2541
lemma COS_BOUNDS: "ALL x::real. - 1 <= cos x & cos x <= 1"
skalberg@14516
  2542
  by (import transc COS_BOUNDS)
skalberg@14516
  2543
obua@17644
  2544
lemma SIN_COS_ADD: "ALL (x::real) y::real.
skalberg@14516
  2545
   (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
skalberg@14516
  2546
   (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 =
obua@17652
  2547
   0"
skalberg@14516
  2548
  by (import transc SIN_COS_ADD)
skalberg@14516
  2549
obua@17652
  2550
lemma SIN_COS_NEG: "ALL x::real. (sin (- x) + sin x) ^ 2 + (cos (- x) - cos x) ^ 2 = 0"
skalberg@14516
  2551
  by (import transc SIN_COS_NEG)
skalberg@14516
  2552
obua@17644
  2553
lemma SIN_ADD: "ALL (x::real) y::real. sin (x + y) = sin x * cos y + cos x * sin y"
skalberg@14516
  2554
  by (import transc SIN_ADD)
skalberg@14516
  2555
obua@17644
  2556
lemma COS_ADD: "ALL (x::real) y::real. cos (x + y) = cos x * cos y - sin x * sin y"
skalberg@14516
  2557
  by (import transc COS_ADD)
skalberg@14516
  2558
obua@17644
  2559
lemma SIN_NEG: "ALL x::real. sin (- x) = - sin x"
skalberg@14516
  2560
  by (import transc SIN_NEG)
skalberg@14516
  2561
obua@17644
  2562
lemma COS_NEG: "ALL x::real. cos (- x) = cos x"
skalberg@14516
  2563
  by (import transc COS_NEG)
skalberg@14516
  2564
obua@17652
  2565
lemma SIN_DOUBLE: "ALL x::real. sin (2 * x) = 2 * (sin x * cos x)"
skalberg@14516
  2566
  by (import transc SIN_DOUBLE)
skalberg@14516
  2567
obua@17652
  2568
lemma COS_DOUBLE: "ALL x::real. cos (2 * x) = cos x ^ 2 - sin x ^ 2"
skalberg@14516
  2569
  by (import transc COS_DOUBLE)
skalberg@14516
  2570
obua@17644
  2571
lemma SIN_PAIRED: "ALL x::real.
obua@17652
  2572
   sums (%n::nat. (- 1) ^ n / real (FACT (2 * n + 1)) * x ^ (2 * n + 1))
obua@17644
  2573
    (sin x)"
skalberg@14516
  2574
  by (import transc SIN_PAIRED)
skalberg@14516
  2575
obua@17694
  2576
lemma SIN_POS: "ALL x::real. 0 < x & x < 2 --> 0 < sin x"
skalberg@14516
  2577
  by (import transc SIN_POS)
skalberg@14516
  2578
obua@17644
  2579
lemma COS_PAIRED: "ALL x::real.
obua@17652
  2580
   sums (%n::nat. (- 1) ^ n / real (FACT (2 * n)) * x ^ (2 * n)) (cos x)"
skalberg@14516
  2581
  by (import transc COS_PAIRED)
skalberg@14516
  2582
obua@17652
  2583
lemma COS_2: "cos 2 < 0"
skalberg@14516
  2584
  by (import transc COS_2)
skalberg@14516
  2585
obua@17652
  2586
lemma COS_ISZERO: "EX! x::real. 0 <= x & x <= 2 & cos x = 0"
skalberg@14516
  2587
  by (import transc COS_ISZERO)
skalberg@14516
  2588
skalberg@14516
  2589
constdefs
skalberg@14516
  2590
  pi :: "real" 
obua@17652
  2591
  "pi == 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
obua@17652
  2592
obua@17652
  2593
lemma pi: "pi = 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
skalberg@14516
  2594
  by (import transc pi)
skalberg@14516
  2595
obua@17652
  2596
lemma PI2: "pi / 2 = (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
skalberg@14516
  2597
  by (import transc PI2)
skalberg@14516
  2598
obua@17652
  2599
lemma COS_PI2: "cos (pi / 2) = 0"
skalberg@14516
  2600
  by (import transc COS_PI2)
skalberg@14516
  2601
obua@17652
  2602
lemma PI2_BOUNDS: "0 < pi / 2 & pi / 2 < 2"
skalberg@14516
  2603
  by (import transc PI2_BOUNDS)
skalberg@14516
  2604
obua@17652
  2605
lemma PI_POS: "0 < pi"
skalberg@14516
  2606
  by (import transc PI_POS)
skalberg@14516
  2607
obua@17652
  2608
lemma SIN_PI2: "sin (pi / 2) = 1"
skalberg@14516
  2609
  by (import transc SIN_PI2)