src/HOL/Import/HOLLightReal.thy
author nipkow
Mon Jan 30 21:49:41 2012 +0100 (2012-01-30)
changeset 46372 6fa9cdb8b850
parent 45051 c478d1876371
child 46783 3e89a5cab8d7
permissions -rw-r--r--
added "'a rel"
kaliszyk@43785
     1
(*  Title:      HOL/Import/HOLLightReal.thy
kaliszyk@43785
     2
    Author:     Cezary Kaliszyk
kaliszyk@43785
     3
*)
kaliszyk@43785
     4
kaliszyk@43785
     5
header {* Compatibility theorems for HOL Light reals *}
kaliszyk@43785
     6
kaliszyk@43785
     7
theory HOLLightReal imports Real begin
kaliszyk@43785
     8
kaliszyk@43785
     9
lemma REAL_OF_NUM_MAX:
kaliszyk@43785
    10
  "max (real (m :: nat)) (real n) = real (max m n)"
kaliszyk@43785
    11
  by simp
kaliszyk@43785
    12
kaliszyk@43785
    13
lemma REAL_OF_NUM_MIN:
kaliszyk@43785
    14
  "min (real (m :: nat)) (real n) = real (min m n)"
kaliszyk@43785
    15
  by simp
kaliszyk@43785
    16
kaliszyk@43785
    17
lemma REAL_POLY_NEG_CLAUSES:
kaliszyk@43785
    18
  "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
kaliszyk@43785
    19
  by simp
kaliszyk@43785
    20
kaliszyk@43785
    21
lemma REAL_MUL_AC:
kaliszyk@43785
    22
  "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
kaliszyk@43785
    23
  by simp
kaliszyk@43785
    24
kaliszyk@43785
    25
lemma REAL_EQ_ADD_LCANCEL_0:
kaliszyk@43785
    26
  "((x :: real) + y = x) = (y = 0)"
kaliszyk@43785
    27
  by simp
kaliszyk@43785
    28
kaliszyk@43785
    29
lemma REAL_EQ_ADD_RCANCEL_0:
kaliszyk@43785
    30
  "((x :: real) + y = y) = (x = 0)"
kaliszyk@43785
    31
  by simp
kaliszyk@43785
    32
kaliszyk@43785
    33
lemma REAL_LT_ANTISYM:
kaliszyk@43785
    34
  "\<not> ((x :: real) < y \<and> y < x)"
kaliszyk@43785
    35
  by simp
kaliszyk@43785
    36
kaliszyk@43785
    37
lemma REAL_LET_ANTISYM:
kaliszyk@43785
    38
  "\<not> ((x :: real) \<le> y \<and> y < x)"
kaliszyk@43785
    39
  by simp
kaliszyk@43785
    40
kaliszyk@43785
    41
lemma REAL_LT_NEGTOTAL:
kaliszyk@43785
    42
  "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
kaliszyk@43785
    43
  by auto
kaliszyk@43785
    44
kaliszyk@43785
    45
lemma REAL_LT_ADDNEG:
kaliszyk@43785
    46
  "((y :: real) < x + - z) = (y + z < x)"
kaliszyk@43785
    47
  by auto
kaliszyk@43785
    48
kaliszyk@43785
    49
lemma REAL_LT_ADDNEG2:
kaliszyk@43785
    50
  "((x :: real) + - y < z) = (x < z + y)"
kaliszyk@43785
    51
  by auto
kaliszyk@43785
    52
kaliszyk@43785
    53
lemma REAL_LT_ADD1:
kaliszyk@43785
    54
  "(x :: real) \<le> y \<longrightarrow> x < y + 1"
kaliszyk@43785
    55
  by simp
kaliszyk@43785
    56
kaliszyk@43785
    57
lemma REAL_SUB_ADD2:
kaliszyk@43785
    58
  "(y :: real) + (x - y) = x"
kaliszyk@43785
    59
  by simp
kaliszyk@43785
    60
kaliszyk@43785
    61
lemma REAL_ADD_SUB:
kaliszyk@43785
    62
  "(x :: real) + y - x = y"
kaliszyk@43785
    63
  by simp
kaliszyk@43785
    64
kaliszyk@43785
    65
lemma REAL_NEG_EQ:
kaliszyk@43785
    66
  "(- (x :: real) = y) = (x = - y)"
kaliszyk@43785
    67
  by auto
kaliszyk@43785
    68
kaliszyk@43785
    69
lemma REAL_LE_ADDR:
kaliszyk@43785
    70
  "((x :: real) \<le> x + y) = (0 \<le> y)"
kaliszyk@43785
    71
  by simp
kaliszyk@43785
    72
kaliszyk@43785
    73
