src/HOL/Hyperreal/HyperArith.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15013 34264f5e4691
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
paulson@14371
     1
(*  Title:      HOL/HyperArith.thy
paulson@14369
     2
    ID:         $Id$
paulson@14369
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@14369
     4
    Copyright   1999  University of Cambridge
paulson@14369
     5
*)
paulson@14369
     6
paulson@14369
     7
header{*Binary arithmetic and Simplification for the Hyperreals*}
paulson@14369
     8
nipkow@15131
     9
theory HyperArith
nipkow@15131
    10
import HyperDef
nipkow@15131
    11
files ("hypreal_arith.ML")
nipkow@15131
    12
begin
paulson@14387
    13
paulson@14387
    14
subsection{*Numerals and Arithmetic*}
paulson@14369
    15
paulson@14369
    16
instance hypreal :: number ..
paulson@14369
    17
paulson@15013
    18
defs (overloaded)
paulson@15013
    19
  hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)"
paulson@15013
    20
    --{*the type constraint is essential!*}
paulson@14369
    21
paulson@14387
    22
instance hypreal :: number_ring
paulson@15013
    23
by (intro_classes, simp add: hypreal_number_of_def) 
paulson@14369
    24
paulson@14369
    25
paulson@14387
    26
text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
paulson@14387
    27
lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
paulson@15013
    28
by (simp add: hypreal_number_of_def real_number_of_def) 
paulson@15013
    29
paulson@14369
    30
paulson@14369
    31
paulson@14369
    32
use "hypreal_arith.ML"
paulson@10751
    33
paulson@10751
    34
setup hypreal_arith_setup
paulson@10751
    35
paulson@14370
    36
lemma hypreal_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::hypreal) \<le> x + y"
paulson@14370
    37
by arith
paulson@14370
    38
paulson@14329
    39
paulson@14371
    40
subsection{*The Function @{term hypreal_of_real}*}
paulson@14369
    41
paulson@14369
    42
lemma number_of_less_hypreal_of_real_iff [simp]:
paulson@14369
    43
     "(number_of w < hypreal_of_real z) = (number_of w < z)"
paulson@14369
    44
apply (subst hypreal_of_real_less_iff [symmetric])
paulson@14369
    45
apply (simp (no_asm))
paulson@14369
    46
done
paulson@14369
    47
paulson@14369
    48
lemma number_of_le_hypreal_of_real_iff [simp]:
paulson@14387
    49
     "(number_of w \<le> hypreal_of_real z) = (number_of w \<le> z)"
paulson@14369
    50
apply (subst hypreal_of_real_le_iff [symmetric])
paulson@14369
    51
apply (simp (no_asm))
paulson@14369
    52
done
paulson@14369
    53
paulson@14369
    54
lemma hypreal_of_real_eq_number_of_iff [simp]:
paulson@14369
    55
     "(hypreal_of_real z = number_of w) = (z = number_of w)"
paulson@14369
    56
apply (subst hypreal_of_real_eq_iff [symmetric])
paulson@14369
    57
apply (simp (no_asm))
paulson@14369
    58
done
paulson@14369
    59
paulson@14369
    60
lemma hypreal_of_real_less_number_of_iff [simp]:
paulson@14369
    61
     "(hypreal_of_real z < number_of w) = (z < number_of w)"
paulson@14369
    62
apply (subst hypreal_of_real_less_iff [symmetric])
paulson@14369
    63
apply (simp (no_asm))
paulson@14369
    64
done
paulson@14369
    65
paulson@14369
    66
lemma hypreal_of_real_le_number_of_iff [simp]:
paulson@14387
    67
     "(hypreal_of_real z \<le> number_of w) = (z \<le> number_of w)"
paulson@14369
    68
apply (subst hypreal_of_real_le_iff [symmetric])
paulson@14369
    69
apply (simp (no_asm))
paulson@14369
    70
done
paulson@14369
    71
paulson@14371
    72
subsection{*Absolute Value Function for the Hyperreals*}
paulson@14371
    73
paulson@14371
    74
declare abs_mult [simp]
paulson@14371
    75
paulson@15003
    76
lemma hrabs_add_less:
paulson@15003
    77
     "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
paulson@15003
    78
by (simp add: abs_if split: split_if_asm)
paulson@14371
    79
paulson@14387
    80
text{*used once in NSA*}
paulson@14371
    81
lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
paulson@14371
    82
by (blast intro!: order_le_less_trans abs_ge_zero)
paulson@14371
    83
paulson@14371
    84
lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
paulson@15003
    85
by (simp add: abs_if)
paulson@14371
    86
paulson@14371
    87
(* Needed in Geom.ML *)
paulson@14371
    88
lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
paulson@15003
    89
by (simp add: abs_if split add: split_if_asm)
paulson@14371
    90
paulson@14371
    91
lemma hypreal_of_real_hrabs:
paulson@14371
    92
    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
paulson@14371
    93
apply (unfold hypreal_of_real_def)
paulson@14371
    94
apply (auto simp add: hypreal_hrabs)
paulson@14371
    95
done
paulson@14371
    96
paulson@14371
    97
paulson@14371
    98
subsection{*Embedding the Naturals into the Hyperreals*}
paulson@14371
    99
