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