lemma REAL_LE_ADDL:
kaliszyk@43785
    74
  "((y :: real) \<le> x + y) = (0 \<le> x)"
kaliszyk@43785
    75
  by simp
kaliszyk@43785
    76
kaliszyk@43785
    77
lemma REAL_LT_ADDR:
kaliszyk@43785
    78
  "((x :: real) < x + y) = (0 < y)"
kaliszyk@43785
    79
  by simp
kaliszyk@43785
    80
kaliszyk@43785
    81
lemma REAL_LT_ADDL:
kaliszyk@43785
    82
  "((y :: real) < x + y) = (0 < x)"
kaliszyk@43785
    83
  by simp
kaliszyk@43785
    84
kaliszyk@43785
    85
lemma REAL_SUB_SUB:
kaliszyk@43785
    86
  "(x :: real) - y - x = - y"
kaliszyk@43785
    87
  by simp
kaliszyk@43785
    88
kaliszyk@43785
    89
lemma REAL_SUB_LNEG:
kaliszyk@43785
    90
  "- (x :: real) - y = - (x + y)"
kaliszyk@43785
    91
  by simp
kaliszyk@43785
    92
kaliszyk@43785
    93
lemma REAL_SUB_NEG2:
kaliszyk@43785
    94
  "- (x :: real) - - y = y - x"
kaliszyk@43785
    95
  by simp
kaliszyk@43785
    96
kaliszyk@43785
    97
lemma REAL_SUB_TRIANGLE:
kaliszyk@43785
    98
  "(a :: real) - b + (b - c) = a - c"
kaliszyk@43785
    99
  by simp
kaliszyk@43785
   100
kaliszyk@43785
   101
lemma REAL_SUB_SUB2:
kaliszyk@43785
   102
  "(x :: real) - (x - y) = y"
kaliszyk@43785
   103
  by simp
kaliszyk@43785
   104
kaliszyk@43785
   105
lemma REAL_ADD_SUB2:
kaliszyk@43785
   106
  "(x :: real) - (x + y) = - y"
kaliszyk@43785
   107
  by simp
kaliszyk@43785
   108
kaliszyk@43785
   109
lemma REAL_POS_NZ:
kaliszyk@43785
   110
  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
kaliszyk@43785
   111
  by simp
kaliszyk@43785
   112
kaliszyk@43785
   113
lemma REAL_DIFFSQ:
kaliszyk@43785
   114
  "((x :: real) + y) * (x - y) = x * x - y * y"
huffman@44282
   115
  by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
kaliszyk@43785
   116
kaliszyk@43785
   117
lemma REAL_ABS_TRIANGLE_LE:
kaliszyk@43785
   118
  "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
kaliszyk@43785
   119
  by auto
kaliszyk@43785
   120
kaliszyk@43785
   121
lemma REAL_ABS_TRIANGLE_LT:
kaliszyk@43785
   122
  "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
kaliszyk@43785
   123
  by auto
kaliszyk@43785
   124
kaliszyk@43785
   125
lemma REAL_ABS_REFL:
kaliszyk@43785
   126
  "(abs (x :: real) = x) = (0 \<le> x)"
kaliszyk@43785
   127
  by auto
kaliszyk@43785
   128
kaliszyk@43785
   129
lemma REAL_ABS_BETWEEN:
kaliszyk@43785
   130
  "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
kaliszyk@43785
   131
  by auto
kaliszyk@43785
   132
kaliszyk@43785
   133
lemma REAL_ABS_BOUND:
kaliszyk@43785
   134
  "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
kaliszyk@43785
   135
  by auto
kaliszyk@43785
   136
kaliszyk@43785
   137
lemma REAL_ABS_STILLNZ:
kaliszyk@43785
   138
  "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
kaliszyk@43785
   139
  by auto
kaliszyk@43785
   140
kaliszyk@43785
   141
lemma REAL_ABS_CASES:
kaliszyk@43785
   142
  "(x :: real) = 0 \<or> 0 < abs x"
kaliszyk@43785
   143
  by simp
kaliszyk@43785
   144
kaliszyk@43785
   145
lemma REAL_ABS_BETWEEN1:
kaliszyk@43785
   146
  "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
kaliszyk@43785
   147
  by auto
kaliszyk@43785
   148
kaliszyk@43785
   149
lemma REAL_ABS_SIGN:
kaliszyk@43785
   150
  "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
kaliszyk@43785
   151
  by auto
kaliszyk@43785
   152
kaliszyk@43785
   153
lemma REAL_ABS_SIGN2:
kaliszyk@43785
   154
  "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
kaliszyk@43785
   155
  by auto
kaliszyk@43785
   156
kaliszyk@43785
   157