paulson@14371
   100
constdefs
paulson@14371
   101
paulson@14378
   102
  hypreal_of_nat   :: "nat => hypreal"
paulson@14378
   103
   "hypreal_of_nat m  == of_nat m"
paulson@14378
   104
paulson@14378
   105
lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
paulson@14378
   106
by (force simp add: hypreal_of_nat_def Nats_def) 
paulson@14371
   107
paulson@14371
   108
paulson@14371
   109
lemma hypreal_of_nat_add [simp]:
paulson@14371
   110
     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
paulson@14371
   111
by (simp add: hypreal_of_nat_def)
paulson@14371
   112
paulson@14371
   113
lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
paulson@14371
   114
by (simp add: hypreal_of_nat_def)
paulson@14371
   115
declare hypreal_of_nat_mult [simp]
paulson@14371
   116
paulson@14371
   117
lemma hypreal_of_nat_less_iff:
paulson@14371
   118
      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
paulson@14371
   119
apply (simp add: hypreal_of_nat_def)
paulson@14371
   120
done
paulson@14371
   121
declare hypreal_of_nat_less_iff [symmetric, simp]
paulson@14371
   122
paulson@14371
   123
(*------------------------------------------------------------*)
paulson@14371
   124
(* naturals embedded in hyperreals                            *)
paulson@14371
   125
(* is a hyperreal c.f. NS extension                           *)
paulson@14371
   126
(*------------------------------------------------------------*)
paulson@14371
   127
paulson@14378
   128
lemma hypreal_of_nat_eq:
paulson@14378
   129
     "hypreal_of_nat (n::nat) = hypreal_of_real (real n)"
paulson@14378
   130
apply (induct n) 
paulson@14378
   131
apply (simp_all add: hypreal_of_nat_def real_of_nat_def)
paulson@14378
   132
done
paulson@14371
   133
paulson@14378
   134
lemma hypreal_of_nat:
paulson@14378
   135
     "hypreal_of_nat m = Abs_hypreal(hyprel``{%n. real m})"
paulson@14378
   136
apply (induct m) 
paulson@14378
   137
apply (simp_all add: hypreal_of_nat_def real_of_nat_def hypreal_zero_def 
paulson@14378
   138
                     hypreal_one_def hypreal_add)
paulson@14378
   139
done
paulson@14371
   140
paulson@14371
   141
lemma hypreal_of_nat_Suc:
paulson@14371
   142
     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
paulson@14378
   143
by (simp add: hypreal_of_nat_def)
paulson@14371
   144
paulson@14371
   145
(*"neg" is used in rewrite rules for binary comparisons*)
paulson@14371
   146
lemma hypreal_of_nat_number_of [simp]:
paulson@14371
   147
     "hypreal_of_nat (number_of v :: nat) =
paulson@14378
   148
         (if neg (number_of v :: int) then 0
paulson@14371
   149
          else (number_of v :: hypreal))"
paulson@14378
   150
by (simp add: hypreal_of_nat_eq)
paulson@14371
   151
paulson@14371
   152
lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
paulson@14378
   153
by (simp add: hypreal_of_nat_def) 
paulson@14371
   154
paulson@14371
   155
lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
paulson@14378
   156
by (simp add: hypreal_of_nat_def) 
paulson@14371
   157
paulson@14378
   158
lemma hypreal_of_nat_le_iff [simp]:
paulson@14378
   159
     "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
paulson@14378
   160
by (simp add: hypreal_of_nat_def) 
paulson@14371
   161
paulson@14378
   162
lemma hypreal_of_nat_ge_zero [simp]: "0 \<le> hypreal_of_nat n"
paulson@14378
   163
by (simp add: hypreal_of_nat_def) 
paulson@14371
   164
paulson@14371
   165
paulson@14309
   166
(*
paulson@14371
   167
FIXME: we should declare this, as for type int, but many proofs would break.
paulson@14309
   168
It replaces x+-y by x-y.
paulson@14309
   169
Addsimps [symmetric hypreal_diff_def]
paulson@14309
   170
*)
paulson@14309
   171
paulson@14369
   172
ML
paulson@14369
   173
{*
paulson@14370
   174
val hypreal_le_add_order = thm"hypreal_le_add_order";
paulson@14371
   175
paulson@14371
   176
val hypreal_of_nat_def = thm"hypreal_of_nat_def";
paulson@14371
   177
paulson@14371
   178
val hrabs_add_less = thm "hrabs_add_less";
paulson@14371
   179
val hrabs_disj = thm "hrabs_disj";
paulson@14371
   180
val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
paulson@14371
   181
val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
paulson@14371
   182
val hypreal_of_nat_add = thm "hypreal_of_nat_add";
paulson@14371
   183
val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
paulson@14371
   184
val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
paulson@14371
   185
val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
paulson@14371
   186
val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
paulson@14371
   187
val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
paulson@14371
   188
val hypreal_of_nat_one = thm "hypreal_of_nat_one";
paulson@14371
   189
val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
paulson@14371
   190
val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
paulson@14371
   191
val hypreal_of_nat = thm"hypreal_of_nat";
paulson@14369
   192
*}
paulson@14369
   193
paulson@10751
   194
end