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