lemma REAL_ABS_CIRCLE:
kaliszyk@43785
   158
  "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
kaliszyk@43785
   159
  by auto
kaliszyk@43785
   160
kaliszyk@43785
   161
lemma REAL_BOUNDS_LT:
kaliszyk@43785
   162
  "(- (k :: real) < x \<and> x < k) = (abs x < k)"
kaliszyk@43785
   163
  by auto
kaliszyk@43785
   164
kaliszyk@43785
   165
lemma REAL_MIN_MAX:
kaliszyk@43785
   166
  "min (x :: real) y = - max (- x) (- y)"
kaliszyk@43785
   167
  by auto
kaliszyk@43785
   168
kaliszyk@43785
   169
lemma REAL_MAX_MIN:
kaliszyk@43785
   170
  "max (x :: real) y = - min (- x) (- y)"
kaliszyk@43785
   171
  by auto
kaliszyk@43785
   172
kaliszyk@43785
   173
lemma REAL_MAX_MAX:
kaliszyk@43785
   174
  "(x :: real) \<le> max x y \<and> y \<le> max x y"
kaliszyk@43785
   175
  by simp
kaliszyk@43785
   176
kaliszyk@43785
   177
lemma REAL_MIN_MIN:
kaliszyk@43785
   178
  "min (x :: real) y \<le> x \<and> min x y \<le> y"
kaliszyk@43785
   179
  by simp
kaliszyk@43785
   180
kaliszyk@43785
   181
lemma REAL_MAX_ACI:
kaliszyk@43785
   182
  "max (x :: real) y = max y x \<and>
kaliszyk@43785
   183
   max (max x y) z = max x (max y z) \<and>
kaliszyk@43785
   184
   max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
kaliszyk@43785
   185
  by auto
kaliszyk@43785
   186
kaliszyk@43785
   187
kaliszyk@43785
   188
lemma REAL_MIN_ACI:
kaliszyk@43785
   189
  "min (x :: real) y = min y x \<and>
kaliszyk@43785
   190
   min (min x y) z = min x (min y z) \<and>
kaliszyk@43785
   191
   min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
kaliszyk@43785
   192
  by auto
kaliszyk@43785
   193
kaliszyk@43785
   194
lemma REAL_EQ_MUL_RCANCEL:
kaliszyk@43785
   195
  "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
kaliszyk@43785
   196
  by auto
kaliszyk@43785
   197
kaliszyk@43785
   198
lemma REAL_MUL_LINV_UNIQ:
kaliszyk@43785
   199
  "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
kaliszyk@43785
   200
  by (metis inverse_inverse_eq inverse_unique)
kaliszyk@43785
   201
kaliszyk@43785
   202
lemma REAL_DIV_RMUL:
kaliszyk@43785
   203
  "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
kaliszyk@43785
   204
  by simp
kaliszyk@43785
   205
kaliszyk@43785
   206
lemma REAL_DIV_LMUL:
kaliszyk@43785
   207
  "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
kaliszyk@43785
   208
  by simp
kaliszyk@43785
   209
kaliszyk@43785
   210
lemma REAL_LT_IMP_NZ:
kaliszyk@43785
   211
  "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
kaliszyk@43785
   212
  by simp
kaliszyk@43785
   213
kaliszyk@43785
   214
lemma REAL_LT_LCANCEL_IMP:
kaliszyk@43785
   215
  "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
kaliszyk@43785
   216
  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
kaliszyk@43785
   217
kaliszyk@43785
   218
lemma REAL_LT_RCANCEL_IMP:
kaliszyk@43785
   219
  "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
kaliszyk@43785
   220
  by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
kaliszyk@43785
   221
kaliszyk@43785
   222
lemma REAL_MUL_POS_LE:
kaliszyk@43785
   223
  "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
kaliszyk@43785
   224
  by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
kaliszyk@43785
   225
kaliszyk@43785
   226
lemma REAL_EQ_RDIV_EQ:
kaliszyk@43785
   227
  "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
kaliszyk@43785
   228
  by auto
kaliszyk@43785
   229
kaliszyk@43785
   230
lemma REAL_EQ_LDIV_EQ:
kaliszyk@43785
   231
  "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
kaliszyk@43785
   232
  by auto
kaliszyk@43785
   233
kaliszyk@43785
   234
lemma REAL_SUB_INV:
kaliszyk@43785
   235
  "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
huffman@45051
   236
  by (simp add: division_ring_inverse_diff divide_real_def)
kaliszyk@43785
   237
kaliszyk@43785
   238
lemma REAL_DOWN:
kaliszyk@43785
   239
  "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
kaliszyk@43785
   240
  by (intro impI exI[of _ "d / 2"]) simp
kaliszyk@43785
   241
