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
     1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     2 
     3 theory HOL4Real imports HOL4Base begin
     4 
     5 ;setup_theory realax
     6 
     7 lemma HREAL_RDISTRIB: "ALL (x::hreal) (y::hreal) z::hreal.
     8    hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"
     9   by (import realax HREAL_RDISTRIB)
    10 
    11 lemma HREAL_EQ_ADDL: "ALL (x::hreal) y::hreal. x ~= hreal_add x y"
    12   by (import realax HREAL_EQ_ADDL)
    13 
    14 lemma HREAL_EQ_LADD: "ALL (x::hreal) (y::hreal) z::hreal.
    15    (hreal_add x y = hreal_add x z) = (y = z)"
    16   by (import realax HREAL_EQ_LADD)
    17 
    18 lemma HREAL_LT_REFL: "ALL x::hreal. ~ hreal_lt x x"
    19   by (import realax HREAL_LT_REFL)
    20 
    21 lemma HREAL_LT_ADDL: "ALL (x::hreal) y::hreal. hreal_lt x (hreal_add x y)"
    22   by (import realax HREAL_LT_ADDL)
    23 
    24 lemma HREAL_LT_NE: "ALL (x::hreal) y::hreal. hreal_lt x y --> x ~= y"
    25   by (import realax HREAL_LT_NE)
    26 
    27 lemma HREAL_LT_ADDR: "ALL (x::hreal) y::hreal. ~ hreal_lt (hreal_add x y) x"
    28   by (import realax HREAL_LT_ADDR)
    29 
    30 lemma HREAL_LT_GT: "ALL (x::hreal) y::hreal. hreal_lt x y --> ~ hreal_lt y x"
    31   by (import realax HREAL_LT_GT)
    32 
    33 lemma HREAL_LT_ADD2: "ALL (x1::hreal) (x2::hreal) (y1::hreal) y2::hreal.
    34    hreal_lt x1 y1 & hreal_lt x2 y2 -->
    35    hreal_lt (hreal_add x1 x2) (hreal_add y1 y2)"
    36   by (import realax HREAL_LT_ADD2)
    37 
    38 lemma HREAL_LT_LADD: "ALL (x::hreal) (y::hreal) z::hreal.
    39    hreal_lt (hreal_add x y) (hreal_add x z) = hreal_lt y z"
    40   by (import realax HREAL_LT_LADD)
    41 
    42 constdefs
    43   treal_0 :: "hreal * hreal" 
    44   "treal_0 == (hreal_1, hreal_1)"
    45 
    46 lemma treal_0: "treal_0 = (hreal_1, hreal_1)"
    47   by (import realax treal_0)
    48 
    49 constdefs
    50   treal_1 :: "hreal * hreal" 
    51   "treal_1 == (hreal_add hreal_1 hreal_1, hreal_1)"
    52 
    53 lemma treal_1: "treal_1 = (hreal_add hreal_1 hreal_1, hreal_1)"
    54   by (import realax treal_1)
    55 
    56 constdefs
    57   treal_neg :: "hreal * hreal => hreal * hreal" 
    58   "treal_neg == %(x::hreal, y::hreal). (y, x)"
    59 
    60 lemma treal_neg: "ALL (x::hreal) y::hreal. treal_neg (x, y) = (y, x)"
    61   by (import realax treal_neg)
    62 
    63 constdefs
    64   treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" 
    65   "treal_add ==
    66 %(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
    67    (hreal_add x1 x2, hreal_add y1 y2)"
    68 
    69 lemma treal_add: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
    70    treal_add (x1, y1) (x2, y2) = (hreal_add x1 x2, hreal_add y1 y2)"
    71   by (import realax treal_add)
    72 
    73 constdefs
    74   treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" 
    75   "treal_mul ==
    76 %(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
    77    (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
    78     hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
    79 
    80 lemma treal_mul: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
    81    treal_mul (x1, y1) (x2, y2) =
    82    (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
    83     hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
    84   by (import realax treal_mul)
    85 
    86 constdefs
    87   treal_lt :: "hreal * hreal => hreal * hreal => bool" 
    88   "treal_lt ==
    89 %(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
    90    hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
    91 
    92 lemma treal_lt: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
    93    treal_lt (x1, y1) (x2, y2) = hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
    94   by (import realax treal_lt)
    95 
    96 constdefs
    97   treal_inv :: "hreal * hreal => hreal * hreal" 
    98   "treal_inv ==
    99 %(x::hreal, y::hreal).
   100    if x = y then treal_0
   101    else if hreal_lt y x
   102         then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
   103         else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1)"
   104 
   105 lemma treal_inv: "ALL (x::hreal) y::hreal.
   106    treal_inv (x, y) =
   107    (if x = y then treal_0
   108     else if hreal_lt y x
   109          then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
   110          else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1))"
   111   by (import realax treal_inv)
   112 
   113 constdefs
   114   treal_eq :: "hreal * hreal => hreal * hreal => bool" 
   115   "treal_eq ==
   116 %(x1::hreal, y1::hreal) (x2::hreal, y2::hreal).
   117    hreal_add x1 y2 = hreal_add x2 y1"
   118 
   119 lemma treal_eq: "ALL (x1::hreal) (y1::hreal) (x2::hreal) y2::hreal.
   120    treal_eq (x1, y1) (x2, y2) = (hreal_add x1 y2 = hreal_add x2 y1)"
   121   by (import realax treal_eq)
   122 
   123 lemma TREAL_EQ_REFL: "ALL x::hreal * hreal. treal_eq x x"
   124   by (import realax TREAL_EQ_REFL)
   125 
   126 lemma TREAL_EQ_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_eq x y = treal_eq y x"
   127   by (import realax TREAL_EQ_SYM)
   128 
   129 lemma TREAL_EQ_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   130    treal_eq x y & treal_eq y z --> treal_eq x z"
   131   by (import realax TREAL_EQ_TRANS)
   132 
   133 lemma TREAL_EQ_EQUIV: "ALL (p::hreal * hreal) q::hreal * hreal.
   134    treal_eq p q = (treal_eq p = treal_eq q)"
   135   by (import realax TREAL_EQ_EQUIV)
   136 
   137 lemma TREAL_EQ_AP: "ALL (p::hreal * hreal) q::hreal * hreal. p = q --> treal_eq p q"
   138   by (import realax TREAL_EQ_AP)
   139 
   140 lemma TREAL_10: "~ treal_eq treal_1 treal_0"
   141   by (import realax TREAL_10)
   142 
   143 lemma TREAL_ADD_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_add x y = treal_add y x"
   144   by (import realax TREAL_ADD_SYM)
   145 
   146 lemma TREAL_MUL_SYM: "ALL (x::hreal * hreal) y::hreal * hreal. treal_mul x y = treal_mul y x"
   147   by (import realax TREAL_MUL_SYM)
   148 
   149 lemma TREAL_ADD_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   150    treal_add x (treal_add y z) = treal_add (treal_add x y) z"
   151   by (import realax TREAL_ADD_ASSOC)
   152 
   153 lemma TREAL_MUL_ASSOC: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   154    treal_mul x (treal_mul y z) = treal_mul (treal_mul x y) z"
   155   by (import realax TREAL_MUL_ASSOC)
   156 
   157 lemma TREAL_LDISTRIB: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   158    treal_mul x (treal_add y z) = treal_add (treal_mul x y) (treal_mul x z)"
   159   by (import realax TREAL_LDISTRIB)
   160 
   161 lemma TREAL_ADD_LID: "ALL x::hreal * hreal. treal_eq (treal_add treal_0 x) x"
   162   by (import realax TREAL_ADD_LID)
   163 
   164 lemma TREAL_MUL_LID: "ALL x::hreal * hreal. treal_eq (treal_mul treal_1 x) x"
   165   by (import realax TREAL_MUL_LID)
   166 
   167 lemma TREAL_ADD_LINV: "ALL x::hreal * hreal. treal_eq (treal_add (treal_neg x) x) treal_0"
   168   by (import realax TREAL_ADD_LINV)
   169 
   170 lemma TREAL_INV_0: "treal_eq (treal_inv treal_0) treal_0"
   171   by (import realax TREAL_INV_0)
   172 
   173 lemma TREAL_MUL_LINV: "ALL x::hreal * hreal.
   174    ~ treal_eq x treal_0 --> treal_eq (treal_mul (treal_inv x) x) treal_1"
   175   by (import realax TREAL_MUL_LINV)
   176 
   177 lemma TREAL_LT_TOTAL: "ALL (x::hreal * hreal) y::hreal * hreal.
   178    treal_eq x y | treal_lt x y | treal_lt y x"
   179   by (import realax TREAL_LT_TOTAL)
   180 
   181 lemma TREAL_LT_REFL: "ALL x::hreal * hreal. ~ treal_lt x x"
   182   by (import realax TREAL_LT_REFL)
   183 
   184 lemma TREAL_LT_TRANS: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   185    treal_lt x y & treal_lt y z --> treal_lt x z"
   186   by (import realax TREAL_LT_TRANS)
   187 
   188 lemma TREAL_LT_ADD: "ALL (x::hreal * hreal) (y::hreal * hreal) z::hreal * hreal.
   189    treal_lt y z --> treal_lt (treal_add x y) (treal_add x z)"
   190   by (import realax TREAL_LT_ADD)
   191 
   192 lemma TREAL_LT_MUL: "ALL (x::hreal * hreal) y::hreal * hreal.
   193    treal_lt treal_0 x & treal_lt treal_0 y -->
   194    treal_lt treal_0 (treal_mul x y)"
   195   by (import realax TREAL_LT_MUL)
   196 
   197 constdefs
   198   treal_of_hreal :: "hreal => hreal * hreal" 
   199   "treal_of_hreal == %x::hreal. (hreal_add x hreal_1, hreal_1)"
   200 
   201 lemma treal_of_hreal: "ALL x::hreal. treal_of_hreal x = (hreal_add x hreal_1, hreal_1)"
   202   by (import realax treal_of_hreal)
   203 
   204 constdefs
   205   hreal_of_treal :: "hreal * hreal => hreal" 
   206   "hreal_of_treal == %(x::hreal, y::hreal). SOME d::hreal. x = hreal_add y d"
   207 
   208 lemma hreal_of_treal: "ALL (x::hreal) y::hreal.
   209    hreal_of_treal (x, y) = (SOME d::hreal. x = hreal_add y d)"
   210   by (import realax hreal_of_treal)
   211 
   212 lemma TREAL_BIJ: "(ALL h::hreal. hreal_of_treal (treal_of_hreal h) = h) &
   213 (ALL r::hreal * hreal.
   214     treal_lt treal_0 r = treal_eq (treal_of_hreal (hreal_of_treal r)) r)"
   215   by (import realax TREAL_BIJ)
   216 
   217 lemma TREAL_ISO: "ALL (h::hreal) i::hreal.
   218    hreal_lt h i --> treal_lt (treal_of_hreal h) (treal_of_hreal i)"
   219   by (import realax TREAL_ISO)
   220 
   221 lemma TREAL_BIJ_WELLDEF: "ALL (h::hreal * hreal) i::hreal * hreal.
   222    treal_eq h i --> hreal_of_treal h = hreal_of_treal i"
   223   by (import realax TREAL_BIJ_WELLDEF)
   224 
   225 lemma TREAL_NEG_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal.
   226    treal_eq x1 x2 --> treal_eq (treal_neg x1) (treal_neg x2)"
   227   by (import realax TREAL_NEG_WELLDEF)
   228 
   229 lemma TREAL_ADD_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
   230    treal_eq x1 x2 --> treal_eq (treal_add x1 y) (treal_add x2 y)"
   231   by (import realax TREAL_ADD_WELLDEFR)
   232 
   233 lemma TREAL_ADD_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
   234    y2::hreal * hreal.
   235    treal_eq x1 x2 & treal_eq y1 y2 -->
   236    treal_eq (treal_add x1 y1) (treal_add x2 y2)"
   237   by (import realax TREAL_ADD_WELLDEF)
   238 
   239 lemma TREAL_MUL_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
   240    treal_eq x1 x2 --> treal_eq (treal_mul x1 y) (treal_mul x2 y)"
   241   by (import realax TREAL_MUL_WELLDEFR)
   242 
   243 lemma TREAL_MUL_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
   244    y2::hreal * hreal.
   245    treal_eq x1 x2 & treal_eq y1 y2 -->
   246    treal_eq (treal_mul x1 y1) (treal_mul x2 y2)"
   247   by (import realax TREAL_MUL_WELLDEF)
   248 
   249 lemma TREAL_LT_WELLDEFR: "ALL (x1::hreal * hreal) (x2::hreal * hreal) y::hreal * hreal.
   250    treal_eq x1 x2 --> treal_lt x1 y = treal_lt x2 y"
   251   by (import realax TREAL_LT_WELLDEFR)
   252 
   253 lemma TREAL_LT_WELLDEFL: "ALL (x::hreal * hreal) (y1::hreal * hreal) y2::hreal * hreal.
   254    treal_eq y1 y2 --> treal_lt x y1 = treal_lt x y2"
   255   by (import realax TREAL_LT_WELLDEFL)
   256 
   257 lemma TREAL_LT_WELLDEF: "ALL (x1::hreal * hreal) (x2::hreal * hreal) (y1::hreal * hreal)
   258    y2::hreal * hreal.
   259    treal_eq x1 x2 & treal_eq y1 y2 --> treal_lt x1 y1 = treal_lt x2 y2"
   260   by (import realax TREAL_LT_WELLDEF)
   261 
   262 lemma TREAL_INV_WELLDEF: "ALL (x1::hreal * hreal) x2::hreal * hreal.
   263    treal_eq x1 x2 --> treal_eq (treal_inv x1) (treal_inv x2)"
   264   by (import realax TREAL_INV_WELLDEF)
   265 
   266 ;end_setup
   267 
   268 ;setup_theory real
   269 
   270 lemma REAL_0: "(op =::real => real => bool) (0::real) (0::real)"
   271   by (import real REAL_0)
   272 
   273 lemma REAL_1: "(op =::real => real => bool) (1::real) (1::real)"
   274   by (import real REAL_1)
   275 
   276 lemma REAL_ADD_LID_UNIQ: "ALL (x::real) y::real. (x + y = y) = (x = 0)"
   277   by (import real REAL_ADD_LID_UNIQ)
   278 
   279 lemma REAL_ADD_RID_UNIQ: "ALL (x::real) y::real. (x + y = x) = (y = 0)"
   280   by (import real REAL_ADD_RID_UNIQ)
   281 
   282 lemma REAL_LNEG_UNIQ: "ALL (x::real) y::real. (x + y = 0) = (x = - y)"
   283   by (import real REAL_LNEG_UNIQ)
   284 
   285 lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)"
   286   by (import real REAL_LT_ANTISYM)
   287 
   288 lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x"
   289   by (import real REAL_LTE_TOTAL)
   290 
   291 lemma REAL_LET_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y <= x)"
   292   by (import real REAL_LET_ANTISYM)
   293 
   294 lemma REAL_LTE_ANTSYM: "ALL (x::real) y::real. ~ (x <= y & y < x)"
   295   by (import real REAL_LTE_ANTSYM)
   296 
   297 lemma REAL_LT_NEGTOTAL: "ALL x::real. x = 0 | 0 < x | 0 < - x"
   298   by (import real REAL_LT_NEGTOTAL)
   299 
   300 lemma REAL_LE_NEGTOTAL: "ALL x::real. 0 <= x | 0 <= - x"
   301   by (import real REAL_LE_NEGTOTAL)
   302 
   303 lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)"
   304   by (import real REAL_LT_ADDNEG)
   305 
   306 lemma REAL_LT_ADDNEG2: "ALL (x::real) (y::real) z::real. (x + - y < z) = (x < z + y)"
   307   by (import real REAL_LT_ADDNEG2)
   308 
   309 lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + 1"
   310   by (import real REAL_LT_ADD1)
   311 
   312 lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x"
   313   by (import real REAL_SUB_ADD2)
   314 
   315 lemma REAL_SUB_LT: "ALL (x::real) y::real. (0 < x - y) = (y < x)"
   316   by (import real REAL_SUB_LT)
   317 
   318 lemma REAL_SUB_LE: "ALL (x::real) y::real. (0 <= x - y) = (y <= x)"
   319   by (import real REAL_SUB_LE)
   320 
   321 lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y"
   322   by (import real REAL_ADD_SUB)
   323 
   324 lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)"
   325   by (import real REAL_NEG_EQ)
   326 
   327 lemma REAL_NEG_MINUS1: "ALL x::real. - x = - 1 * x"
   328   by (import real REAL_NEG_MINUS1)
   329 
   330 lemma REAL_LT_LMUL_0: "ALL (x::real) y::real. 0 < x --> (0 < x * y) = (0 < y)"
   331   by (import real REAL_LT_LMUL_0)
   332 
   333 lemma REAL_LT_RMUL_0: "ALL (x::real) y::real. 0 < y --> (0 < x * y) = (0 < x)"
   334   by (import real REAL_LT_RMUL_0)
   335 
   336 lemma REAL_LT_LMUL: "ALL (x::real) (y::real) z::real. 0 < x --> (x * y < x * z) = (y < z)"
   337   by (import real REAL_LT_LMUL)
   338 
   339 lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = 1 --> x = inverse y"
   340   by (import real REAL_LINV_UNIQ)
   341 
   342 lemma REAL_LE_INV: "(All::(real => bool) => bool)
   343  (%x::real.
   344      (op -->::bool => bool => bool)
   345       ((op <=::real => real => bool) (0::real) x)
   346       ((op <=::real => real => bool) (0::real) ((inverse::real => real) x)))"
   347   by (import real REAL_LE_INV)
   348 
   349 lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = (0 <= y)"
   350   by (import real REAL_LE_ADDR)
   351 
   352 lemma REAL_LE_ADDL: "ALL (x::real) y::real. (y <= x + y) = (0 <= x)"
   353   by (import real REAL_LE_ADDL)
   354 
   355 lemma REAL_LT_ADDR: "ALL (x::real) y::real. (x < x + y) = (0 < y)"
   356   by (import real REAL_LT_ADDR)
   357 
   358 lemma REAL_LT_ADDL: "ALL (x::real) y::real. (y < x + y) = (0 < x)"
   359   by (import real REAL_LT_ADDL)
   360 
   361 lemma REAL_LT_NZ: "ALL n::nat. (real n ~= 0) = (0 < real n)"
   362   by (import real REAL_LT_NZ)
   363 
   364 lemma REAL_NZ_IMP_LT: "ALL n::nat. n ~= 0 --> 0 < real n"
   365   by (import real REAL_NZ_IMP_LT)
   366 
   367 lemma REAL_LT_RDIV_0: "ALL (y::real) z::real. 0 < z --> (0 < y / z) = (0 < y)"
   368   by (import real REAL_LT_RDIV_0)
   369 
   370 lemma REAL_LT_RDIV: "ALL (x::real) (y::real) z::real. 0 < z --> (x / z < y / z) = (x < y)"
   371   by (import real REAL_LT_RDIV)
   372 
   373 lemma REAL_LT_FRACTION_0: "ALL (n::nat) d::real. n ~= 0 --> (0 < d / real n) = (0 < d)"
   374   by (import real REAL_LT_FRACTION_0)
   375 
   376 lemma REAL_LT_MULTIPLE: "ALL (x::nat) xa::real. 1 < x --> (xa < real x * xa) = (0 < xa)"
   377   by (import real REAL_LT_MULTIPLE)
   378 
   379 lemma REAL_LT_FRACTION: "ALL (n::nat) d::real. 1 < n --> (d / real n < d) = (0 < d)"
   380   by (import real REAL_LT_FRACTION)
   381 
   382 lemma REAL_LT_HALF2: "ALL d::real. (d / 2 < d) = (0 < d)"
   383   by (import real REAL_LT_HALF2)
   384 
   385 lemma REAL_DIV_LMUL: "ALL (x::real) y::real. y ~= 0 --> y * (x / y) = x"
   386   by (import real REAL_DIV_LMUL)
   387 
   388 lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= 0 --> x / y * y = x"
   389   by (import real REAL_DIV_RMUL)
   390 
   391 lemma REAL_DOWN: "(All::(real => bool) => bool)
   392  (%x::real.
   393      (op -->::bool => bool => bool)
   394       ((op <::real => real => bool) (0::real) x)
   395       ((Ex::(real => bool) => bool)
   396         (%xa::real.
   397             (op &::bool => bool => bool)
   398              ((op <::real => real => bool) (0::real) xa)
   399              ((op <::real => real => bool) xa x))))"
   400   by (import real REAL_DOWN)
   401 
   402 lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y"
   403   by (import real REAL_SUB_SUB)
   404 
   405 lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b - (c + d) = a - c + (b - d)"
   406   by (import real REAL_ADD2_SUB2)
   407 
   408 lemma REAL_SUB_LNEG: "ALL (x::real) y::real. - x - y = - (x + y)"
   409   by (import real REAL_SUB_LNEG)
   410 
   411 lemma REAL_SUB_NEG2: "ALL (x::real) y::real. - x - - y = y - x"
   412   by (import real REAL_SUB_NEG2)
   413 
   414 lemma REAL_SUB_TRIANGLE: "ALL (a::real) (b::real) c::real. a - b + (b - c) = a - c"
   415   by (import real REAL_SUB_TRIANGLE)
   416 
   417 lemma REAL_INV_MUL: "ALL (x::real) y::real.
   418    x ~= 0 & y ~= 0 --> inverse (x * y) = inverse x * inverse y"
   419   by (import real REAL_INV_MUL)
   420 
   421 lemma REAL_SUB_INV2: "ALL (x::real) y::real.
   422    x ~= 0 & y ~= 0 --> inverse x - inverse y = (y - x) / (x * y)"
   423   by (import real REAL_SUB_INV2)
   424 
   425 lemma REAL_SUB_SUB2: "ALL (x::real) y::real. x - (x - y) = y"
   426   by (import real REAL_SUB_SUB2)
   427 
   428 lemma REAL_ADD_SUB2: "ALL (x::real) y::real. x - (x + y) = - y"
   429   by (import real REAL_ADD_SUB2)
   430 
   431 lemma REAL_LE_MUL2: "ALL (x1::real) (x2::real) (y1::real) y2::real.
   432    0 <= x1 & 0 <= y1 & x1 <= x2 & y1 <= y2 --> x1 * y1 <= x2 * y2"
   433   by (import real REAL_LE_MUL2)
   434 
   435 lemma REAL_LE_DIV: "ALL (x::real) xa::real. 0 <= x & 0 <= xa --> 0 <= x / xa"
   436   by (import real REAL_LE_DIV)
   437 
   438 lemma REAL_LT_1: "ALL (x::real) y::real. 0 <= x & x < y --> x / y < 1"
   439   by (import real REAL_LT_1)
   440 
   441 lemma REAL_POS_NZ: "(All::(real => bool) => bool)
   442  (%x::real.
   443      (op -->::bool => bool => bool)
   444       ((op <::real => real => bool) (0::real) x)
   445       ((Not::bool => bool) ((op =::real => real => bool) x (0::real))))"
   446   by (import real REAL_POS_NZ)
   447 
   448 lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real. x ~= 0 & x * xa = x * xb --> xa = xb"
   449   by (import real REAL_EQ_LMUL_IMP)
   450 
   451 lemma REAL_FACT_NZ: "ALL n::nat. real (FACT n) ~= 0"
   452   by (import real REAL_FACT_NZ)
   453 
   454 lemma REAL_DIFFSQ: "ALL (x::real) y::real. (x + y) * (x - y) = x * x - y * y"
   455   by (import real REAL_DIFFSQ)
   456 
   457 lemma REAL_POASQ: "ALL x::real. (0 < x * x) = (x ~= 0)"
   458   by (import real REAL_POASQ)
   459 
   460 lemma REAL_SUMSQ: "ALL (x::real) y::real. (x * x + y * y = 0) = (x = 0 & y = 0)"
   461   by (import real REAL_SUMSQ)
   462 
   463 lemma REAL_DIV_MUL2: "ALL (x::real) z::real.
   464    x ~= 0 & z ~= 0 --> (ALL y::real. y / z = x * y / (x * z))"
   465   by (import real REAL_DIV_MUL2)
   466 
   467 lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b --> a <= (a + b) / 2"
   468   by (import real REAL_MIDDLE1)
   469 
   470 lemma REAL_MIDDLE2: "ALL (a::real) b::real. a <= b --> (a + b) / 2 <= b"
   471   by (import real REAL_MIDDLE2)
   472 
   473 lemma ABS_LT_MUL2: "ALL (w::real) (x::real) (y::real) z::real.
   474    abs w < y & abs x < z --> abs (w * x) < y * z"
   475   by (import real ABS_LT_MUL2)
   476 
   477 lemma ABS_REFL: "ALL x::real. (abs x = x) = (0 <= x)"
   478   by (import real ABS_REFL)
   479 
   480 lemma ABS_BETWEEN: "ALL (x::real) (y::real) d::real.
   481    (0 < d & x - d < y & y < x + d) = (abs (y - x) < d)"
   482   by (import real ABS_BETWEEN)
   483 
   484 lemma ABS_BOUND: "ALL (x::real) (y::real) d::real. abs (x - y) < d --> y < x + d"
   485   by (import real ABS_BOUND)
   486 
   487 lemma ABS_STILLNZ: "ALL (x::real) y::real. abs (x - y) < abs y --> x ~= 0"
   488   by (import real ABS_STILLNZ)
   489 
   490 lemma ABS_CASES: "ALL x::real. x = 0 | 0 < abs x"
   491   by (import real ABS_CASES)
   492 
   493 lemma ABS_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & abs (y - x) < z - x --> y < z"
   494   by (import real ABS_BETWEEN1)
   495 
   496 lemma ABS_SIGN: "ALL (x::real) y::real. abs (x - y) < y --> 0 < x"
   497   by (import real ABS_SIGN)
   498 
   499 lemma ABS_SIGN2: "ALL (x::real) y::real. abs (x - y) < - y --> x < 0"
   500   by (import real ABS_SIGN2)
   501 
   502 lemma ABS_CIRCLE: "ALL (x::real) (y::real) h::real.
   503    abs h < abs y - abs x --> abs (x + h) < abs y"
   504   by (import real ABS_CIRCLE)
   505 
   506 lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real.
   507    x0 < y0 & abs (x - x0) < (y0 - x0) / 2 & abs (y - y0) < (y0 - x0) / 2 -->
   508    x < y"
   509   by (import real ABS_BETWEEN2)
   510 
   511 lemma POW_PLUS1: "ALL e>0. ALL n::nat. 1 + real n * e <= (1 + e) ^ n"
   512   by (import real POW_PLUS1)
   513 
   514 lemma POW_M1: "(All::(nat => bool) => bool)
   515  (%n::nat.
   516      (op =::real => real => bool)
   517       ((abs::real => real)
   518         ((op ^::real => nat => real) ((uminus::real => real) (1::real)) n))
   519       (1::real))"
   520   by (import real POW_M1)
   521 
   522 lemma REAL_LE1_POW2: "(All::(real => bool) => bool)
   523  (%x::real.
   524      (op -->::bool => bool => bool)
   525       ((op <=::real => real => bool) (1::real) x)
   526       ((op <=::real => real => bool) (1::real)
   527         ((op ^::real => nat => real) x
   528           ((number_of::bin => nat)
   529             ((op BIT::bin => bit => bin)
   530               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   531               (bit.B0::bit))))))"
   532   by (import real REAL_LE1_POW2)
   533 
   534 lemma REAL_LT1_POW2: "(All::(real => bool) => bool)
   535  (%x::real.
   536      (op -->::bool => bool => bool)
   537       ((op <::real => real => bool) (1::real) x)
   538       ((op <::real => real => bool) (1::real)
   539         ((op ^::real => nat => real) x
   540           ((number_of::bin => nat)
   541             ((op BIT::bin => bit => bin)
   542               ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   543               (bit.B0::bit))))))"
   544   by (import real REAL_LT1_POW2)
   545 
   546 lemma POW_POS_LT: "ALL (x::real) n::nat. 0 < x --> 0 < x ^ Suc n"
   547   by (import real POW_POS_LT)
   548 
   549 lemma POW_LT: "ALL (n::nat) (x::real) y::real. 0 <= x & x < y --> x ^ Suc n < y ^ Suc n"
   550   by (import real POW_LT)
   551 
   552 lemma POW_ZERO_EQ: "ALL (n::nat) x::real. (x ^ Suc n = 0) = (x = 0)"
   553   by (import real POW_ZERO_EQ)
   554 
   555 lemma REAL_POW_LT2: "ALL (n::nat) (x::real) y::real. n ~= 0 & 0 <= x & x < y --> x ^ n < y ^ n"
   556   by (import real REAL_POW_LT2)
   557 
   558 lemma REAL_POW_MONO_LT: "ALL (m::nat) (n::nat) x::real. 1 < x & m < n --> x ^ m < x ^ n"
   559   by (import real REAL_POW_MONO_LT)
   560 
   561 lemma REAL_SUP_SOMEPOS: "ALL P::real => bool.
   562    (EX x::real. P x & 0 < x) & (EX z::real. ALL x::real. P x --> x < z) -->
   563    (EX s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
   564   by (import real REAL_SUP_SOMEPOS)
   565 
   566 lemma SUP_LEMMA1: "ALL (P::real => bool) (s::real) d::real.
   567    (ALL y::real. (EX x::real. P (x + d) & y < x) = (y < s)) -->
   568    (ALL y::real. (EX x::real. P x & y < x) = (y < s + d))"
   569   by (import real SUP_LEMMA1)
   570 
   571 lemma SUP_LEMMA2: "ALL P::real => bool. Ex P --> (EX (d::real) x::real. P (x + d) & 0 < x)"
   572   by (import real SUP_LEMMA2)
   573 
   574 lemma SUP_LEMMA3: "ALL d::real.
   575    (EX z::real. ALL x::real. (P::real => bool) x --> x < z) -->
   576    (EX x::real. ALL xa::real. P (xa + d) --> xa < x)"
   577   by (import real SUP_LEMMA3)
   578 
   579 lemma REAL_SUP_EXISTS: "ALL P::real => bool.
   580    Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
   581    (EX x::real. ALL y::real. (EX x::real. P x & y < x) = (y < x))"
   582   by (import real REAL_SUP_EXISTS)
   583 
   584 constdefs
   585   sup :: "(real => bool) => real" 
   586   "sup ==
   587 %P::real => bool.
   588    SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s)"
   589 
   590 lemma sup: "ALL P::real => bool.
   591    sup P = (SOME s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
   592   by (import real sup)
   593 
   594 lemma REAL_SUP: "ALL P::real => bool.
   595    Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
   596    (ALL y::real. (EX x::real. P x & y < x) = (y < sup P))"
   597   by (import real REAL_SUP)
   598 
   599 lemma REAL_SUP_UBOUND: "ALL P::real => bool.
   600    Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
   601    (ALL y::real. P y --> y <= sup P)"
   602   by (import real REAL_SUP_UBOUND)
   603 
   604 lemma SETOK_LE_LT: "ALL P::real => bool.
   605    (Ex P & (EX z::real. ALL x::real. P x --> x <= z)) =
   606    (Ex P & (EX z::real. ALL x::real. P x --> x < z))"
   607   by (import real SETOK_LE_LT)
   608 
   609 lemma REAL_SUP_LE: "ALL P::real => bool.
   610    Ex P & (EX z::real. ALL x::real. P x --> x <= z) -->
   611    (ALL y::real. (EX x::real. P x & y < x) = (y < sup P))"
   612   by (import real REAL_SUP_LE)
   613 
   614 lemma REAL_SUP_UBOUND_LE: "ALL P::real => bool.
   615    Ex P & (EX z::real. ALL x::real. P x --> x <= z) -->
   616    (ALL y::real. P y --> y <= sup P)"
   617   by (import real REAL_SUP_UBOUND_LE)
   618 
   619 lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n::nat. real n * y <= x & x < real (Suc n) * y"
   620   by (import real REAL_ARCH_LEAST)
   621 
   622 consts
   623   sumc :: "nat => nat => (nat => real) => real" 
   624 
   625 specification (sumc) sumc: "(ALL (n::nat) f::nat => real. sumc n 0 f = 0) &
   626 (ALL (n::nat) (m::nat) f::nat => real.
   627     sumc n (Suc m) f = sumc n m f + f (n + m))"
   628   by (import real sumc)
   629 
   630 consts
   631   sum :: "nat * nat => (nat => real) => real" 
   632 
   633 defs
   634   sum_def: "(op ==::(nat * nat => (nat => real) => real)
   635         => (nat * nat => (nat => real) => real) => prop)
   636  (real.sum::nat * nat => (nat => real) => real)
   637  ((split::(nat => nat => (nat => real) => real)
   638           => nat * nat => (nat => real) => real)
   639    (sumc::nat => nat => (nat => real) => real))"
   640 
   641 lemma SUM_DEF: "ALL (m::nat) (n::nat) f::nat => real. real.sum (m, n) f = sumc m n f"
   642   by (import real SUM_DEF)
   643 
   644 lemma sum: "ALL (x::nat => real) (xa::nat) xb::nat.
   645    real.sum (xa, 0) x = 0 &
   646    real.sum (xa, Suc xb) x = real.sum (xa, xb) x + x (xa + xb)"
   647   by (import real sum)
   648 
   649 lemma SUM_TWO: "ALL (f::nat => real) (n::nat) p::nat.
   650    real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f"
   651   by (import real SUM_TWO)
   652 
   653 lemma SUM_DIFF: "ALL (f::nat => real) (m::nat) n::nat.
   654    real.sum (m, n) f = real.sum (0, m + n) f - real.sum (0, m) f"
   655   by (import real SUM_DIFF)
   656 
   657 lemma ABS_SUM: "ALL (f::nat => real) (m::nat) n::nat.
   658    abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))"
   659   by (import real ABS_SUM)
   660 
   661 lemma SUM_LE: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
   662    (ALL r::nat. m <= r & r < n + m --> f r <= g r) -->
   663    real.sum (m, n) f <= real.sum (m, n) g"
   664   by (import real SUM_LE)
   665 
   666 lemma SUM_EQ: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
   667    (ALL r::nat. m <= r & r < n + m --> f r = g r) -->
   668    real.sum (m, n) f = real.sum (m, n) g"
   669   by (import real SUM_EQ)
   670 
   671 lemma SUM_POS: "ALL f::nat => real.
   672    (ALL n::nat. 0 <= f n) --> (ALL (m::nat) n::nat. 0 <= real.sum (m, n) f)"
   673   by (import real SUM_POS)
   674 
   675 lemma SUM_POS_GEN: "ALL (f::nat => real) m::nat.
   676    (ALL n::nat. m <= n --> 0 <= f n) -->
   677    (ALL n::nat. 0 <= real.sum (m, n) f)"
   678   by (import real SUM_POS_GEN)
   679 
   680 lemma SUM_ABS: "ALL (f::nat => real) (m::nat) x::nat.
   681    abs (real.sum (m, x) (%m::nat. abs (f m))) =
   682    real.sum (m, x) (%m::nat. abs (f m))"
   683   by (import real SUM_ABS)
   684 
   685 lemma SUM_ABS_LE: "ALL (f::nat => real) (m::nat) n::nat.
   686    abs (real.sum (m, n) f) <= real.sum (m, n) (%n::nat. abs (f n))"
   687   by (import real SUM_ABS_LE)
   688 
   689 lemma SUM_ZERO: "ALL (f::nat => real) N::nat.
   690    (ALL n::nat. N <= n --> f n = 0) -->
   691    (ALL (m::nat) n::nat. N <= m --> real.sum (m, n) f = 0)"
   692   by (import real SUM_ZERO)
   693 
   694 lemma SUM_ADD: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
   695    real.sum (m, n) (%n::nat. f n + g n) =
   696    real.sum (m, n) f + real.sum (m, n) g"
   697   by (import real SUM_ADD)
   698 
   699 lemma SUM_CMUL: "ALL (f::nat => real) (c::real) (m::nat) n::nat.
   700    real.sum (m, n) (%n::nat. c * f n) = c * real.sum (m, n) f"
   701   by (import real SUM_CMUL)
   702 
   703 lemma SUM_NEG: "ALL (f::nat => real) (n::nat) d::nat.
   704    real.sum (n, d) (%n::nat. - f n) = - real.sum (n, d) f"
   705   by (import real SUM_NEG)
   706 
   707 lemma SUM_SUB: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
   708    real.sum (m, n) (%x::nat. f x - g x) =
   709    real.sum (m, n) f - real.sum (m, n) g"
   710   by (import real SUM_SUB)
   711 
   712 lemma SUM_SUBST: "ALL (f::nat => real) (g::nat => real) (m::nat) n::nat.
   713    (ALL p::nat. m <= p & p < m + n --> f p = g p) -->
   714    real.sum (m, n) f = real.sum (m, n) g"
   715   by (import real SUM_SUBST)
   716 
   717 lemma SUM_NSUB: "ALL (n::nat) (f::nat => real) c::real.
   718    real.sum (0, n) f - real n * c = real.sum (0, n) (%p::nat. f p - c)"
   719   by (import real SUM_NSUB)
   720 
   721 lemma SUM_BOUND: "ALL (f::nat => real) (k::real) (m::nat) n::nat.
   722    (ALL p::nat. m <= p & p < m + n --> f p <= k) -->
   723    real.sum (m, n) f <= real n * k"
   724   by (import real SUM_BOUND)
   725 
   726 lemma SUM_GROUP: "ALL (n::nat) (k::nat) f::nat => real.
   727    real.sum (0, n) (%m::nat. real.sum (m * k, k) f) = real.sum (0, n * k) f"
   728   by (import real SUM_GROUP)
   729 
   730 lemma SUM_1: "ALL (f::nat => real) n::nat. real.sum (n, 1) f = f n"
   731   by (import real SUM_1)
   732 
   733 lemma SUM_2: "ALL (f::nat => real) n::nat. real.sum (n, 2) f = f n + f (n + 1)"
   734   by (import real SUM_2)
   735 
   736 lemma SUM_OFFSET: "ALL (f::nat => real) (n::nat) k::nat.
   737    real.sum (0, n) (%m::nat. f (m + k)) =
   738    real.sum (0, n + k) f - real.sum (0, k) f"
   739   by (import real SUM_OFFSET)
   740 
   741 lemma SUM_REINDEX: "ALL (f::nat => real) (m::nat) (k::nat) n::nat.
   742    real.sum (m + k, n) f = real.sum (m, n) (%r::nat. f (r + k))"
   743   by (import real SUM_REINDEX)
   744 
   745 lemma SUM_0: "ALL (m::nat) n::nat. real.sum (m, n) (%r::nat. 0) = 0"
   746   by (import real SUM_0)
   747 
   748 lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool)
   749  (%n::nat.
   750      (All::((nat => nat) => bool) => bool)
   751       (%p::nat => nat.
   752           (op -->::bool => bool => bool)
   753            ((All::(nat => bool) => bool)
   754              (%y::nat.
   755                  (op -->::bool => bool => bool)
   756                   ((op <::nat => nat => bool) y n)
   757                   ((Ex1::(nat => bool) => bool)
   758                     (%x::nat.
   759                         (op &::bool => bool => bool)
   760                          ((op <::nat => nat => bool) x n)
   761                          ((op =::nat => nat => bool) (p x) y)))))
   762            ((All::((nat => real) => bool) => bool)
   763              (%f::nat => real.
   764                  (op =::real => real => bool)
   765                   ((real.sum::nat * nat => (nat => real) => real)
   766                     ((Pair::nat => nat => nat * nat) (0::nat) n)
   767                     (%n::nat. f (p n)))
   768                   ((real.sum::nat * nat => (nat => real) => real)
   769                     ((Pair::nat => nat => nat * nat) (0::nat) n) f)))))"
   770   by (import real SUM_PERMUTE_0)
   771 
   772 lemma SUM_CANCEL: "ALL (f::nat => real) (n::nat) d::nat.
   773    real.sum (n, d) (%n::nat. f (Suc n) - f n) = f (n + d) - f n"
   774   by (import real SUM_CANCEL)
   775 
   776 lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x = xa / xb) = (x * xb = xa)"
   777   by (import real REAL_EQ_RDIV_EQ)
   778 
   779 lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real. 0 < xb --> (x / xb = xa) = (x = xa * xb)"
   780   by (import real REAL_EQ_LDIV_EQ)
   781 
   782 ;end_setup
   783 
   784 ;setup_theory topology
   785 
   786 constdefs
   787   re_Union :: "(('a => bool) => bool) => 'a => bool" 
   788   "re_Union ==
   789 %(P::('a::type => bool) => bool) x::'a::type.
   790    EX s::'a::type => bool. P s & s x"
   791 
   792 lemma re_Union: "ALL P::('a::type => bool) => bool.
   793    re_Union P = (%x::'a::type. EX s::'a::type => bool. P s & s x)"
   794   by (import topology re_Union)
   795 
   796 constdefs
   797   re_union :: "('a => bool) => ('a => bool) => 'a => bool" 
   798   "re_union ==
   799 %(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x | Q x"
   800 
   801 lemma re_union: "ALL (P::'a::type => bool) Q::'a::type => bool.
   802    re_union P Q = (%x::'a::type. P x | Q x)"
   803   by (import topology re_union)
   804 
   805 constdefs
   806   re_intersect :: "('a => bool) => ('a => bool) => 'a => bool" 
   807   "re_intersect ==
   808 %(P::'a::type => bool) (Q::'a::type => bool) x::'a::type. P x & Q x"
   809 
   810 lemma re_intersect: "ALL (P::'a::type => bool) Q::'a::type => bool.
   811    re_intersect P Q = (%x::'a::type. P x & Q x)"
   812   by (import topology re_intersect)
   813 
   814 constdefs
   815   re_null :: "'a => bool" 
   816   "re_null == %x::'a::type. False"
   817 
   818 lemma re_null: "re_null = (%x::'a::type. False)"
   819   by (import topology re_null)
   820 
   821 constdefs
   822   re_universe :: "'a => bool" 
   823   "re_universe == %x::'a::type. True"
   824 
   825 lemma re_universe: "re_universe = (%x::'a::type. True)"
   826   by (import topology re_universe)
   827 
   828 constdefs
   829   re_subset :: "('a => bool) => ('a => bool) => bool" 
   830   "re_subset ==
   831 %(P::'a::type => bool) Q::'a::type => bool. ALL x::'a::type. P x --> Q x"
   832 
   833 lemma re_subset: "ALL (P::'a::type => bool) Q::'a::type => bool.
   834    re_subset P Q = (ALL x::'a::type. P x --> Q x)"
   835   by (import topology re_subset)
   836 
   837 constdefs
   838   re_compl :: "('a => bool) => 'a => bool" 
   839   "re_compl == %(P::'a::type => bool) x::'a::type. ~ P x"
   840 
   841 lemma re_compl: "ALL P::'a::type => bool. re_compl P = (%x::'a::type. ~ P x)"
   842   by (import topology re_compl)
   843 
   844 lemma SUBSET_REFL: "ALL P::'a::type => bool. re_subset P P"
   845   by (import topology SUBSET_REFL)
   846 
   847 lemma COMPL_MEM: "ALL (P::'a::type => bool) x::'a::type. P x = (~ re_compl P x)"
   848   by (import topology COMPL_MEM)
   849 
   850 lemma SUBSET_ANTISYM: "ALL (P::'a::type => bool) Q::'a::type => bool.
   851    (re_subset P Q & re_subset Q P) = (P = Q)"
   852   by (import topology SUBSET_ANTISYM)
   853 
   854 lemma SUBSET_TRANS: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
   855    re_subset P Q & re_subset Q R --> re_subset P R"
   856   by (import topology SUBSET_TRANS)
   857 
   858 constdefs
   859   istopology :: "(('a => bool) => bool) => bool" 
   860   "istopology ==
   861 %L::('a::type => bool) => bool.
   862    L re_null &
   863    L re_universe &
   864    (ALL (a::'a::type => bool) b::'a::type => bool.
   865        L a & L b --> L (re_intersect a b)) &
   866    (ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P))"
   867 
   868 lemma istopology: "ALL L::('a::type => bool) => bool.
   869    istopology L =
   870    (L re_null &
   871     L re_universe &
   872     (ALL (a::'a::type => bool) b::'a::type => bool.
   873         L a & L b --> L (re_intersect a b)) &
   874     (ALL P::('a::type => bool) => bool. re_subset P L --> L (re_Union P)))"
   875   by (import topology istopology)
   876 
   877 typedef (open) ('a) topology = "(Collect::((('a::type => bool) => bool) => bool)
   878           => (('a::type => bool) => bool) set)
   879  (istopology::(('a::type => bool) => bool) => bool)" 
   880   by (rule typedef_helper,import topology topology_TY_DEF)
   881 
   882 lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology]
   883 
   884 consts
   885   topology :: "(('a => bool) => bool) => 'a topology" 
   886   "open" :: "'a topology => ('a => bool) => bool" 
   887 
   888 specification ("open" topology) topology_tybij: "(ALL a::'a::type topology. topology (open a) = a) &
   889 (ALL r::('a::type => bool) => bool. istopology r = (open (topology r) = r))"
   890   by (import topology topology_tybij)
   891 
   892 lemma TOPOLOGY: "ALL L::'a::type topology.
   893    open L re_null &
   894    open L re_universe &
   895    (ALL (a::'a::type => bool) b::'a::type => bool.
   896        open L a & open L b --> open L (re_intersect a b)) &
   897    (ALL P::('a::type => bool) => bool.
   898        re_subset P (open L) --> open L (re_Union P))"
   899   by (import topology TOPOLOGY)
   900 
   901 lemma TOPOLOGY_UNION: "ALL (x::'a::type topology) xa::('a::type => bool) => bool.
   902    re_subset xa (open x) --> open x (re_Union xa)"
   903   by (import topology TOPOLOGY_UNION)
   904 
   905 constdefs
   906   neigh :: "'a topology => ('a => bool) * 'a => bool" 
   907   "neigh ==
   908 %(top::'a::type topology) (N::'a::type => bool, x::'a::type).
   909    EX P::'a::type => bool. open top P & re_subset P N & P x"
   910 
   911 lemma neigh: "ALL (top::'a::type topology) (N::'a::type => bool) x::'a::type.
   912    neigh top (N, x) =
   913    (EX P::'a::type => bool. open top P & re_subset P N & P x)"
   914   by (import topology neigh)
   915 
   916 lemma OPEN_OWN_NEIGH: "ALL (S'::'a::type => bool) (top::'a::type topology) x::'a::type.
   917    open top S' & S' x --> neigh top (S', x)"
   918   by (import topology OPEN_OWN_NEIGH)
   919 
   920 lemma OPEN_UNOPEN: "ALL (S'::'a::type => bool) top::'a::type topology.
   921    open top S' =
   922    (re_Union (%P::'a::type => bool. open top P & re_subset P S') = S')"
   923   by (import topology OPEN_UNOPEN)
   924 
   925 lemma OPEN_SUBOPEN: "ALL (S'::'a::type => bool) top::'a::type topology.
   926    open top S' =
   927    (ALL x::'a::type.
   928        S' x --> (EX P::'a::type => bool. P x & open top P & re_subset P S'))"
   929   by (import topology OPEN_SUBOPEN)
   930 
   931 lemma OPEN_NEIGH: "ALL (S'::'a::type => bool) top::'a::type topology.
   932    open top S' =
   933    (ALL x::'a::type.
   934        S' x --> (EX N::'a::type => bool. neigh top (N, x) & re_subset N S'))"
   935   by (import topology OPEN_NEIGH)
   936 
   937 constdefs
   938   closed :: "'a topology => ('a => bool) => bool" 
   939   "closed == %(L::'a::type topology) S'::'a::type => bool. open L (re_compl S')"
   940 
   941 lemma closed: "ALL (L::'a::type topology) S'::'a::type => bool.
   942    closed L S' = open L (re_compl S')"
   943   by (import topology closed)
   944 
   945 constdefs
   946   limpt :: "'a topology => 'a => ('a => bool) => bool" 
   947   "limpt ==
   948 %(top::'a::type topology) (x::'a::type) S'::'a::type => bool.
   949    ALL N::'a::type => bool.
   950       neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y)"
   951 
   952 lemma limpt: "ALL (top::'a::type topology) (x::'a::type) S'::'a::type => bool.
   953    limpt top x S' =
   954    (ALL N::'a::type => bool.
   955        neigh top (N, x) --> (EX y::'a::type. x ~= y & S' y & N y))"
   956   by (import topology limpt)
   957 
   958 lemma CLOSED_LIMPT: "ALL (top::'a::type topology) S'::'a::type => bool.
   959    closed top S' = (ALL x::'a::type. limpt top x S' --> S' x)"
   960   by (import topology CLOSED_LIMPT)
   961 
   962 constdefs
   963   ismet :: "('a * 'a => real) => bool" 
   964   "ismet ==
   965 %m::'a::type * 'a::type => real.
   966    (ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) &
   967    (ALL (x::'a::type) (y::'a::type) z::'a::type.
   968        m (y, z) <= m (x, y) + m (x, z))"
   969 
   970 lemma ismet: "ALL m::'a::type * 'a::type => real.
   971    ismet m =
   972    ((ALL (x::'a::type) y::'a::type. (m (x, y) = 0) = (x = y)) &
   973     (ALL (x::'a::type) (y::'a::type) z::'a::type.
   974         m (y, z) <= m (x, y) + m (x, z)))"
   975   by (import topology ismet)
   976 
   977 typedef (open) ('a) metric = "(Collect::(('a::type * 'a::type => real) => bool)
   978           => ('a::type * 'a::type => real) set)
   979  (ismet::('a::type * 'a::type => real) => bool)" 
   980   by (rule typedef_helper,import topology metric_TY_DEF)
   981 
   982 lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric]
   983 
   984 consts
   985   metric :: "('a * 'a => real) => 'a metric" 
   986   dist :: "'a metric => 'a * 'a => real" 
   987 
   988 specification (dist metric) metric_tybij: "(ALL a::'a::type metric. metric (dist a) = a) &
   989 (ALL r::'a::type * 'a::type => real. ismet r = (dist (metric r) = r))"
   990   by (import topology metric_tybij)
   991 
   992 lemma METRIC_ISMET: "ALL m::'a::type metric. ismet (dist m)"
   993   by (import topology METRIC_ISMET)
   994 
   995 lemma METRIC_ZERO: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
   996    (dist m (x, y) = 0) = (x = y)"
   997   by (import topology METRIC_ZERO)
   998 
   999 lemma METRIC_SAME: "ALL (m::'a::type metric) x::'a::type. dist m (x, x) = 0"
  1000   by (import topology METRIC_SAME)
  1001 
  1002 lemma METRIC_POS: "ALL (m::'a::type metric) (x::'a::type) y::'a::type. 0 <= dist m (x, y)"
  1003   by (import topology METRIC_POS)
  1004 
  1005 lemma METRIC_SYM: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
  1006    dist m (x, y) = dist m (y, x)"
  1007   by (import topology METRIC_SYM)
  1008 
  1009 lemma METRIC_TRIANGLE: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type.
  1010    dist m (x, z) <= dist m (x, y) + dist m (y, z)"
  1011   by (import topology METRIC_TRIANGLE)
  1012 
  1013 lemma METRIC_NZ: "ALL (m::'a::type metric) (x::'a::type) y::'a::type.
  1014    x ~= y --> 0 < dist m (x, y)"
  1015   by (import topology METRIC_NZ)
  1016 
  1017 constdefs
  1018   mtop :: "'a metric => 'a topology" 
  1019   "mtop ==
  1020 %m::'a::type metric.
  1021    topology
  1022     (%S'::'a::type => bool.
  1023         ALL x::'a::type.
  1024            S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
  1025 
  1026 lemma mtop: "ALL m::'a::type metric.
  1027    mtop m =
  1028    topology
  1029     (%S'::'a::type => bool.
  1030         ALL x::'a::type.
  1031            S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
  1032   by (import topology mtop)
  1033 
  1034 lemma mtop_istopology: "ALL m::'a::type metric.
  1035    istopology
  1036     (%S'::'a::type => bool.
  1037         ALL x::'a::type.
  1038            S' x --> (EX e>0. ALL y::'a::type. dist m (x, y) < e --> S' y))"
  1039   by (import topology mtop_istopology)
  1040 
  1041 lemma MTOP_OPEN: "ALL (S'::'a::type => bool) x::'a::type metric.
  1042    open (mtop x) S' =
  1043    (ALL xa::'a::type.
  1044        S' xa --> (EX e>0. ALL y::'a::type. dist x (xa, y) < e --> S' y))"
  1045   by (import topology MTOP_OPEN)
  1046 
  1047 constdefs
  1048   B :: "'a metric => 'a * real => 'a => bool" 
  1049   "B ==
  1050 %(m::'a::type metric) (x::'a::type, e::real) y::'a::type. dist m (x, y) < e"
  1051 
  1052 lemma ball: "ALL (m::'a::type metric) (x::'a::type) e::real.
  1053    B m (x, e) = (%y::'a::type. dist m (x, y) < e)"
  1054   by (import topology ball)
  1055 
  1056 lemma BALL_OPEN: "ALL (m::'a::type metric) (x::'a::type) e::real.
  1057    0 < e --> open (mtop m) (B m (x, e))"
  1058   by (import topology BALL_OPEN)
  1059 
  1060 lemma BALL_NEIGH: "ALL (m::'a::type metric) (x::'a::type) e::real.
  1061    0 < e --> neigh (mtop m) (B m (x, e), x)"
  1062   by (import topology BALL_NEIGH)
  1063 
  1064 lemma MTOP_LIMPT: "ALL (m::'a::type metric) (x::'a::type) S'::'a::type => bool.
  1065    limpt (mtop m) x S' =
  1066    (ALL e>0. EX y::'a::type. x ~= y & S' y & dist m (x, y) < e)"
  1067   by (import topology MTOP_LIMPT)
  1068 
  1069 lemma ISMET_R1: "ismet (%(x::real, y::real). abs (y - x))"
  1070   by (import topology ISMET_R1)
  1071 
  1072 constdefs
  1073   mr1 :: "real metric" 
  1074   "mr1 == metric (%(x::real, y::real). abs (y - x))"
  1075 
  1076 lemma mr1: "mr1 = metric (%(x::real, y::real). abs (y - x))"
  1077   by (import topology mr1)
  1078 
  1079 lemma MR1_DEF: "ALL (x::real) y::real. dist mr1 (x, y) = abs (y - x)"
  1080   by (import topology MR1_DEF)
  1081 
  1082 lemma MR1_ADD: "ALL (x::real) d::real. dist mr1 (x, x + d) = abs d"
  1083   by (import topology MR1_ADD)
  1084 
  1085 lemma MR1_SUB: "ALL (x::real) d::real. dist mr1 (x, x - d) = abs d"
  1086   by (import topology MR1_SUB)
  1087 
  1088 lemma MR1_ADD_POS: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x + d) = d"
  1089   by (import topology MR1_ADD_POS)
  1090 
  1091 lemma MR1_SUB_LE: "ALL (x::real) d::real. 0 <= d --> dist mr1 (x, x - d) = d"
  1092   by (import topology MR1_SUB_LE)
  1093 
  1094 lemma MR1_ADD_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x + d) = d"
  1095   by (import topology MR1_ADD_LT)
  1096 
  1097 lemma MR1_SUB_LT: "ALL (x::real) d::real. 0 < d --> dist mr1 (x, x - d) = d"
  1098   by (import topology MR1_SUB_LT)
  1099 
  1100 lemma MR1_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & dist mr1 (x, y) < z - x --> y < z"
  1101   by (import topology MR1_BETWEEN1)
  1102 
  1103 lemma MR1_LIMPT: "ALL x::real. limpt (mtop mr1) x re_universe"
  1104   by (import topology MR1_LIMPT)
  1105 
  1106 ;end_setup
  1107 
  1108 ;setup_theory nets
  1109 
  1110 constdefs
  1111   dorder :: "('a => 'a => bool) => bool" 
  1112   "dorder ==
  1113 %g::'a::type => 'a::type => bool.
  1114    ALL (x::'a::type) y::'a::type.
  1115       g x x & g y y -->
  1116       (EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y))"
  1117 
  1118 lemma dorder: "ALL g::'a::type => 'a::type => bool.
  1119    dorder g =
  1120    (ALL (x::'a::type) y::'a::type.
  1121        g x x & g y y -->
  1122        (EX z::'a::type. g z z & (ALL w::'a::type. g w z --> g w x & g w y)))"
  1123   by (import nets dorder)
  1124 
  1125 constdefs
  1126   tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool" 
  1127   "tends ==
  1128 %(s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology,
  1129    g::'b::type => 'b::type => bool).
  1130    ALL N::'a::type => bool.
  1131       neigh top (N, l) -->
  1132       (EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m)))"
  1133 
  1134 lemma tends: "ALL (s::'b::type => 'a::type) (l::'a::type) (top::'a::type topology)
  1135    g::'b::type => 'b::type => bool.
  1136    tends s l (top, g) =
  1137    (ALL N::'a::type => bool.
  1138        neigh top (N, l) -->
  1139        (EX n::'b::type. g n n & (ALL m::'b::type. g m n --> N (s m))))"
  1140   by (import nets tends)
  1141 
  1142 constdefs
  1143   bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool" 
  1144   "bounded ==
  1145 %(m::'a::type metric, g::'b::type => 'b::type => bool)
  1146    f::'b::type => 'a::type.
  1147    EX (k::real) (x::'a::type) N::'b::type.
  1148       g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k)"
  1149 
  1150 lemma bounded: "ALL (m::'a::type metric) (g::'b::type => 'b::type => bool)
  1151    f::'b::type => 'a::type.
  1152    bounded (m, g) f =
  1153    (EX (k::real) (x::'a::type) N::'b::type.
  1154        g N N & (ALL n::'b::type. g n N --> dist m (f n, x) < k))"
  1155   by (import nets bounded)
  1156 
  1157 constdefs
  1158   tendsto :: "'a metric * 'a => 'a => 'a => bool" 
  1159   "tendsto ==
  1160 %(m::'a::type metric, x::'a::type) (y::'a::type) z::'a::type.
  1161    0 < dist m (x, y) & dist m (x, y) <= dist m (x, z)"
  1162 
  1163 lemma tendsto: "ALL (m::'a::type metric) (x::'a::type) (y::'a::type) z::'a::type.
  1164    tendsto (m, x) y z = (0 < dist m (x, y) & dist m (x, y) <= dist m (x, z))"
  1165   by (import nets tendsto)
  1166 
  1167 lemma DORDER_LEMMA: "ALL g::'a::type => 'a::type => bool.
  1168    dorder g -->
  1169    (ALL (P::'a::type => bool) Q::'a::type => bool.
  1170        (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m)) &
  1171        (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> Q m)) -->
  1172        (EX n::'a::type. g n n & (ALL m::'a::type. g m n --> P m & Q m)))"
  1173   by (import nets DORDER_LEMMA)
  1174 
  1175 lemma DORDER_NGE: "dorder nat_ge"
  1176   by (import nets DORDER_NGE)
  1177 
  1178 lemma DORDER_TENDSTO: "ALL (m::'a::type metric) x::'a::type. dorder (tendsto (m, x))"
  1179   by (import nets DORDER_TENDSTO)
  1180 
  1181 lemma MTOP_TENDS: "ALL (d::'a::type metric) (g::'b::type => 'b::type => bool)
  1182    (x::'b::type => 'a::type) x0::'a::type.
  1183    tends x x0 (mtop d, g) =
  1184    (ALL e>0.
  1185        EX n::'b::type.
  1186           g n n & (ALL m::'b::type. g m n --> dist d (x m, x0) < e))"
  1187   by (import nets MTOP_TENDS)
  1188 
  1189 lemma MTOP_TENDS_UNIQ: "ALL (g::'b::type => 'b::type => bool) d::'a::type metric.
  1190    dorder g -->
  1191    tends (x::'b::type => 'a::type) (x0::'a::type) (mtop d, g) &
  1192    tends x (x1::'a::type) (mtop d, g) -->
  1193    x0 = x1"
  1194   by (import nets MTOP_TENDS_UNIQ)
  1195 
  1196 lemma SEQ_TENDS: "ALL (d::'a::type metric) (x::nat => 'a::type) x0::'a::type.
  1197    tends x x0 (mtop d, nat_ge) =
  1198    (ALL xa>0. EX xb::nat. ALL xc::nat. xb <= xc --> dist d (x xc, x0) < xa)"
  1199   by (import nets SEQ_TENDS)
  1200 
  1201 lemma LIM_TENDS: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type)
  1202    (x0::'a::type) y0::'b::type.
  1203    limpt (mtop m1) x0 re_universe -->
  1204    tends f y0 (mtop m2, tendsto (m1, x0)) =
  1205    (ALL e>0.
  1206        EX d>0.
  1207           ALL x::'a::type.
  1208              0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
  1209              dist m2 (f x, y0) < e)"
  1210   by (import nets LIM_TENDS)
  1211 
  1212 lemma LIM_TENDS2: "ALL (m1::'a::type metric) (m2::'b::type metric) (f::'a::type => 'b::type)
  1213    (x0::'a::type) y0::'b::type.
  1214    limpt (mtop m1) x0 re_universe -->
  1215    tends f y0 (mtop m2, tendsto (m1, x0)) =
  1216    (ALL e>0.
  1217        EX d>0.
  1218           ALL x::'a::type.
  1219              0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
  1220              dist m2 (f x, y0) < e)"
  1221   by (import nets LIM_TENDS2)
  1222 
  1223 lemma MR1_BOUNDED: "ALL (g::'a::type => 'a::type => bool) f::'a::type => real.
  1224    bounded (mr1, g) f =
  1225    (EX (k::real) N::'a::type.
  1226        g N N & (ALL n::'a::type. g n N --> abs (f n) < k))"
  1227   by (import nets MR1_BOUNDED)
  1228 
  1229 lemma NET_NULL: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
  1230    tends x x0 (mtop mr1, g) = tends (%n::'a::type. x n - x0) 0 (mtop mr1, g)"
  1231   by (import nets NET_NULL)
  1232 
  1233 lemma NET_CONV_BOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
  1234    tends x x0 (mtop mr1, g) --> bounded (mr1, g) x"
  1235   by (import nets NET_CONV_BOUNDED)
  1236 
  1237 lemma NET_CONV_NZ: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
  1238    tends x x0 (mtop mr1, g) & x0 ~= 0 -->
  1239    (EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n ~= 0))"
  1240   by (import nets NET_CONV_NZ)
  1241 
  1242 lemma NET_CONV_IBOUNDED: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
  1243    tends x x0 (mtop mr1, g) & x0 ~= 0 -->
  1244    bounded (mr1, g) (%n::'a::type. inverse (x n))"
  1245   by (import nets NET_CONV_IBOUNDED)
  1246 
  1247 lemma NET_NULL_ADD: "ALL g::'a::type => 'a::type => bool.
  1248    dorder g -->
  1249    (ALL (x::'a::type => real) y::'a::type => real.
  1250        tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) -->
  1251        tends (%n::'a::type. x n + y n) 0 (mtop mr1, g))"
  1252   by (import nets NET_NULL_ADD)
  1253 
  1254 lemma NET_NULL_MUL: "ALL g::'a::type => 'a::type => bool.
  1255    dorder g -->
  1256    (ALL (x::'a::type => real) y::'a::type => real.
  1257        bounded (mr1, g) x & tends y 0 (mtop mr1, g) -->
  1258        tends (%n::'a::type. x n * y n) 0 (mtop mr1, g))"
  1259   by (import nets NET_NULL_MUL)
  1260 
  1261 lemma NET_NULL_CMUL: "ALL (g::'a::type => 'a::type => bool) (k::real) x::'a::type => real.
  1262    tends x 0 (mtop mr1, g) --> tends (%n::'a::type. k * x n) 0 (mtop mr1, g)"
  1263   by (import nets NET_NULL_CMUL)
  1264 
  1265 lemma NET_ADD: "ALL g::'a::type => 'a::type => bool.
  1266    dorder g -->
  1267    (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
  1268        tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
  1269        tends (%n::'a::type. x n + y n) (x0 + y0) (mtop mr1, g))"
  1270   by (import nets NET_ADD)
  1271 
  1272 lemma NET_NEG: "ALL g::'a::type => 'a::type => bool.
  1273    dorder g -->
  1274    (ALL (x::'a::type => real) x0::real.
  1275        tends x x0 (mtop mr1, g) =
  1276        tends (%n::'a::type. - x n) (- x0) (mtop mr1, g))"
  1277   by (import nets NET_NEG)
  1278 
  1279 lemma NET_SUB: "ALL g::'a::type => 'a::type => bool.
  1280    dorder g -->
  1281    (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
  1282        tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
  1283        tends (%xa::'a::type. x xa - y xa) (x0 - y0) (mtop mr1, g))"
  1284   by (import nets NET_SUB)
  1285 
  1286 lemma NET_MUL: "ALL g::'a::type => 'a::type => bool.
  1287    dorder g -->
  1288    (ALL (x::'a::type => real) (y::'a::type => real) (x0::real) y0::real.
  1289        tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
  1290        tends (%n::'a::type. x n * y n) (x0 * y0) (mtop mr1, g))"
  1291   by (import nets NET_MUL)
  1292 
  1293 lemma NET_INV: "ALL g::'a::type => 'a::type => bool.
  1294    dorder g -->
  1295    (ALL (x::'a::type => real) x0::real.
  1296        tends x x0 (mtop mr1, g) & x0 ~= 0 -->
  1297        tends (%n::'a::type. inverse (x n)) (inverse x0) (mtop mr1, g))"
  1298   by (import nets NET_INV)
  1299 
  1300 lemma NET_DIV: "ALL g::'a::type => 'a::type => bool.
  1301    dorder g -->
  1302    (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
  1303        tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 -->
  1304        tends (%xa::'a::type. x xa / y xa) (x0 / y0) (mtop mr1, g))"
  1305   by (import nets NET_DIV)
  1306 
  1307 lemma NET_ABS: "ALL (g::'a::type => 'a::type => bool) (x::'a::type => real) x0::real.
  1308    tends x x0 (mtop mr1, g) -->
  1309    tends (%n::'a::type. abs (x n)) (abs x0) (mtop mr1, g)"
  1310   by (import nets NET_ABS)
  1311 
  1312 lemma NET_LE: "ALL g::'a::type => 'a::type => bool.
  1313    dorder g -->
  1314    (ALL (x::'a::type => real) (x0::real) (y::'a::type => real) y0::real.
  1315        tends x x0 (mtop mr1, g) &
  1316        tends y y0 (mtop mr1, g) &
  1317        (EX N::'a::type. g N N & (ALL n::'a::type. g n N --> x n <= y n)) -->
  1318        x0 <= y0)"
  1319   by (import nets NET_LE)
  1320 
  1321 ;end_setup
  1322 
  1323 ;setup_theory seq
  1324 
  1325 consts
  1326   "hol4-->" :: "(nat => real) => real => bool" ("hol4-->")
  1327 
  1328 defs
  1329   "hol4-->_def": "hol4--> == %(x::nat => real) x0::real. tends x x0 (mtop mr1, nat_ge)"
  1330 
  1331 lemma tends_num_real: "ALL (x::nat => real) x0::real. hol4--> x x0 = tends x x0 (mtop mr1, nat_ge)"
  1332   by (import seq tends_num_real)
  1333 
  1334 lemma SEQ: "ALL (x::nat => real) x0::real.
  1335    hol4--> x x0 =
  1336    (ALL e>0. EX N::nat. ALL n::nat. N <= n --> abs (x n - x0) < e)"
  1337   by (import seq SEQ)
  1338 
  1339 lemma SEQ_CONST: "ALL k::real. hol4--> (%x::nat. k) k"
  1340   by (import seq SEQ_CONST)
  1341 
  1342 lemma SEQ_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1343    hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n + y n) (x0 + y0)"
  1344   by (import seq SEQ_ADD)
  1345 
  1346 lemma SEQ_MUL: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1347    hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n * y n) (x0 * y0)"
  1348   by (import seq SEQ_MUL)
  1349 
  1350 lemma SEQ_NEG: "ALL (x::nat => real) x0::real.
  1351    hol4--> x x0 = hol4--> (%n::nat. - x n) (- x0)"
  1352   by (import seq SEQ_NEG)
  1353 
  1354 lemma SEQ_INV: "ALL (x::nat => real) x0::real.
  1355    hol4--> x x0 & x0 ~= 0 --> hol4--> (%n::nat. inverse (x n)) (inverse x0)"
  1356   by (import seq SEQ_INV)
  1357 
  1358 lemma SEQ_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1359    hol4--> x x0 & hol4--> y y0 --> hol4--> (%n::nat. x n - y n) (x0 - y0)"
  1360   by (import seq SEQ_SUB)
  1361 
  1362 lemma SEQ_DIV: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1363    hol4--> x x0 & hol4--> y y0 & y0 ~= 0 -->
  1364    hol4--> (%n::nat. x n / y n) (x0 / y0)"
  1365   by (import seq SEQ_DIV)
  1366 
  1367 lemma SEQ_UNIQ: "ALL (x::nat => real) (x1::real) x2::real.
  1368    hol4--> x x1 & hol4--> x x2 --> x1 = x2"
  1369   by (import seq SEQ_UNIQ)
  1370 
  1371 constdefs
  1372   convergent :: "(nat => real) => bool" 
  1373   "convergent == %f::nat => real. Ex (hol4--> f)"
  1374 
  1375 lemma convergent: "ALL f::nat => real. convergent f = Ex (hol4--> f)"
  1376   by (import seq convergent)
  1377 
  1378 constdefs
  1379   cauchy :: "(nat => real) => bool" 
  1380   "cauchy ==
  1381 %f::nat => real.
  1382    ALL e>0.
  1383       EX N::nat.
  1384          ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e"
  1385 
  1386 lemma cauchy: "ALL f::nat => real.
  1387    cauchy f =
  1388    (ALL e>0.
  1389        EX N::nat.
  1390           ALL (m::nat) n::nat. N <= m & N <= n --> abs (f m - f n) < e)"
  1391   by (import seq cauchy)
  1392 
  1393 constdefs
  1394   lim :: "(nat => real) => real" 
  1395   "lim == %f::nat => real. Eps (hol4--> f)"
  1396 
  1397 lemma lim: "ALL f::nat => real. lim f = Eps (hol4--> f)"
  1398   by (import seq lim)
  1399 
  1400 lemma SEQ_LIM: "ALL f::nat => real. convergent f = hol4--> f (lim f)"
  1401   by (import seq SEQ_LIM)
  1402 
  1403 constdefs
  1404   subseq :: "(nat => nat) => bool" 
  1405   "subseq == %f::nat => nat. ALL (m::nat) n::nat. m < n --> f m < f n"
  1406 
  1407 lemma subseq: "ALL f::nat => nat. subseq f = (ALL (m::nat) n::nat. m < n --> f m < f n)"
  1408   by (import seq subseq)
  1409 
  1410 lemma SUBSEQ_SUC: "ALL f::nat => nat. subseq f = (ALL n::nat. f n < f (Suc n))"
  1411   by (import seq SUBSEQ_SUC)
  1412 
  1413 consts
  1414   mono :: "(nat => real) => bool" 
  1415 
  1416 defs
  1417   mono_def: "seq.mono ==
  1418 %f::nat => real.
  1419    (ALL (m::nat) n::nat. m <= n --> f m <= f n) |
  1420    (ALL (m::nat) n::nat. m <= n --> f n <= f m)"
  1421 
  1422 lemma mono: "ALL f::nat => real.
  1423    seq.mono f =
  1424    ((ALL (m::nat) n::nat. m <= n --> f m <= f n) |
  1425     (ALL (m::nat) n::nat. m <= n --> f n <= f m))"
  1426   by (import seq mono)
  1427 
  1428 lemma MONO_SUC: "ALL f::nat => real.
  1429    seq.mono f =
  1430    ((ALL x::nat. f x <= f (Suc x)) | (ALL n::nat. f (Suc n) <= f n))"
  1431   by (import seq MONO_SUC)
  1432 
  1433 lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool)
  1434  (%s::nat => real.
  1435      (All::(nat => bool) => bool)
  1436       (%N::nat.
  1437           (Ex::(real => bool) => bool)
  1438            (%k::real.
  1439                (All::(nat => bool) => bool)
  1440                 (%n::nat.
  1441                     (op -->::bool => bool => bool)
  1442                      ((op <::nat => nat => bool) n N)
  1443                      ((op <::real => real => bool)
  1444                        ((abs::real => real) (s n)) k)))))"
  1445   by (import seq MAX_LEMMA)
  1446 
  1447 lemma SEQ_BOUNDED: "ALL s::nat => real.
  1448    bounded (mr1, nat_ge) s = (EX k::real. ALL n::nat. abs (s n) < k)"
  1449   by (import seq SEQ_BOUNDED)
  1450 
  1451 lemma SEQ_BOUNDED_2: "ALL (f::nat => real) (k::real) k'::real.
  1452    (ALL n::nat. k <= f n & f n <= k') --> bounded (mr1, nat_ge) f"
  1453   by (import seq SEQ_BOUNDED_2)
  1454 
  1455 lemma SEQ_CBOUNDED: "ALL f::nat => real. cauchy f --> bounded (mr1, nat_ge) f"
  1456   by (import seq SEQ_CBOUNDED)
  1457 
  1458 lemma SEQ_ICONV: "ALL f::nat => real.
  1459    bounded (mr1, nat_ge) f &
  1460    (ALL (m::nat) n::nat. n <= m --> f n <= f m) -->
  1461    convergent f"
  1462   by (import seq SEQ_ICONV)
  1463 
  1464 lemma SEQ_NEG_CONV: "ALL f::nat => real. convergent f = convergent (%n::nat. - f n)"
  1465   by (import seq SEQ_NEG_CONV)
  1466 
  1467 lemma SEQ_NEG_BOUNDED: "ALL f::nat => real.
  1468    bounded (mr1, nat_ge) (%n::nat. - f n) = bounded (mr1, nat_ge) f"
  1469   by (import seq SEQ_NEG_BOUNDED)
  1470 
  1471 lemma SEQ_BCONV: "ALL f::nat => real. bounded (mr1, nat_ge) f & seq.mono f --> convergent f"
  1472   by (import seq SEQ_BCONV)
  1473 
  1474 lemma SEQ_MONOSUB: "ALL s::nat => real. EX f::nat => nat. subseq f & seq.mono (%n::nat. s (f n))"
  1475   by (import seq SEQ_MONOSUB)
  1476 
  1477 lemma SEQ_SBOUNDED: "ALL (s::nat => real) f::nat => nat.
  1478    bounded (mr1, nat_ge) s --> bounded (mr1, nat_ge) (%n::nat. s (f n))"
  1479   by (import seq SEQ_SBOUNDED)
  1480 
  1481 lemma SEQ_SUBLE: "ALL f::nat => nat. subseq f --> (ALL n::nat. n <= f n)"
  1482   by (import seq SEQ_SUBLE)
  1483 
  1484 lemma SEQ_DIRECT: "ALL f::nat => nat.
  1485    subseq f --> (ALL (N1::nat) N2::nat. EX x::nat. N1 <= x & N2 <= f x)"
  1486   by (import seq SEQ_DIRECT)
  1487 
  1488 lemma SEQ_CAUCHY: "ALL f::nat => real. cauchy f = convergent f"
  1489   by (import seq SEQ_CAUCHY)
  1490 
  1491 lemma SEQ_LE: "ALL (f::nat => real) (g::nat => real) (l::real) m::real.
  1492    hol4--> f l &
  1493    hol4--> g m & (EX x::nat. ALL xa::nat. x <= xa --> f xa <= g xa) -->
  1494    l <= m"
  1495   by (import seq SEQ_LE)
  1496 
  1497 lemma SEQ_SUC: "ALL (f::nat => real) l::real. hol4--> f l = hol4--> (%n::nat. f (Suc n)) l"
  1498   by (import seq SEQ_SUC)
  1499 
  1500 lemma SEQ_ABS: "ALL f::nat => real. hol4--> (%n::nat. abs (f n)) 0 = hol4--> f 0"
  1501   by (import seq SEQ_ABS)
  1502 
  1503 lemma SEQ_ABS_IMP: "ALL (f::nat => real) l::real.
  1504    hol4--> f l --> hol4--> (%n::nat. abs (f n)) (abs l)"
  1505   by (import seq SEQ_ABS_IMP)
  1506 
  1507 lemma SEQ_INV0: "ALL f::nat => real.
  1508    (ALL y::real. EX N::nat. ALL n::nat. N <= n --> y < f n) -->
  1509    hol4--> (%n::nat. inverse (f n)) 0"
  1510   by (import seq SEQ_INV0)
  1511 
  1512 lemma SEQ_POWER_ABS: "ALL c::real. abs c < 1 --> hol4--> (op ^ (abs c)) 0"
  1513   by (import seq SEQ_POWER_ABS)
  1514 
  1515 lemma SEQ_POWER: "ALL c::real. abs c < 1 --> hol4--> (op ^ c) 0"
  1516   by (import seq SEQ_POWER)
  1517 
  1518 lemma NEST_LEMMA: "ALL (f::nat => real) g::nat => real.
  1519    (ALL n::nat. f n <= f (Suc n)) &
  1520    (ALL n::nat. g (Suc n) <= g n) & (ALL n::nat. f n <= g n) -->
  1521    (EX (l::real) m::real.
  1522        l <= m &
  1523        ((ALL n::nat. f n <= l) & hol4--> f l) &
  1524        (ALL n::nat. m <= g n) & hol4--> g m)"
  1525   by (import seq NEST_LEMMA)
  1526 
  1527 lemma NEST_LEMMA_UNIQ: "ALL (f::nat => real) g::nat => real.
  1528    (ALL n::nat. f n <= f (Suc n)) &
  1529    (ALL n::nat. g (Suc n) <= g n) &
  1530    (ALL n::nat. f n <= g n) & hol4--> (%n::nat. f n - g n) 0 -->
  1531    (EX x::real.
  1532        ((ALL n::nat. f n <= x) & hol4--> f x) &
  1533        (ALL n::nat. x <= g n) & hol4--> g x)"
  1534   by (import seq NEST_LEMMA_UNIQ)
  1535 
  1536 lemma BOLZANO_LEMMA: "ALL P::real * real => bool.
  1537    (ALL (a::real) (b::real) c::real.
  1538        a <= b & b <= c & P (a, b) & P (b, c) --> P (a, c)) &
  1539    (ALL x::real.
  1540        EX d>0.
  1541           ALL (a::real) b::real.
  1542              a <= x & x <= b & b - a < d --> P (a, b)) -->
  1543    (ALL (a::real) b::real. a <= b --> P (a, b))"
  1544   by (import seq BOLZANO_LEMMA)
  1545 
  1546 constdefs
  1547   sums :: "(nat => real) => real => bool" 
  1548   "sums == %f::nat => real. hol4--> (%n::nat. real.sum (0, n) f)"
  1549 
  1550 lemma sums: "ALL (f::nat => real) s::real.
  1551    sums f s = hol4--> (%n::nat. real.sum (0, n) f) s"
  1552   by (import seq sums)
  1553 
  1554 constdefs
  1555   summable :: "(nat => real) => bool" 
  1556   "summable == %f::nat => real. Ex (sums f)"
  1557 
  1558 lemma summable: "ALL f::nat => real. summable f = Ex (sums f)"
  1559   by (import seq summable)
  1560 
  1561 constdefs
  1562   suminf :: "(nat => real) => real" 
  1563   "suminf == %f::nat => real. Eps (sums f)"
  1564 
  1565 lemma suminf: "ALL f::nat => real. suminf f = Eps (sums f)"
  1566   by (import seq suminf)
  1567 
  1568 lemma SUM_SUMMABLE: "ALL (f::nat => real) l::real. sums f l --> summable f"
  1569   by (import seq SUM_SUMMABLE)
  1570 
  1571 lemma SUMMABLE_SUM: "ALL f::nat => real. summable f --> sums f (suminf f)"
  1572   by (import seq SUMMABLE_SUM)
  1573 
  1574 lemma SUM_UNIQ: "ALL (f::nat => real) x::real. sums f x --> x = suminf f"
  1575   by (import seq SUM_UNIQ)
  1576 
  1577 lemma SER_0: "ALL (f::nat => real) n::nat.
  1578    (ALL m::nat. n <= m --> f m = 0) --> sums f (real.sum (0, n) f)"
  1579   by (import seq SER_0)
  1580 
  1581 lemma SER_POS_LE: "ALL (f::nat => real) n::nat.
  1582    summable f & (ALL m::nat. n <= m --> 0 <= f m) -->
  1583    real.sum (0, n) f <= suminf f"
  1584   by (import seq SER_POS_LE)
  1585 
  1586 lemma SER_POS_LT: "ALL (f::nat => real) n::nat.
  1587    summable f & (ALL m::nat. n <= m --> 0 < f m) -->
  1588    real.sum (0, n) f < suminf f"
  1589   by (import seq SER_POS_LT)
  1590 
  1591 lemma SER_GROUP: "ALL (f::nat => real) k::nat.
  1592    summable f & 0 < k --> sums (%n::nat. real.sum (n * k, k) f) (suminf f)"
  1593   by (import seq SER_GROUP)
  1594 
  1595 lemma SER_PAIR: "ALL f::nat => real.
  1596    summable f --> sums (%n::nat. real.sum (2 * n, 2) f) (suminf f)"
  1597   by (import seq SER_PAIR)
  1598 
  1599 lemma SER_OFFSET: "ALL f::nat => real.
  1600    summable f -->
  1601    (ALL k::nat. sums (%n::nat. f (n + k)) (suminf f - real.sum (0, k) f))"
  1602   by (import seq SER_OFFSET)
  1603 
  1604 lemma SER_POS_LT_PAIR: "ALL (f::nat => real) n::nat.
  1605    summable f & (ALL d::nat. 0 < f (n + 2 * d) + f (n + (2 * d + 1))) -->
  1606    real.sum (0, n) f < suminf f"
  1607   by (import seq SER_POS_LT_PAIR)
  1608 
  1609 lemma SER_ADD: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1610    sums x x0 & sums y y0 --> sums (%n::nat. x n + y n) (x0 + y0)"
  1611   by (import seq SER_ADD)
  1612 
  1613 lemma SER_CMUL: "ALL (x::nat => real) (x0::real) c::real.
  1614    sums x x0 --> sums (%n::nat. c * x n) (c * x0)"
  1615   by (import seq SER_CMUL)
  1616 
  1617 lemma SER_NEG: "ALL (x::nat => real) x0::real. sums x x0 --> sums (%xa::nat. - x xa) (- x0)"
  1618   by (import seq SER_NEG)
  1619 
  1620 lemma SER_SUB: "ALL (x::nat => real) (x0::real) (y::nat => real) y0::real.
  1621    sums x x0 & sums y y0 --> sums (%xa::nat. x xa - y xa) (x0 - y0)"
  1622   by (import seq SER_SUB)
  1623 
  1624 lemma SER_CDIV: "ALL (x::nat => real) (x0::real) c::real.
  1625    sums x x0 --> sums (%xa::nat. x xa / c) (x0 / c)"
  1626   by (import seq SER_CDIV)
  1627 
  1628 lemma SER_CAUCHY: "ALL f::nat => real.
  1629    summable f =
  1630    (ALL e>0.
  1631        EX N::nat.
  1632           ALL (m::nat) n::nat. N <= m --> abs (real.sum (m, n) f) < e)"
  1633   by (import seq SER_CAUCHY)
  1634 
  1635 lemma SER_ZERO: "ALL f::nat => real. summable f --> hol4--> f 0"
  1636   by (import seq SER_ZERO)
  1637 
  1638 lemma SER_COMPAR: "ALL (f::nat => real) g::nat => real.
  1639    (EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g -->
  1640    summable f"
  1641   by (import seq SER_COMPAR)
  1642 
  1643 lemma SER_COMPARA: "ALL (f::nat => real) g::nat => real.
  1644    (EX x::nat. ALL xa::nat. x <= xa --> abs (f xa) <= g xa) & summable g -->
  1645    summable (%k::nat. abs (f k))"
  1646   by (import seq SER_COMPARA)
  1647 
  1648 lemma SER_LE: "ALL (f::nat => real) g::nat => real.
  1649    (ALL n::nat. f n <= g n) & summable f & summable g -->
  1650    suminf f <= suminf g"
  1651   by (import seq SER_LE)
  1652 
  1653 lemma SER_LE2: "ALL (f::nat => real) g::nat => real.
  1654    (ALL n::nat. abs (f n) <= g n) & summable g -->
  1655    summable f & suminf f <= suminf g"
  1656   by (import seq SER_LE2)
  1657 
  1658 lemma SER_ACONV: "ALL f::nat => real. summable (%n::nat. abs (f n)) --> summable f"
  1659   by (import seq SER_ACONV)
  1660 
  1661 lemma SER_ABS: "ALL f::nat => real.
  1662    summable (%n::nat. abs (f n)) -->
  1663    abs (suminf f) <= suminf (%n::nat. abs (f n))"
  1664   by (import seq SER_ABS)
  1665 
  1666 lemma GP_FINITE: "ALL x::real.
  1667    x ~= 1 --> (ALL n::nat. real.sum (0, n) (op ^ x) = (x ^ n - 1) / (x - 1))"
  1668   by (import seq GP_FINITE)
  1669 
  1670 lemma GP: "ALL x::real. abs x < 1 --> sums (op ^ x) (inverse (1 - x))"
  1671   by (import seq GP)
  1672 
  1673 lemma ABS_NEG_LEMMA: "(All::(real => bool) => bool)
  1674  (%c::real.
  1675      (op -->::bool => bool => bool)
  1676       ((op <=::real => real => bool) c (0::real))
  1677       ((All::(real => bool) => bool)
  1678         (%x::real.
  1679             (All::(real => bool) => bool)
  1680              (%y::real.
  1681                  (op -->::bool => bool => bool)
  1682                   ((op <=::real => real => bool) ((abs::real => real) x)
  1683                     ((op *::real => real => real) c
  1684                       ((abs::real => real) y)))
  1685                   ((op =::real => real => bool) x (0::real))))))"
  1686   by (import seq ABS_NEG_LEMMA)
  1687 
  1688 lemma SER_RATIO: "ALL (f::nat => real) (c::real) N::nat.
  1689    c < 1 & (ALL n::nat. N <= n --> abs (f (Suc n)) <= c * abs (f n)) -->
  1690    summable f"
  1691   by (import seq SER_RATIO)
  1692 
  1693 ;end_setup
  1694 
  1695 ;setup_theory lim
  1696 
  1697 constdefs
  1698   tends_real_real :: "(real => real) => real => real => bool" 
  1699   "tends_real_real ==
  1700 %(f::real => real) (l::real) x0::real.
  1701    tends f l (mtop mr1, tendsto (mr1, x0))"
  1702 
  1703 lemma tends_real_real: "ALL (f::real => real) (l::real) x0::real.
  1704    tends_real_real f l x0 = tends f l (mtop mr1, tendsto (mr1, x0))"
  1705   by (import lim tends_real_real)
  1706 
  1707 lemma LIM: "ALL (f::real => real) (y0::real) x0::real.
  1708    tends_real_real f y0 x0 =
  1709    (ALL e>0.
  1710        EX d>0.
  1711           ALL x::real.
  1712              0 < abs (x - x0) & abs (x - x0) < d --> abs (f x - y0) < e)"
  1713   by (import lim LIM)
  1714 
  1715 lemma LIM_CONST: "ALL k::real. All (tends_real_real (%x::real. k) k)"
  1716   by (import lim LIM_CONST)
  1717 
  1718 lemma LIM_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1719    tends_real_real f l x & tends_real_real g m x -->
  1720    tends_real_real (%x::real. f x + g x) (l + m) x"
  1721   by (import lim LIM_ADD)
  1722 
  1723 lemma LIM_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1724    tends_real_real f l x & tends_real_real g m x -->
  1725    tends_real_real (%x::real. f x * g x) (l * m) x"
  1726   by (import lim LIM_MUL)
  1727 
  1728 lemma LIM_NEG: "ALL (f::real => real) (l::real) x::real.
  1729    tends_real_real f l x = tends_real_real (%x::real. - f x) (- l) x"
  1730   by (import lim LIM_NEG)
  1731 
  1732 lemma LIM_INV: "ALL (f::real => real) (l::real) x::real.
  1733    tends_real_real f l x & l ~= 0 -->
  1734    tends_real_real (%x::real. inverse (f x)) (inverse l) x"
  1735   by (import lim LIM_INV)
  1736 
  1737 lemma LIM_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1738    tends_real_real f l x & tends_real_real g m x -->
  1739    tends_real_real (%x::real. f x - g x) (l - m) x"
  1740   by (import lim LIM_SUB)
  1741 
  1742 lemma LIM_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1743    tends_real_real f l x & tends_real_real g m x & m ~= 0 -->
  1744    tends_real_real (%x::real. f x / g x) (l / m) x"
  1745   by (import lim LIM_DIV)
  1746 
  1747 lemma LIM_NULL: "ALL (f::real => real) (l::real) x::real.
  1748    tends_real_real f l x = tends_real_real (%x::real. f x - l) 0 x"
  1749   by (import lim LIM_NULL)
  1750 
  1751 lemma LIM_X: "ALL x0::real. tends_real_real (%x::real. x) x0 x0"
  1752   by (import lim LIM_X)
  1753 
  1754 lemma LIM_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real.
  1755    tends_real_real f l x & tends_real_real f m x --> l = m"
  1756   by (import lim LIM_UNIQ)
  1757 
  1758 lemma LIM_EQUAL: "ALL (f::real => real) (g::real => real) (l::real) x0::real.
  1759    (ALL x::real. x ~= x0 --> f x = g x) -->
  1760    tends_real_real f l x0 = tends_real_real g l x0"
  1761   by (import lim LIM_EQUAL)
  1762 
  1763 lemma LIM_TRANSFORM: "ALL (f::real => real) (g::real => real) (x0::real) l::real.
  1764    tends_real_real (%x::real. f x - g x) 0 x0 & tends_real_real g l x0 -->
  1765    tends_real_real f l x0"
  1766   by (import lim LIM_TRANSFORM)
  1767 
  1768 constdefs
  1769   diffl :: "(real => real) => real => real => bool" 
  1770   "diffl ==
  1771 %(f::real => real) (l::real) x::real.
  1772    tends_real_real (%h::real. (f (x + h) - f x) / h) l 0"
  1773 
  1774 lemma diffl: "ALL (f::real => real) (l::real) x::real.
  1775    diffl f l x = tends_real_real (%h::real. (f (x + h) - f x) / h) l 0"
  1776   by (import lim diffl)
  1777 
  1778 constdefs
  1779   contl :: "(real => real) => real => bool" 
  1780   "contl ==
  1781 %(f::real => real) x::real. tends_real_real (%h::real. f (x + h)) (f x) 0"
  1782 
  1783 lemma contl: "ALL (f::real => real) x::real.
  1784    contl f x = tends_real_real (%h::real. f (x + h)) (f x) 0"
  1785   by (import lim contl)
  1786 
  1787 constdefs
  1788   differentiable :: "(real => real) => real => bool" 
  1789   "differentiable == %(f::real => real) x::real. EX l::real. diffl f l x"
  1790 
  1791 lemma differentiable: "ALL (f::real => real) x::real.
  1792    differentiable f x = (EX l::real. diffl f l x)"
  1793   by (import lim differentiable)
  1794 
  1795 lemma DIFF_UNIQ: "ALL (f::real => real) (l::real) (m::real) x::real.
  1796    diffl f l x & diffl f m x --> l = m"
  1797   by (import lim DIFF_UNIQ)
  1798 
  1799 lemma DIFF_CONT: "ALL (f::real => real) (l::real) x::real. diffl f l x --> contl f x"
  1800   by (import lim DIFF_CONT)
  1801 
  1802 lemma CONTL_LIM: "ALL (f::real => real) x::real. contl f x = tends_real_real f (f x) x"
  1803   by (import lim CONTL_LIM)
  1804 
  1805 lemma DIFF_CARAT: "ALL (f::real => real) (l::real) x::real.
  1806    diffl f l x =
  1807    (EX g::real => real.
  1808        (ALL z::real. f z - f x = g z * (z - x)) & contl g x & g x = l)"
  1809   by (import lim DIFF_CARAT)
  1810 
  1811 lemma CONT_CONST: "ALL k::real. All (contl (%x::real. k))"
  1812   by (import lim CONT_CONST)
  1813 
  1814 lemma CONT_ADD: "ALL (f::real => real) (g::real => real) x::real.
  1815    contl f x & contl g x --> contl (%x::real. f x + g x) x"
  1816   by (import lim CONT_ADD)
  1817 
  1818 lemma CONT_MUL: "ALL (f::real => real) (g::real => real) x::real.
  1819    contl f x & contl g x --> contl (%x::real. f x * g x) x"
  1820   by (import lim CONT_MUL)
  1821 
  1822 lemma CONT_NEG: "ALL (f::real => real) x::real. contl f x --> contl (%x::real. - f x) x"
  1823   by (import lim CONT_NEG)
  1824 
  1825 lemma CONT_INV: "ALL (f::real => real) x::real.
  1826    contl f x & f x ~= 0 --> contl (%x::real. inverse (f x)) x"
  1827   by (import lim CONT_INV)
  1828 
  1829 lemma CONT_SUB: "ALL (f::real => real) (g::real => real) x::real.
  1830    contl f x & contl g x --> contl (%x::real. f x - g x) x"
  1831   by (import lim CONT_SUB)
  1832 
  1833 lemma CONT_DIV: "ALL (f::real => real) (g::real => real) x::real.
  1834    contl f x & contl g x & g x ~= 0 --> contl (%x::real. f x / g x) x"
  1835   by (import lim CONT_DIV)
  1836 
  1837 lemma CONT_COMPOSE: "ALL (f::real => real) (g::real => real) x::real.
  1838    contl f x & contl g (f x) --> contl (%x::real. g (f x)) x"
  1839   by (import lim CONT_COMPOSE)
  1840 
  1841 lemma IVT: "ALL (f::real => real) (a::real) (b::real) y::real.
  1842    a <= b &
  1843    (f a <= y & y <= f b) & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1844    (EX x::real. a <= x & x <= b & f x = y)"
  1845   by (import lim IVT)
  1846 
  1847 lemma IVT2: "ALL (f::real => real) (a::real) (b::real) y::real.
  1848    a <= b &
  1849    (f b <= y & y <= f a) & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1850    (EX x::real. a <= x & x <= b & f x = y)"
  1851   by (import lim IVT2)
  1852 
  1853 lemma DIFF_CONST: "ALL k::real. All (diffl (%x::real. k) 0)"
  1854   by (import lim DIFF_CONST)
  1855 
  1856 lemma DIFF_ADD: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1857    diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x"
  1858   by (import lim DIFF_ADD)
  1859 
  1860 lemma DIFF_MUL: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1861    diffl f l x & diffl g m x -->
  1862    diffl (%x::real. f x * g x) (l * g x + m * f x) x"
  1863   by (import lim DIFF_MUL)
  1864 
  1865 lemma DIFF_CMUL: "ALL (f::real => real) (c::real) (l::real) x::real.
  1866    diffl f l x --> diffl (%x::real. c * f x) (c * l) x"
  1867   by (import lim DIFF_CMUL)
  1868 
  1869 lemma DIFF_NEG: "ALL (f::real => real) (l::real) x::real.
  1870    diffl f l x --> diffl (%x::real. - f x) (- l) x"
  1871   by (import lim DIFF_NEG)
  1872 
  1873 lemma DIFF_SUB: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1874    diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x"
  1875   by (import lim DIFF_SUB)
  1876 
  1877 lemma DIFF_CHAIN: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1878    diffl f l (g x) & diffl g m x --> diffl (%x::real. f (g x)) (l * m) x"
  1879   by (import lim DIFF_CHAIN)
  1880 
  1881 lemma DIFF_X: "All (diffl (%x::real. x) 1)"
  1882   by (import lim DIFF_X)
  1883 
  1884 lemma DIFF_POW: "ALL (n::nat) x::real. diffl (%x::real. x ^ n) (real n * x ^ (n - 1)) x"
  1885   by (import lim DIFF_POW)
  1886 
  1887 lemma DIFF_XM1: "ALL x::real. x ~= 0 --> diffl inverse (- (inverse x ^ 2)) x"
  1888   by (import lim DIFF_XM1)
  1889 
  1890 lemma DIFF_INV: "ALL (f::real => real) (l::real) x::real.
  1891    diffl f l x & f x ~= 0 -->
  1892    diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x"
  1893   by (import lim DIFF_INV)
  1894 
  1895 lemma DIFF_DIV: "ALL (f::real => real) (g::real => real) (l::real) (m::real) x::real.
  1896    diffl f l x & diffl g m x & g x ~= 0 -->
  1897    diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x"
  1898   by (import lim DIFF_DIV)
  1899 
  1900 lemma DIFF_SUM: "ALL (f::nat => real => real) (f'::nat => real => real) (m::nat) (n::nat)
  1901    x::real.
  1902    (ALL r::nat. m <= r & r < m + n --> diffl (f r) (f' r x) x) -->
  1903    diffl (%x::real. real.sum (m, n) (%n::nat. f n x))
  1904     (real.sum (m, n) (%r::nat. f' r x)) x"
  1905   by (import lim DIFF_SUM)
  1906 
  1907 lemma CONT_BOUNDED: "ALL (f::real => real) (a::real) b::real.
  1908    a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1909    (EX M::real. ALL x::real. a <= x & x <= b --> f x <= M)"
  1910   by (import lim CONT_BOUNDED)
  1911 
  1912 lemma CONT_HASSUP: "(All::((real => real) => bool) => bool)
  1913  (%f::real => real.
  1914      (All::(real => bool) => bool)
  1915       (%a::real.
  1916           (All::(real => bool) => bool)
  1917            (%b::real.
  1918                (op -->::bool => bool => bool)
  1919                 ((op &::bool => bool => bool)
  1920                   ((op <=::real => real => bool) a b)
  1921                   ((All::(real => bool) => bool)
  1922                     (%x::real.
  1923                         (op -->::bool => bool => bool)
  1924                          ((op &::bool => bool => bool)
  1925                            ((op <=::real => real => bool) a x)
  1926                            ((op <=::real => real => bool) x b))
  1927                          ((contl::(real => real) => real => bool) f x))))
  1928                 ((Ex::(real => bool) => bool)
  1929                   (%M::real.
  1930                       (op &::bool => bool => bool)
  1931                        ((All::(real => bool) => bool)
  1932                          (%x::real.
  1933                              (op -->::bool => bool => bool)
  1934                               ((op &::bool => bool => bool)
  1935                                 ((op <=::real => real => bool) a x)
  1936                                 ((op <=::real => real => bool) x b))
  1937                               ((op <=::real => real => bool) (f x) M)))
  1938                        ((All::(real => bool) => bool)
  1939                          (%N::real.
  1940                              (op -->::bool => bool => bool)
  1941                               ((op <::real => real => bool) N M)
  1942                               ((Ex::(real => bool) => bool)
  1943                                 (%x::real.
  1944                                     (op &::bool => bool => bool)
  1945                                      ((op <=::real => real => bool) a x)
  1946                                      ((op &::bool => bool => bool)
  1947  ((op <=::real => real => bool) x b)
  1948  ((op <::real => real => bool) N (f x))))))))))))"
  1949   by (import lim CONT_HASSUP)
  1950 
  1951 lemma CONT_ATTAINS: "ALL (f::real => real) (a::real) b::real.
  1952    a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1953    (EX x::real.
  1954        (ALL xa::real. a <= xa & xa <= b --> f xa <= x) &
  1955        (EX xa::real. a <= xa & xa <= b & f xa = x))"
  1956   by (import lim CONT_ATTAINS)
  1957 
  1958 lemma CONT_ATTAINS2: "ALL (f::real => real) (a::real) b::real.
  1959    a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1960    (EX x::real.
  1961        (ALL xa::real. a <= xa & xa <= b --> x <= f xa) &
  1962        (EX xa::real. a <= xa & xa <= b & f xa = x))"
  1963   by (import lim CONT_ATTAINS2)
  1964 
  1965 lemma CONT_ATTAINS_ALL: "ALL (f::real => real) (a::real) b::real.
  1966    a <= b & (ALL x::real. a <= x & x <= b --> contl f x) -->
  1967    (EX (x::real) M::real.
  1968        x <= M &
  1969        (ALL y::real.
  1970            x <= y & y <= M --> (EX x::real. a <= x & x <= b & f x = y)) &
  1971        (ALL xa::real. a <= xa & xa <= b --> x <= f xa & f xa <= M))"
  1972   by (import lim CONT_ATTAINS_ALL)
  1973 
  1974 lemma DIFF_LINC: "ALL (f::real => real) (x::real) l::real.
  1975    diffl f l x & 0 < l -->
  1976    (EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x + h))"
  1977   by (import lim DIFF_LINC)
  1978 
  1979 lemma DIFF_LDEC: "ALL (f::real => real) (x::real) l::real.
  1980    diffl f l x & l < 0 -->
  1981    (EX d>0. ALL h::real. 0 < h & h < d --> f x < f (x - h))"
  1982   by (import lim DIFF_LDEC)
  1983 
  1984 lemma DIFF_LMAX: "ALL (f::real => real) (x::real) l::real.
  1985    diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y <= f x) -->
  1986    l = 0"
  1987   by (import lim DIFF_LMAX)
  1988 
  1989 lemma DIFF_LMIN: "ALL (f::real => real) (x::real) l::real.
  1990    diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f x <= f y) -->
  1991    l = 0"
  1992   by (import lim DIFF_LMIN)
  1993 
  1994 lemma DIFF_LCONST: "ALL (f::real => real) (x::real) l::real.
  1995    diffl f l x & (EX d>0. ALL y::real. abs (x - y) < d --> f y = f x) -->
  1996    l = 0"
  1997   by (import lim DIFF_LCONST)
  1998 
  1999 lemma INTERVAL_LEMMA: "ALL (a::real) (b::real) x::real.
  2000    a < x & x < b -->
  2001    (EX d>0. ALL y::real. abs (x - y) < d --> a <= y & y <= b)"
  2002   by (import lim INTERVAL_LEMMA)
  2003 
  2004 lemma ROLLE: "ALL (f::real => real) (a::real) b::real.
  2005    a < b &
  2006    f a = f b &
  2007    (ALL x::real. a <= x & x <= b --> contl f x) &
  2008    (ALL x::real. a < x & x < b --> differentiable f x) -->
  2009    (EX z::real. a < z & z < b & diffl f 0 z)"
  2010   by (import lim ROLLE)
  2011 
  2012 lemma MVT_LEMMA: "ALL (f::real => real) (a::real) b::real.
  2013    f a - (f b - f a) / (b - a) * a = f b - (f b - f a) / (b - a) * b"
  2014   by (import lim MVT_LEMMA)
  2015 
  2016 lemma MVT: "ALL (f::real => real) (a::real) b::real.
  2017    a < b &
  2018    (ALL x::real. a <= x & x <= b --> contl f x) &
  2019    (ALL x::real. a < x & x < b --> differentiable f x) -->
  2020    (EX (l::real) z::real.
  2021        a < z & z < b & diffl f l z & f b - f a = (b - a) * l)"
  2022   by (import lim MVT)
  2023 
  2024 lemma DIFF_ISCONST_END: "ALL (f::real => real) (a::real) b::real.
  2025    a < b &
  2026    (ALL x::real. a <= x & x <= b --> contl f x) &
  2027    (ALL x::real. a < x & x < b --> diffl f 0 x) -->
  2028    f b = f a"
  2029   by (import lim DIFF_ISCONST_END)
  2030 
  2031 lemma DIFF_ISCONST: "ALL (f::real => real) (a::real) b::real.
  2032    a < b &
  2033    (ALL x::real. a <= x & x <= b --> contl f x) &
  2034    (ALL x::real. a < x & x < b --> diffl f 0 x) -->
  2035    (ALL x::real. a <= x & x <= b --> f x = f a)"
  2036   by (import lim DIFF_ISCONST)
  2037 
  2038 lemma DIFF_ISCONST_ALL: "ALL f::real => real. All (diffl f 0) --> (ALL (x::real) y::real. f x = f y)"
  2039   by (import lim DIFF_ISCONST_ALL)
  2040 
  2041 lemma INTERVAL_ABS: "ALL (x::real) (z::real) d::real.
  2042    (x - d <= z & z <= x + d) = (abs (z - x) <= d)"
  2043   by (import lim INTERVAL_ABS)
  2044 
  2045 lemma CONT_INJ_LEMMA: "ALL (f::real => real) (g::real => real) (x::real) d::real.
  2046    0 < d &
  2047    (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
  2048    (ALL z::real. abs (z - x) <= d --> contl f z) -->
  2049    ~ (ALL z::real. abs (z - x) <= d --> f z <= f x)"
  2050   by (import lim CONT_INJ_LEMMA)
  2051 
  2052 lemma CONT_INJ_LEMMA2: "ALL (f::real => real) (g::real => real) (x::real) d::real.
  2053    0 < d &
  2054    (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
  2055    (ALL z::real. abs (z - x) <= d --> contl f z) -->
  2056    ~ (ALL z::real. abs (z - x) <= d --> f x <= f z)"
  2057   by (import lim CONT_INJ_LEMMA2)
  2058 
  2059 lemma CONT_INJ_RANGE: "ALL (f::real => real) (g::real => real) (x::real) d::real.
  2060    0 < d &
  2061    (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
  2062    (ALL z::real. abs (z - x) <= d --> contl f z) -->
  2063    (EX e>0.
  2064        ALL y::real.
  2065           abs (y - f x) <= e --> (EX z::real. abs (z - x) <= d & f z = y))"
  2066   by (import lim CONT_INJ_RANGE)
  2067 
  2068 lemma CONT_INVERSE: "ALL (f::real => real) (g::real => real) (x::real) d::real.
  2069    0 < d &
  2070    (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
  2071    (ALL z::real. abs (z - x) <= d --> contl f z) -->
  2072    contl g (f x)"
  2073   by (import lim CONT_INVERSE)
  2074 
  2075 lemma DIFF_INVERSE: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real.
  2076    0 < d &
  2077    (ALL z::real. abs (z - x) <= d --> g (f z) = z) &
  2078    (ALL z::real. abs (z - x) <= d --> contl f z) & diffl f l x & l ~= 0 -->
  2079    diffl g (inverse l) (f x)"
  2080   by (import lim DIFF_INVERSE)
  2081 
  2082 lemma DIFF_INVERSE_LT: "ALL (f::real => real) (g::real => real) (l::real) (x::real) d::real.
  2083    0 < d &
  2084    (ALL z::real. abs (z - x) < d --> g (f z) = z) &
  2085    (ALL z::real. abs (z - x) < d --> contl f z) & diffl f l x & l ~= 0 -->
  2086    diffl g (inverse l) (f x)"
  2087   by (import lim DIFF_INVERSE_LT)
  2088 
  2089 lemma INTERVAL_CLEMMA: "ALL (a::real) (b::real) x::real.
  2090    a < x & x < b -->
  2091    (EX d>0. ALL y::real. abs (y - x) <= d --> a < y & y < b)"
  2092   by (import lim INTERVAL_CLEMMA)
  2093 
  2094 lemma DIFF_INVERSE_OPEN: "ALL (f::real => real) (g::real => real) (l::real) (a::real) (x::real)
  2095    b::real.
  2096    a < x &
  2097    x < b &
  2098    (ALL z::real. a < z & z < b --> g (f z) = z & contl f z) &
  2099    diffl f l x & l ~= 0 -->
  2100    diffl g (inverse l) (f x)"
  2101   by (import lim DIFF_INVERSE_OPEN)
  2102 
  2103 ;end_setup
  2104 
  2105 ;setup_theory powser
  2106 
  2107 lemma POWDIFF_LEMMA: "ALL (n::nat) (x::real) y::real.
  2108    real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (Suc n - p)) =
  2109    y * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))"
  2110   by (import powser POWDIFF_LEMMA)
  2111 
  2112 lemma POWDIFF: "ALL (n::nat) (x::real) y::real.
  2113    x ^ Suc n - y ^ Suc n =
  2114    (x - y) * real.sum (0, Suc n) (%p::nat. x ^ p * y ^ (n - p))"
  2115   by (import powser POWDIFF)
  2116 
  2117 lemma POWREV: "ALL (n::nat) (x::real) y::real.
  2118    real.sum (0, Suc n) (%xa::nat. x ^ xa * y ^ (n - xa)) =
  2119    real.sum (0, Suc n) (%xa::nat. x ^ (n - xa) * y ^ xa)"
  2120   by (import powser POWREV)
  2121 
  2122 lemma POWSER_INSIDEA: "ALL (f::nat => real) (x::real) z::real.
  2123    summable (%n::nat. f n * x ^ n) & abs z < abs x -->
  2124    summable (%n::nat. abs (f n) * z ^ n)"
  2125   by (import powser POWSER_INSIDEA)
  2126 
  2127 lemma POWSER_INSIDE: "ALL (f::nat => real) (x::real) z::real.
  2128    summable (%n::nat. f n * x ^ n) & abs z < abs x -->
  2129    summable (%n::nat. f n * z ^ n)"
  2130   by (import powser POWSER_INSIDE)
  2131 
  2132 constdefs
  2133   diffs :: "(nat => real) => nat => real" 
  2134   "diffs == %(c::nat => real) n::nat. real (Suc n) * c (Suc n)"
  2135 
  2136 lemma diffs: "ALL c::nat => real. diffs c = (%n::nat. real (Suc n) * c (Suc n))"
  2137   by (import powser diffs)
  2138 
  2139 lemma DIFFS_NEG: "ALL c::nat => real. diffs (%n::nat. - c n) = (%x::nat. - diffs c x)"
  2140   by (import powser DIFFS_NEG)
  2141 
  2142 lemma DIFFS_LEMMA: "ALL (n::nat) (c::nat => real) x::real.
  2143    real.sum (0, n) (%n::nat. diffs c n * x ^ n) =
  2144    real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) +
  2145    real n * (c n * x ^ (n - 1))"
  2146   by (import powser DIFFS_LEMMA)
  2147 
  2148 lemma DIFFS_LEMMA2: "ALL (n::nat) (c::nat => real) x::real.
  2149    real.sum (0, n) (%n::nat. real n * (c n * x ^ (n - 1))) =
  2150    real.sum (0, n) (%n::nat. diffs c n * x ^ n) -
  2151    real n * (c n * x ^ (n - 1))"
  2152   by (import powser DIFFS_LEMMA2)
  2153 
  2154 lemma DIFFS_EQUIV: "ALL (c::nat => real) x::real.
  2155    summable (%n::nat. diffs c n * x ^ n) -->
  2156    sums (%n::nat. real n * (c n * x ^ (n - 1)))
  2157     (suminf (%n::nat. diffs c n * x ^ n))"
  2158   by (import powser DIFFS_EQUIV)
  2159 
  2160 lemma TERMDIFF_LEMMA1: "ALL (m::nat) (z::real) h::real.
  2161    real.sum (0, m) (%p::nat. (z + h) ^ (m - p) * z ^ p - z ^ m) =
  2162    real.sum (0, m) (%p::nat. z ^ p * ((z + h) ^ (m - p) - z ^ (m - p)))"
  2163   by (import powser TERMDIFF_LEMMA1)
  2164 
  2165 lemma TERMDIFF_LEMMA2: "ALL (z::real) (h::real) n::nat.
  2166    h ~= 0 -->
  2167    ((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1) =
  2168    h *
  2169    real.sum (0, n - 1)
  2170     (%p::nat.
  2171         z ^ p *
  2172         real.sum (0, n - 1 - p)
  2173          (%q::nat. (z + h) ^ q * z ^ (n - 2 - p - q)))"
  2174   by (import powser TERMDIFF_LEMMA2)
  2175 
  2176 lemma TERMDIFF_LEMMA3: "ALL (z::real) (h::real) (n::nat) k'::real.
  2177    h ~= 0 & abs z <= k' & abs (z + h) <= k' -->
  2178    abs (((z + h) ^ n - z ^ n) / h - real n * z ^ (n - 1))
  2179    <= real n * (real (n - 1) * (k' ^ (n - 2) * abs h))"
  2180   by (import powser TERMDIFF_LEMMA3)
  2181 
  2182 lemma TERMDIFF_LEMMA4: "ALL (f::real => real) (k'::real) k::real.
  2183    0 < k &
  2184    (ALL h::real. 0 < abs h & abs h < k --> abs (f h) <= k' * abs h) -->
  2185    tends_real_real f 0 0"
  2186   by (import powser TERMDIFF_LEMMA4)
  2187 
  2188 lemma TERMDIFF_LEMMA5: "ALL (f::nat => real) (g::real => nat => real) k::real.
  2189    0 < k &
  2190    summable f &
  2191    (ALL h::real.
  2192        0 < abs h & abs h < k -->
  2193        (ALL n::nat. abs (g h n) <= f n * abs h)) -->
  2194    tends_real_real (%h::real. suminf (g h)) 0 0"
  2195   by (import powser TERMDIFF_LEMMA5)
  2196 
  2197 lemma TERMDIFF: "ALL (c::nat => real) (k'::real) x::real.
  2198    summable (%n::nat. c n * k' ^ n) &
  2199    summable (%n::nat. diffs c n * k' ^ n) &
  2200    summable (%n::nat. diffs (diffs c) n * k' ^ n) & abs x < abs k' -->
  2201    diffl (%x::real. suminf (%n::nat. c n * x ^ n))
  2202     (suminf (%n::nat. diffs c n * x ^ n)) x"
  2203   by (import powser TERMDIFF)
  2204 
  2205 ;end_setup
  2206 
  2207 ;setup_theory transc
  2208 
  2209 constdefs
  2210   exp :: "real => real" 
  2211   "exp == %x::real. suminf (%n::nat. inverse (real (FACT n)) * x ^ n)"
  2212 
  2213 lemma exp: "ALL x::real. exp x = suminf (%n::nat. inverse (real (FACT n)) * x ^ n)"
  2214   by (import transc exp)
  2215 
  2216 constdefs
  2217   cos :: "real => real" 
  2218   "cos ==
  2219 %x::real.
  2220    suminf
  2221     (%n::nat.
  2222         (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)"
  2223 
  2224 lemma cos: "ALL x::real.
  2225    cos x =
  2226    suminf
  2227     (%n::nat.
  2228         (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)"
  2229   by (import transc cos)
  2230 
  2231 constdefs
  2232   sin :: "real => real" 
  2233   "sin ==
  2234 %x::real.
  2235    suminf
  2236     (%n::nat.
  2237         (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
  2238         x ^ n)"
  2239 
  2240 lemma sin: "ALL x::real.
  2241    sin x =
  2242    suminf
  2243     (%n::nat.
  2244         (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
  2245         x ^ n)"
  2246   by (import transc sin)
  2247 
  2248 lemma EXP_CONVERGES: "ALL x::real. sums (%n::nat. inverse (real (FACT n)) * x ^ n) (exp x)"
  2249   by (import transc EXP_CONVERGES)
  2250 
  2251 lemma SIN_CONVERGES: "ALL x::real.
  2252    sums
  2253     (%n::nat.
  2254         (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
  2255         x ^ n)
  2256     (sin x)"
  2257   by (import transc SIN_CONVERGES)
  2258 
  2259 lemma COS_CONVERGES: "ALL x::real.
  2260    sums
  2261     (%n::nat.
  2262         (if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) * x ^ n)
  2263     (cos x)"
  2264   by (import transc COS_CONVERGES)
  2265 
  2266 lemma EXP_FDIFF: "diffs (%n::nat. inverse (real (FACT n))) =
  2267 (%n::nat. inverse (real (FACT n)))"
  2268   by (import transc EXP_FDIFF)
  2269 
  2270 lemma SIN_FDIFF: "diffs
  2271  (%n::nat. if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) =
  2272 (%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0)"
  2273   by (import transc SIN_FDIFF)
  2274 
  2275 lemma COS_FDIFF: "diffs (%n::nat. if EVEN n then (- 1) ^ (n div 2) / real (FACT n) else 0) =
  2276 (%n::nat. - (if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)))"
  2277   by (import transc COS_FDIFF)
  2278 
  2279 lemma SIN_NEGLEMMA: "ALL x::real.
  2280    - sin x =
  2281    suminf
  2282     (%n::nat.
  2283         - ((if EVEN n then 0 else (- 1) ^ ((n - 1) div 2) / real (FACT n)) *
  2284            x ^ n))"
  2285   by (import transc SIN_NEGLEMMA)
  2286 
  2287 lemma DIFF_EXP: "ALL x::real. diffl exp (exp x) x"
  2288   by (import transc DIFF_EXP)
  2289 
  2290 lemma DIFF_SIN: "ALL x::real. diffl sin (cos x) x"
  2291   by (import transc DIFF_SIN)
  2292 
  2293 lemma DIFF_COS: "ALL x::real. diffl cos (- sin x) x"
  2294   by (import transc DIFF_COS)
  2295 
  2296 lemma DIFF_COMPOSITE: "(diffl (f::real => real) (l::real) (x::real) & f x ~= 0 -->
  2297  diffl (%x::real. inverse (f x)) (- (l / f x ^ 2)) x) &
  2298 (diffl f l x & diffl (g::real => real) (m::real) x & g x ~= 0 -->
  2299  diffl (%x::real. f x / g x) ((l * g x - m * f x) / g x ^ 2) x) &
  2300 (diffl f l x & diffl g m x --> diffl (%x::real. f x + g x) (l + m) x) &
  2301 (diffl f l x & diffl g m x -->
  2302  diffl (%x::real. f x * g x) (l * g x + m * f x) x) &
  2303 (diffl f l x & diffl g m x --> diffl (%x::real. f x - g x) (l - m) x) &
  2304 (diffl f l x --> diffl (%x::real. - f x) (- l) x) &
  2305 (diffl g m x -->
  2306  diffl (%x::real. g x ^ (n::nat)) (real n * g x ^ (n - 1) * m) x) &
  2307 (diffl g m x --> diffl (%x::real. exp (g x)) (exp (g x) * m) x) &
  2308 (diffl g m x --> diffl (%x::real. sin (g x)) (cos (g x) * m) x) &
  2309 (diffl g m x --> diffl (%x::real. cos (g x)) (- sin (g x) * m) x)"
  2310   by (import transc DIFF_COMPOSITE)
  2311 
  2312 lemma EXP_0: "exp 0 = 1"
  2313   by (import transc EXP_0)
  2314 
  2315 lemma EXP_LE_X: "ALL x>=0. 1 + x <= exp x"
  2316   by (import transc EXP_LE_X)
  2317 
  2318 lemma EXP_LT_1: "ALL x>0. 1 < exp x"
  2319   by (import transc EXP_LT_1)
  2320 
  2321 lemma EXP_ADD_MUL: "ALL (x::real) y::real. exp (x + y) * exp (- x) = exp y"
  2322   by (import transc EXP_ADD_MUL)
  2323 
  2324 lemma EXP_NEG_MUL: "ALL x::real. exp x * exp (- x) = 1"
  2325   by (import transc EXP_NEG_MUL)
  2326 
  2327 lemma EXP_NEG_MUL2: "ALL x::real. exp (- x) * exp x = 1"
  2328   by (import transc EXP_NEG_MUL2)
  2329 
  2330 lemma EXP_NEG: "ALL x::real. exp (- x) = inverse (exp x)"
  2331   by (import transc EXP_NEG)
  2332 
  2333 lemma EXP_ADD: "ALL (x::real) y::real. exp (x + y) = exp x * exp y"
  2334   by (import transc EXP_ADD)
  2335 
  2336 lemma EXP_POS_LE: "ALL x::real. 0 <= exp x"
  2337   by (import transc EXP_POS_LE)
  2338 
  2339 lemma EXP_NZ: "ALL x::real. exp x ~= 0"
  2340   by (import transc EXP_NZ)
  2341 
  2342 lemma EXP_POS_LT: "ALL x::real. 0 < exp x"
  2343   by (import transc EXP_POS_LT)
  2344 
  2345 lemma EXP_N: "ALL (n::nat) x::real. exp (real n * x) = exp x ^ n"
  2346   by (import transc EXP_N)
  2347 
  2348 lemma EXP_SUB: "ALL (x::real) y::real. exp (x - y) = exp x / exp y"
  2349   by (import transc EXP_SUB)
  2350 
  2351 lemma EXP_MONO_IMP: "ALL (x::real) y::real. x < y --> exp x < exp y"
  2352   by (import transc EXP_MONO_IMP)
  2353 
  2354 lemma EXP_MONO_LT: "ALL (x::real) y::real. (exp x < exp y) = (x < y)"
  2355   by (import transc EXP_MONO_LT)
  2356 
  2357 lemma EXP_MONO_LE: "ALL (x::real) y::real. (exp x <= exp y) = (x <= y)"
  2358   by (import transc EXP_MONO_LE)
  2359 
  2360 lemma EXP_INJ: "ALL (x::real) y::real. (exp x = exp y) = (x = y)"
  2361   by (import transc EXP_INJ)
  2362 
  2363 lemma EXP_TOTAL_LEMMA: "ALL y>=1. EX x>=0. x <= y - 1 & exp x = y"
  2364   by (import transc EXP_TOTAL_LEMMA)
  2365 
  2366 lemma EXP_TOTAL: "ALL y>0. EX x::real. exp x = y"
  2367   by (import transc EXP_TOTAL)
  2368 
  2369 constdefs
  2370   ln :: "real => real" 
  2371   "ln == %x::real. SOME u::real. exp u = x"
  2372 
  2373 lemma ln: "ALL x::real. ln x = (SOME u::real. exp u = x)"
  2374   by (import transc ln)
  2375 
  2376 lemma LN_EXP: "ALL x::real. ln (exp x) = x"
  2377   by (import transc LN_EXP)
  2378 
  2379 lemma EXP_LN: "ALL x::real. (exp (ln x) = x) = (0 < x)"
  2380   by (import transc EXP_LN)
  2381 
  2382 lemma LN_MUL: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x * y) = ln x + ln y"
  2383   by (import transc LN_MUL)
  2384 
  2385 lemma LN_INJ: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x = ln y) = (x = y)"
  2386   by (import transc LN_INJ)
  2387 
  2388 lemma LN_1: "ln 1 = 0"
  2389   by (import transc LN_1)
  2390 
  2391 lemma LN_INV: "ALL x>0. ln (inverse x) = - ln x"
  2392   by (import transc LN_INV)
  2393 
  2394 lemma LN_DIV: "ALL (x::real) y::real. 0 < x & 0 < y --> ln (x / y) = ln x - ln y"
  2395   by (import transc LN_DIV)
  2396 
  2397 lemma LN_MONO_LT: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x < ln y) = (x < y)"
  2398   by (import transc LN_MONO_LT)
  2399 
  2400 lemma LN_MONO_LE: "ALL (x::real) y::real. 0 < x & 0 < y --> (ln x <= ln y) = (x <= y)"
  2401   by (import transc LN_MONO_LE)
  2402 
  2403 lemma LN_POW: "ALL (n::nat) x::real. 0 < x --> ln (x ^ n) = real n * ln x"
  2404   by (import transc LN_POW)
  2405 
  2406 lemma LN_LE: "ALL x>=0. ln (1 + x) <= x"
  2407   by (import transc LN_LE)
  2408 
  2409 lemma LN_LT_X: "ALL x>0. ln x < x"
  2410   by (import transc LN_LT_X)
  2411 
  2412 lemma LN_POS: "ALL x>=1. 0 <= ln x"
  2413   by (import transc LN_POS)
  2414 
  2415 constdefs
  2416   root :: "nat => real => real" 
  2417   "root == %(n::nat) x::real. SOME u::real. (0 < x --> 0 < u) & u ^ n = x"
  2418 
  2419 lemma root: "ALL (n::nat) x::real.
  2420    root n x = (SOME u::real. (0 < x --> 0 < u) & u ^ n = x)"
  2421   by (import transc root)
  2422 
  2423 constdefs
  2424   sqrt :: "real => real" 
  2425   "sqrt == root 2"
  2426 
  2427 lemma sqrt: "ALL x::real. sqrt x = root 2 x"
  2428   by (import transc sqrt)
  2429 
  2430 lemma ROOT_LT_LEMMA: "ALL (n::nat) x::real. 0 < x --> exp (ln x / real (Suc n)) ^ Suc n = x"
  2431   by (import transc ROOT_LT_LEMMA)
  2432 
  2433 lemma ROOT_LN: "ALL (n::nat) x::real. 0 < x --> root (Suc n) x = exp (ln x / real (Suc n))"
  2434   by (import transc ROOT_LN)
  2435 
  2436 lemma ROOT_0: "ALL n::nat. root (Suc n) 0 = 0"
  2437   by (import transc ROOT_0)
  2438 
  2439 lemma ROOT_1: "ALL n::nat. root (Suc n) 1 = 1"
  2440   by (import transc ROOT_1)
  2441 
  2442 lemma ROOT_POS_LT: "ALL (n::nat) x::real. 0 < x --> 0 < root (Suc n) x"
  2443   by (import transc ROOT_POS_LT)
  2444 
  2445 lemma ROOT_POW_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) x ^ Suc n = x"
  2446   by (import transc ROOT_POW_POS)
  2447 
  2448 lemma POW_ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> root (Suc n) (x ^ Suc n) = x"
  2449   by (import transc POW_ROOT_POS)
  2450 
  2451 lemma ROOT_POS: "ALL (n::nat) x::real. 0 <= x --> 0 <= root (Suc n) x"
  2452   by (import transc ROOT_POS)
  2453 
  2454 lemma ROOT_POS_UNIQ: "ALL (n::nat) (x::real) y::real.
  2455    0 <= x & 0 <= y & y ^ Suc n = x --> root (Suc n) x = y"
  2456   by (import transc ROOT_POS_UNIQ)
  2457 
  2458 lemma ROOT_MUL: "ALL (n::nat) (x::real) y::real.
  2459    0 <= x & 0 <= y -->
  2460    root (Suc n) (x * y) = root (Suc n) x * root (Suc n) y"
  2461   by (import transc ROOT_MUL)
  2462 
  2463 lemma ROOT_INV: "ALL (n::nat) x::real.
  2464    0 <= x --> root (Suc n) (inverse x) = inverse (root (Suc n) x)"
  2465   by (import transc ROOT_INV)
  2466 
  2467 lemma ROOT_DIV: "ALL (x::nat) (xa::real) xb::real.
  2468    0 <= xa & 0 <= xb -->
  2469    root (Suc x) (xa / xb) = root (Suc x) xa / root (Suc x) xb"
  2470   by (import transc ROOT_DIV)
  2471 
  2472 lemma ROOT_MONO_LE: "ALL (x::real) y::real.
  2473    0 <= x & x <= y --> root (Suc (n::nat)) x <= root (Suc n) y"
  2474   by (import transc ROOT_MONO_LE)
  2475 
  2476 lemma SQRT_0: "sqrt 0 = 0"
  2477   by (import transc SQRT_0)
  2478 
  2479 lemma SQRT_1: "sqrt 1 = 1"
  2480   by (import transc SQRT_1)
  2481 
  2482 lemma SQRT_POS_LT: "ALL x>0. 0 < sqrt x"
  2483   by (import transc SQRT_POS_LT)
  2484 
  2485 lemma SQRT_POS_LE: "ALL x>=0. 0 <= sqrt x"
  2486   by (import transc SQRT_POS_LE)
  2487 
  2488 lemma SQRT_POW2: "ALL x::real. (sqrt x ^ 2 = x) = (0 <= x)"
  2489   by (import transc SQRT_POW2)
  2490 
  2491 lemma SQRT_POW_2: "ALL x>=0. sqrt x ^ 2 = x"
  2492   by (import transc SQRT_POW_2)
  2493 
  2494 lemma POW_2_SQRT: "0 <= (x::real) --> sqrt (x ^ 2) = x"
  2495   by (import transc POW_2_SQRT)
  2496 
  2497 lemma SQRT_POS_UNIQ: "ALL (x::real) xa::real. 0 <= x & 0 <= xa & xa ^ 2 = x --> sqrt x = xa"
  2498   by (import transc SQRT_POS_UNIQ)
  2499 
  2500 lemma SQRT_MUL: "ALL (x::real) xa::real.
  2501    0 <= x & 0 <= xa --> sqrt (x * xa) = sqrt x * sqrt xa"
  2502   by (import transc SQRT_MUL)
  2503 
  2504 lemma SQRT_INV: "ALL x>=0. sqrt (inverse x) = inverse (sqrt x)"
  2505   by (import transc SQRT_INV)
  2506 
  2507 lemma SQRT_DIV: "ALL (x::real) xa::real.
  2508    0 <= x & 0 <= xa --> sqrt (x / xa) = sqrt x / sqrt xa"
  2509   by (import transc SQRT_DIV)
  2510 
  2511 lemma SQRT_MONO_LE: "ALL (x::real) xa::real. 0 <= x & x <= xa --> sqrt x <= sqrt xa"
  2512   by (import transc SQRT_MONO_LE)
  2513 
  2514 lemma SQRT_EVEN_POW2: "ALL n::nat. EVEN n --> sqrt (2 ^ n) = 2 ^ (n div 2)"
  2515   by (import transc SQRT_EVEN_POW2)
  2516 
  2517 lemma REAL_DIV_SQRT: "ALL x>=0. x / sqrt x = sqrt x"
  2518   by (import transc REAL_DIV_SQRT)
  2519 
  2520 lemma SQRT_EQ: "ALL (x::real) y::real. x ^ 2 = y & 0 <= x --> x = sqrt y"
  2521   by (import transc SQRT_EQ)
  2522 
  2523 lemma SIN_0: "sin 0 = 0"
  2524   by (import transc SIN_0)
  2525 
  2526 lemma COS_0: "cos 0 = 1"
  2527   by (import transc COS_0)
  2528 
  2529 lemma SIN_CIRCLE: "ALL x::real. sin x ^ 2 + cos x ^ 2 = 1"
  2530   by (import transc SIN_CIRCLE)
  2531 
  2532 lemma SIN_BOUND: "ALL x::real. abs (sin x) <= 1"
  2533   by (import transc SIN_BOUND)
  2534 
  2535 lemma SIN_BOUNDS: "ALL x::real. - 1 <= sin x & sin x <= 1"
  2536   by (import transc SIN_BOUNDS)
  2537 
  2538 lemma COS_BOUND: "ALL x::real. abs (cos x) <= 1"
  2539   by (import transc COS_BOUND)
  2540 
  2541 lemma COS_BOUNDS: "ALL x::real. - 1 <= cos x & cos x <= 1"
  2542   by (import transc COS_BOUNDS)
  2543 
  2544 lemma SIN_COS_ADD: "ALL (x::real) y::real.
  2545    (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +
  2546    (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2 =
  2547    0"
  2548   by (import transc SIN_COS_ADD)
  2549 
  2550 lemma SIN_COS_NEG: "ALL x::real. (sin (- x) + sin x) ^ 2 + (cos (- x) - cos x) ^ 2 = 0"
  2551   by (import transc SIN_COS_NEG)
  2552 
  2553 lemma SIN_ADD: "ALL (x::real) y::real. sin (x + y) = sin x * cos y + cos x * sin y"
  2554   by (import transc SIN_ADD)
  2555 
  2556 lemma COS_ADD: "ALL (x::real) y::real. cos (x + y) = cos x * cos y - sin x * sin y"
  2557   by (import transc COS_ADD)
  2558 
  2559 lemma SIN_NEG: "ALL x::real. sin (- x) = - sin x"
  2560   by (import transc SIN_NEG)
  2561 
  2562 lemma COS_NEG: "ALL x::real. cos (- x) = cos x"
  2563   by (import transc COS_NEG)
  2564 
  2565 lemma SIN_DOUBLE: "ALL x::real. sin (2 * x) = 2 * (sin x * cos x)"
  2566   by (import transc SIN_DOUBLE)
  2567 
  2568 lemma COS_DOUBLE: "ALL x::real. cos (2 * x) = cos x ^ 2 - sin x ^ 2"
  2569   by (import transc COS_DOUBLE)
  2570 
  2571 lemma SIN_PAIRED: "ALL x::real.
  2572    sums (%n::nat. (- 1) ^ n / real (FACT (2 * n + 1)) * x ^ (2 * n + 1))
  2573     (sin x)"
  2574   by (import transc SIN_PAIRED)
  2575 
  2576 lemma SIN_POS: "ALL x::real. 0 < x & x < 2 --> 0 < sin x"
  2577   by (import transc SIN_POS)
  2578 
  2579 lemma COS_PAIRED: "ALL x::real.
  2580    sums (%n::nat. (- 1) ^ n / real (FACT (2 * n)) * x ^ (2 * n)) (cos x)"
  2581   by (import transc COS_PAIRED)
  2582 
  2583 lemma COS_2: "cos 2 < 0"
  2584   by (import transc COS_2)
  2585 
  2586 lemma COS_ISZERO: "EX! x::real. 0 <= x & x <= 2 & cos x = 0"
  2587   by (import transc COS_ISZERO)
  2588 
  2589 constdefs
  2590   pi :: "real" 
  2591   "pi == 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
  2592 
  2593 lemma pi: "pi = 2 * (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
  2594   by (import transc pi)
  2595 
  2596 lemma PI2: "pi / 2 = (SOME x::real. 0 <= x & x <= 2 & cos x = 0)"
  2597   by (import transc PI2)
  2598 
  2599 lemma COS_PI2: "cos (pi / 2) = 0"
  2600   by (import transc COS_PI2)
  2601 
  2602 lemma PI2_BOUNDS: "0 < pi / 2 & pi / 2 < 2"
  2603   by (import transc PI2_BOUNDS)
  2604 
  2605 lemma PI_POS: "0 < pi"
  2606   by (import transc PI_POS)
  2607 
  2608 lemma SIN_PI2: "sin (pi / 2) = 1"
  2609   by (import transc SIN_PI2)
  2610 
  2611 lemma COS_PI: "cos pi = - 1"
  2612   by (import transc COS_PI)
  2613 
  2614 lemma SIN_PI: "sin pi = 0"
  2615   by (import transc SIN_PI)
  2616 
  2617 lemma SIN_COS: "ALL x::real. sin x = cos (pi / 2 - x)"
  2618   by (import transc SIN_COS)
  2619 
  2620 lemma COS_SIN: "ALL x::real. cos x = sin (pi / 2 - x)"
  2621   by (import transc COS_SIN)
  2622 
  2623 lemma SIN_PERIODIC_PI: "ALL x::real. sin (x + pi) = - sin x"
  2624   by (import transc SIN_PERIODIC_PI)
  2625 
  2626 lemma COS_PERIODIC_PI: "ALL x::real. cos (x + pi) = - cos x"
  2627   by (import transc COS_PERIODIC_PI)
  2628 
  2629 lemma SIN_PERIODIC: "ALL x::real. sin (x + 2 * pi) = sin x"
  2630   by (import transc SIN_PERIODIC)
  2631 
  2632 lemma COS_PERIODIC: "ALL x::real. cos (x + 2 * pi) = cos x"
  2633   by (import transc COS_PERIODIC)
  2634 
  2635 lemma COS_NPI: "ALL n::nat. cos (real n * pi) = (- 1) ^ n"
  2636   by (import transc COS_NPI)
  2637 
  2638 lemma SIN_NPI: "ALL n::nat. sin (real n * pi) = 0"
  2639   by (import transc SIN_NPI)
  2640 
  2641 lemma SIN_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < sin x"
  2642   by (import transc SIN_POS_PI2)
  2643 
  2644 lemma COS_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < cos x"
  2645   by (import transc COS_POS_PI2)
  2646 
  2647 lemma COS_POS_PI: "ALL x::real. - (pi / 2) < x & x < pi / 2 --> 0 < cos x"
  2648   by (import transc COS_POS_PI)
  2649 
  2650 lemma SIN_POS_PI: "ALL x::real. 0 < x & x < pi --> 0 < sin x"
  2651   by (import transc SIN_POS_PI)
  2652 
  2653 lemma COS_POS_PI2_LE: "ALL x::real. 0 <= x & x <= pi / 2 --> 0 <= cos x"
  2654   by (import transc COS_POS_PI2_LE)
  2655 
  2656 lemma COS_POS_PI_LE: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> 0 <= cos x"
  2657   by (import transc COS_POS_PI_LE)
  2658 
  2659 lemma SIN_POS_PI2_LE: "ALL x::real. 0 <= x & x <= pi / 2 --> 0 <= sin x"
  2660   by (import transc SIN_POS_PI2_LE)
  2661 
  2662 lemma SIN_POS_PI_LE: "ALL x::real. 0 <= x & x <= pi --> 0 <= sin x"
  2663   by (import transc SIN_POS_PI_LE)
  2664 
  2665 lemma COS_TOTAL: "ALL y::real.
  2666    - 1 <= y & y <= 1 --> (EX! x::real. 0 <= x & x <= pi & cos x = y)"
  2667   by (import transc COS_TOTAL)
  2668 
  2669 lemma SIN_TOTAL: "ALL y::real.
  2670    - 1 <= y & y <= 1 -->
  2671    (EX! x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y)"
  2672   by (import transc SIN_TOTAL)
  2673 
  2674 lemma COS_ZERO_LEMMA: "ALL x::real.
  2675    0 <= x & cos x = 0 --> (EX n::nat. ~ EVEN n & x = real n * (pi / 2))"
  2676   by (import transc COS_ZERO_LEMMA)
  2677 
  2678 lemma SIN_ZERO_LEMMA: "ALL x::real.
  2679    0 <= x & sin x = 0 --> (EX n::nat. EVEN n & x = real n * (pi / 2))"
  2680   by (import transc SIN_ZERO_LEMMA)
  2681 
  2682 lemma COS_ZERO: "ALL x::real.
  2683    (cos x = 0) =
  2684    ((EX n::nat. ~ EVEN n & x = real n * (pi / 2)) |
  2685     (EX n::nat. ~ EVEN n & x = - (real n * (pi / 2))))"
  2686   by (import transc COS_ZERO)
  2687 
  2688 lemma SIN_ZERO: "ALL x::real.
  2689    (sin x = 0) =
  2690    ((EX n::nat. EVEN n & x = real n * (pi / 2)) |
  2691     (EX n::nat. EVEN n & x = - (real n * (pi / 2))))"
  2692   by (import transc SIN_ZERO)
  2693 
  2694 constdefs
  2695   tan :: "real => real" 
  2696   "tan == %x::real. sin x / cos x"
  2697 
  2698 lemma tan: "ALL x::real. tan x = sin x / cos x"
  2699   by (import transc tan)
  2700 
  2701 lemma TAN_0: "tan 0 = 0"
  2702   by (import transc TAN_0)
  2703 
  2704 lemma TAN_PI: "tan pi = 0"
  2705   by (import transc TAN_PI)
  2706 
  2707 lemma TAN_NPI: "ALL n::nat. tan (real n * pi) = 0"
  2708   by (import transc TAN_NPI)
  2709 
  2710 lemma TAN_NEG: "ALL x::real. tan (- x) = - tan x"
  2711   by (import transc TAN_NEG)
  2712 
  2713 lemma TAN_PERIODIC: "ALL x::real. tan (x + 2 * pi) = tan x"
  2714   by (import transc TAN_PERIODIC)
  2715 
  2716 lemma TAN_ADD: "ALL (x::real) y::real.
  2717    cos x ~= 0 & cos y ~= 0 & cos (x + y) ~= 0 -->
  2718    tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)"
  2719   by (import transc TAN_ADD)
  2720 
  2721 lemma TAN_DOUBLE: "ALL x::real.
  2722    cos x ~= 0 & cos (2 * x) ~= 0 -->
  2723    tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)"
  2724   by (import transc TAN_DOUBLE)
  2725 
  2726 lemma TAN_POS_PI2: "ALL x::real. 0 < x & x < pi / 2 --> 0 < tan x"
  2727   by (import transc TAN_POS_PI2)
  2728 
  2729 lemma DIFF_TAN: "ALL x::real. cos x ~= 0 --> diffl tan (inverse (cos x ^ 2)) x"
  2730   by (import transc DIFF_TAN)
  2731 
  2732 lemma TAN_TOTAL_LEMMA: "ALL y>0. EX x>0. x < pi / 2 & y < tan x"
  2733   by (import transc TAN_TOTAL_LEMMA)
  2734 
  2735 lemma TAN_TOTAL_POS: "ALL y>=0. EX x>=0. x < pi / 2 & tan x = y"
  2736   by (import transc TAN_TOTAL_POS)
  2737 
  2738 lemma TAN_TOTAL: "ALL y::real. EX! x::real. - (pi / 2) < x & x < pi / 2 & tan x = y"
  2739   by (import transc TAN_TOTAL)
  2740 
  2741 constdefs
  2742   asn :: "real => real" 
  2743   "asn == %y::real. SOME x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y"
  2744 
  2745 lemma asn: "ALL y::real.
  2746    asn y = (SOME x::real. - (pi / 2) <= x & x <= pi / 2 & sin x = y)"
  2747   by (import transc asn)
  2748 
  2749 constdefs
  2750   acs :: "real => real" 
  2751   "acs == %y::real. SOME x::real. 0 <= x & x <= pi & cos x = y"
  2752 
  2753 lemma acs: "ALL y::real. acs y = (SOME x::real. 0 <= x & x <= pi & cos x = y)"
  2754   by (import transc acs)
  2755 
  2756 constdefs
  2757   atn :: "real => real" 
  2758   "atn == %y::real. SOME x::real. - (pi / 2) < x & x < pi / 2 & tan x = y"
  2759 
  2760 lemma atn: "ALL y::real. atn y = (SOME x::real. - (pi / 2) < x & x < pi / 2 & tan x = y)"
  2761   by (import transc atn)
  2762 
  2763 lemma ASN: "ALL y::real.
  2764    - 1 <= y & y <= 1 -->
  2765    - (pi / 2) <= asn y & asn y <= pi / 2 & sin (asn y) = y"
  2766   by (import transc ASN)
  2767 
  2768 lemma ASN_SIN: "ALL y::real. - 1 <= y & y <= 1 --> sin (asn y) = y"
  2769   by (import transc ASN_SIN)
  2770 
  2771 lemma ASN_BOUNDS: "ALL y::real. - 1 <= y & y <= 1 --> - (pi / 2) <= asn y & asn y <= pi / 2"
  2772   by (import transc ASN_BOUNDS)
  2773 
  2774 lemma ASN_BOUNDS_LT: "ALL y::real. - 1 < y & y < 1 --> - (pi / 2) < asn y & asn y < pi / 2"
  2775   by (import transc ASN_BOUNDS_LT)
  2776 
  2777 lemma SIN_ASN: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> asn (sin x) = x"
  2778   by (import transc SIN_ASN)
  2779 
  2780 lemma ACS: "ALL y::real.
  2781    - 1 <= y & y <= 1 --> 0 <= acs y & acs y <= pi & cos (acs y) = y"
  2782   by (import transc ACS)
  2783 
  2784 lemma ACS_COS: "ALL y::real. - 1 <= y & y <= 1 --> cos (acs y) = y"
  2785   by (import transc ACS_COS)
  2786 
  2787 lemma ACS_BOUNDS: "ALL y::real. - 1 <= y & y <= 1 --> 0 <= acs y & acs y <= pi"
  2788   by (import transc ACS_BOUNDS)
  2789 
  2790 lemma ACS_BOUNDS_LT: "ALL y::real. - 1 < y & y < 1 --> 0 < acs y & acs y < pi"
  2791   by (import transc ACS_BOUNDS_LT)
  2792 
  2793 lemma COS_ACS: "ALL x::real. 0 <= x & x <= pi --> acs (cos x) = x"
  2794   by (import transc COS_ACS)
  2795 
  2796 lemma ATN: "ALL y::real. - (pi / 2) < atn y & atn y < pi / 2 & tan (atn y) = y"
  2797   by (import transc ATN)
  2798 
  2799 lemma ATN_TAN: "ALL x::real. tan (atn x) = x"
  2800   by (import transc ATN_TAN)
  2801 
  2802 lemma ATN_BOUNDS: "ALL x::real. - (pi / 2) < atn x & atn x < pi / 2"
  2803   by (import transc ATN_BOUNDS)
  2804 
  2805 lemma TAN_ATN: "ALL x::real. - (pi / 2) < x & x < pi / 2 --> atn (tan x) = x"
  2806   by (import transc TAN_ATN)
  2807 
  2808 lemma TAN_SEC: "ALL x::real. cos x ~= 0 --> 1 + tan x ^ 2 = inverse (cos x) ^ 2"
  2809   by (import transc TAN_SEC)
  2810 
  2811 lemma SIN_COS_SQ: "ALL x::real. 0 <= x & x <= pi --> sin x = sqrt (1 - cos x ^ 2)"
  2812   by (import transc SIN_COS_SQ)
  2813 
  2814 lemma COS_SIN_SQ: "ALL x::real. - (pi / 2) <= x & x <= pi / 2 --> cos x = sqrt (1 - sin x ^ 2)"
  2815   by (import transc COS_SIN_SQ)
  2816 
  2817 lemma COS_ATN_NZ: "ALL x::real. cos (atn x) ~= 0"
  2818   by (import transc COS_ATN_NZ)
  2819 
  2820 lemma COS_ASN_NZ: "ALL x::real. - 1 < x & x < 1 --> cos (asn x) ~= 0"
  2821   by (import transc COS_ASN_NZ)
  2822 
  2823 lemma SIN_ACS_NZ: "ALL x::real. - 1 < x & x < 1 --> sin (acs x) ~= 0"
  2824   by (import transc SIN_ACS_NZ)
  2825 
  2826 lemma COS_SIN_SQRT: "ALL x::real. 0 <= cos x --> cos x = sqrt (1 - sin x ^ 2)"
  2827   by (import transc COS_SIN_SQRT)
  2828 
  2829 lemma SIN_COS_SQRT: "ALL x::real. 0 <= sin x --> sin x = sqrt (1 - cos x ^ 2)"
  2830   by (import transc SIN_COS_SQRT)
  2831 
  2832 lemma DIFF_LN: "ALL x>0. diffl ln (inverse x) x"
  2833   by (import transc DIFF_LN)
  2834 
  2835 lemma DIFF_ASN_LEMMA: "ALL x::real. - 1 < x & x < 1 --> diffl asn (inverse (cos (asn x))) x"
  2836   by (import transc DIFF_ASN_LEMMA)
  2837 
  2838 lemma DIFF_ASN: "ALL x::real. - 1 < x & x < 1 --> diffl asn (inverse (sqrt (1 - x ^ 2))) x"
  2839   by (import transc DIFF_ASN)
  2840 
  2841 lemma DIFF_ACS_LEMMA: "ALL x::real. - 1 < x & x < 1 --> diffl acs (inverse (- sin (acs x))) x"
  2842   by (import transc DIFF_ACS_LEMMA)
  2843 
  2844 lemma DIFF_ACS: "ALL x::real. - 1 < x & x < 1 --> diffl acs (- inverse (sqrt (1 - x ^ 2))) x"
  2845   by (import transc DIFF_ACS)
  2846 
  2847 lemma DIFF_ATN: "ALL x::real. diffl atn (inverse (1 + x ^ 2)) x"
  2848   by (import transc DIFF_ATN)
  2849 
  2850 constdefs
  2851   division :: "real * real => (nat => real) => bool" 
  2852   "(op ==::(real * real => (nat => real) => bool)
  2853         => (real * real => (nat => real) => bool) => prop)
  2854  (division::real * real => (nat => real) => bool)
  2855  ((split::(real => real => (nat => real) => bool)
  2856           => real * real => (nat => real) => bool)
  2857    (%(a::real) (b::real) D::nat => real.
  2858        (op &::bool => bool => bool)
  2859         ((op =::real => real => bool) (D (0::nat)) a)
  2860         ((Ex::(nat => bool) => bool)
  2861           (%N::nat.
  2862               (op &::bool => bool => bool)
  2863                ((All::(nat => bool) => bool)
  2864                  (%n::nat.
  2865                      (op -->::bool => bool => bool)
  2866                       ((op <::nat => nat => bool) n N)
  2867                       ((op <::real => real => bool) (D n)
  2868                         (D ((Suc::nat => nat) n)))))
  2869                ((All::(nat => bool) => bool)
  2870                  (%n::nat.
  2871                      (op -->::bool => bool => bool)
  2872                       ((op <=::nat => nat => bool) N n)
  2873                       ((op =::real => real => bool) (D n) b)))))))"
  2874 
  2875 lemma division: "(All::(real => bool) => bool)
  2876  (%a::real.
  2877      (All::(real => bool) => bool)
  2878       (%b::real.
  2879           (All::((nat => real) => bool) => bool)
  2880            (%D::nat => real.
  2881                (op =::bool => bool => bool)
  2882                 ((division::real * real => (nat => real) => bool)
  2883                   ((Pair::real => real => real * real) a b) D)
  2884                 ((op &::bool => bool => bool)
  2885                   ((op =::real => real => bool) (D (0::nat)) a)
  2886                   ((Ex::(nat => bool) => bool)
  2887                     (%N::nat.
  2888                         (op &::bool => bool => bool)
  2889                          ((All::(nat => bool) => bool)
  2890                            (%n::nat.
  2891                                (op -->::bool => bool => bool)
  2892                                 ((op <::nat => nat => bool) n N)
  2893                                 ((op <::real => real => bool) (D n)
  2894                                   (D ((Suc::nat => nat) n)))))
  2895                          ((All::(nat => bool) => bool)
  2896                            (%n::nat.
  2897                                (op -->::bool => bool => bool)
  2898                                 ((op <=::nat => nat => bool) N n)
  2899                                 ((op =::real => real => bool) (D n)
  2900                                   b)))))))))"
  2901   by (import transc division)
  2902 
  2903 constdefs
  2904   dsize :: "(nat => real) => nat" 
  2905   "(op ==::((nat => real) => nat) => ((nat => real) => nat) => prop)
  2906  (dsize::(nat => real) => nat)
  2907  (%D::nat => real.
  2908      (Eps::(nat => bool) => nat)
  2909       (%N::nat.
  2910           (op &::bool => bool => bool)
  2911            ((All::(nat => bool) => bool)
  2912              (%n::nat.
  2913                  (op -->::bool => bool => bool)
  2914                   ((op <::nat => nat => bool) n N)
  2915                   ((op <::real => real => bool) (D n)
  2916                     (D ((Suc::nat => nat) n)))))
  2917            ((All::(nat => bool) => bool)
  2918              (%n::nat.
  2919                  (op -->::bool => bool => bool)
  2920                   ((op <=::nat => nat => bool) N n)
  2921                   ((op =::real => real => bool) (D n) (D N))))))"
  2922 
  2923 lemma dsize: "(All::((nat => real) => bool) => bool)
  2924  (%D::nat => real.
  2925      (op =::nat => nat => bool) ((dsize::(nat => real) => nat) D)
  2926       ((Eps::(nat => bool) => nat)
  2927         (%N::nat.
  2928             (op &::bool => bool => bool)
  2929              ((All::(nat => bool) => bool)
  2930                (%n::nat.
  2931                    (op -->::bool => bool => bool)
  2932                     ((op <::nat => nat => bool) n N)
  2933                     ((op <::real => real => bool) (D n)
  2934                       (D ((Suc::nat => nat) n)))))
  2935              ((All::(nat => bool) => bool)
  2936                (%n::nat.
  2937                    (op -->::bool => bool => bool)
  2938                     ((op <=::nat => nat => bool) N n)
  2939                     ((op =::real => real => bool) (D n) (D N)))))))"
  2940   by (import transc dsize)
  2941 
  2942 constdefs
  2943   tdiv :: "real * real => (nat => real) * (nat => real) => bool" 
  2944   "tdiv ==
  2945 %(a::real, b::real) (D::nat => real, p::nat => real).
  2946    division (a, b) D & (ALL n::nat. D n <= p n & p n <= D (Suc n))"
  2947 
  2948 lemma tdiv: "ALL (a::real) (b::real) (D::nat => real) p::nat => real.
  2949    tdiv (a, b) (D, p) =
  2950    (division (a, b) D & (ALL n::nat. D n <= p n & p n <= D (Suc n)))"
  2951   by (import transc tdiv)
  2952 
  2953 constdefs
  2954   gauge :: "(real => bool) => (real => real) => bool" 
  2955   "gauge == %(E::real => bool) g::real => real. ALL x::real. E x --> 0 < g x"
  2956 
  2957 lemma gauge: "ALL (E::real => bool) g::real => real.
  2958    gauge E g = (ALL x::real. E x --> 0 < g x)"
  2959   by (import transc gauge)
  2960 
  2961 constdefs
  2962   fine :: "(real => real) => (nat => real) * (nat => real) => bool" 
  2963   "(op ==::((real => real) => (nat => real) * (nat => real) => bool)
  2964         => ((real => real) => (nat => real) * (nat => real) => bool)
  2965            => prop)
  2966  (fine::(real => real) => (nat => real) * (nat => real) => bool)
  2967  (%g::real => real.
  2968      (split::((nat => real) => (nat => real) => bool)
  2969              => (nat => real) * (nat => real) => bool)
  2970       (%(D::nat => real) p::nat => real.
  2971           (All::(nat => bool) => bool)
  2972            (%n::nat.
  2973                (op -->::bool => bool => bool)
  2974                 ((op <::nat => nat => bool) n
  2975                   ((dsize::(nat => real) => nat) D))
  2976                 ((op <::real => real => bool)
  2977                   ((op -::real => real => real) (D ((Suc::nat => nat) n))
  2978                     (D n))
  2979                   (g (p n))))))"
  2980 
  2981 lemma fine: "(All::((real => real) => bool) => bool)
  2982  (%g::real => real.
  2983      (All::((nat => real) => bool) => bool)
  2984       (%D::nat => real.
  2985           (All::((nat => real) => bool) => bool)
  2986            (%p::nat => real.
  2987                (op =::bool => bool => bool)
  2988                 ((fine::(real => real)
  2989                         => (nat => real) * (nat => real) => bool)
  2990                   g ((Pair::(nat => real)
  2991                             => (nat => real)
  2992                                => (nat => real) * (nat => real))
  2993                       D p))
  2994                 ((All::(nat => bool) => bool)
  2995                   (%n::nat.
  2996                       (op -->::bool => bool => bool)
  2997                        ((op <::nat => nat => bool) n
  2998                          ((dsize::(nat => real) => nat) D))
  2999                        ((op <::real => real => bool)
  3000                          ((op -::real => real => real)
  3001                            (D ((Suc::nat => nat) n)) (D n))
  3002                          (g (p n))))))))"
  3003   by (import transc fine)
  3004 
  3005 constdefs
  3006   rsum :: "(nat => real) * (nat => real) => (real => real) => real" 
  3007   "rsum ==
  3008 %(D::nat => real, p::nat => real) f::real => real.
  3009    real.sum (0, dsize D) (%n::nat. f (p n) * (D (Suc n) - D n))"
  3010 
  3011 lemma rsum: "ALL (D::nat => real) (p::nat => real) f::real => real.
  3012    rsum (D, p) f =
  3013    real.sum (0, dsize D) (%n::nat. f (p n) * (D (Suc n) - D n))"
  3014   by (import transc rsum)
  3015 
  3016 constdefs
  3017   Dint :: "real * real => (real => real) => real => bool" 
  3018   "Dint ==
  3019 %(a::real, b::real) (f::real => real) k::real.
  3020    ALL e>0.
  3021       EX g::real => real.
  3022          gauge (%x::real. a <= x & x <= b) g &
  3023          (ALL (D::nat => real) p::nat => real.
  3024              tdiv (a, b) (D, p) & fine g (D, p) -->
  3025              abs (rsum (D, p) f - k) < e)"
  3026 
  3027 lemma Dint: "ALL (a::real) (b::real) (f::real => real) k::real.
  3028    Dint (a, b) f k =
  3029    (ALL e>0.
  3030        EX g::real => real.
  3031           gauge (%x::real. a <= x & x <= b) g &
  3032           (ALL (D::nat => real) p::nat => real.
  3033               tdiv (a, b) (D, p) & fine g (D, p) -->
  3034               abs (rsum (D, p) f - k) < e))"
  3035   by (import transc Dint)
  3036 
  3037 lemma DIVISION_0: "ALL (a::real) b::real. a = b --> dsize (%n::nat. if n = 0 then a else b) = 0"
  3038   by (import transc DIVISION_0)
  3039 
  3040 lemma DIVISION_1: "ALL (a::real) b::real. a < b --> dsize (%n::nat. if n = 0 then a else b) = 1"
  3041   by (import transc DIVISION_1)
  3042 
  3043 lemma DIVISION_SINGLE: "ALL (a::real) b::real.
  3044    a <= b --> division (a, b) (%n::nat. if n = 0 then a else b)"
  3045   by (import transc DIVISION_SINGLE)
  3046 
  3047 lemma DIVISION_LHS: "ALL (D::nat => real) (a::real) b::real. division (a, b) D --> D 0 = a"
  3048   by (import transc DIVISION_LHS)
  3049 
  3050 lemma DIVISION_THM: "(All::((nat => real) => bool) => bool)
  3051  (%D::nat => real.
  3052      (All::(real => bool) => bool)
  3053       (%a::real.
  3054           (All::(real => bool) => bool)
  3055            (%b::real.
  3056                (op =::bool => bool => bool)
  3057                 ((division::real * real => (nat => real) => bool)
  3058                   ((Pair::real => real => real * real) a b) D)
  3059                 ((op &::bool => bool => bool)
  3060                   ((op =::real => real => bool) (D (0::nat)) a)
  3061                   ((op &::bool => bool => bool)
  3062                     ((All::(nat => bool) => bool)
  3063                       (%n::nat.
  3064                           (op -->::bool => bool => bool)
  3065                            ((op <::nat => nat => bool) n
  3066                              ((dsize::(nat => real) => nat) D))
  3067                            ((op <::real => real => bool) (D n)
  3068                              (D ((Suc::nat => nat) n)))))
  3069                     ((All::(nat => bool) => bool)
  3070                       (%n::nat.
  3071                           (op -->::bool => bool => bool)
  3072                            ((op <=::nat => nat => bool)
  3073                              ((dsize::(nat => real) => nat) D) n)
  3074                            ((op =::real => real => bool) (D n) b))))))))"
  3075   by (import transc DIVISION_THM)
  3076 
  3077 lemma DIVISION_RHS: "ALL (D::nat => real) (a::real) b::real.
  3078    division (a, b) D --> D (dsize D) = b"
  3079   by (import transc DIVISION_RHS)
  3080 
  3081 lemma DIVISION_LT_GEN: "ALL (D::nat => real) (a::real) (b::real) (m::nat) n::nat.
  3082    division (a, b) D & m < n & n <= dsize D --> D m < D n"
  3083   by (import transc DIVISION_LT_GEN)
  3084 
  3085 lemma DIVISION_LT: "(All::((nat => real) => bool) => bool)
  3086  (%D::nat => real.
  3087      (All::(real => bool) => bool)
  3088       (%a::real.
  3089           (All::(real => bool) => bool)
  3090            (%b::real.
  3091                (op -->::bool => bool => bool)
  3092                 ((division::real * real => (nat => real) => bool)
  3093                   ((Pair::real => real => real * real) a b) D)
  3094                 ((All::(nat => bool) => bool)
  3095                   (%n::nat.
  3096                       (op -->::bool => bool => bool)
  3097                        ((op <::nat => nat => bool) n
  3098                          ((dsize::(nat => real) => nat) D))
  3099                        ((op <::real => real => bool) (D (0::nat))
  3100                          (D ((Suc::nat => nat) n))))))))"
  3101   by (import transc DIVISION_LT)
  3102 
  3103 lemma DIVISION_LE: "ALL (D::nat => real) (a::real) b::real. division (a, b) D --> a <= b"
  3104   by (import transc DIVISION_LE)
  3105 
  3106 lemma DIVISION_GT: "(All::((nat => real) => bool) => bool)
  3107  (%D::nat => real.
  3108      (All::(real => bool) => bool)
  3109       (%a::real.
  3110           (All::(real => bool) => bool)
  3111            (%b::real.
  3112                (op -->::bool => bool => bool)
  3113                 ((division::real * real => (nat => real) => bool)
  3114                   ((Pair::real => real => real * real) a b) D)
  3115                 ((All::(nat => bool) => bool)
  3116                   (%n::nat.
  3117                       (op -->::bool => bool => bool)
  3118                        ((op <::nat => nat => bool) n
  3119                          ((dsize::(nat => real) => nat) D))
  3120                        ((op <::real => real => bool) (D n)
  3121                          (D ((dsize::(nat => real) => nat) D))))))))"
  3122   by (import transc DIVISION_GT)
  3123 
  3124 lemma DIVISION_EQ: "ALL (D::nat => real) (a::real) b::real.
  3125    division (a, b) D --> (a = b) = (dsize D = 0)"
  3126   by (import transc DIVISION_EQ)
  3127 
  3128 lemma DIVISION_LBOUND: "ALL (D::nat => real) (a::real) b::real.
  3129    division (a, b) D --> (ALL r::nat. a <= D r)"
  3130   by (import transc DIVISION_LBOUND)
  3131 
  3132 lemma DIVISION_LBOUND_LT: "ALL (D::nat => real) (a::real) b::real.
  3133    division (a, b) D & dsize D ~= 0 --> (ALL n::nat. a < D (Suc n))"
  3134   by (import transc DIVISION_LBOUND_LT)
  3135 
  3136 lemma DIVISION_UBOUND: "ALL (D::nat => real) (a::real) b::real.
  3137    division (a, b) D --> (ALL r::nat. D r <= b)"
  3138   by (import transc DIVISION_UBOUND)
  3139 
  3140 lemma DIVISION_UBOUND_LT: "ALL (D::nat => real) (a::real) (b::real) n::nat.
  3141    division (a, b) D & n < dsize D --> D n < b"
  3142   by (import transc DIVISION_UBOUND_LT)
  3143 
  3144 lemma DIVISION_APPEND: "ALL (a::real) (b::real) c::real.
  3145    (EX (D1::nat => real) p1::nat => real.
  3146        tdiv (a, b) (D1, p1) & fine (g::real => real) (D1, p1)) &
  3147    (EX (D2::nat => real) p2::nat => real.
  3148        tdiv (b, c) (D2, p2) & fine g (D2, p2)) -->
  3149    (EX (x::nat => real) p::nat => real. tdiv (a, c) (x, p) & fine g (x, p))"
  3150   by (import transc DIVISION_APPEND)
  3151 
  3152 lemma DIVISION_EXISTS: "ALL (a::real) (b::real) g::real => real.
  3153    a <= b & gauge (%x::real. a <= x & x <= b) g -->
  3154    (EX (D::nat => real) p::nat => real. tdiv (a, b) (D, p) & fine g (D, p))"
  3155   by (import transc DIVISION_EXISTS)
  3156 
  3157 lemma GAUGE_MIN: "ALL (E::real => bool) (g1::real => real) g2::real => real.
  3158    gauge E g1 & gauge E g2 -->
  3159    gauge E (%x::real. if g1 x < g2 x then g1 x else g2 x)"
  3160   by (import transc GAUGE_MIN)
  3161 
  3162 lemma FINE_MIN: "ALL (g1::real => real) (g2::real => real) (D::nat => real) p::nat => real.
  3163    fine (%x::real. if g1 x < g2 x then g1 x else g2 x) (D, p) -->
  3164    fine g1 (D, p) & fine g2 (D, p)"
  3165   by (import transc FINE_MIN)
  3166 
  3167 lemma DINT_UNIQ: "ALL (a::real) (b::real) (f::real => real) (k1::real) k2::real.
  3168    a <= b & Dint (a, b) f k1 & Dint (a, b) f k2 --> k1 = k2"
  3169   by (import transc DINT_UNIQ)
  3170 
  3171 lemma INTEGRAL_NULL: "ALL (f::real => real) a::real. Dint (a, a) f 0"
  3172   by (import transc INTEGRAL_NULL)
  3173 
  3174 lemma FTC1: "ALL (f::real => real) (f'::real => real) (a::real) b::real.
  3175    a <= b & (ALL x::real. a <= x & x <= b --> diffl f (f' x) x) -->
  3176    Dint (a, b) f' (f b - f a)"
  3177   by (import transc FTC1)
  3178 
  3179 lemma MCLAURIN: "ALL (f::real => real) (diff::nat => real => real) (h::real) n::nat.
  3180    0 < h &
  3181    0 < n &
  3182    diff 0 = f &
  3183    (ALL (m::nat) t::real.
  3184        m < n & 0 <= t & t <= h --> diffl (diff m) (diff (Suc m) t) t) -->
  3185    (EX t>0.
  3186        t < h &
  3187        f h =
  3188        real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * h ^ m) +
  3189        diff n t / real (FACT n) * h ^ n)"
  3190   by (import transc MCLAURIN)
  3191 
  3192 lemma MCLAURIN_NEG: "ALL (f::real => real) (diff::nat => real => real) (h::real) n::nat.
  3193    h < 0 &
  3194    0 < n &
  3195    diff 0 = f &
  3196    (ALL (m::nat) t::real.
  3197        m < n & h <= t & t <= 0 --> diffl (diff m) (diff (Suc m) t) t) -->
  3198    (EX t::real.
  3199        h < t &
  3200        t < 0 &
  3201        f h =
  3202        real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * h ^ m) +
  3203        diff n t / real (FACT n) * h ^ n)"
  3204   by (import transc MCLAURIN_NEG)
  3205 
  3206 lemma MCLAURIN_ALL_LT: "ALL (f::real => real) diff::nat => real => real.
  3207    diff 0 = f &
  3208    (ALL (m::nat) x::real. diffl (diff m) (diff (Suc m) x) x) -->
  3209    (ALL (x::real) n::nat.
  3210        x ~= 0 & 0 < n -->
  3211        (EX t::real.
  3212            0 < abs t &
  3213            abs t < abs x &
  3214            f x =
  3215            real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) +
  3216            diff n t / real (FACT n) * x ^ n))"
  3217   by (import transc MCLAURIN_ALL_LT)
  3218 
  3219 lemma MCLAURIN_ZERO: "ALL (diff::nat => real => real) (n::nat) x::real.
  3220    x = 0 & 0 < n -->
  3221    real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) = diff 0 0"
  3222   by (import transc MCLAURIN_ZERO)
  3223 
  3224 lemma MCLAURIN_ALL_LE: "ALL (f::real => real) diff::nat => real => real.
  3225    diff 0 = f &
  3226    (ALL (m::nat) x::real. diffl (diff m) (diff (Suc m) x) x) -->
  3227    (ALL (x::real) n::nat.
  3228        EX t::real.
  3229           abs t <= abs x &
  3230           f x =
  3231           real.sum (0, n) (%m::nat. diff m 0 / real (FACT m) * x ^ m) +
  3232           diff n t / real (FACT n) * x ^ n)"
  3233   by (import transc MCLAURIN_ALL_LE)
  3234 
  3235 lemma MCLAURIN_EXP_LT: "ALL (x::real) n::nat.
  3236    x ~= 0 & 0 < n -->
  3237    (EX xa::real.
  3238        0 < abs xa &
  3239        abs xa < abs x &
  3240        exp x =
  3241        real.sum (0, n) (%m::nat. x ^ m / real (FACT m)) +
  3242        exp xa / real (FACT n) * x ^ n)"
  3243   by (import transc MCLAURIN_EXP_LT)
  3244 
  3245 lemma MCLAURIN_EXP_LE: "ALL (x::real) n::nat.
  3246    EX xa::real.
  3247       abs xa <= abs x &
  3248       exp x =
  3249       real.sum (0, n) (%m::nat. x ^ m / real (FACT m)) +
  3250       exp xa / real (FACT n) * x ^ n"
  3251   by (import transc MCLAURIN_EXP_LE)
  3252 
  3253 lemma DIFF_LN_COMPOSITE: "ALL (g::real => real) (m::real) x::real.
  3254    diffl g m x & 0 < g x -->
  3255    diffl (%x::real. ln (g x)) (inverse (g x) * m) x"
  3256   by (import transc DIFF_LN_COMPOSITE)
  3257 
  3258 ;end_setup
  3259 
  3260 ;setup_theory poly
  3261 
  3262 consts
  3263   poly :: "real list => real => real" 
  3264 
  3265 specification (poly_primdef: poly) poly_def: "(ALL x::real. poly [] x = 0) &
  3266 (ALL (h::real) (t::real list) x::real. poly (h # t) x = h + x * poly t x)"
  3267   by (import poly poly_def)
  3268 
  3269 consts
  3270   poly_add :: "real list => real list => real list" 
  3271 
  3272 specification (poly_add_primdef: poly_add) poly_add_def: "(ALL l2::real list. poly_add [] l2 = l2) &
  3273 (ALL (h::real) (t::real list) l2::real list.
  3274     poly_add (h # t) l2 =
  3275     (if l2 = [] then h # t else (h + hd l2) # poly_add t (tl l2)))"
  3276   by (import poly poly_add_def)
  3277 
  3278 consts
  3279   "##" :: "real => real list => real list" ("##")
  3280 
  3281 specification ("##") poly_cmul_def: "(ALL c::real. ## c [] = []) &
  3282 (ALL (c::real) (h::real) t::real list. ## c (h # t) = c * h # ## c t)"
  3283   by (import poly poly_cmul_def)
  3284 
  3285 consts
  3286   poly_neg :: "real list => real list" 
  3287 
  3288 defs
  3289   poly_neg_primdef: "poly_neg == ## (- 1)"
  3290 
  3291 lemma poly_neg_def: "poly_neg = ## (- 1)"
  3292   by (import poly poly_neg_def)
  3293 
  3294 consts
  3295   poly_mul :: "real list => real list => real list" 
  3296 
  3297 specification (poly_mul_primdef: poly_mul) poly_mul_def: "(ALL l2::real list. poly_mul [] l2 = []) &
  3298 (ALL (h::real) (t::real list) l2::real list.
  3299     poly_mul (h # t) l2 =
  3300     (if t = [] then ## h l2 else poly_add (## h l2) (0 # poly_mul t l2)))"
  3301   by (import poly poly_mul_def)
  3302 
  3303 consts
  3304   poly_exp :: "real list => nat => real list" 
  3305 
  3306 specification (poly_exp_primdef: poly_exp) poly_exp_def: "(ALL p::real list. poly_exp p 0 = [1]) &
  3307 (ALL (p::real list) n::nat. poly_exp p (Suc n) = poly_mul p (poly_exp p n))"
  3308   by (import poly poly_exp_def)
  3309 
  3310 consts
  3311   poly_diff_aux :: "nat => real list => real list" 
  3312 
  3313 specification (poly_diff_aux_primdef: poly_diff_aux) poly_diff_aux_def: "(ALL n::nat. poly_diff_aux n [] = []) &
  3314 (ALL (n::nat) (h::real) t::real list.
  3315     poly_diff_aux n (h # t) = real n * h # poly_diff_aux (Suc n) t)"
  3316   by (import poly poly_diff_aux_def)
  3317 
  3318 constdefs
  3319   diff :: "real list => real list" 
  3320   "diff == %l::real list. if l = [] then [] else poly_diff_aux 1 (tl l)"
  3321 
  3322 lemma poly_diff_def: "ALL l::real list. diff l = (if l = [] then [] else poly_diff_aux 1 (tl l))"
  3323   by (import poly poly_diff_def)
  3324 
  3325 lemma POLY_ADD_CLAUSES: "poly_add [] (p2::real list) = p2 &
  3326 poly_add (p1::real list) [] = p1 &
  3327 poly_add ((h1::real) # (t1::real list)) ((h2::real) # (t2::real list)) =
  3328 (h1 + h2) # poly_add t1 t2"
  3329   by (import poly POLY_ADD_CLAUSES)
  3330 
  3331 lemma POLY_CMUL_CLAUSES: "## (c::real) [] = [] & ## c ((h::real) # (t::real list)) = c * h # ## c t"
  3332   by (import poly POLY_CMUL_CLAUSES)
  3333 
  3334 lemma POLY_NEG_CLAUSES: "poly_neg [] = [] & poly_neg ((h::real) # (t::real list)) = - h # poly_neg t"
  3335   by (import poly POLY_NEG_CLAUSES)
  3336 
  3337 lemma POLY_MUL_CLAUSES: "poly_mul [] (p2::real list) = [] &
  3338 poly_mul [h1::real] p2 = ## h1 p2 &
  3339 poly_mul (h1 # (k1::real) # (t1::real list)) p2 =
  3340 poly_add (## h1 p2) (0 # poly_mul (k1 # t1) p2)"
  3341   by (import poly POLY_MUL_CLAUSES)
  3342 
  3343 lemma POLY_DIFF_CLAUSES: "diff [] = [] &
  3344 diff [c::real] = [] & diff ((h::real) # (t::real list)) = poly_diff_aux 1 t"
  3345   by (import poly POLY_DIFF_CLAUSES)
  3346 
  3347 lemma POLY_ADD: "ALL (t::real list) (p2::real list) x::real.
  3348    poly (poly_add t p2) x = poly t x + poly p2 x"
  3349   by (import poly POLY_ADD)
  3350 
  3351 lemma POLY_CMUL: "ALL (t::real list) (c::real) x::real. poly (## c t) x = c * poly t x"
  3352   by (import poly POLY_CMUL)
  3353 
  3354 lemma POLY_NEG: "ALL (x::real list) xa::real. poly (poly_neg x) xa = - poly x xa"
  3355   by (import poly POLY_NEG)
  3356 
  3357 lemma POLY_MUL: "ALL (x::real) (t::real list) p2::real list.
  3358    poly (poly_mul t p2) x = poly t x * poly p2 x"
  3359   by (import poly POLY_MUL)
  3360 
  3361 lemma POLY_EXP: "ALL (p::real list) (n::nat) x::real. poly (poly_exp p n) x = poly p x ^ n"
  3362   by (import poly POLY_EXP)
  3363 
  3364 lemma POLY_DIFF_LEMMA: "ALL (t::real list) (n::nat) x::real.
  3365    diffl (%x::real. x ^ Suc n * poly t x)
  3366     (x ^ n * poly (poly_diff_aux (Suc n) t) x) x"
  3367   by (import poly POLY_DIFF_LEMMA)
  3368 
  3369 lemma POLY_DIFF: "ALL (t::real list) x::real. diffl (poly t) (poly (diff t) x) x"
  3370   by (import poly POLY_DIFF)
  3371 
  3372 lemma POLY_DIFFERENTIABLE: "ALL l::real list. All (differentiable (poly l))"
  3373   by (import poly POLY_DIFFERENTIABLE)
  3374 
  3375 lemma POLY_CONT: "ALL l::real list. All (contl (poly l))"
  3376   by (import poly POLY_CONT)
  3377 
  3378 lemma POLY_IVT_POS: "ALL (x::real list) (xa::real) xb::real.
  3379    xa < xb & poly x xa < 0 & 0 < poly x xb -->
  3380    (EX xc::real. xa < xc & xc < xb & poly x xc = 0)"
  3381   by (import poly POLY_IVT_POS)
  3382 
  3383 lemma POLY_IVT_NEG: "ALL (p::real list) (a::real) b::real.
  3384    a < b & 0 < poly p a & poly p b < 0 -->
  3385    (EX x::real. a < x & x < b & poly p x = 0)"
  3386   by (import poly POLY_IVT_NEG)
  3387 
  3388 lemma POLY_MVT: "ALL (p::real list) (a::real) b::real.
  3389    a < b -->
  3390    (EX x::real.
  3391        a < x & x < b & poly p b - poly p a = (b - a) * poly (diff p) x)"
  3392   by (import poly POLY_MVT)
  3393 
  3394 lemma POLY_ADD_RZERO: "ALL x::real list. poly (poly_add x []) = poly x"
  3395   by (import poly POLY_ADD_RZERO)
  3396 
  3397 lemma POLY_MUL_ASSOC: "ALL (x::real list) (xa::real list) xb::real list.
  3398    poly (poly_mul x (poly_mul xa xb)) = poly (poly_mul (poly_mul x xa) xb)"
  3399   by (import poly POLY_MUL_ASSOC)
  3400 
  3401 lemma POLY_EXP_ADD: "ALL (x::nat) (xa::nat) xb::real list.
  3402    poly (poly_exp xb (xa + x)) =
  3403    poly (poly_mul (poly_exp xb xa) (poly_exp xb x))"
  3404   by (import poly POLY_EXP_ADD)
  3405 
  3406 lemma POLY_DIFF_AUX_ADD: "ALL (t::real list) (p2::real list) n::nat.
  3407    poly (poly_diff_aux n (poly_add t p2)) =
  3408    poly (poly_add (poly_diff_aux n t) (poly_diff_aux n p2))"
  3409   by (import poly POLY_DIFF_AUX_ADD)
  3410 
  3411 lemma POLY_DIFF_AUX_CMUL: "ALL (t::real list) (c::real) n::nat.
  3412    poly (poly_diff_aux n (## c t)) = poly (## c (poly_diff_aux n t))"
  3413   by (import poly POLY_DIFF_AUX_CMUL)
  3414 
  3415 lemma POLY_DIFF_AUX_NEG: "ALL (x::real list) xa::nat.
  3416    poly (poly_diff_aux xa (poly_neg x)) =
  3417    poly (poly_neg (poly_diff_aux xa x))"
  3418   by (import poly POLY_DIFF_AUX_NEG)
  3419 
  3420 lemma POLY_DIFF_AUX_MUL_LEMMA: "ALL (t::real list) n::nat.
  3421    poly (poly_diff_aux (Suc n) t) = poly (poly_add (poly_diff_aux n t) t)"
  3422   by (import poly POLY_DIFF_AUX_MUL_LEMMA)
  3423 
  3424 lemma POLY_DIFF_ADD: "ALL (t::real list) p2::real list.
  3425    poly (diff (poly_add t p2)) = poly (poly_add (diff t) (diff p2))"
  3426   by (import poly POLY_DIFF_ADD)
  3427 
  3428 lemma POLY_DIFF_CMUL: "ALL (t::real list) c::real. poly (diff (## c t)) = poly (## c (diff t))"
  3429   by (import poly POLY_DIFF_CMUL)
  3430 
  3431 lemma POLY_DIFF_NEG: "ALL x::real list. poly (diff (poly_neg x)) = poly (poly_neg (diff x))"
  3432   by (import poly POLY_DIFF_NEG)
  3433 
  3434 lemma POLY_DIFF_MUL_LEMMA: "ALL (x::real list) xa::real.
  3435    poly (diff (xa # x)) = poly (poly_add (0 # diff x) x)"
  3436   by (import poly POLY_DIFF_MUL_LEMMA)
  3437 
  3438 lemma POLY_DIFF_MUL: "ALL (t::real list) p2::real list.
  3439    poly (diff (poly_mul t p2)) =
  3440    poly (poly_add (poly_mul t (diff p2)) (poly_mul (diff t) p2))"
  3441   by (import poly POLY_DIFF_MUL)
  3442 
  3443 lemma POLY_DIFF_EXP: "ALL (p::real list) n::nat.
  3444    poly (diff (poly_exp p (Suc n))) =
  3445    poly (poly_mul (## (real (Suc n)) (poly_exp p n)) (diff p))"
  3446   by (import poly POLY_DIFF_EXP)
  3447 
  3448 lemma POLY_DIFF_EXP_PRIME: "ALL (n::nat) a::real.
  3449    poly (diff (poly_exp [- a, 1] (Suc n))) =
  3450    poly (## (real (Suc n)) (poly_exp [- a, 1] n))"
  3451   by (import poly POLY_DIFF_EXP_PRIME)
  3452 
  3453 lemma POLY_LINEAR_REM: "ALL (t::real list) h::real.
  3454    EX (q::real list) r::real.
  3455       h # t = poly_add [r] (poly_mul [- (a::real), 1] q)"
  3456   by (import poly POLY_LINEAR_REM)
  3457 
  3458 lemma POLY_LINEAR_DIVIDES: "ALL (a::real) t::real list.
  3459    (poly t a = 0) = (t = [] | (EX q::real list. t = poly_mul [- a, 1] q))"
  3460   by (import poly POLY_LINEAR_DIVIDES)
  3461 
  3462 lemma POLY_LENGTH_MUL: "ALL x::real list. length (poly_mul [- (a::real), 1] x) = Suc (length x)"
  3463   by (import poly POLY_LENGTH_MUL)
  3464 
  3465 lemma POLY_ROOTS_INDEX_LEMMA: "(All::(nat => bool) => bool)
  3466  (%n::nat.
  3467      (All::(real list => bool) => bool)
  3468       (%p::real list.
  3469           (op -->::bool => bool => bool)
  3470            ((op &::bool => bool => bool)
  3471              ((Not::bool => bool)
  3472                ((op =::(real => real) => (real => real) => bool)
  3473                  ((poly::real list => real => real) p)
  3474                  ((poly::real list => real => real) ([]::real list))))
  3475              ((op =::nat => nat => bool) ((size::real list => nat) p) n))
  3476            ((Ex::((nat => real) => bool) => bool)
  3477              (%i::nat => real.
  3478                  (All::(real => bool) => bool)
  3479                   (%x::real.
  3480                       (op -->::bool => bool => bool)
  3481                        ((op =::real => real => bool)
  3482                          ((poly::real list => real => real) p x) (0::real))
  3483                        ((Ex::(nat => bool) => bool)
  3484                          (%m::nat.
  3485                              (op &::bool => bool => bool)
  3486                               ((op <=::nat => nat => bool) m n)
  3487                               ((op =::real => real => bool) x (i m)))))))))"
  3488   by (import poly POLY_ROOTS_INDEX_LEMMA)
  3489 
  3490 lemma POLY_ROOTS_INDEX_LENGTH: "(All::(real list => bool) => bool)
  3491  (%p::real list.
  3492      (op -->::bool => bool => bool)
  3493       ((Not::bool => bool)
  3494         ((op =::(real => real) => (real => real) => bool)
  3495           ((poly::real list => real => real) p)
  3496           ((poly::real list => real => real) ([]::real list))))
  3497       ((Ex::((nat => real) => bool) => bool)
  3498         (%i::nat => real.
  3499             (All::(real => bool) => bool)
  3500              (%x::real.
  3501                  (op -->::bool => bool => bool)
  3502                   ((op =::real => real => bool)
  3503                     ((poly::real list => real => real) p x) (0::real))
  3504                   ((Ex::(nat => bool) => bool)
  3505                     (%n::nat.
  3506                         (op &::bool => bool => bool)
  3507                          ((op <=::nat => nat => bool) n
  3508                            ((size::real list => nat) p))
  3509                          ((op =::real => real => bool) x (i n))))))))"
  3510   by (import poly POLY_ROOTS_INDEX_LENGTH)
  3511 
  3512 lemma POLY_ROOTS_FINITE_LEMMA: "(All::(real list => bool) => bool)
  3513  (%p::real list.
  3514      (op -->::bool => bool => bool)
  3515       ((Not::bool => bool)
  3516         ((op =::(real => real) => (real => real) => bool)
  3517           ((poly::real list => real => real) p)
  3518           ((poly::real list => real => real) ([]::real list))))
  3519       ((Ex::(nat => bool) => bool)
  3520         (%N::nat.
  3521             (Ex::((nat => real) => bool) => bool)
  3522              (%i::nat => real.
  3523                  (All::(real => bool) => bool)
  3524                   (%x::real.
  3525                       (op -->::bool => bool => bool)
  3526                        ((op =::real => real => bool)
  3527                          ((poly::real list => real => real) p x) (0::real))
  3528                        ((Ex::(nat => bool) => bool)
  3529                          (%n::nat.
  3530                              (op &::bool => bool => bool)
  3531                               ((op <::nat => nat => bool) n N)
  3532                               ((op =::real => real => bool) x (i n)))))))))"
  3533   by (import poly POLY_ROOTS_FINITE_LEMMA)
  3534 
  3535 lemma FINITE_LEMMA: "(All::((nat => real) => bool) => bool)
  3536  (%i::nat => real.
  3537      (All::(nat => bool) => bool)
  3538       (%x::nat.
  3539           (All::((real => bool) => bool) => bool)
  3540            (%xa::real => bool.
  3541                (op -->::bool => bool => bool)
  3542                 ((All::(real => bool) => bool)
  3543                   (%xb::real.
  3544                       (op -->::bool => bool => bool) (xa xb)
  3545                        ((Ex::(nat => bool) => bool)
  3546                          (%n::nat.
  3547                              (op &::bool => bool => bool)
  3548                               ((op <::nat => nat => bool) n x)
  3549                               ((op =::real => real => bool) xb (i n))))))
  3550                 ((Ex::(real => bool) => bool)
  3551                   (%a::real.
  3552                       (All::(real => bool) => bool)
  3553                        (%x::real.
  3554                            (op -->::bool => bool => bool) (xa x)
  3555                             ((op <::real => real => bool) x a)))))))"
  3556   by (import poly FINITE_LEMMA)
  3557 
  3558 lemma POLY_ROOTS_FINITE: "(All::(real list => bool) => bool)
  3559  (%p::real list.
  3560      (op =::bool => bool => bool)
  3561       ((Not::bool => bool)
  3562         ((op =::(real => real) => (real => real) => bool)
  3563           ((poly::real list => real => real) p)
  3564           ((poly::real list => real => real) ([]::real list))))
  3565       ((Ex::(nat => bool) => bool)
  3566         (%N::nat.
  3567             (Ex::((nat => real) => bool) => bool)
  3568              (%i::nat => real.
  3569                  (All::(real => bool) => bool)
  3570                   (%x::real.
  3571                       (op -->::bool => bool => bool)
  3572                        ((op =::real => real => bool)
  3573                          ((poly::real list => real => real) p x) (0::real))
  3574                        ((Ex::(nat => bool) => bool)
  3575                          (%n::nat.
  3576                              (op &::bool => bool => bool)
  3577                               ((op <::nat => nat => bool) n N)
  3578                               ((op =::real => real => bool) x (i n)))))))))"
  3579   by (import poly POLY_ROOTS_FINITE)
  3580 
  3581 lemma POLY_ENTIRE_LEMMA: "ALL (p::real list) q::real list.
  3582    poly p ~= poly [] & poly q ~= poly [] --> poly (poly_mul p q) ~= poly []"
  3583   by (import poly POLY_ENTIRE_LEMMA)
  3584 
  3585 lemma POLY_ENTIRE: "ALL (p::real list) q::real list.
  3586    (poly (poly_mul p q) = poly []) = (poly p = poly [] | poly q = poly [])"
  3587   by (import poly POLY_ENTIRE)
  3588 
  3589 lemma POLY_MUL_LCANCEL: "ALL (x::real list) (xa::real list) xb::real list.
  3590    (poly (poly_mul x xa) = poly (poly_mul x xb)) =
  3591    (poly x = poly [] | poly xa = poly xb)"
  3592   by (import poly POLY_MUL_LCANCEL)
  3593 
  3594 lemma POLY_EXP_EQ_0: "ALL (p::real list) n::nat.
  3595    (poly (poly_exp p n) = poly []) = (poly p = poly [] & n ~= 0)"
  3596   by (import poly POLY_EXP_EQ_0)
  3597 
  3598 lemma POLY_PRIME_EQ_0: "ALL a::real. poly [a, 1] ~= poly []"
  3599   by (import poly POLY_PRIME_EQ_0)
  3600 
  3601 lemma POLY_EXP_PRIME_EQ_0: "ALL (a::real) n::nat. poly (poly_exp [a, 1] n) ~= poly []"
  3602   by (import poly POLY_EXP_PRIME_EQ_0)
  3603 
  3604 lemma POLY_ZERO_LEMMA: "ALL (h::real) t::real list.
  3605    poly (h # t) = poly [] --> h = 0 & poly t = poly []"
  3606   by (import poly POLY_ZERO_LEMMA)
  3607 
  3608 lemma POLY_ZERO: "ALL t::real list. (poly t = poly []) = list_all (%c::real. c = 0) t"
  3609   by (import poly POLY_ZERO)
  3610 
  3611 lemma POLY_DIFF_AUX_ISZERO: "ALL (t::real list) n::nat.
  3612    list_all (%c::real. c = 0) (poly_diff_aux (Suc n) t) =
  3613    list_all (%c::real. c = 0) t"
  3614   by (import poly POLY_DIFF_AUX_ISZERO)
  3615 
  3616 lemma POLY_DIFF_ISZERO: "ALL x::real list.
  3617    poly (diff x) = poly [] --> (EX h::real. poly x = poly [h])"
  3618   by (import poly POLY_DIFF_ISZERO)
  3619 
  3620 lemma POLY_DIFF_ZERO: "ALL x::real list. poly x = poly [] --> poly (diff x) = poly []"
  3621   by (import poly POLY_DIFF_ZERO)
  3622 
  3623 lemma POLY_DIFF_WELLDEF: "ALL (p::real list) q::real list.
  3624    poly p = poly q --> poly (diff p) = poly (diff q)"
  3625   by (import poly POLY_DIFF_WELLDEF)
  3626 
  3627 constdefs
  3628   poly_divides :: "real list => real list => bool" 
  3629   "poly_divides ==
  3630 %(p1::real list) p2::real list.
  3631    EX q::real list. poly p2 = poly (poly_mul p1 q)"
  3632 
  3633 lemma poly_divides: "ALL (p1::real list) p2::real list.
  3634    poly_divides p1 p2 = (EX q::real list. poly p2 = poly (poly_mul p1 q))"
  3635   by (import poly poly_divides)
  3636 
  3637 lemma POLY_PRIMES: "ALL (a::real) (p::real list) q::real list.
  3638    poly_divides [a, 1] (poly_mul p q) =
  3639    (poly_divides [a, 1] p | poly_divides [a, 1] q)"
  3640   by (import poly POLY_PRIMES)
  3641 
  3642 lemma POLY_DIVIDES_REFL: "ALL p::real list. poly_divides p p"
  3643   by (import poly POLY_DIVIDES_REFL)
  3644 
  3645 lemma POLY_DIVIDES_TRANS: "ALL (p::real list) (q::real list) r::real list.
  3646    poly_divides p q & poly_divides q r --> poly_divides p r"
  3647   by (import poly POLY_DIVIDES_TRANS)
  3648 
  3649 lemma POLY_DIVIDES_EXP: "ALL (p::real list) (m::nat) n::nat.
  3650    m <= n --> poly_divides (poly_exp p m) (poly_exp p n)"
  3651   by (import poly POLY_DIVIDES_EXP)
  3652 
  3653 lemma POLY_EXP_DIVIDES: "ALL (p::real list) (q::real list) (m::nat) n::nat.
  3654    poly_divides (poly_exp p n) q & m <= n --> poly_divides (poly_exp p m) q"
  3655   by (import poly POLY_EXP_DIVIDES)
  3656 
  3657 lemma POLY_DIVIDES_ADD: "ALL (p::real list) (q::real list) r::real list.
  3658    poly_divides p q & poly_divides p r --> poly_divides p (poly_add q r)"
  3659   by (import poly POLY_DIVIDES_ADD)
  3660 
  3661 lemma POLY_DIVIDES_SUB: "ALL (p::real list) (q::real list) r::real list.
  3662    poly_divides p q & poly_divides p (poly_add q r) --> poly_divides p r"
  3663   by (import poly POLY_DIVIDES_SUB)
  3664 
  3665 lemma POLY_DIVIDES_SUB2: "ALL (p::real list) (q::real list) r::real list.
  3666    poly_divides p r & poly_divides p (poly_add q r) --> poly_divides p q"
  3667   by (import poly POLY_DIVIDES_SUB2)
  3668 
  3669 lemma POLY_DIVIDES_ZERO: "ALL (p::real list) q::real list. poly p = poly [] --> poly_divides q p"
  3670   by (import poly POLY_DIVIDES_ZERO)
  3671 
  3672 lemma POLY_ORDER_EXISTS: "ALL (a::real) (d::nat) p::real list.
  3673    length p = d & poly p ~= poly [] -->
  3674    (EX x::nat.
  3675        poly_divides (poly_exp [- a, 1] x) p &
  3676        ~ poly_divides (poly_exp [- a, 1] (Suc x)) p)"
  3677   by (import poly POLY_ORDER_EXISTS)
  3678 
  3679 lemma POLY_ORDER: "ALL (p::real list) a::real.
  3680    poly p ~= poly [] -->
  3681    (EX! n::nat.
  3682        poly_divides (poly_exp [- a, 1] n) p &
  3683        ~ poly_divides (poly_exp [- a, 1] (Suc n)) p)"
  3684   by (import poly POLY_ORDER)
  3685 
  3686 constdefs
  3687   poly_order :: "real => real list => nat" 
  3688   "poly_order ==
  3689 %(a::real) p::real list.
  3690    SOME n::nat.
  3691       poly_divides (poly_exp [- a, 1] n) p &
  3692       ~ poly_divides (poly_exp [- a, 1] (Suc n)) p"
  3693 
  3694 lemma poly_order: "ALL (a::real) p::real list.
  3695    poly_order a p =
  3696    (SOME n::nat.
  3697        poly_divides (poly_exp [- a, 1] n) p &
  3698        ~ poly_divides (poly_exp [- a, 1] (Suc n)) p)"
  3699   by (import poly poly_order)
  3700 
  3701 lemma ORDER: "ALL (p::real list) (a::real) n::nat.
  3702    (poly_divides (poly_exp [- a, 1] n) p &
  3703     ~ poly_divides (poly_exp [- a, 1] (Suc n)) p) =
  3704    (n = poly_order a p & poly p ~= poly [])"
  3705   by (import poly ORDER)
  3706 
  3707 lemma ORDER_THM: "ALL (p::real list) a::real.
  3708    poly p ~= poly [] -->
  3709    poly_divides (poly_exp [- a, 1] (poly_order a p)) p &
  3710    ~ poly_divides (poly_exp [- a, 1] (Suc (poly_order a p))) p"
  3711   by (import poly ORDER_THM)
  3712 
  3713 lemma ORDER_UNIQUE: "ALL (p::real list) (a::real) n::nat.
  3714    poly p ~= poly [] &
  3715    poly_divides (poly_exp [- a, 1] n) p &
  3716    ~ poly_divides (poly_exp [- a, 1] (Suc n)) p -->
  3717    n = poly_order a p"
  3718   by (import poly ORDER_UNIQUE)
  3719 
  3720 lemma ORDER_POLY: "ALL (p::real list) (q::real list) a::real.
  3721    poly p = poly q --> poly_order a p = poly_order a q"
  3722   by (import poly ORDER_POLY)
  3723 
  3724 lemma ORDER_ROOT: "ALL (p::real list) a::real.
  3725    (poly p a = 0) = (poly p = poly [] | poly_order a p ~= 0)"
  3726   by (import poly ORDER_ROOT)
  3727 
  3728 lemma ORDER_DIVIDES: "ALL (p::real list) (a::real) n::nat.
  3729    poly_divides (poly_exp [- a, 1] n) p =
  3730    (poly p = poly [] | n <= poly_order a p)"
  3731   by (import poly ORDER_DIVIDES)
  3732 
  3733 lemma ORDER_DECOMP: "ALL (p::real list) a::real.
  3734    poly p ~= poly [] -->
  3735    (EX x::real list.
  3736        poly p = poly (poly_mul (poly_exp [- a, 1] (poly_order a p)) x) &
  3737        ~ poly_divides [- a, 1] x)"
  3738   by (import poly ORDER_DECOMP)
  3739 
  3740 lemma ORDER_MUL: "ALL (a::real) (p::real list) q::real list.
  3741    poly (poly_mul p q) ~= poly [] -->
  3742    poly_order a (poly_mul p q) = poly_order a p + poly_order a q"
  3743   by (import poly ORDER_MUL)
  3744 
  3745 lemma ORDER_DIFF: "ALL (p::real list) a::real.
  3746    poly (diff p) ~= poly [] & poly_order a p ~= 0 -->
  3747    poly_order a p = Suc (poly_order a (diff p))"
  3748   by (import poly ORDER_DIFF)
  3749 
  3750 lemma POLY_SQUAREFREE_DECOMP_ORDER: "ALL (p::real list) (q::real list) (d::real list) (e::real list)
  3751    (r::real list) s::real list.
  3752    poly (diff p) ~= poly [] &
  3753    poly p = poly (poly_mul q d) &
  3754    poly (diff p) = poly (poly_mul e d) &
  3755    poly d = poly (poly_add (poly_mul r p) (poly_mul s (diff p))) -->
  3756    (ALL a::real. poly_order a q = (if poly_order a p = 0 then 0 else 1))"
  3757   by (import poly POLY_SQUAREFREE_DECOMP_ORDER)
  3758 
  3759 constdefs
  3760   rsquarefree :: "real list => bool" 
  3761   "rsquarefree ==
  3762 %p::real list.
  3763    poly p ~= poly [] &
  3764    (ALL a::real. poly_order a p = 0 | poly_order a p = 1)"
  3765 
  3766 lemma rsquarefree: "ALL p::real list.
  3767    rsquarefree p =
  3768    (poly p ~= poly [] &
  3769     (ALL a::real. poly_order a p = 0 | poly_order a p = 1))"
  3770   by (import poly rsquarefree)
  3771 
  3772 lemma RSQUAREFREE_ROOTS: "ALL p::real list.
  3773    rsquarefree p = (ALL a::real. ~ (poly p a = 0 & poly (diff p) a = 0))"
  3774   by (import poly RSQUAREFREE_ROOTS)
  3775 
  3776 lemma RSQUAREFREE_DECOMP: "ALL (p::real list) a::real.
  3777    rsquarefree p & poly p a = 0 -->
  3778    (EX q::real list. poly p = poly (poly_mul [- a, 1] q) & poly q a ~= 0)"
  3779   by (import poly RSQUAREFREE_DECOMP)
  3780 
  3781 lemma POLY_SQUAREFREE_DECOMP: "ALL (p::real list) (q::real list) (d::real list) (e::real list)
  3782    (r::real list) s::real list.
  3783    poly (diff p) ~= poly [] &
  3784    poly p = poly (poly_mul q d) &
  3785    poly (diff p) = poly (poly_mul e d) &
  3786    poly d = poly (poly_add (poly_mul r p) (poly_mul s (diff p))) -->
  3787    rsquarefree q & (ALL x::real. (poly q x = 0) = (poly p x = 0))"
  3788   by (import poly POLY_SQUAREFREE_DECOMP)
  3789 
  3790 consts
  3791   normalize :: "real list => real list" 
  3792 
  3793 specification (normalize) normalize: "normalize [] = [] &
  3794 (ALL (h::real) t::real list.
  3795     normalize (h # t) =
  3796     (if normalize t = [] then if h = 0 then [] else [h]
  3797      else h # normalize t))"
  3798   by (import poly normalize)
  3799 
  3800 lemma POLY_NORMALIZE: "ALL t::real list. poly (normalize t) = poly t"
  3801   by (import poly POLY_NORMALIZE)
  3802 
  3803 constdefs
  3804   degree :: "real list => nat" 
  3805   "degree == %p::real list. PRE (length (normalize p))"
  3806 
  3807 lemma degree: "ALL p::real list. degree p = PRE (length (normalize p))"
  3808   by (import poly degree)
  3809 
  3810 lemma DEGREE_ZERO: "ALL p::real list. poly p = poly [] --> degree p = 0"
  3811   by (import poly DEGREE_ZERO)
  3812 
  3813 lemma POLY_ROOTS_FINITE_SET: "ALL p::real list.
  3814    poly p ~= poly [] --> FINITE (GSPEC (%x::real. (x, poly p x = 0)))"
  3815   by (import poly POLY_ROOTS_FINITE_SET)
  3816 
  3817 lemma POLY_MONO: "ALL (x::real) (k::real) xa::real list.
  3818    abs x <= k --> abs (poly xa x) <= poly (map abs xa) k"
  3819   by (import poly POLY_MONO)
  3820 
  3821 ;end_setup
  3822 
  3823 end
  3824