src/HOL/Import/HOL/HOL4Real.thy
author skalberg
Fri, 01 Apr 2005 18:59:17 +0200
changeset 15647 b1f486a9c56b
parent 15071 b65fc0787fbe
child 16417 9bc16273c2d4
permissions -rw-r--r--
Updated import configuration.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
     1
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
     2
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     3
theory HOL4Real = HOL4Base:
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     4
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     5
;setup_theory realax
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     6
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     7
lemma HREAL_RDISTRIB: "ALL x y z.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     8
   hreal_mul (hreal_add x y) z = hreal_add (hreal_mul x z) (hreal_mul y z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
     9
  by (import realax HREAL_RDISTRIB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    10
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    11
lemma HREAL_EQ_ADDL: "ALL x y. x ~= hreal_add x y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    12
  by (import realax HREAL_EQ_ADDL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    13
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    14
lemma HREAL_EQ_LADD: "ALL x y z. (hreal_add x y = hreal_add x z) = (y = z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    15
  by (import realax HREAL_EQ_LADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    16
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    17
lemma HREAL_LT_REFL: "ALL x. ~ hreal_lt x x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    18
  by (import realax HREAL_LT_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    19
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    20
lemma HREAL_LT_ADDL: "ALL x y. hreal_lt x (hreal_add x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    21
  by (import realax HREAL_LT_ADDL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    22
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    23
lemma HREAL_LT_NE: "ALL x y. hreal_lt x y --> x ~= y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    24
  by (import realax HREAL_LT_NE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    25
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    26
lemma HREAL_LT_ADDR: "ALL x y. ~ hreal_lt (hreal_add x y) x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    27
  by (import realax HREAL_LT_ADDR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    28
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    29
lemma HREAL_LT_GT: "ALL x y. hreal_lt x y --> ~ hreal_lt y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    30
  by (import realax HREAL_LT_GT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    31
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    32
lemma HREAL_LT_ADD2: "ALL x1 x2 y1 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    33
   hreal_lt x1 y1 & hreal_lt x2 y2 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    34
   hreal_lt (hreal_add x1 x2) (hreal_add y1 y2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    35
  by (import realax HREAL_LT_ADD2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    36
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    37
lemma HREAL_LT_LADD: "ALL x y z. hreal_lt (hreal_add x y) (hreal_add x z) = hreal_lt y z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    38
  by (import realax HREAL_LT_LADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    39
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    40
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    41
  treal_0 :: "hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    42
  "treal_0 == (hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    43
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    44
lemma treal_0: "treal_0 = (hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    45
  by (import realax treal_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    46
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    47
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    48
  treal_1 :: "hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    49
  "treal_1 == (hreal_add hreal_1 hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    50
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    51
lemma treal_1: "treal_1 = (hreal_add hreal_1 hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    52
  by (import realax treal_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    53
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    54
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    55
  treal_neg :: "hreal * hreal => hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    56
  "treal_neg == %(x, y). (y, x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    57
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    58
lemma treal_neg: "ALL x y. treal_neg (x, y) = (y, x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    59
  by (import realax treal_neg)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    60
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    61
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    62
  treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    63
  "treal_add == %(x1, y1) (x2, y2). (hreal_add x1 x2, hreal_add y1 y2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    64
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    65
lemma treal_add: "ALL x1 y1 x2 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    66
   treal_add (x1, y1) (x2, y2) = (hreal_add x1 x2, hreal_add y1 y2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    67
  by (import realax treal_add)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    68
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    69
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    70
  treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    71
  "treal_mul ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    72
%(x1, y1) (x2, y2).
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    73
   (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    74
    hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    75
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    76
lemma treal_mul: "ALL x1 y1 x2 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    77
   treal_mul (x1, y1) (x2, y2) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    78
   (hreal_add (hreal_mul x1 x2) (hreal_mul y1 y2),
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    79
    hreal_add (hreal_mul x1 y2) (hreal_mul y1 x2))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    80
  by (import realax treal_mul)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    81
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    82
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    83
  treal_lt :: "hreal * hreal => hreal * hreal => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    84
  "treal_lt == %(x1, y1) (x2, y2). hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    85
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    86
lemma treal_lt: "ALL x1 y1 x2 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    87
   treal_lt (x1, y1) (x2, y2) = hreal_lt (hreal_add x1 y2) (hreal_add x2 y1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    88
  by (import realax treal_lt)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    89
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    90
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    91
  treal_inv :: "hreal * hreal => hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    92
  "treal_inv ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    93
%(x, y).
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    94
   if x = y then treal_0
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    95
   else if hreal_lt y x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    96
        then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    97
        else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    98
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
    99
lemma treal_inv: "ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   100
   treal_inv (x, y) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   101
   (if x = y then treal_0
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   102
    else if hreal_lt y x
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   103
         then (hreal_add (hreal_inv (hreal_sub x y)) hreal_1, hreal_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   104
         else (hreal_1, hreal_add (hreal_inv (hreal_sub y x)) hreal_1))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   105
  by (import realax treal_inv)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   106
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   107
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   108
  treal_eq :: "hreal * hreal => hreal * hreal => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   109
  "treal_eq == %(x1, y1) (x2, y2). hreal_add x1 y2 = hreal_add x2 y1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   110
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   111
lemma treal_eq: "ALL x1 y1 x2 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   112
   treal_eq (x1, y1) (x2, y2) = (hreal_add x1 y2 = hreal_add x2 y1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   113
  by (import realax treal_eq)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   114
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   115
lemma TREAL_EQ_REFL: "ALL x. treal_eq x x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   116
  by (import realax TREAL_EQ_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   117
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   118
lemma TREAL_EQ_SYM: "ALL x y. treal_eq x y = treal_eq y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   119
  by (import realax TREAL_EQ_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   120
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   121
lemma TREAL_EQ_TRANS: "ALL x y z. treal_eq x y & treal_eq y z --> treal_eq x z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   122
  by (import realax TREAL_EQ_TRANS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   123
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   124
lemma TREAL_EQ_EQUIV: "ALL p q. treal_eq p q = (treal_eq p = treal_eq q)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   125
  by (import realax TREAL_EQ_EQUIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   126
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   127
lemma TREAL_EQ_AP: "ALL p q. p = q --> treal_eq p q"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   128
  by (import realax TREAL_EQ_AP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   129
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   130
lemma TREAL_10: "~ treal_eq treal_1 treal_0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   131
  by (import realax TREAL_10)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   132
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   133
lemma TREAL_ADD_SYM: "ALL x y. treal_add x y = treal_add y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   134
  by (import realax TREAL_ADD_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   135
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   136
lemma TREAL_MUL_SYM: "ALL x y. treal_mul x y = treal_mul y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   137
  by (import realax TREAL_MUL_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   138
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   139
lemma TREAL_ADD_ASSOC: "ALL x y z. treal_add x (treal_add y z) = treal_add (treal_add x y) z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   140
  by (import realax TREAL_ADD_ASSOC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   141
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   142
lemma TREAL_MUL_ASSOC: "ALL x y z. treal_mul x (treal_mul y z) = treal_mul (treal_mul x y) z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   143
  by (import realax TREAL_MUL_ASSOC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   144
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   145
lemma TREAL_LDISTRIB: "ALL x y z.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   146
   treal_mul x (treal_add y z) = treal_add (treal_mul x y) (treal_mul x z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   147
  by (import realax TREAL_LDISTRIB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   148
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   149
lemma TREAL_ADD_LID: "ALL x. treal_eq (treal_add treal_0 x) x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   150
  by (import realax TREAL_ADD_LID)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   151
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   152
lemma TREAL_MUL_LID: "ALL x. treal_eq (treal_mul treal_1 x) x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   153
  by (import realax TREAL_MUL_LID)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   154
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   155
lemma TREAL_ADD_LINV: "ALL x. treal_eq (treal_add (treal_neg x) x) treal_0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   156
  by (import realax TREAL_ADD_LINV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   157
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   158
lemma TREAL_INV_0: "treal_eq (treal_inv treal_0) treal_0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   159
  by (import realax TREAL_INV_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   160
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   161
lemma TREAL_MUL_LINV: "ALL x. ~ treal_eq x treal_0 --> treal_eq (treal_mul (treal_inv x) x) treal_1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   162
  by (import realax TREAL_MUL_LINV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   163
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   164
lemma TREAL_LT_TOTAL: "ALL x y. treal_eq x y | treal_lt x y | treal_lt y x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   165
  by (import realax TREAL_LT_TOTAL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   166
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   167
lemma TREAL_LT_REFL: "ALL x. ~ treal_lt x x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   168
  by (import realax TREAL_LT_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   169
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   170
lemma TREAL_LT_TRANS: "ALL x y z. treal_lt x y & treal_lt y z --> treal_lt x z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   171
  by (import realax TREAL_LT_TRANS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   172
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   173
lemma TREAL_LT_ADD: "ALL x y z. treal_lt y z --> treal_lt (treal_add x y) (treal_add x z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   174
  by (import realax TREAL_LT_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   175
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   176
lemma TREAL_LT_MUL: "ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   177
   treal_lt treal_0 x & treal_lt treal_0 y -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   178
   treal_lt treal_0 (treal_mul x y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   179
  by (import realax TREAL_LT_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   180
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   181
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   182
  treal_of_hreal :: "hreal => hreal * hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   183
  "treal_of_hreal == %x. (hreal_add x hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   184
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   185
lemma treal_of_hreal: "ALL x. treal_of_hreal x = (hreal_add x hreal_1, hreal_1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   186
  by (import realax treal_of_hreal)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   187
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   188
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   189
  hreal_of_treal :: "hreal * hreal => hreal" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   190
  "hreal_of_treal == %(x, y). SOME d. x = hreal_add y d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   191
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   192
lemma hreal_of_treal: "ALL x y. hreal_of_treal (x, y) = (SOME d. x = hreal_add y d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   193
  by (import realax hreal_of_treal)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   194
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   195
lemma TREAL_BIJ: "(ALL h. hreal_of_treal (treal_of_hreal h) = h) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   196
(ALL r. treal_lt treal_0 r = treal_eq (treal_of_hreal (hreal_of_treal r)) r)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   197
  by (import realax TREAL_BIJ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   198
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   199
lemma TREAL_ISO: "ALL h i. hreal_lt h i --> treal_lt (treal_of_hreal h) (treal_of_hreal i)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   200
  by (import realax TREAL_ISO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   201
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   202
lemma TREAL_BIJ_WELLDEF: "ALL h i. treal_eq h i --> hreal_of_treal h = hreal_of_treal i"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   203
  by (import realax TREAL_BIJ_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   204
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   205
lemma TREAL_NEG_WELLDEF: "ALL x1 x2. treal_eq x1 x2 --> treal_eq (treal_neg x1) (treal_neg x2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   206
  by (import realax TREAL_NEG_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   207
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   208
lemma TREAL_ADD_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 --> treal_eq (treal_add x1 y) (treal_add x2 y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   209
  by (import realax TREAL_ADD_WELLDEFR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   210
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   211
lemma TREAL_ADD_WELLDEF: "ALL x1 x2 y1 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   212
   treal_eq x1 x2 & treal_eq y1 y2 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   213
   treal_eq (treal_add x1 y1) (treal_add x2 y2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   214
  by (import realax TREAL_ADD_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   215
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   216
lemma TREAL_MUL_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 --> treal_eq (treal_mul x1 y) (treal_mul x2 y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   217
  by (import realax TREAL_MUL_WELLDEFR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   218
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   219
lemma TREAL_MUL_WELLDEF: "ALL x1 x2 y1 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   220
   treal_eq x1 x2 & treal_eq y1 y2 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   221
   treal_eq (treal_mul x1 y1) (treal_mul x2 y2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   222
  by (import realax TREAL_MUL_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   223
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   224
lemma TREAL_LT_WELLDEFR: "ALL x1 x2 y. treal_eq x1 x2 --> treal_lt x1 y = treal_lt x2 y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   225
  by (import realax TREAL_LT_WELLDEFR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   226
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   227
lemma TREAL_LT_WELLDEFL: "ALL x y1 y2. treal_eq y1 y2 --> treal_lt x y1 = treal_lt x y2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   228
  by (import realax TREAL_LT_WELLDEFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   229
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   230
lemma TREAL_LT_WELLDEF: "ALL x1 x2 y1 y2.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   231
   treal_eq x1 x2 & treal_eq y1 y2 --> treal_lt x1 y1 = treal_lt x2 y2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   232
  by (import realax TREAL_LT_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   233
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   234
lemma TREAL_INV_WELLDEF: "ALL x1 x2. treal_eq x1 x2 --> treal_eq (treal_inv x1) (treal_inv x2)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   235
  by (import realax TREAL_INV_WELLDEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   236
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   237
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   238
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   239
;setup_theory real
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   240
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   241
lemma REAL_0: "(0::real) = (0::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   242
  by (import real REAL_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   243
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   244
lemma REAL_1: "(1::real) = (1::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   245
  by (import real REAL_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   246
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   247
lemma REAL_ADD_LID_UNIQ: "ALL (x::real) y::real. (x + y = y) = (x = (0::real))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   248
  by (import real REAL_ADD_LID_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   249
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   250
lemma REAL_ADD_RID_UNIQ: "ALL (x::real) y::real. (x + y = x) = (y = (0::real))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   251
  by (import real REAL_ADD_RID_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   252
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   253
lemma REAL_LNEG_UNIQ: "ALL (x::real) y::real. (x + y = (0::real)) = (x = - y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   254
  by (import real REAL_LNEG_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   255
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   256
lemma REAL_LT_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   257
  by (import real REAL_LT_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   258
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   259
lemma REAL_LTE_TOTAL: "ALL (x::real) y::real. x < y | y <= x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   260
  by (import real REAL_LTE_TOTAL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   261
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   262
lemma REAL_LET_ANTISYM: "ALL (x::real) y::real. ~ (x < y & y <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   263
  by (import real REAL_LET_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   264
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   265
lemma REAL_LTE_ANTSYM: "ALL (x::real) y::real. ~ (x <= y & y < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   266
  by (import real REAL_LTE_ANTSYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   267
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   268
lemma REAL_LT_NEGTOTAL: "ALL x::real. x = (0::real) | (0::real) < x | (0::real) < - x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   269
  by (import real REAL_LT_NEGTOTAL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   270
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   271
lemma REAL_LE_NEGTOTAL: "ALL x::real. (0::real) <= x | (0::real) <= - x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   272
  by (import real REAL_LE_NEGTOTAL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   273
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   274
lemma REAL_LT_ADDNEG: "ALL (x::real) (y::real) z::real. (y < x + - z) = (y + z < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   275
  by (import real REAL_LT_ADDNEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   276
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   277
lemma REAL_LT_ADDNEG2: "ALL (x::real) (y::real) z::real. (x + - y < z) = (x < z + y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   278
  by (import real REAL_LT_ADDNEG2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   279
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   280
lemma REAL_LT_ADD1: "ALL (x::real) y::real. x <= y --> x < y + (1::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   281
  by (import real REAL_LT_ADD1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   282
14796
1e83aa391ade updated;
wenzelm
parents: 14694
diff changeset
   283
lemma REAL_SUB_ADD2: "ALL (x::real) y::real. y + (x - y) = x"
1e83aa391ade updated;
wenzelm
parents: 14694
diff changeset
   284
  by (import real REAL_SUB_ADD2)
1e83aa391ade updated;
wenzelm
parents: 14694
diff changeset
   285
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   286
lemma REAL_SUB_LT: "ALL (x::real) y::real. ((0::real) < x - y) = (y < x)"
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   287
  by (import real REAL_SUB_LT)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   288
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   289
lemma REAL_SUB_LE: "ALL (x::real) y::real. ((0::real) <= x - y) = (y <= x)"
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   290
  by (import real REAL_SUB_LE)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   291
14796
1e83aa391ade updated;
wenzelm
parents: 14694
diff changeset
   292
lemma REAL_ADD_SUB: "ALL (x::real) y::real. x + y - x = y"
1e83aa391ade updated;
wenzelm
parents: 14694
diff changeset
   293
  by (import real REAL_ADD_SUB)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   294
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   295
lemma REAL_NEG_EQ: "ALL (x::real) y::real. (- x = y) = (x = - y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   296
  by (import real REAL_NEG_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   297
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   298
lemma REAL_NEG_MINUS1: "ALL x::real. - x = - (1::real) * x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   299
  by (import real REAL_NEG_MINUS1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   300
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   301
lemma REAL_LT_LMUL_0: "ALL (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   302
   (0::real) < x --> ((0::real) < x * y) = ((0::real) < y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   303
  by (import real REAL_LT_LMUL_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   304
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   305
lemma REAL_LT_RMUL_0: "ALL (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   306
   (0::real) < y --> ((0::real) < x * y) = ((0::real) < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   307
  by (import real REAL_LT_RMUL_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   308
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   309
lemma REAL_LT_LMUL: "ALL (x::real) (y::real) z::real. (0::real) < x --> (x * y < x * z) = (y < z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   310
  by (import real REAL_LT_LMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   311
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   312
lemma REAL_LINV_UNIQ: "ALL (x::real) y::real. x * y = (1::real) --> x = inverse y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   313
  by (import real REAL_LINV_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   314
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   315
lemma REAL_LE_INV: "ALL x>=0::real. (0::real) <= inverse x"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   316
  by (import real REAL_LE_INV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   317
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   318
lemma REAL_LE_ADDR: "ALL (x::real) y::real. (x <= x + y) = ((0::real) <= y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   319
  by (import real REAL_LE_ADDR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   320
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   321
lemma REAL_LE_ADDL: "ALL (x::real) y::real. (y <= x + y) = ((0::real) <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   322
  by (import real REAL_LE_ADDL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   323
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   324
lemma REAL_LT_ADDR: "ALL (x::real) y::real. (x < x + y) = ((0::real) < y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   325
  by (import real REAL_LT_ADDR)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   326
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   327
lemma REAL_LT_ADDL: "ALL (x::real) y::real. (y < x + y) = ((0::real) < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   328
  by (import real REAL_LT_ADDL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   329
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   330
lemma REAL_LT_NZ: "ALL n::nat. (real n ~= (0::real)) = ((0::real) < real n)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   331
  by (import real REAL_LT_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   332
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   333
lemma REAL_NZ_IMP_LT: "ALL n::nat. n ~= (0::nat) --> (0::real) < real n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   334
  by (import real REAL_NZ_IMP_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   335
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   336
lemma REAL_LT_RDIV_0: "ALL (y::real) z::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   337
   (0::real) < z --> ((0::real) < y / z) = ((0::real) < y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   338
  by (import real REAL_LT_RDIV_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   339
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   340
lemma REAL_LT_RDIV: "ALL (x::real) (y::real) z::real. (0::real) < z --> (x / z < y / z) = (x < y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   341
  by (import real REAL_LT_RDIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   342
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   343
lemma REAL_LT_FRACTION_0: "ALL (n::nat) d::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   344
   n ~= (0::nat) --> ((0::real) < d / real n) = ((0::real) < d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   345
  by (import real REAL_LT_FRACTION_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   346
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   347
lemma REAL_LT_MULTIPLE: "ALL (x::nat) xa::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   348
   (1::nat) < x --> (xa < real x * xa) = ((0::real) < xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   349
  by (import real REAL_LT_MULTIPLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   350
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   351
lemma REAL_LT_FRACTION: "ALL (n::nat) d::real. (1::nat) < n --> (d / real n < d) = ((0::real) < d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   352
  by (import real REAL_LT_FRACTION)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   353
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   354
lemma REAL_LT_HALF2: "ALL d::real. (d / (2::real) < d) = ((0::real) < d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   355
  by (import real REAL_LT_HALF2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   356
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   357
lemma REAL_DIV_LMUL: "ALL (x::real) y::real. y ~= (0::real) --> y * (x / y) = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   358
  by (import real REAL_DIV_LMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   359
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   360
lemma REAL_DIV_RMUL: "ALL (x::real) y::real. y ~= (0::real) --> x / y * y = x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   361
  by (import real REAL_DIV_RMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   362
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   363
lemma REAL_DOWN: "ALL x>0::real. EX xa>0::real. xa < x"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   364
  by (import real REAL_DOWN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   365
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   366
lemma REAL_SUB_SUB: "ALL (x::real) y::real. x - y - x = - y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   367
  by (import real REAL_SUB_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   368
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   369
lemma REAL_ADD2_SUB2: "ALL (a::real) (b::real) (c::real) d::real. a + b - (c + d) = a - c + (b - d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   370
  by (import real REAL_ADD2_SUB2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   371
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   372
lemma REAL_LET_ADD: "ALL (x::real) y::real. (0::real) <= x & (0::real) < y --> (0::real) < x + y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   373
  by (import real REAL_LET_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   374
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   375
lemma REAL_LTE_ADD: "ALL (x::real) y::real. (0::real) < x & (0::real) <= y --> (0::real) < x + y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   376
  by (import real REAL_LTE_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   377
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   378
lemma REAL_SUB_LNEG: "ALL (x::real) y::real. - x - y = - (x + y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   379
  by (import real REAL_SUB_LNEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   380
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   381
lemma REAL_SUB_NEG2: "ALL (x::real) y::real. - x - - y = y - x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   382
  by (import real REAL_SUB_NEG2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   383
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   384
lemma REAL_SUB_TRIANGLE: "ALL (a::real) (b::real) c::real. a - b + (b - c) = a - c"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   385
  by (import real REAL_SUB_TRIANGLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   386
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   387
lemma REAL_INV_MUL: "ALL (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   388
   x ~= (0::real) & y ~= (0::real) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   389
   inverse (x * y) = inverse x * inverse y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   390
  by (import real REAL_INV_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   391
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   392
lemma REAL_SUB_INV2: "ALL (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   393
   x ~= (0::real) & y ~= (0::real) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   394
   inverse x - inverse y = (y - x) / (x * y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   395
  by (import real REAL_SUB_INV2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   396
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   397
lemma REAL_SUB_SUB2: "ALL (x::real) y::real. x - (x - y) = y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   398
  by (import real REAL_SUB_SUB2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   399
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   400
lemma REAL_ADD_SUB2: "ALL (x::real) y::real. x - (x + y) = - y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   401
  by (import real REAL_ADD_SUB2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   402
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   403
lemma REAL_LE_MUL2: "ALL (x1::real) (x2::real) (y1::real) y2::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   404
   (0::real) <= x1 & (0::real) <= y1 & x1 <= x2 & y1 <= y2 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   405
   x1 * y1 <= x2 * y2"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   406
  by (import real REAL_LE_MUL2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   407
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   408
lemma REAL_LE_LDIV: "ALL (x::real) (y::real) z::real. (0::real) < x & y <= z * x --> y / x <= z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   409
  by (import real REAL_LE_LDIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   410
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   411
lemma REAL_LE_RDIV: "ALL (x::real) (y::real) z::real. (0::real) < x & y * x <= z --> y <= z / x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   412
  by (import real REAL_LE_RDIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   413
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   414
lemma REAL_LT_DIV: "ALL (x::real) xa::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   415
   (0::real) < x & (0::real) < xa --> (0::real) < x / xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   416
  by (import real REAL_LT_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   417
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   418
lemma REAL_LE_DIV: "ALL (x::real) xa::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   419
   (0::real) <= x & (0::real) <= xa --> (0::real) <= x / xa"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   420
  by (import real REAL_LE_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   421
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   422
lemma REAL_LT_1: "ALL (x::real) y::real. (0::real) <= x & x < y --> x / y < (1::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   423
  by (import real REAL_LT_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   424
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   425
lemma REAL_POS_NZ: "ALL x>0::real. x ~= (0::real)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   426
  by (import real REAL_POS_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   427
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   428
lemma REAL_EQ_LMUL_IMP: "ALL (x::real) (xa::real) xb::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   429
   x ~= (0::real) & x * xa = x * xb --> xa = xb"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   430
  by (import real REAL_EQ_LMUL_IMP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   431
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   432
lemma REAL_FACT_NZ: "ALL n. real (FACT n) ~= 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   433
  by (import real REAL_FACT_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   434
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   435
lemma REAL_DIFFSQ: "ALL (x::real) y::real. (x + y) * (x - y) = x * x - y * y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   436
  by (import real REAL_DIFFSQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   437
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   438
lemma REAL_POASQ: "ALL x::real. ((0::real) < x * x) = (x ~= (0::real))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   439
  by (import real REAL_POASQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   440
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   441
lemma REAL_SUMSQ: "ALL (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   442
   (x * x + y * y = (0::real)) = (x = (0::real) & y = (0::real))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   443
  by (import real REAL_SUMSQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   444
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   445
lemma REAL_MIDDLE1: "ALL (a::real) b::real. a <= b --> a <= (a + b) / (2::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   446
  by (import real REAL_MIDDLE1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   447
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   448
lemma REAL_MIDDLE2: "ALL (a::real) b::real. a <= b --> (a + b) / (2::real) <= b"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   449
  by (import real REAL_MIDDLE2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   450
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   451
lemma ABS_LT_MUL2: "ALL (w::real) (x::real) (y::real) z::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   452
   abs w < y & abs x < z --> abs (w * x) < y * z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   453
  by (import real ABS_LT_MUL2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   454
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   455
lemma ABS_REFL: "ALL x::real. (abs x = x) = ((0::real) <= x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   456
  by (import real ABS_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   457
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   458
lemma ABS_BETWEEN: "ALL (x::real) (y::real) d::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   459
   ((0::real) < d & x - d < y & y < x + d) = (abs (y - x) < d)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   460
  by (import real ABS_BETWEEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   461
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   462
lemma ABS_BOUND: "ALL (x::real) (y::real) d::real. abs (x - y) < d --> y < x + d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   463
  by (import real ABS_BOUND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   464
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   465
lemma ABS_STILLNZ: "ALL (x::real) y::real. abs (x - y) < abs y --> x ~= (0::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   466
  by (import real ABS_STILLNZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   467
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   468
lemma ABS_CASES: "ALL x::real. x = (0::real) | (0::real) < abs x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   469
  by (import real ABS_CASES)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   470
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   471
lemma ABS_BETWEEN1: "ALL (x::real) (y::real) z::real. x < z & abs (y - x) < z - x --> y < z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   472
  by (import real ABS_BETWEEN1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   473
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   474
lemma ABS_SIGN: "ALL (x::real) y::real. abs (x - y) < y --> (0::real) < x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   475
  by (import real ABS_SIGN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   476
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   477
lemma ABS_SIGN2: "ALL (x::real) y::real. abs (x - y) < - y --> x < (0::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   478
  by (import real ABS_SIGN2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   479
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   480
lemma ABS_CIRCLE: "ALL (x::real) (y::real) h::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   481
   abs h < abs y - abs x --> abs (x + h) < abs y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   482
  by (import real ABS_CIRCLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   483
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   484
lemma REAL_SUB_ABS: "ALL (x::real) y::real. abs x - abs y <= abs (x - y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   485
  by (import real REAL_SUB_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   486
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   487
lemma ABS_SUB_ABS: "ALL (x::real) y::real. abs (abs x - abs y) <= abs (x - y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   488
  by (import real ABS_SUB_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   489
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   490
lemma ABS_BETWEEN2: "ALL (x0::real) (x::real) (y0::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   491
   x0 < y0 &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   492
   abs (x - x0) < (y0 - x0) / (2::real) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   493
   abs (y - y0) < (y0 - x0) / (2::real) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   494
   x < y"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   495
  by (import real ABS_BETWEEN2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   496
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   497
lemma POW_PLUS1: "ALL e>0. ALL n. 1 + real n * e <= (1 + e) ^ n"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   498
  by (import real POW_PLUS1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   499
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   500
lemma POW_M1: "ALL n::nat. abs ((- (1::real)) ^ n) = (1::real)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   501
  by (import real POW_M1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   502
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   503
lemma REAL_LE1_POW2: "ALL x>=1::real. (1::real) <= x ^ 2"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   504
  by (import real REAL_LE1_POW2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   505
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   506
lemma REAL_LT1_POW2: "ALL x>1::real. (1::real) < x ^ 2"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   507
  by (import real REAL_LT1_POW2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   508
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   509
lemma POW_POS_LT: "ALL (x::real) n::nat. (0::real) < x --> (0::real) < x ^ Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   510
  by (import real POW_POS_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   511
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   512
lemma POW_LT: "ALL (n::nat) (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   513
   (0::real) <= x & x < y --> x ^ Suc n < y ^ Suc n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   514
  by (import real POW_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   515
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   516
lemma POW_ZERO_EQ: "ALL (n::nat) x::real. (x ^ Suc n = (0::real)) = (x = (0::real))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   517
  by (import real POW_ZERO_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   518
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   519
lemma REAL_POW_LT2: "ALL (n::nat) (x::real) y::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   520
   n ~= (0::nat) & (0::real) <= x & x < y --> x ^ n < y ^ n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   521
  by (import real REAL_POW_LT2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   522
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   523
lemma REAL_SUP_SOMEPOS: "ALL P::real => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   524
   (EX x::real. P x & (0::real) < x) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   525
   (EX z::real. ALL x::real. P x --> x < z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   526
   (EX s::real. ALL y::real. (EX x::real. P x & y < x) = (y < s))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   527
  by (import real REAL_SUP_SOMEPOS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   528
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   529
lemma SUP_LEMMA1: "ALL (P::real => bool) (s::real) d::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   530
   (ALL y::real. (EX x::real. P (x + d) & y < x) = (y < s)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   531
   (ALL y::real. (EX x::real. P x & y < x) = (y < s + d))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   532
  by (import real SUP_LEMMA1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   533
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   534
lemma SUP_LEMMA2: "ALL P::real => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   535
   Ex P --> (EX (d::real) x::real. P (x + d) & (0::real) < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   536
  by (import real SUP_LEMMA2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   537
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   538
lemma SUP_LEMMA3: "ALL d::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   539
   (EX z::real. ALL x::real. (P::real => bool) x --> x < z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   540
   (EX x::real. ALL xa::real. P (xa + d) --> xa < x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   541
  by (import real SUP_LEMMA3)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   542
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   543
lemma REAL_SUP_EXISTS: "ALL P::real => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   544
   Ex P & (EX z::real. ALL x::real. P x --> x < z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   545
   (EX x::real. ALL y::real. (EX x::real. P x & y < x) = (y < x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   546
  by (import real REAL_SUP_EXISTS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   547
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   548
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   549
  sup :: "(real => bool) => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   550
  "sup == %P. SOME s. ALL y. (EX x. P x & y < x) = (y < s)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   551
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   552
lemma sup: "ALL P. sup P = (SOME s. ALL y. (EX x. P x & y < x) = (y < s))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   553
  by (import real sup)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   554
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   555
lemma REAL_SUP: "ALL P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   556
   Ex P & (EX z. ALL x. P x --> x < z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   557
   (ALL y. (EX x. P x & y < x) = (y < sup P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   558
  by (import real REAL_SUP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   559
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   560
lemma REAL_SUP_UBOUND: "ALL P. Ex P & (EX z. ALL x. P x --> x < z) --> (ALL y. P y --> y <= sup P)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   561
  by (import real REAL_SUP_UBOUND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   562
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   563
lemma SETOK_LE_LT: "ALL P::real => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   564
   (Ex P & (EX z::real. ALL x::real. P x --> x <= z)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   565
   (Ex P & (EX z::real. ALL x::real. P x --> x < z))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   566
  by (import real SETOK_LE_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   567
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   568
lemma REAL_SUP_LE: "ALL P.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   569
   Ex P & (EX z. ALL x. P x --> x <= z) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   570
   (ALL y. (EX x. P x & y < x) = (y < sup P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   571
  by (import real REAL_SUP_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   572
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   573
lemma REAL_SUP_UBOUND_LE: "ALL P. Ex P & (EX z. ALL x. P x --> x <= z) --> (ALL y. P y --> y <= sup P)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   574
  by (import real REAL_SUP_UBOUND_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   575
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   576
lemma REAL_ARCH_LEAST: "ALL y>0. ALL x>=0. EX n. real n * y <= x & x < real (Suc n) * y"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   577
  by (import real REAL_ARCH_LEAST)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   578
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   579
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   580
  sumc :: "nat => nat => (nat => real) => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   581
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   582
specification (sumc) sumc: "(ALL n f. sumc n 0 f = 0) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   583
(ALL n m f. sumc n (Suc m) f = sumc n m f + f (n + m))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   584
  by (import real sumc)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   585
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
   586
consts
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   587
  sum :: "nat * nat => (nat => real) => real" 
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
   588
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
   589
defs
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   590
  sum_def: "(op ==::(nat * nat => (nat => real) => real)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   591
        => (nat * nat => (nat => real) => real) => prop)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   592
 (real.sum::nat * nat => (nat => real) => real)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   593
 ((split::(nat => nat => (nat => real) => real)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   594
          => nat * nat => (nat => real) => real)
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   595
   (sumc::nat => nat => (nat => real) => real))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   596
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   597
lemma SUM_DEF: "ALL m n f. real.sum (m, n) f = sumc m n f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   598
  by (import real SUM_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   599
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   600
lemma sum: "ALL x xa xb.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   601
   real.sum (xa, 0) x = 0 &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   602
   real.sum (xa, Suc xb) x = real.sum (xa, xb) x + x (xa + xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   603
  by (import real sum)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   604
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   605
lemma SUM_TWO: "ALL f n p. real.sum (0, n) f + real.sum (n, p) f = real.sum (0, n + p) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   606
  by (import real SUM_TWO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   607
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   608
lemma SUM_DIFF: "ALL f m n. real.sum (m, n) f = real.sum (0, m + n) f - real.sum (0, m) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   609
  by (import real SUM_DIFF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   610
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   611
lemma ABS_SUM: "ALL f m n. abs (real.sum (m, n) f) <= real.sum (m, n) (%n. abs (f n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   612
  by (import real ABS_SUM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   613
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   614
lemma SUM_LE: "ALL f g m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   615
   (ALL r. m <= r & r < n + m --> f r <= g r) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   616
   real.sum (m, n) f <= real.sum (m, n) g"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   617
  by (import real SUM_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   618
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   619
lemma SUM_EQ: "ALL f g m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   620
   (ALL r. m <= r & r < n + m --> f r = g r) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   621
   real.sum (m, n) f = real.sum (m, n) g"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   622
  by (import real SUM_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   623
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   624
lemma SUM_POS: "ALL f. (ALL n. 0 <= f n) --> (ALL m n. 0 <= real.sum (m, n) f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   625
  by (import real SUM_POS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   626
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   627
lemma SUM_POS_GEN: "ALL f m. (ALL n. m <= n --> 0 <= f n) --> (ALL n. 0 <= real.sum (m, n) f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   628
  by (import real SUM_POS_GEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   629
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   630
lemma SUM_ABS: "ALL f m x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   631
   abs (real.sum (m, x) (%m. abs (f m))) = real.sum (m, x) (%m. abs (f m))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   632
  by (import real SUM_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   633
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   634
lemma SUM_ABS_LE: "ALL f m n. abs (real.sum (m, n) f) <= real.sum (m, n) (%n. abs (f n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   635
  by (import real SUM_ABS_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   636
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   637
lemma SUM_ZERO: "ALL f N.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   638
   (ALL n. N <= n --> f n = 0) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   639
   (ALL m n. N <= m --> real.sum (m, n) f = 0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   640
  by (import real SUM_ZERO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   641
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   642
lemma SUM_ADD: "ALL f g m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   643
   real.sum (m, n) (%n. f n + g n) = real.sum (m, n) f + real.sum (m, n) g"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   644
  by (import real SUM_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   645
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   646
lemma SUM_CMUL: "ALL f c m n. real.sum (m, n) (%n. c * f n) = c * real.sum (m, n) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   647
  by (import real SUM_CMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   648
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   649
lemma SUM_NEG: "ALL f n d. real.sum (n, d) (%n. - f n) = - real.sum (n, d) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   650
  by (import real SUM_NEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   651
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   652
lemma SUM_SUB: "ALL f g m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   653
   real.sum (m, n) (%x. f x - g x) = real.sum (m, n) f - real.sum (m, n) g"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   654
  by (import real SUM_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   655
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   656
lemma SUM_SUBST: "ALL f g m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   657
   (ALL p. m <= p & p < m + n --> f p = g p) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   658
   real.sum (m, n) f = real.sum (m, n) g"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   659
  by (import real SUM_SUBST)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   660
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   661
lemma SUM_NSUB: "ALL n f c. real.sum (0, n) f - real n * c = real.sum (0, n) (%p. f p - c)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   662
  by (import real SUM_NSUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   663
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   664
lemma SUM_BOUND: "ALL f k m n.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   665
   (ALL p. m <= p & p < m + n --> f p <= k) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   666
   real.sum (m, n) f <= real n * k"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   667
  by (import real SUM_BOUND)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   668
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   669
lemma SUM_GROUP: "ALL n k f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   670
   real.sum (0, n) (%m. real.sum (m * k, k) f) = real.sum (0, n * k) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   671
  by (import real SUM_GROUP)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   672
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   673
lemma SUM_1: "ALL f n. real.sum (n, 1) f = f n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   674
  by (import real SUM_1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   675
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   676
lemma SUM_2: "ALL f n. real.sum (n, 2) f = f n + f (n + 1)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   677
  by (import real SUM_2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   678
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   679
lemma SUM_OFFSET: "ALL f n k.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   680
   real.sum (0, n) (%m. f (m + k)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   681
   real.sum (0, n + k) f - real.sum (0, k) f"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   682
  by (import real SUM_OFFSET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   683
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   684
lemma SUM_REINDEX: "ALL f m k n. real.sum (m + k, n) f = real.sum (m, n) (%r. f (r + k))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   685
  by (import real SUM_REINDEX)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   686
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   687
lemma SUM_0: "ALL m n. real.sum (m, n) (%r. 0) = 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   688
  by (import real SUM_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   689
14847
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   690
lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   691
 (%n::nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   692
     (All::((nat => nat) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   693
      (%p::nat => nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   694
          (op -->::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   695
           ((All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   696
             (%y::nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   697
                 (op -->::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   698
                  ((op <::nat => nat => bool) y n)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   699
                  ((Ex1::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   700
                    (%x::nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   701
                        (op &::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   702
                         ((op <::nat => nat => bool) x n)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   703
                         ((op =::nat => nat => bool) (p x) y)))))
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   704
           ((All::((nat => real) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   705
             (%f::nat => real.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   706
                 (op =::real => real => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   707
                  ((real.sum::nat * nat => (nat => real) => real)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   708
                    ((Pair::nat => nat => nat * nat) (0::nat) n)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   709
                    (%n::nat. f (p n)))
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   710
                  ((real.sum::nat * nat => (nat => real) => real)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
   711
                    ((Pair::nat => nat => nat * nat) (0::nat) n) f)))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   712
  by (import real SUM_PERMUTE_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   713
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   714
lemma SUM_CANCEL: "ALL f n d. real.sum (n, d) (%n. f (Suc n) - f n) = f (n + d) - f n"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   715
  by (import real SUM_CANCEL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   716
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   717
lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   718
   (0::real) < xb --> (x = xa / xb) = (x * xb = xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   719
  by (import real REAL_EQ_RDIV_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   720
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   721
lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   722
   (0::real) < xb --> (x / xb = xa) = (x = xa * xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   723
  by (import real REAL_EQ_LDIV_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   724
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   725
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   726
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   727
;setup_theory topology
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   728
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   729
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   730
  re_Union :: "(('a => bool) => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   731
  "re_Union == %P x. EX s. P s & s x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   732
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   733
lemma re_Union: "ALL P. re_Union P = (%x. EX s. P s & s x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   734
  by (import topology re_Union)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   735
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   736
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   737
  re_union :: "('a => bool) => ('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   738
  "re_union == %P Q x. P x | Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   739
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   740
lemma re_union: "ALL P Q. re_union P Q = (%x. P x | Q x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   741
  by (import topology re_union)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   742
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   743
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   744
  re_intersect :: "('a => bool) => ('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   745
  "re_intersect == %P Q x. P x & Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   746
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   747
lemma re_intersect: "ALL P Q. re_intersect P Q = (%x. P x & Q x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   748
  by (import topology re_intersect)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   749
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   750
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   751
  re_null :: "'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   752
  "re_null == %x. False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   753
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   754
lemma re_null: "re_null = (%x. False)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   755
  by (import topology re_null)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   756
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   757
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   758
  re_universe :: "'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   759
  "re_universe == %x. True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   760
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   761
lemma re_universe: "re_universe = (%x. True)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   762
  by (import topology re_universe)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   763
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   764
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   765
  re_subset :: "('a => bool) => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   766
  "re_subset == %P Q. ALL x. P x --> Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   767
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   768
lemma re_subset: "ALL P Q. re_subset P Q = (ALL x. P x --> Q x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   769
  by (import topology re_subset)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   770
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   771
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   772
  re_compl :: "('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   773
  "re_compl == %P x. ~ P x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   774
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   775
lemma re_compl: "ALL P. re_compl P = (%x. ~ P x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   776
  by (import topology re_compl)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   777
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   778
lemma SUBSET_REFL: "ALL P. re_subset P P"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   779
  by (import topology SUBSET_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   780
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   781
lemma COMPL_MEM: "ALL P x. P x = (~ re_compl P x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   782
  by (import topology COMPL_MEM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   783
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   784
lemma SUBSET_ANTISYM: "ALL P Q. (re_subset P Q & re_subset Q P) = (P = Q)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   785
  by (import topology SUBSET_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   786
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   787
lemma SUBSET_TRANS: "ALL P Q R. re_subset P Q & re_subset Q R --> re_subset P R"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   788
  by (import topology SUBSET_TRANS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   789
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   790
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   791
  istopology :: "(('a => bool) => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   792
  "istopology ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   793
%L. L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   794
    L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   795
    (ALL a b. L a & L b --> L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   796
    (ALL P. re_subset P L --> L (re_Union P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   797
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   798
lemma istopology: "ALL L.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   799
   istopology L =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   800
   (L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   801
    L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   802
    (ALL a b. L a & L b --> L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   803
    (ALL P. re_subset P L --> L (re_Union P)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   804
  by (import topology istopology)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   805
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   806
typedef (open) ('a) topology = "(Collect::((('a => bool) => bool) => bool) => (('a => bool) => bool) set)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   807
 (istopology::(('a => bool) => bool) => bool)" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   808
  by (rule typedef_helper,import topology topology_TY_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   809
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   810
lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   811
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   812
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   813
  topology :: "(('a => bool) => bool) => 'a topology" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   814
  "open" :: "'a topology => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   815
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   816
specification ("open" topology) topology_tybij: "(ALL a::'a topology. topology (open a) = a) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   817
(ALL r::('a => bool) => bool. istopology r = (open (topology r) = r))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   818
  by (import topology topology_tybij)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   819
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   820
lemma TOPOLOGY: "ALL L.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   821
   open L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   822
   open L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   823
   (ALL a b. open L a & open L b --> open L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   824
   (ALL P. re_subset P (open L) --> open L (re_Union P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   825
  by (import topology TOPOLOGY)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   826
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   827
lemma TOPOLOGY_UNION: "ALL x xa. re_subset xa (open x) --> open x (re_Union xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   828
  by (import topology TOPOLOGY_UNION)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   829
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   830
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   831
  neigh :: "'a topology => ('a => bool) * 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   832
  "neigh == %top (N, x). EX P. open top P & re_subset P N & P x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   833
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   834
lemma neigh: "ALL top N x. neigh top (N, x) = (EX P. open top P & re_subset P N & P x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   835
  by (import topology neigh)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   836
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   837
lemma OPEN_OWN_NEIGH: "ALL S' top x. open top S' & S' x --> neigh top (S', x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   838
  by (import topology OPEN_OWN_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   839
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   840
lemma OPEN_UNOPEN: "ALL S' top. open top S' = (re_Union (%P. open top P & re_subset P S') = S')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   841
  by (import topology OPEN_UNOPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   842
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   843
lemma OPEN_SUBOPEN: "ALL S' top.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   844
   open top S' = (ALL x. S' x --> (EX P. P x & open top P & re_subset P S'))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   845
  by (import topology OPEN_SUBOPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   846
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   847
lemma OPEN_NEIGH: "ALL S' top.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   848
   open top S' = (ALL x. S' x --> (EX N. neigh top (N, x) & re_subset N S'))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   849
  by (import topology OPEN_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   850
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   851
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   852
  closed :: "'a topology => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   853
  "closed == %L S'. open L (re_compl S')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   854
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   855
lemma closed: "ALL L S'. closed L S' = open L (re_compl S')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   856
  by (import topology closed)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   857
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   858
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   859
  limpt :: "'a topology => 'a => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   860
  "limpt == %top x S'. ALL N. neigh top (N, x) --> (EX y. x ~= y & S' y & N y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   861
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   862
lemma limpt: "ALL top x S'.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   863
   limpt top x S' =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   864
   (ALL N. neigh top (N, x) --> (EX y. x ~= y & S' y & N y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   865
  by (import topology limpt)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   866
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   867
lemma CLOSED_LIMPT: "ALL top S'. closed top S' = (ALL x. limpt top x S' --> S' x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   868
  by (import topology CLOSED_LIMPT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   869
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   870
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   871
  ismet :: "('a * 'a => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   872
  "ismet ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   873
%m. (ALL x y. (m (x, y) = 0) = (x = y)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   874
    (ALL x y z. m (y, z) <= m (x, y) + m (x, z))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   875
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   876
lemma ismet: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   877
   ismet m =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   878
   ((ALL x y. (m (x, y) = 0) = (x = y)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   879
    (ALL x y z. m (y, z) <= m (x, y) + m (x, z)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   880
  by (import topology ismet)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   881
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   882
typedef (open) ('a) metric = "(Collect::(('a * 'a => real) => bool) => ('a * 'a => real) set)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   883
 (ismet::('a * 'a => real) => bool)" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   884
  by (rule typedef_helper,import topology metric_TY_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   885
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   886
lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   887
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   888
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   889
  metric :: "('a * 'a => real) => 'a metric" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   890
  dist :: "'a metric => 'a * 'a => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   891
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   892
specification (dist metric) metric_tybij: "(ALL a::'a metric. metric (dist a) = a) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   893
(ALL r::'a * 'a => real. ismet r = (dist (metric r) = r))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   894
  by (import topology metric_tybij)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   895
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   896
lemma METRIC_ISMET: "ALL m. ismet (dist m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   897
  by (import topology METRIC_ISMET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   898
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   899
lemma METRIC_ZERO: "ALL m x y. (dist m (x, y) = 0) = (x = y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   900
  by (import topology METRIC_ZERO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   901
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   902
lemma METRIC_SAME: "ALL m x. dist m (x, x) = 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   903
  by (import topology METRIC_SAME)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   904
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   905
lemma METRIC_POS: "ALL m x y. 0 <= dist m (x, y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   906
  by (import topology METRIC_POS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   907
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   908
lemma METRIC_SYM: "ALL m x y. dist m (x, y) = dist m (y, x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   909
  by (import topology METRIC_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   910
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   911
lemma METRIC_TRIANGLE: "ALL m x y z. dist m (x, z) <= dist m (x, y) + dist m (y, z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   912
  by (import topology METRIC_TRIANGLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   913
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   914
lemma METRIC_NZ: "ALL m x y. x ~= y --> 0 < dist m (x, y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   915
  by (import topology METRIC_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   916
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   917
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   918
  mtop :: "'a metric => 'a topology" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   919
  "mtop ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   920
%m. topology
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   921
     (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   922
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   923
lemma mtop: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   924
   mtop m =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   925
   topology
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   926
    (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   927
  by (import topology mtop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   928
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   929
lemma mtop_istopology: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   930
   istopology
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   931
    (%S'. ALL x. S' x --> (EX e>0. ALL y. dist m (x, y) < e --> S' y))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   932
  by (import topology mtop_istopology)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   933
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   934
lemma MTOP_OPEN: "ALL S' x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   935
   open (mtop x) S' =
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   936
   (ALL xa. S' xa --> (EX e>0. ALL y. dist x (xa, y) < e --> S' y))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   937
  by (import topology MTOP_OPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   938
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   939
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   940
  B :: "'a metric => 'a * real => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   941
  "B == %m (x, e) y. dist m (x, y) < e"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   942
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   943
lemma ball: "ALL m x e. B m (x, e) = (%y. dist m (x, y) < e)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   944
  by (import topology ball)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   945
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   946
lemma BALL_OPEN: "ALL m x e. 0 < e --> open (mtop m) (B m (x, e))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   947
  by (import topology BALL_OPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   948
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   949
lemma BALL_NEIGH: "ALL m x e. 0 < e --> neigh (mtop m) (B m (x, e), x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   950
  by (import topology BALL_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   951
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   952
lemma MTOP_LIMPT: "ALL m x S'.
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
   953
   limpt (mtop m) x S' = (ALL e>0. EX y. x ~= y & S' y & dist m (x, y) < e)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   954
  by (import topology MTOP_LIMPT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   955
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   956
lemma ISMET_R1: "ismet (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   957
  by (import topology ISMET_R1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   958
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   959
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   960
  mr1 :: "real metric" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   961
  "mr1 == metric (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   962
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   963
lemma mr1: "mr1 = metric (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   964
  by (import topology mr1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   965
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   966
lemma MR1_DEF: "ALL x y. dist mr1 (x, y) = abs (y - x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   967
  by (import topology MR1_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   968
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   969
lemma MR1_ADD: "ALL x d. dist mr1 (x, x + d) = abs d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   970
  by (import topology MR1_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   971
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   972
lemma MR1_SUB: "ALL x d. dist mr1 (x, x - d) = abs d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   973
  by (import topology MR1_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   974
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   975
lemma MR1_ADD_POS: "ALL x d. 0 <= d --> dist mr1 (x, x + d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   976
  by (import topology MR1_ADD_POS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   977
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   978
lemma MR1_SUB_LE: "ALL x d. 0 <= d --> dist mr1 (x, x - d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   979
  by (import topology MR1_SUB_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   980
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   981
lemma MR1_ADD_LT: "ALL x d. 0 < d --> dist mr1 (x, x + d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   982
  by (import topology MR1_ADD_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   983
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   984
lemma MR1_SUB_LT: "ALL x d. 0 < d --> dist mr1 (x, x - d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   985
  by (import topology MR1_SUB_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   986
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   987
lemma MR1_BETWEEN1: "ALL x y z. x < z & dist mr1 (x, y) < z - x --> y < z"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   988
  by (import topology MR1_BETWEEN1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   989
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   990
lemma MR1_LIMPT: "ALL x. limpt (mtop mr1) x re_universe"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   991
  by (import topology MR1_LIMPT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   992
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   993
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   994
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   995
;setup_theory nets
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   996
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   997
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   998
  dorder :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   999
  "dorder ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1000
%g. ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1001
       g x x & g y y --> (EX z. g z z & (ALL w. g w z --> g w x & g w y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1002
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1003
lemma dorder: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1004
   dorder g =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1005
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1006
       g x x & g y y --> (EX z. g z z & (ALL w. g w z --> g w x & g w y)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1007
  by (import nets dorder)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1008
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1009
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1010
  tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1011
  "tends ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1012
%(s::'b => 'a) (l::'a) (top::'a topology, g::'b => 'b => bool).
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1013
   ALL N::'a => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1014
      neigh top (N, l) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1015
      (EX n::'b. g n n & (ALL m::'b. g m n --> N (s m)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1016
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1017
lemma tends: "ALL (s::'b => 'a) (l::'a) (top::'a topology) g::'b => 'b => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1018
   tends s l (top, g) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1019
   (ALL N::'a => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1020
       neigh top (N, l) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1021
       (EX n::'b. g n n & (ALL m::'b. g m n --> N (s m))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1022
  by (import nets tends)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1023
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1024
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1025
  bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1026
  "bounded ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1027
%(m, g) f. EX k x N. g N N & (ALL n. g n N --> dist m (f n, x) < k)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1028
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1029
lemma bounded: "ALL m g f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1030
   bounded (m, g) f =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1031
   (EX k x N. g N N & (ALL n. g n N --> dist m (f n, x) < k))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1032
  by (import nets bounded)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1033
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1034
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1035
  tendsto :: "'a metric * 'a => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1036
  "tendsto == %(m, x) y z. 0 < dist m (x, y) & dist m (x, y) <= dist m (x, z)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1037
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1038
lemma tendsto: "ALL m x y z.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1039
   tendsto (m, x) y z = (0 < dist m (x, y) & dist m (x, y) <= dist m (x, z))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1040
  by (import nets tendsto)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1041
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1042
lemma DORDER_LEMMA: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1043
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1044
   (ALL P Q.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1045
       (EX n. g n n & (ALL m. g m n --> P m)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1046
       (EX n. g n n & (ALL m. g m n --> Q m)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1047
       (EX n. g n n & (ALL m. g m n --> P m & Q m)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1048
  by (import nets DORDER_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1049
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1050
lemma DORDER_NGE: "dorder nat_ge"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1051
  by (import nets DORDER_NGE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1052
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1053
lemma DORDER_TENDSTO: "ALL m x. dorder (tendsto (m, x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1054
  by (import nets DORDER_TENDSTO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1055
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1056
lemma MTOP_TENDS: "ALL d g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1057
   tends x x0 (mtop d, g) =
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1058
   (ALL e>0. EX n. g n n & (ALL m. g m n --> dist d (x m, x0) < e))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1059
  by (import nets MTOP_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1060
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1061
lemma MTOP_TENDS_UNIQ: "ALL (g::'b => 'b => bool) d::'a metric.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1062
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1063
   tends (x::'b => 'a) (x0::'a) (mtop d, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1064
   tends x (x1::'a) (mtop d, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1065
   x0 = x1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1066
  by (import nets MTOP_TENDS_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1067
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1068
lemma SEQ_TENDS: "ALL d x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1069
   tends x x0 (mtop d, nat_ge) =
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1070
   (ALL xa>0. EX xb. ALL xc. xb <= xc --> dist d (x xc, x0) < xa)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1071
  by (import nets SEQ_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1072
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1073
lemma LIM_TENDS: "ALL m1 m2 f x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1074
   limpt (mtop m1) x0 re_universe -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1075
   tends f y0 (mtop m2, tendsto (m1, x0)) =
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1076
   (ALL e>0.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1077
       EX d>0.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1078
          ALL x.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1079
             0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1080
             dist m2 (f x, y0) < e)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1081
  by (import nets LIM_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1082
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1083
lemma LIM_TENDS2: "ALL m1 m2 f x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1084
   limpt (mtop m1) x0 re_universe -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1085
   tends f y0 (mtop m2, tendsto (m1, x0)) =
15647
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1086
   (ALL e>0.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1087
       EX d>0.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1088
          ALL x.
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1089
             0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
b1f486a9c56b Updated import configuration.
skalberg
parents: 15071
diff changeset
  1090
             dist m2 (f x, y0) < e)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1091
  by (import nets LIM_TENDS2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1092
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1093
lemma MR1_BOUNDED: "ALL g f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1094
   bounded (mr1, g) f = (EX k N. g N N & (ALL n. g n N --> abs (f n) < k))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1095
  by (import nets MR1_BOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1096
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1097
lemma NET_NULL: "ALL g x x0. tends x x0 (mtop mr1, g) = tends (%n. x n - x0) 0 (mtop mr1, g)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1098
  by (import nets NET_NULL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1099
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1100
lemma NET_CONV_BOUNDED: "ALL g x x0. tends x x0 (mtop mr1, g) --> bounded (mr1, g) x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1101
  by (import nets NET_CONV_BOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1102
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1103
lemma NET_CONV_NZ: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1104
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1105
   (EX N. g N N & (ALL n. g n N --> x n ~= 0))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1106
  by (import nets NET_CONV_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1107
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1108
lemma NET_CONV_IBOUNDED: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1109
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1110
   bounded (mr1, g) (%n. inverse (x n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1111
  by (import nets NET_CONV_IBOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1112
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1113
lemma NET_NULL_ADD: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1114
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1115
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1116
       tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1117
       tends (%n. x n + y n) 0 (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1118
  by (import nets NET_NULL_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1119
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1120
lemma NET_NULL_MUL: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1121
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1122
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1123
       bounded (mr1, g) x & tends y 0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1124
       tends (%n. x n * y n) 0 (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1125
  by (import nets NET_NULL_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1126
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1127
lemma NET_NULL_CMUL: "ALL g k x. tends x 0 (mtop mr1, g) --> tends (%n. k * x n) 0 (mtop mr1, g)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1128
  by (import nets NET_NULL_CMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1129
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1130
lemma NET_ADD: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1131
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1132
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1133
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1134
       tends (%n. x n + y n) (x0 + y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1135
  by (import nets NET_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1136
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1137
lemma NET_NEG: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1138
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1139
   (ALL x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1140
       tends x x0 (mtop mr1, g) = tends (%n. - x n) (- x0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1141
  by (import nets NET_NEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1142
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1143
lemma NET_SUB: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1144
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1145
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1146
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1147
       tends (%xa. x xa - y xa) (x0 - y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1148
  by (import nets NET_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1149
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1150
lemma NET_MUL: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1151
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1152
   (ALL x y x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1153
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1154
       tends (%n. x n * y n) (x0 * y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1155
  by (import nets NET_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1156
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1157
lemma NET_INV: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1158
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1159
   (ALL x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1160
       tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1161
       tends (%n. inverse (x n)) (inverse x0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1162
  by (import nets NET_INV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1163
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1164
lemma NET_DIV: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1165
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1166
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1167
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1168
       tends (%xa. x xa / y xa) (x0 / y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1169
  by (import nets NET_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1170
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1171
lemma NET_ABS: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1172
   tends x x0 (mtop mr1, g) --> tends (%n. abs (x n)) (abs x0) (mtop mr1, g)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1173
  by (import nets NET_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1174
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1175
lemma NET_LE: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1176
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1177
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1178
       tends x x0 (mtop mr1, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1179
       tends y y0 (mtop mr1, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1180
       (EX N. g N N & (ALL n. g n N --> x n <= y n)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1181
       x0 <= y0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1182
  by (import nets NET_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1183
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1184
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1185
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1186
;setup_theory seq
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1187
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1188
consts
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1189
  "-->" :: "(nat => real) => real => bool" ("-->")
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1190
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1191
defs
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1192
  "-->_def": "--> == %x x0. tends x x0 (mtop mr1, nat_ge)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1193
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1194
lemma tends_num_real: "ALL x x0. --> x x0 = tends x x0 (mtop mr1, nat_ge)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1195
  by (import seq tends_num_real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1196
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1197
lemma SEQ: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1198
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1199
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1200
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1201
          (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1202
           ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1203
           ((All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1204
             (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1205
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1206
                  ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1207
                  ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1208
                    (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1209
                        (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1210
                         (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1211
                             (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1212
                              ((op <=::nat => nat => bool) N n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1213
                              ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1214
                                ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1215
                                  ((op -::real => real => real) (x n) x0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1216
                                e))))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1217
  by (import seq SEQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1218
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1219
lemma SEQ_CONST: "ALL k. --> (%x. k) k"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1220
  by (import seq SEQ_CONST)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1221
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1222
lemma SEQ_ADD: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1223
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1224
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1225
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1226
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1227
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1228
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1229
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1230
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1231
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1232
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1233
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1234
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1235
                       (%n::nat. (op +::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1236
                       ((op +::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1237
  by (import seq SEQ_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1238
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1239
lemma SEQ_MUL: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1240
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1241
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1242
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1243
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1244
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1245
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1246
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1247
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1248
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1249
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1250
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1251
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1252
                       (%n::nat. (op *::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1253
                       ((op *::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1254
  by (import seq SEQ_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1255
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1256
lemma SEQ_NEG: "ALL x x0. --> x x0 = --> (%n. - x n) (- x0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1257
  by (import seq SEQ_NEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1258
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1259
lemma SEQ_INV: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1260
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1261
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1262
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1263
          (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1264
           ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1265
             ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1266
             ((Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1267
               ((op =::real => real => bool) x0 (0::real))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1268
           ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1269
             (%n::nat. (inverse::real => real) (x n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1270
             ((inverse::real => real) x0))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1271
  by (import seq SEQ_INV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1272
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1273
lemma SEQ_SUB: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1274
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1275
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1276
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1277
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1278
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1279
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1280
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1281
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1282
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1283
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1284
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1285
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1286
                       (%n::nat. (op -::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1287
                       ((op -::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1288
  by (import seq SEQ_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1289
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1290
lemma SEQ_DIV: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1291
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1292
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1293
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1294
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1295
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1296
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1297
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1298
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1299
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1300
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1301
                       ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1302
                         ((-->::(nat => real) => real => bool) y y0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1303
                         ((Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1304
                           ((op =::real => real => bool) y0 (0::real)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1305
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1306
                       (%n::nat. (op /::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1307
                       ((op /::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1308
  by (import seq SEQ_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1309
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1310
lemma SEQ_UNIQ: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1311
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1312
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1313
      (%x1::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1314
          (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1315
           (%x2::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1316
               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1317
                ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1318
                  ((-->::(nat => real) => real => bool) x x1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1319
                  ((-->::(nat => real) => real => bool) x x2))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1320
                ((op =::real => real => bool) x1 x2))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1321
  by (import seq SEQ_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1322
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1323
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1324
  convergent :: "(nat => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1325
  "convergent == %f. Ex (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1326
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1327
lemma convergent: "ALL f. convergent f = Ex (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1328
  by (import seq convergent)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1329
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1330
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1331
  cauchy :: "(nat => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1332
  "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1333
 (cauchy::(nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1334
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1335
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1336
      (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1337
          (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1338
           ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1339
           ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1340
             (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1341
                 (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1342
                  (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1343
                      (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1344
                       (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1345
                           (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1346
                            ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1347
                              ((op <=::nat => nat => bool) N m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1348
                              ((op <=::nat => nat => bool) N n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1349
                            ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1350
                              ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1351
                                ((op -::real => real => real) (f m) (f n)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1352
                              e)))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1353
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1354
lemma cauchy: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1355
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1356
     (op =::bool => bool => bool) ((cauchy::(nat => real) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1357
      ((All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1358
        (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1359
            (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1360
             ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1361
             ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1362
               (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1363
                   (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1364
                    (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1365
                        (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1366
                         (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1367
                             (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1368
                              ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1369
                                ((op <=::nat => nat => bool) N m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1370
                                ((op <=::nat => nat => bool) N n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1371
                              ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1372
                                ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1373
                                  ((op -::real => real => real) (f m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1374
                                    (f n)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1375
                                e))))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1376
  by (import seq cauchy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1377
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1378
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1379
  lim :: "(nat => real) => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1380
  "lim == %f. Eps (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1381
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1382
lemma lim: "ALL f. lim f = Eps (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1383
  by (import seq lim)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1384
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1385
lemma SEQ_LIM: "ALL f. convergent f = --> f (lim f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1386
  by (import seq SEQ_LIM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1387
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1388
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1389
  subseq :: "(nat => nat) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1390
  "(op ==::((nat => nat) => bool) => ((nat => nat) => bool) => prop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1391
 (subseq::(nat => nat) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1392
 (%f::nat => nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1393
     (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1394
      (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1395
          (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1396
           (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1397
               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1398
                ((op <::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1399
                ((op <::nat => nat => bool) (f m) (f n)))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1400
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1401
lemma subseq: "(All::((nat => nat) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1402
 (%f::nat => nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1403
     (op =::bool => bool => bool) ((subseq::(nat => nat) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1404
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1405
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1406
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1407
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1408
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1409
                  ((op <::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1410
                  ((op <::nat => nat => bool) (f m) (f n))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1411
  by (import seq subseq)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1412
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1413
lemma SUBSEQ_SUC: "ALL f. subseq f = (ALL n. f n < f (Suc n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1414
  by (import seq SUBSEQ_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1415
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1416
consts
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1417
  mono :: "(nat => real) => bool" 
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1418
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1419
defs
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1420
  mono_def: "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1421
 (seq.mono::(nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1422
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1423
     (op |::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1424
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1425
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1426
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1427
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1428
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1429
                  ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1430
                  ((op <=::real => real => bool) (f m) (f n)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1431
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1432
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1433
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1434
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1435
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1436
                  ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1437
                  ((op <=::real => real => bool) (f n) (f m))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1438
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1439
lemma mono: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1440
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1441
     (op =::bool => bool => bool) ((seq.mono::(nat => real) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1442
      ((op |::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1443
        ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1444
          (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1445
              (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1446
               (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1447
                   (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1448
                    ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1449
                    ((op <=::real => real => bool) (f m) (f n)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1450
        ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1451
          (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1452
              (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1453
               (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1454
                   (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1455
                    ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1456
                    ((op <=::real => real => bool) (f n) (f m)))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1457
  by (import seq mono)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1458
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1459
lemma MONO_SUC: "ALL f. seq.mono f = ((ALL x. f x <= f (Suc x)) | (ALL n. f (Suc n) <= f n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1460
  by (import seq MONO_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1461
14847
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1462
lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1463
 (%s::nat => real.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1464
     (All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1465
      (%N::nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1466
          (Ex::(real => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1467
           (%k::real.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1468
               (All::(nat => bool) => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1469
                (%n::nat.
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1470
                    (op -->::bool => bool => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1471
                     ((op <::nat => nat => bool) n N)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1472
                     ((op <::real => real => bool)
44d92c12b255 updated;
wenzelm
parents: 14796
diff changeset
  1473
                       ((abs::real => real) (s n)) k)))))"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1474
  by (import seq MAX_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1475
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1476
lemma SEQ_BOUNDED: "ALL s. bounded (mr1, nat_ge) s = (EX k. ALL n. abs (s n) < k)"