kaliszyk@43785
   242
lemma REAL_POW_MONO_LT:
kaliszyk@43785
   243
  "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
kaliszyk@43785
   244
  by simp
kaliszyk@43785
   245
kaliszyk@43785
   246
lemma REAL_POW_MONO:
kaliszyk@43785
   247
  "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
kaliszyk@43785
   248
  by (cases "m < n", cases "x = 1") auto
kaliszyk@43785
   249
kaliszyk@43785
   250
lemma REAL_EQ_LCANCEL_IMP:
kaliszyk@43785
   251
  "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
kaliszyk@43785
   252
  by auto
kaliszyk@43785
   253
kaliszyk@43785
   254
lemma REAL_LE_DIV:
kaliszyk@43785
   255
  "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
kaliszyk@43785
   256
  by (simp add: zero_le_divide_iff)
kaliszyk@43785
   257
kaliszyk@43785
   258
lemma REAL_10: "(1::real) \<noteq> 0"
kaliszyk@43785
   259
  by simp
kaliszyk@43785
   260
kaliszyk@43785
   261
lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
kaliszyk@43785
   262
  by simp
kaliszyk@43785
   263
kaliszyk@43785
   264
lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
kaliszyk@43785
   265
  by simp
kaliszyk@43785
   266
kaliszyk@43785
   267
lemma REAL_ADD_LINV:  "-x + x = (0::real)"
kaliszyk@43785
   268
  by simp
kaliszyk@43785
   269
kaliszyk@43785
   270
lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
kaliszyk@43785
   271
  by simp
kaliszyk@43785
   272
kaliszyk@43785
   273
lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
kaliszyk@43785
   274
  by auto
kaliszyk@43785
   275
kaliszyk@43785
   276
lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
kaliszyk@43785
   277
  by auto
kaliszyk@43785
   278
kaliszyk@43785
   279
lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
kaliszyk@43785
   280
  by (simp add: real_of_nat_Suc)
kaliszyk@43785
   281
kaliszyk@43785
   282
lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
kaliszyk@43785
   283
  by (simp add: abs_if)
kaliszyk@43785
   284
kaliszyk@43785
   285
lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
kaliszyk@43785
   286
  by simp
kaliszyk@43785
   287
kaliszyk@43785
   288
lemma REAL_POLY_CLAUSES:
kaliszyk@43785
   289
  "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
kaliszyk@43785
   290
   (\<forall>(x :: real) y. x + y = y + x) \<and>
kaliszyk@43785
   291
   (\<forall>(x :: real). 0 + x = x) \<and>
kaliszyk@43785
   292
   (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
kaliszyk@43785
   293
   (\<forall>(x :: real) y. x * y = y * x) \<and>
kaliszyk@43785
   294
   (\<forall>(x :: real). 1 * x = x) \<and>
kaliszyk@43785
   295
   (\<forall>(x :: real). 0 * x = 0) \<and>
kaliszyk@43785
   296
   (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
kaliszyk@43785
   297
   (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
huffman@44282
   298
  by (auto simp add: right_distrib)
kaliszyk@43785
   299
kaliszyk@43785
   300
lemma REAL_COMPLETE:
kaliszyk@43785
   301
  "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
kaliszyk@43785
   302
   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
kaliszyk@43785
   303
          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
kaliszyk@44633
   304
  using complete_real[unfolded Ball_def, of "Collect P"] by auto
kaliszyk@43785
   305
kaliszyk@43785
   306
lemma REAL_COMPLETE_SOMEPOS:
kaliszyk@43785
   307
  "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
kaliszyk@43785
   308
   (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
kaliszyk@43785
   309
          (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
kaliszyk@43785
   310
  using REAL_COMPLETE by auto
kaliszyk@43785
   311
kaliszyk@43785
   312
lemma REAL_ADD_AC:
kaliszyk@43785
   313
  "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
kaliszyk@43785
   314
  by simp
kaliszyk@43785
   315
kaliszyk@43785
   316
lemma REAL_LE_RNEG:
kaliszyk@43785
   317
  "((x :: real) \<le> - y) = (x + y \<le> 0)"
kaliszyk@43785
   318
  by auto
kaliszyk@43785
   319
kaliszyk@43785
   320
lemma REAL_LE_NEGTOTAL:
kaliszyk@43785
   321
  "0 \<le> (x :: real) \<or> 0 \<le> - x"
kaliszyk@43785
   322
  by auto
kaliszyk@43785
   323
kaliszyk@43785
   324
lemma DEF_real_sgn:
kaliszyk@43785
   325
  "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
kaliszyk@43785
   326
  by (simp add: ext)
kaliszyk@43785
   327
kaliszyk@43785
   328
end