src/HOL/Import/HOL/HOL4Real.thy
author wenzelm
Fri, 21 May 2004 21:42:05 +0200
changeset 14796 1e83aa391ade
parent 14694 49873d345a39
child 14847 44d92c12b255
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
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   685
lemma SUM_PERMUTE_0: "ALL n p.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   686
   (ALL y<n. EX! x. x < n & p x = y) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   687
   (ALL f. real.sum (0, n) (%n. f (p n)) = real.sum (0, n) f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   688
  by (import real SUM_PERMUTE_0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   689
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   690
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
   691
  by (import real SUM_CANCEL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   692
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   693
lemma REAL_EQ_RDIV_EQ: "ALL (x::real) (xa::real) xb::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   694
   (0::real) < xb --> (x = xa / xb) = (x * xb = xa)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   695
  by (import real REAL_EQ_RDIV_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   696
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   697
lemma REAL_EQ_LDIV_EQ: "ALL (x::real) (xa::real) xb::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   698
   (0::real) < xb --> (x / xb = xa) = (x = xa * xb)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   699
  by (import real REAL_EQ_LDIV_EQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   700
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   701
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   702
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   703
;setup_theory topology
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   704
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   705
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   706
  re_Union :: "(('a => bool) => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   707
  "re_Union == %P x. EX s. P s & s x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   708
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   709
lemma re_Union: "ALL P. re_Union P = (%x. EX s. P s & s x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   710
  by (import topology re_Union)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   711
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   712
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   713
  re_union :: "('a => bool) => ('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   714
  "re_union == %P Q x. P x | Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   715
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   716
lemma re_union: "ALL P Q. re_union P Q = (%x. P x | Q x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   717
  by (import topology re_union)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   718
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   719
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   720
  re_intersect :: "('a => bool) => ('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   721
  "re_intersect == %P Q x. P x & Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   722
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   723
lemma re_intersect: "ALL P Q. re_intersect P Q = (%x. P x & Q x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   724
  by (import topology re_intersect)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   725
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   726
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   727
  re_null :: "'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   728
  "re_null == %x. False"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   729
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   730
lemma re_null: "re_null = (%x. False)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   731
  by (import topology re_null)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   732
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   733
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   734
  re_universe :: "'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   735
  "re_universe == %x. True"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   736
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   737
lemma re_universe: "re_universe = (%x. True)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   738
  by (import topology re_universe)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   739
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   740
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   741
  re_subset :: "('a => bool) => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   742
  "re_subset == %P Q. ALL x. P x --> Q x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   743
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   744
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
   745
  by (import topology re_subset)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   746
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   747
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   748
  re_compl :: "('a => bool) => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   749
  "re_compl == %P x. ~ P x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   750
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   751
lemma re_compl: "ALL P. re_compl P = (%x. ~ P x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   752
  by (import topology re_compl)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   753
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   754
lemma SUBSET_REFL: "ALL P. re_subset P P"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   755
  by (import topology SUBSET_REFL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   756
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   757
lemma COMPL_MEM: "ALL P x. P x = (~ re_compl P x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   758
  by (import topology COMPL_MEM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   759
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   760
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
   761
  by (import topology SUBSET_ANTISYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   762
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   763
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
   764
  by (import topology SUBSET_TRANS)
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
  istopology :: "(('a => bool) => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   768
  "istopology ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   769
%L. L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   770
    L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   771
    (ALL a b. L a & L b --> L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   772
    (ALL P. re_subset P L --> L (re_Union P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   773
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   774
lemma istopology: "ALL L.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   775
   istopology L =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   776
   (L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   777
    L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   778
    (ALL a b. L a & L b --> L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   779
    (ALL P. re_subset P L --> L (re_Union P)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   780
  by (import topology istopology)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   781
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   782
typedef (open) ('a) topology = "(Collect::((('a => bool) => bool) => bool) => (('a => bool) => bool) set)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   783
 (istopology::(('a => bool) => bool) => bool)" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   784
  by (rule typedef_helper,import topology topology_TY_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   785
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   786
lemmas topology_TY_DEF = typedef_hol2hol4 [OF type_definition_topology]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   787
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   788
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   789
  topology :: "(('a => bool) => bool) => 'a topology" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   790
  "open" :: "'a topology => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   791
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   792
specification ("open" topology) topology_tybij: "(ALL a::'a topology. topology (open a) = a) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   793
(ALL r::('a => bool) => bool. istopology r = (open (topology r) = r))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   794
  by (import topology topology_tybij)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   795
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   796
lemma TOPOLOGY: "ALL L.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   797
   open L re_null &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   798
   open L re_universe &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   799
   (ALL a b. open L a & open L b --> open L (re_intersect a b)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   800
   (ALL P. re_subset P (open L) --> open L (re_Union P))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   801
  by (import topology TOPOLOGY)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   802
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   803
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
   804
  by (import topology TOPOLOGY_UNION)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   805
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   806
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   807
  neigh :: "'a topology => ('a => bool) * 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   808
  "neigh == %top (N, x). EX P. open top P & re_subset P N & P x"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   809
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   810
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
   811
  by (import topology neigh)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   812
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   813
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
   814
  by (import topology OPEN_OWN_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   815
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   816
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
   817
  by (import topology OPEN_UNOPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   818
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   819
lemma OPEN_SUBOPEN: "ALL S' top.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   820
   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
   821
  by (import topology OPEN_SUBOPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   822
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   823
lemma OPEN_NEIGH: "ALL S' top.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   824
   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
   825
  by (import topology OPEN_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   826
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   827
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   828
  closed :: "'a topology => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   829
  "closed == %L S'. open L (re_compl S')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   830
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   831
lemma closed: "ALL L S'. closed L S' = open L (re_compl S')"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   832
  by (import topology closed)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   833
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   834
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   835
  limpt :: "'a topology => 'a => ('a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   836
  "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
   837
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   838
lemma limpt: "ALL top x S'.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   839
   limpt top x S' =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   840
   (ALL N. neigh top (N, x) --> (EX y. x ~= y & S' y & N y))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   841
  by (import topology limpt)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   842
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   843
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
   844
  by (import topology CLOSED_LIMPT)
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
  ismet :: "('a * 'a => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   848
  "ismet ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   849
%m. (ALL x y. (m (x, y) = 0) = (x = y)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   850
    (ALL x y z. m (y, z) <= m (x, y) + m (x, z))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   851
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   852
lemma ismet: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   853
   ismet m =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   854
   ((ALL x y. (m (x, y) = 0) = (x = y)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   855
    (ALL x y z. m (y, z) <= m (x, y) + m (x, z)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   856
  by (import topology ismet)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   857
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   858
typedef (open) ('a) metric = "(Collect::(('a * 'a => real) => bool) => ('a * 'a => real) set)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   859
 (ismet::('a * 'a => real) => bool)" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   860
  by (rule typedef_helper,import topology metric_TY_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   861
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   862
lemmas metric_TY_DEF = typedef_hol2hol4 [OF type_definition_metric]
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   863
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   864
consts
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   865
  metric :: "('a * 'a => real) => 'a metric" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   866
  dist :: "'a metric => 'a * 'a => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   867
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   868
specification (dist metric) metric_tybij: "(ALL a::'a metric. metric (dist a) = a) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   869
(ALL r::'a * 'a => real. ismet r = (dist (metric r) = r))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   870
  by (import topology metric_tybij)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   871
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   872
lemma METRIC_ISMET: "ALL m. ismet (dist m)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   873
  by (import topology METRIC_ISMET)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   874
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   875
lemma METRIC_ZERO: "ALL m x y. (dist m (x, y) = 0) = (x = y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   876
  by (import topology METRIC_ZERO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   877
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   878
lemma METRIC_SAME: "ALL m x. dist m (x, x) = 0"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   879
  by (import topology METRIC_SAME)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   880
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   881
lemma METRIC_POS: "ALL m x y. 0 <= dist m (x, y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   882
  by (import topology METRIC_POS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   883
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   884
lemma METRIC_SYM: "ALL m x y. dist m (x, y) = dist m (y, x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   885
  by (import topology METRIC_SYM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   886
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   887
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
   888
  by (import topology METRIC_TRIANGLE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   889
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   890
lemma METRIC_NZ: "ALL m x y. x ~= y --> 0 < dist m (x, y)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   891
  by (import topology METRIC_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   892
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   893
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   894
  mtop :: "'a metric => 'a topology" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   895
  "mtop ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   896
%m. topology
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   897
     (%S'. ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   898
              S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   899
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   900
lemma mtop: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   901
   mtop m =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   902
   topology
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   903
    (%S'. ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   904
             S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   905
  by (import topology mtop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   906
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   907
lemma mtop_istopology: "ALL m.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   908
   istopology
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   909
    (%S'. ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   910
             S' x --> (EX e. 0 < e & (ALL y. dist m (x, y) < e --> S' y)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   911
  by (import topology mtop_istopology)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   912
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   913
lemma MTOP_OPEN: "ALL S' x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   914
   open (mtop x) S' =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   915
   (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
   916
  by (import topology MTOP_OPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   917
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   918
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   919
  B :: "'a metric => 'a * real => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   920
  "B == %m (x, e) y. dist m (x, y) < e"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   921
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   922
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
   923
  by (import topology ball)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   924
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   925
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
   926
  by (import topology BALL_OPEN)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   927
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   928
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
   929
  by (import topology BALL_NEIGH)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   930
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   931
lemma MTOP_LIMPT: "ALL m x S'.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   932
   limpt (mtop m) x S' =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   933
   (ALL e. 0 < e --> (EX y. x ~= y & S' y & dist m (x, y) < e))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   934
  by (import topology MTOP_LIMPT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   935
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   936
lemma ISMET_R1: "ismet (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   937
  by (import topology ISMET_R1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   938
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   939
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   940
  mr1 :: "real metric" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   941
  "mr1 == metric (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   942
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   943
lemma mr1: "mr1 = metric (%(x, y). abs (y - x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   944
  by (import topology mr1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   945
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   946
lemma MR1_DEF: "ALL x y. dist mr1 (x, y) = abs (y - x)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   947
  by (import topology MR1_DEF)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   948
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   949
lemma MR1_ADD: "ALL x d. dist mr1 (x, x + d) = abs d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   950
  by (import topology MR1_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   951
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   952
lemma MR1_SUB: "ALL x d. dist mr1 (x, x - d) = abs d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   953
  by (import topology MR1_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   954
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   955
lemma MR1_ADD_POS: "ALL x d. 0 <= d --> dist mr1 (x, x + d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   956
  by (import topology MR1_ADD_POS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   957
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   958
lemma MR1_SUB_LE: "ALL x d. 0 <= d --> dist mr1 (x, x - d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   959
  by (import topology MR1_SUB_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   960
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   961
lemma MR1_ADD_LT: "ALL x d. 0 < d --> dist mr1 (x, x + d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   962
  by (import topology MR1_ADD_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   963
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   964
lemma MR1_SUB_LT: "ALL x d. 0 < d --> dist mr1 (x, x - d) = d"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   965
  by (import topology MR1_SUB_LT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   966
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   967
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
   968
  by (import topology MR1_BETWEEN1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   969
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   970
lemma MR1_LIMPT: "ALL x. limpt (mtop mr1) x re_universe"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   971
  by (import topology MR1_LIMPT)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   972
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   973
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   974
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   975
;setup_theory nets
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   976
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   977
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   978
  dorder :: "('a => 'a => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   979
  "dorder ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   980
%g. ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   981
       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
   982
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   983
lemma dorder: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   984
   dorder g =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   985
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   986
       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
   987
  by (import nets dorder)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   988
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   989
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   990
  tends :: "('b => 'a) => 'a => 'a topology * ('b => 'b => bool) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   991
  "tends ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   992
%(s::'b => 'a) (l::'a) (top::'a topology, g::'b => 'b => bool).
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   993
   ALL N::'a => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   994
      neigh top (N, l) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   995
      (EX n::'b. g n n & (ALL m::'b. g m n --> N (s m)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   996
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   997
lemma tends: "ALL (s::'b => 'a) (l::'a) (top::'a topology) g::'b => 'b => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   998
   tends s l (top, g) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
   999
   (ALL N::'a => bool.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1000
       neigh top (N, l) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1001
       (EX n::'b. g n n & (ALL m::'b. g m n --> N (s m))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1002
  by (import nets tends)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1003
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1004
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1005
  bounded :: "'a metric * ('b => 'b => bool) => ('b => 'a) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1006
  "bounded ==
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1007
%(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
  1008
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1009
lemma bounded: "ALL m g f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1010
   bounded (m, g) f =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1011
   (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
  1012
  by (import nets bounded)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1013
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1014
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1015
  tendsto :: "'a metric * 'a => 'a => 'a => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1016
  "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
  1017
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1018
lemma tendsto: "ALL m x y z.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1019
   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
  1020
  by (import nets tendsto)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1021
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1022
lemma DORDER_LEMMA: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1023
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1024
   (ALL P Q.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1025
       (EX n. g n n & (ALL m. g m n --> P m)) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1026
       (EX n. g n n & (ALL m. g m n --> Q m)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1027
       (EX n. g n n & (ALL m. g m n --> P m & Q m)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1028
  by (import nets DORDER_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1029
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1030
lemma DORDER_NGE: "dorder nat_ge"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1031
  by (import nets DORDER_NGE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1032
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1033
lemma DORDER_TENDSTO: "ALL m x. dorder (tendsto (m, x))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1034
  by (import nets DORDER_TENDSTO)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1035
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1036
lemma MTOP_TENDS: "ALL d g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1037
   tends x x0 (mtop d, g) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1038
   (ALL e.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1039
       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
  1040
  by (import nets MTOP_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1041
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1042
lemma MTOP_TENDS_UNIQ: "ALL (g::'b => 'b => bool) d::'a metric.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1043
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1044
   tends (x::'b => 'a) (x0::'a) (mtop d, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1045
   tends x (x1::'a) (mtop d, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1046
   x0 = x1"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1047
  by (import nets MTOP_TENDS_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1048
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1049
lemma SEQ_TENDS: "ALL d x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1050
   tends x x0 (mtop d, nat_ge) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1051
   (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
  1052
  by (import nets SEQ_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1053
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1054
lemma LIM_TENDS: "ALL m1 m2 f x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1055
   limpt (mtop m1) x0 re_universe -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1056
   tends f y0 (mtop m2, tendsto (m1, x0)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1057
   (ALL e.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1058
       0 < e -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1059
       (EX d. 0 < d &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1060
              (ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1061
                  0 < dist m1 (x, x0) & dist m1 (x, x0) <= d -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1062
                  dist m2 (f x, y0) < e)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1063
  by (import nets LIM_TENDS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1064
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1065
lemma LIM_TENDS2: "ALL m1 m2 f x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1066
   limpt (mtop m1) x0 re_universe -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1067
   tends f y0 (mtop m2, tendsto (m1, x0)) =
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1068
   (ALL e.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1069
       0 < e -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1070
       (EX d. 0 < d &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1071
              (ALL x.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1072
                  0 < dist m1 (x, x0) & dist m1 (x, x0) < d -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1073
                  dist m2 (f x, y0) < e)))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1074
  by (import nets LIM_TENDS2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1075
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1076
lemma MR1_BOUNDED: "ALL g f.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1077
   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
  1078
  by (import nets MR1_BOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1079
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1080
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
  1081
  by (import nets NET_NULL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1082
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1083
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
  1084
  by (import nets NET_CONV_BOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1085
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1086
lemma NET_CONV_NZ: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1087
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1088
   (EX N. g N N & (ALL n. g n N --> x n ~= 0))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1089
  by (import nets NET_CONV_NZ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1090
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1091
lemma NET_CONV_IBOUNDED: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1092
   tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1093
   bounded (mr1, g) (%n. inverse (x n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1094
  by (import nets NET_CONV_IBOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1095
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1096
lemma NET_NULL_ADD: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1097
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1098
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1099
       tends x 0 (mtop mr1, g) & tends y 0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1100
       tends (%n. x n + y n) 0 (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1101
  by (import nets NET_NULL_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1102
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1103
lemma NET_NULL_MUL: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1104
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1105
   (ALL x y.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1106
       bounded (mr1, g) x & tends y 0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1107
       tends (%n. x n * y n) 0 (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1108
  by (import nets NET_NULL_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1109
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1110
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
  1111
  by (import nets NET_NULL_CMUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1112
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1113
lemma NET_ADD: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1114
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1115
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1116
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1117
       tends (%n. x n + y n) (x0 + y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1118
  by (import nets NET_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1119
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1120
lemma NET_NEG: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1121
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1122
   (ALL x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1123
       tends x x0 (mtop mr1, g) = tends (%n. - x n) (- x0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1124
  by (import nets NET_NEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1125
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1126
lemma NET_SUB: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1127
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1128
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1129
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1130
       tends (%xa. x xa - y xa) (x0 - y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1131
  by (import nets NET_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1132
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1133
lemma NET_MUL: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1134
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1135
   (ALL x y x0 y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1136
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1137
       tends (%n. x n * y n) (x0 * y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1138
  by (import nets NET_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1139
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1140
lemma NET_INV: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1141
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1142
   (ALL x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1143
       tends x x0 (mtop mr1, g) & x0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1144
       tends (%n. inverse (x n)) (inverse x0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1145
  by (import nets NET_INV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1146
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1147
lemma NET_DIV: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1148
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1149
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1150
       tends x x0 (mtop mr1, g) & tends y y0 (mtop mr1, g) & y0 ~= 0 -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1151
       tends (%xa. x xa / y xa) (x0 / y0) (mtop mr1, g))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1152
  by (import nets NET_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1153
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1154
lemma NET_ABS: "ALL g x x0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1155
   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
  1156
  by (import nets NET_ABS)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1157
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1158
lemma NET_LE: "ALL g.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1159
   dorder g -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1160
   (ALL x x0 y y0.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1161
       tends x x0 (mtop mr1, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1162
       tends y y0 (mtop mr1, g) &
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1163
       (EX N. g N N & (ALL n. g n N --> x n <= y n)) -->
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1164
       x0 <= y0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1165
  by (import nets NET_LE)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1166
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1167
;end_setup
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1168
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1169
;setup_theory seq
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1170
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1171
consts
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1172
  "-->" :: "(nat => real) => real => bool" ("-->")
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1173
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1174
defs
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1175
  "-->_def": "--> == %x x0. tends x x0 (mtop mr1, nat_ge)"
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1176
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1177
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
  1178
  by (import seq tends_num_real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1179
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1180
lemma SEQ: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1181
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1182
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1183
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1184
          (op =::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1185
           ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1186
           ((All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1187
             (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1188
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1189
                  ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1190
                  ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1191
                    (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1192
                        (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1193
                         (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1194
                             (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1195
                              ((op <=::nat => nat => bool) N n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1196
                              ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1197
                                ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1198
                                  ((op -::real => real => real) (x n) x0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1199
                                e))))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1200
  by (import seq SEQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1201
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1202
lemma SEQ_CONST: "ALL k. --> (%x. k) k"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1203
  by (import seq SEQ_CONST)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1204
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1205
lemma SEQ_ADD: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1206
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1207
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1208
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1209
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1210
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1211
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1212
                (%y0::real.
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 &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1215
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1216
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1217
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1218
                       (%n::nat. (op +::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1219
                       ((op +::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1220
  by (import seq SEQ_ADD)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1221
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1222
lemma SEQ_MUL: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1223
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1224
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1225
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1226
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1227
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1228
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1229
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1230
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1231
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1232
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1233
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1234
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1235
                       (%n::nat. (op *::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1236
                       ((op *::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1237
  by (import seq SEQ_MUL)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1238
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1239
lemma SEQ_NEG: "ALL x x0. --> x x0 = --> (%n. - x n) (- x0)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1240
  by (import seq SEQ_NEG)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1241
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1242
lemma SEQ_INV: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1243
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1244
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1245
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1246
          (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1247
           ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1248
             ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1249
             ((Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1250
               ((op =::real => real => bool) x0 (0::real))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1251
           ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1252
             (%n::nat. (inverse::real => real) (x n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1253
             ((inverse::real => real) x0))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1254
  by (import seq SEQ_INV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1255
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1256
lemma SEQ_SUB: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1257
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1258
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1259
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1260
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1261
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1262
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1263
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1264
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1265
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1266
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1267
                       ((-->::(nat => real) => real => bool) y y0))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1268
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1269
                       (%n::nat. (op -::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1270
                       ((op -::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1271
  by (import seq SEQ_SUB)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1272
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1273
lemma SEQ_DIV: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1274
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1275
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1276
      (%x0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1277
          (All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1278
           (%y::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1279
               (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1280
                (%y0::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1281
                    (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1282
                     ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1283
                       ((-->::(nat => real) => real => bool) x x0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1284
                       ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1285
                         ((-->::(nat => real) => real => bool) y y0)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1286
                         ((Not::bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1287
                           ((op =::real => real => bool) y0 (0::real)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1288
                     ((-->::(nat => real) => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1289
                       (%n::nat. (op /::real => real => real) (x n) (y n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1290
                       ((op /::real => real => real) x0 y0))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1291
  by (import seq SEQ_DIV)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1292
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1293
lemma SEQ_UNIQ: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1294
 (%x::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1295
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1296
      (%x1::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1297
          (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1298
           (%x2::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1299
               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1300
                ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1301
                  ((-->::(nat => real) => real => bool) x x1)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1302
                  ((-->::(nat => real) => real => bool) x x2))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1303
                ((op =::real => real => bool) x1 x2))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1304
  by (import seq SEQ_UNIQ)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1305
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1306
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1307
  convergent :: "(nat => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1308
  "convergent == %f. Ex (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1309
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1310
lemma convergent: "ALL f. convergent f = Ex (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1311
  by (import seq convergent)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1312
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1313
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1314
  cauchy :: "(nat => real) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1315
  "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1316
 (cauchy::(nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1317
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1318
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1319
      (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1320
          (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1321
           ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1322
           ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1323
             (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1324
                 (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1325
                  (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1326
                      (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1327
                       (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1328
                           (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1329
                            ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1330
                              ((op <=::nat => nat => bool) N m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1331
                              ((op <=::nat => nat => bool) N n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1332
                            ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1333
                              ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1334
                                ((op -::real => real => real) (f m) (f n)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1335
                              e)))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1336
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1337
lemma cauchy: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1338
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1339
     (op =::bool => bool => bool) ((cauchy::(nat => real) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1340
      ((All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1341
        (%e::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1342
            (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1343
             ((op <::real => real => bool) (0::real) e)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1344
             ((Ex::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1345
               (%N::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1346
                   (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1347
                    (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1348
                        (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1349
                         (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1350
                             (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1351
                              ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1352
                                ((op <=::nat => nat => bool) N m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1353
                                ((op <=::nat => nat => bool) N n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1354
                              ((op <::real => real => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1355
                                ((abs::real => real)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1356
                                  ((op -::real => real => real) (f m)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1357
                                    (f n)))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1358
                                e))))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1359
  by (import seq cauchy)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1360
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1361
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1362
  lim :: "(nat => real) => real" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1363
  "lim == %f. Eps (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1364
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1365
lemma lim: "ALL f. lim f = Eps (--> f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1366
  by (import seq lim)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1367
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1368
lemma SEQ_LIM: "ALL f. convergent f = --> f (lim f)"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1369
  by (import seq SEQ_LIM)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1370
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1371
constdefs
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1372
  subseq :: "(nat => nat) => bool" 
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1373
  "(op ==::((nat => nat) => bool) => ((nat => nat) => bool) => prop)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1374
 (subseq::(nat => nat) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1375
 (%f::nat => nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1376
     (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1377
      (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1378
          (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1379
           (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1380
               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1381
                ((op <::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1382
                ((op <::nat => nat => bool) (f m) (f n)))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1383
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1384
lemma subseq: "(All::((nat => nat) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1385
 (%f::nat => nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1386
     (op =::bool => bool => bool) ((subseq::(nat => nat) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1387
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1388
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1389
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1390
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1391
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1392
                  ((op <::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1393
                  ((op <::nat => nat => bool) (f m) (f n))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1394
  by (import seq subseq)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1395
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1396
lemma SUBSEQ_SUC: "ALL f. subseq f = (ALL n. f n < f (Suc n))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1397
  by (import seq SUBSEQ_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1398
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1399
consts
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1400
  mono :: "(nat => real) => bool" 
14694
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1401
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1402
defs
49873d345a39 removed 'constdefs' hack;
wenzelm
parents: 14516
diff changeset
  1403
  mono_def: "(op ==::((nat => real) => bool) => ((nat => real) => bool) => prop)
14516
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1404
 (seq.mono::(nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1405
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1406
     (op |::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1407
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1408
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1409
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1410
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1411
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1412
                  ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1413
                  ((op <=::real => real => bool) (f m) (f n)))))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1414
      ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1415
        (%m::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1416
            (All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1417
             (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1418
                 (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1419
                  ((op <=::nat => nat => bool) m n)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1420
                  ((op <=::real => real => bool) (f n) (f m))))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1421
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1422
lemma mono: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1423
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1424
     (op =::bool => bool => bool) ((seq.mono::(nat => real) => bool) f)
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
  by (import seq mono)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1441
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1442
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
  1443
  by (import seq MONO_SUC)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1444
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1445
lemma MAX_LEMMA: "ALL (s::nat => real) N::nat. EX k::real. ALL n<N. abs (s n) < k"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1446
  by (import seq MAX_LEMMA)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1447
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1448
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
  1449
  by (import seq SEQ_BOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1450
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1451
lemma SEQ_BOUNDED_2: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1452
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1453
     (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1454
      (%k::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1455
          (All::(real => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1456
           (%k'::real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1457
               (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1458
                ((All::(nat => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1459
                  (%n::nat.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1460
                      (op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1461
                       ((op <=::real => real => bool) k (f n))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1462
                       ((op <=::real => real => bool) (f n) k')))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1463
                ((bounded::real metric * (nat => nat => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1464
                           => (nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1465
                  ((Pair::real metric
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1466
                          => (nat => nat => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1467
                             => real metric * (nat => nat => bool))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1468
                    (mr1::real metric) (nat_ge::nat => nat => bool))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1469
                  f))))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1470
  by (import seq SEQ_BOUNDED_2)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1471
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1472
lemma SEQ_CBOUNDED: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1473
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1474
     (op -->::bool => bool => bool) ((cauchy::(nat => real) => bool) f)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1475
      ((bounded::real metric * (nat => nat => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1476
                 => (nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1477
        ((Pair::real metric
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1478
                => (nat => nat => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1479
                   => real metric * (nat => nat => bool))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1480
          (mr1::real metric) (nat_ge::nat => nat => bool))
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1481
        f))"
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1482
  by (import seq SEQ_CBOUNDED)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1483
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1484
lemma SEQ_ICONV: "(All::((nat => real) => bool) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1485
 (%f::nat => real.
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1486
     (op -->::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1487
      ((op &::bool => bool => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1488
        ((bounded::real metric * (nat => nat => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1489
                   => (nat => real) => bool)
a183dec876ab Added HOL proof importer.
skalberg
parents:
diff changeset
  1490
          ((Pair::real metric