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