src/HOL/Hyperreal/NSA.thy
author huffman
Sat, 16 Sep 2006 19:12:03 +0200
changeset 20554 c433e78d4203
parent 20552 2c31dd358c21
child 20562 c2f672be8522
permissions -rw-r--r--
define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : NSA.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
     4
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
     5
Converted to Isar and polished by lcp
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
     6
*)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
     8
header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15003
diff changeset
    10
theory NSA
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
    11
imports HyperArith "../Real/RComplete"
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15003
diff changeset
    12
begin
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    14
definition
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    16
  hnorm :: "'a::norm star \<Rightarrow> real star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    17
  "hnorm = *f* norm"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    18
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    19
  Infinitesimal  :: "('a::real_normed_vector) star set"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    20
  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    22
  HFinite :: "('a::real_normed_vector) star set"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    23
  "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    25
  HInfinite :: "('a::real_normed_vector) star set"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    26
  "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
    28
  approx :: "['a::real_normed_vector star, 'a star] => bool"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
    29
    (infixl "@=" 50)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
    30
    --{*the `infinitely close' relation*}
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    31
  "(x @= y) = ((x + -y) \<in> Infinitesimal)"
14653
0848ab6fe5fc constdefs: proper order;
wenzelm
parents: 14565
diff changeset
    32
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
    33
  st        :: "hypreal => hypreal"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
    34
    --{*the standard part of a hyperreal*}
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    35
  "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
    37
  monad     :: "'a::real_normed_vector star => 'a star set"
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    38
  "monad x = {y. x @= y}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    39
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
    40
  galaxy    :: "'a::real_normed_vector star => 'a star set"
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    41
  "galaxy x = {y. (x + -y) \<in> HFinite}"
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    42
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    43
const_syntax (xsymbols)
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    44
  approx  (infixl "\<approx>" 50)
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    45
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    46
const_syntax (HTML output)
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
    47
  approx  (infixl "\<approx>" 50)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
    48
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
    49
20554
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    50
lemma hypreal_of_real_of_real_eq: "hypreal_of_real r = of_real r"
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    51
proof -
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    52
  have "hypreal_of_real r = hypreal_of_real (of_real r)" by simp
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    53
  also have "\<dots> = of_real r" by (rule star_of_of_real)
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    54
  finally show ?thesis .
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    55
qed
14565
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14477
diff changeset
    56
20554
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    57
lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
c433e78d4203 define new constant of_real for class real_algebra_1;
huffman
parents: 20552
diff changeset
    58
by (simp add: Reals_def image_def hypreal_of_real_of_real_eq)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
    59
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
    60
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    61
subsection{*Nonstandard extension of the norm function*}
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    62
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    63
declare hnorm_def [transfer_unfold]
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    64
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    65
lemma hnorm_ge_zero [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    66
  "\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    67
by transfer (rule norm_ge_zero)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    68
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    69
lemma hnorm_eq_zero [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    70
  "\<And>x::'a::real_normed_vector star. (hnorm x = 0) = (x = 0)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    71
by transfer (rule norm_eq_zero)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    72
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    73
lemma hnorm_triangle_ineq:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    74
  "\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    75
by transfer (rule norm_triangle_ineq)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    76
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    77
lemma hnorm_scaleR:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    78
  "\<And>a (x::'a::real_normed_vector star).
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    79
   hnorm (( *f2* scaleR) a x) = \<bar>a\<bar> * hnorm x"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    80
by transfer (rule norm_scaleR)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    81
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    82
lemma hnorm_mult_ineq:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    83
  "\<And>x y::'a::real_normed_algebra star. hnorm (x * y) \<le> hnorm x * hnorm y"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    84
by transfer (rule norm_mult_ineq)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    85
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    86
lemma hnorm_mult:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    87
  "\<And>x y::'a::real_normed_div_algebra star. hnorm (x * y) = hnorm x * hnorm y"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    88
by transfer (rule norm_mult)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    89
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    90
lemma hnorm_one [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    91
  "hnorm (1\<Colon>'a::real_normed_div_algebra star) = 1"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    92
by transfer (rule norm_one)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    93
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    94
lemma hnorm_zero [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    95
  "hnorm (0\<Colon>'a::real_normed_vector star) = 0"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    96
by transfer (rule norm_zero)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    97
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    98
lemma zero_less_hnorm_iff [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
    99
  "\<And>x::'a::real_normed_vector star. (0 < hnorm x) = (x \<noteq> 0)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   100
by transfer (rule zero_less_norm_iff)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   101
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   102
lemma hnorm_minus_cancel [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   103
  "\<And>x::'a::real_normed_vector star. hnorm (- x) = hnorm x"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   104
by transfer (rule norm_minus_cancel)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   105
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   106
lemma hnorm_minus_commute:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   107
  "\<And>a b::'a::real_normed_vector star. hnorm (a - b) = hnorm (b - a)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   108
by transfer (rule norm_minus_commute)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   109
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   110
lemma hnorm_triangle_ineq2:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   111
  "\<And>a b::'a::real_normed_vector star. hnorm a - hnorm b \<le> hnorm (a - b)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   112
by transfer (rule norm_triangle_ineq2)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   113
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   114
lemma hnorm_triangle_ineq4:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   115
  "\<And>a b::'a::real_normed_vector star. hnorm (a - b) \<le> hnorm a + hnorm b"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   116
by transfer (rule norm_triangle_ineq4)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   117
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   118
lemma nonzero_hnorm_inverse:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   119
  "\<And>a::'a::real_normed_div_algebra star.
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   120
   a \<noteq> 0 \<Longrightarrow> hnorm (inverse a) = inverse (hnorm a)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   121
by transfer (rule nonzero_norm_inverse)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   122
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   123
lemma hnorm_inverse:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   124
  "\<And>a::'a::{real_normed_div_algebra,division_by_zero} star.
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   125
   hnorm (inverse a) = inverse (hnorm a)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   126
by transfer (rule norm_inverse)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   127
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   128
lemma hypreal_hnorm_def [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   129
  "\<And>r::hypreal. hnorm r \<equiv> \<bar>r\<bar>"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   130
by transfer (rule real_norm_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   131
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   132
lemma hnorm_add_less:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   133
  fixes x y :: "'a::real_normed_vector star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   134
  shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x + y) < r + s"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   135
by (rule order_le_less_trans [OF hnorm_triangle_ineq add_strict_mono])
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   136
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   137
lemma hnorm_mult_less:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   138
  fixes x y :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   139
  shows "\<lbrakk>hnorm x < r; hnorm y < s\<rbrakk> \<Longrightarrow> hnorm (x * y) < r * s"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   140
apply (rule order_le_less_trans [OF hnorm_mult_ineq])
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   141
apply (simp add: mult_strict_mono')
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   142
done
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   143
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   144
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   145
subsection{*Closure Laws for the Standard Reals*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   146
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14371
diff changeset
   147
lemma SReal_add [simp]:
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14371
diff changeset
   148
     "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x + y \<in> Reals"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   149
apply (auto simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   150
apply (rule_tac x = "r + ra" in exI, simp)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   151
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   152
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   153
lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   154
apply (simp add: SReal_def, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   155
apply (rule_tac x = "r * ra" in exI)
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15531
diff changeset
   156
apply (simp (no_asm))
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   157
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   158
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   159
lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   160
apply (simp add: SReal_def)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   161
apply (blast intro: star_of_inverse [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   162
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   163
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   164
lemma SReal_divide: "[| (x::hypreal) \<in> Reals;  y \<in> Reals |] ==> x/y \<in> Reals"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   165
by (simp (no_asm_simp) add: SReal_mult SReal_inverse divide_inverse)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   166
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   167
lemma SReal_minus: "(x::hypreal) \<in> Reals ==> -x \<in> Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   168
apply (simp add: SReal_def)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   169
apply (blast intro: star_of_minus [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   170
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   171
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   172
lemma SReal_minus_iff [simp]: "(-x \<in> Reals) = ((x::hypreal) \<in> Reals)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   173
apply auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   174
apply (erule_tac [2] SReal_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   175
apply (drule SReal_minus, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   176
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   177
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   178
lemma SReal_add_cancel:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   179
     "[| (x::hypreal) + y \<in> Reals; y \<in> Reals |] ==> x \<in> Reals"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   180
apply (drule_tac x = y in SReal_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   181
apply (drule SReal_add, assumption, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   182
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   183
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   184
lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   185
apply (auto simp add: SReal_def)
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   186
apply (rule_tac x="abs r" in exI)
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   187
apply simp
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   188
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   189
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   190
lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   191
by (simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   192
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   193
lemma SReal_number_of [simp]: "(number_of w ::hypreal) \<in> Reals"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   194
apply (simp only: star_of_number_of [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   195
apply (rule SReal_hypreal_of_real)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   196
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   197
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   198
(** As always with numerals, 0 and 1 are special cases **)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   199
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   200
lemma Reals_0 [simp]: "(0::hypreal) \<in> Reals"
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   201
apply (subst numeral_0_eq_0 [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   202
apply (rule SReal_number_of)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   203
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   204
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   205
lemma Reals_1 [simp]: "(1::hypreal) \<in> Reals"
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
   206
apply (subst numeral_1_eq_1 [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   207
apply (rule SReal_number_of)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   208
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   209
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   210
lemma SReal_divide_number_of: "r \<in> Reals ==> r/(number_of w::hypreal) \<in> Reals"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   211
apply (simp only: divide_inverse)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   212
apply (blast intro!: SReal_number_of SReal_mult SReal_inverse)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   213
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   214
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   215
text{*epsilon is not in Reals because it is an infinitesimal*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   216
lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   217
apply (simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   218
apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   219
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   220
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   221
lemma SReal_omega_not_mem: "omega \<notin> Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   222
apply (simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   223
apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   224
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   225
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   226
lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   227
by (simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   228
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   229
lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   230
by (simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   231
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   232
lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   233
by (auto simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   234
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   235
lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   236
apply (auto simp add: SReal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   237
apply (rule inj_hypreal_of_real [THEN inv_f_f, THEN subst], blast)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   238
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   239
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   240
lemma SReal_hypreal_of_real_image:
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   241
      "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   242
apply (simp add: SReal_def, blast)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   243
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   244
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   245
lemma SReal_dense:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   246
     "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   247
apply (auto simp add: SReal_iff)
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14468
diff changeset
   248
apply (drule dense, safe)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   249
apply (rule_tac x = "hypreal_of_real r" in bexI, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   250
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   251
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   252
text{*Completeness of Reals, but both lemmas are unused.*}
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   253
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   254
lemma SReal_sup_lemma:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   255
     "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   256
      (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   257
by (blast dest!: SReal_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   258
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   259
lemma SReal_sup_lemma2:
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   260
     "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   261
      ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   262
          (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   263
apply (rule conjI)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   264
apply (fast dest!: SReal_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   265
apply (auto, frule subsetD, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   266
apply (drule SReal_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   267
apply (auto, rule_tac x = ya in exI, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   268
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   269
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   270
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   271
subsection{*Lifting of the Ub and Lub Properties*}
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   272
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   273
lemma hypreal_of_real_isUb_iff:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   274
      "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   275
       (isUb (UNIV :: real set) Q Y)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   276
by (simp add: isUb_def setle_def)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   277
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   278
lemma hypreal_of_real_isLub1:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   279
     "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   280
      ==> isLub (UNIV :: real set) Q Y"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   281
apply (simp add: isLub_def leastP_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   282
apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   283
            simp add: hypreal_of_real_isUb_iff setge_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   284
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   285
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   286
lemma hypreal_of_real_isLub2:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   287
      "isLub (UNIV :: real set) Q Y
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   288
       ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   289
apply (simp add: isLub_def leastP_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   290
apply (auto simp add: hypreal_of_real_isUb_iff setge_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   291
apply (frule_tac x2 = x in isUbD2a [THEN SReal_iff [THEN iffD1], THEN exE])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   292
 prefer 2 apply assumption
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   293
apply (drule_tac x = xa in spec)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   294
apply (auto simp add: hypreal_of_real_isUb_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   295
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   296
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   297
lemma hypreal_of_real_isLub_iff:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   298
     "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   299
      (isLub (UNIV :: real set) Q Y)"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   300
by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   301
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   302
lemma lemma_isUb_hypreal_of_real:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   303
     "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   304
by (auto simp add: SReal_iff isUb_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   305
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   306
lemma lemma_isLub_hypreal_of_real:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   307
     "isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   308
by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   309
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   310
lemma lemma_isLub_hypreal_of_real2:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   311
     "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   312
by (auto simp add: isLub_def leastP_def isUb_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   313
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   314
lemma SReal_complete:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   315
     "[| P \<subseteq> Reals;  \<exists>x. x \<in> P;  \<exists>Y. isUb Reals P Y |]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   316
      ==> \<exists>t::hypreal. isLub Reals P t"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   317
apply (frule SReal_hypreal_of_real_image)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   318
apply (auto, drule lemma_isUb_hypreal_of_real)
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   319
apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   320
            simp add: hypreal_of_real_isLub_iff hypreal_of_real_isUb_iff)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   321
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   322
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   323
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   324
subsection{* Set of Finite Elements is a Subring of the Extended Reals*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   325
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   326
lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   327
apply (simp add: HFinite_def)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   328
apply (blast intro!: SReal_add hnorm_add_less)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   329
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   330
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   331
lemma HFinite_mult:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   332
  fixes x y :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   333
  shows "[|x \<in> HFinite; y \<in> HFinite|] ==> x*y \<in> HFinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   334
apply (simp add: HFinite_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   335
apply (blast intro!: SReal_mult hnorm_mult_less)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   336
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   337
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   338
lemma HFinite_minus_iff: "(-x \<in> HFinite) = (x \<in> HFinite)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   339
by (simp add: HFinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   340
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   341
lemma HFinite_star_of [simp]: "star_of x \<in> HFinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   342
apply (simp add: HFinite_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   343
apply (rule_tac x="star_of (norm x) + 1" in bexI)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   344
apply (transfer, simp)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   345
apply (blast intro: SReal_add SReal_hypreal_of_real Reals_1)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   346
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   347
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   348
lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   349
by (auto simp add: SReal_def)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   350
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   351
lemma HFinite_hypreal_of_real: "hypreal_of_real x \<in> HFinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   352
by (rule HFinite_star_of)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   353
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   354
lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   355
by (simp add: HFinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   356
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   357
lemma HFinite_hrabs_iff [iff]: "(abs (x::hypreal) \<in> HFinite) = (x \<in> HFinite)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   358
by (simp add: HFinite_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   359
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   360
lemma HFinite_hnorm_iff [iff]: "(hnorm x \<in> HFinite) = (x \<in> HFinite)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   361
by (simp add: HFinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   362
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   363
lemma HFinite_number_of [simp]: "number_of w \<in> HFinite"
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   364
by (unfold star_number_def, rule HFinite_star_of)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   365
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   366
(** As always with numerals, 0 and 1 are special cases **)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   367
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   368
lemma HFinite_0 [simp]: "0 \<in> HFinite"
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   369
by (unfold star_zero_def, rule HFinite_star_of)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   370
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   371
lemma HFinite_1 [simp]: "1 \<in> HFinite"
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   372
by (unfold star_one_def, rule HFinite_star_of)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   373
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   374
lemma HFinite_bounded:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   375
  "[|(x::hypreal) \<in> HFinite; y \<le> x; 0 \<le> y |] ==> y \<in> HFinite"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   376
apply (case_tac "x \<le> 0")
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   377
apply (drule_tac y = x in order_trans)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   378
apply (drule_tac [2] order_antisym)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   379
apply (auto simp add: linorder_not_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   380
apply (auto intro: order_le_less_trans simp add: abs_if HFinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   381
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   382
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   383
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   384
subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   385
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   386
lemma InfinitesimalI:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   387
  "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   388
by (simp add: Infinitesimal_def)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   389
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   390
lemma InfinitesimalD:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   391
      "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> hnorm x < r"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   392
by (simp add: Infinitesimal_def)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   393
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   394
lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   395
by (simp add: Infinitesimal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   396
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   397
lemma hypreal_sum_of_halves: "x/(2::hypreal) + x/(2::hypreal) = x"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   398
by auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   399
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   400
lemma Infinitesimal_add:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   401
     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   402
apply (rule InfinitesimalI)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   403
apply (rule hypreal_sum_of_halves [THEN subst])
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14468
diff changeset
   404
apply (drule half_gt_zero)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   405
apply (blast intro: hnorm_add_less SReal_divide_number_of dest: InfinitesimalD)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   406
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   407
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   408
lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   409
by (simp add: Infinitesimal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   410
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   411
lemma Infinitesimal_diff:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   412
     "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   413
by (simp add: diff_def Infinitesimal_add)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   414
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   415
lemma Infinitesimal_mult:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   416
  fixes x y :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   417
  shows "[|x \<in> Infinitesimal; y \<in> Infinitesimal|] ==> (x * y) \<in> Infinitesimal"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   418
apply (rule InfinitesimalI)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   419
apply (case_tac "y = 0", simp)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   420
apply (subgoal_tac "hnorm (x * y) < 1 * r", simp only: mult_1)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   421
apply (rule hnorm_mult_less)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   422
apply (simp_all add: InfinitesimalD)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   423
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   424
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   425
lemma Infinitesimal_HFinite_mult:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   426
  fixes x y :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   427
  shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   428
apply (rule InfinitesimalI)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   429
apply (drule HFiniteD, clarify)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   430
apply (subgoal_tac "0 < t")
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   431
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   432
apply (subgoal_tac "0 < r / t")
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   433
apply (rule hnorm_mult_less)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   434
apply (simp add: InfinitesimalD SReal_divide)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   435
apply assumption
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   436
apply (simp only: divide_pos_pos)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   437
apply (erule order_le_less_trans [OF hnorm_ge_zero])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   438
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   439
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   440
lemma Infinitesimal_HFinite_mult2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   441
  fixes x y :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   442
  shows "[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (y * x) \<in> Infinitesimal"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   443
apply (rule InfinitesimalI)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   444
apply (drule HFiniteD, clarify)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   445
apply (subgoal_tac "0 < t")
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   446
apply (subgoal_tac "hnorm (y * x) < t * (r / t)", simp)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   447
apply (subgoal_tac "0 < r / t")
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   448
apply (rule hnorm_mult_less)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   449
apply assumption
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   450
apply (simp add: InfinitesimalD SReal_divide)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   451
apply (simp only: divide_pos_pos)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   452
apply (erule order_le_less_trans [OF hnorm_ge_zero])
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   453
done
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   454
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   455
lemma Compl_HFinite: "- HFinite = HInfinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   456
apply (auto simp add: HInfinite_def HFinite_def linorder_not_less)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   457
apply (rule_tac y="r + 1" in order_less_le_trans, simp)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   458
apply (simp add: SReal_add Reals_1)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   459
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   460
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   461
lemma HInfinite_inverse_Infinitesimal:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   462
  fixes x :: "'a::real_normed_div_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   463
  shows "x \<in> HInfinite ==> inverse x \<in> Infinitesimal"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   464
apply (rule InfinitesimalI)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   465
apply (subgoal_tac "x \<noteq> 0")
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   466
apply (rule inverse_less_imp_less)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   467
apply (simp add: nonzero_hnorm_inverse)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   468
apply (simp add: HInfinite_def SReal_inverse)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   469
apply assumption
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   470
apply (clarify, simp add: Compl_HFinite [symmetric])
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   471
done
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   472
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   473
lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < hnorm x) \<Longrightarrow> x \<in> HInfinite"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   474
by (simp add: HInfinite_def)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   475
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   476
lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < hnorm x"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   477
by (simp add: HInfinite_def)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   478
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   479
lemma HInfinite_mult:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   480
  fixes x y :: "'a::real_normed_div_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   481
  shows "[|x \<in> HInfinite; y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   482
apply (rule HInfiniteI, simp only: hnorm_mult)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   483
apply (subgoal_tac "r * 1 < hnorm x * hnorm y", simp only: mult_1)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   484
apply (case_tac "x = 0", simp add: HInfinite_def)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   485
apply (rule mult_strict_mono)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   486
apply (simp_all add: HInfiniteD)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   487
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   488
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   489
lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   490
by (auto dest: add_less_le_mono)
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   491
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   492
lemma HInfinite_add_ge_zero:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   493
     "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (x + y): HInfinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   494
by (auto intro!: hypreal_add_zero_less_le_mono 
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   495
       simp add: abs_if add_commute add_nonneg_nonneg HInfinite_def)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   496
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   497
lemma HInfinite_add_ge_zero2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   498
     "[|(x::hypreal) \<in> HInfinite; 0 \<le> y; 0 \<le> x|] ==> (y + x): HInfinite"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   499
by (auto intro!: HInfinite_add_ge_zero simp add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   500
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   501
lemma HInfinite_add_gt_zero:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   502
     "[|(x::hypreal) \<in> HInfinite; 0 < y; 0 < x|] ==> (x + y): HInfinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   503
by (blast intro: HInfinite_add_ge_zero order_less_imp_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   504
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   505
lemma HInfinite_minus_iff: "(-x \<in> HInfinite) = (x \<in> HInfinite)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   506
by (simp add: HInfinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   507
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   508
lemma HInfinite_add_le_zero:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   509
     "[|(x::hypreal) \<in> HInfinite; y \<le> 0; x \<le> 0|] ==> (x + y): HInfinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   510
apply (drule HInfinite_minus_iff [THEN iffD2])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   511
apply (rule HInfinite_minus_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   512
apply (auto intro: HInfinite_add_ge_zero)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   513
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   514
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   515
lemma HInfinite_add_lt_zero:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   516
     "[|(x::hypreal) \<in> HInfinite; y < 0; x < 0|] ==> (x + y): HInfinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   517
by (blast intro: HInfinite_add_le_zero order_less_imp_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   518
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   519
lemma HFinite_sum_squares:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   520
  fixes a b c :: "'a::real_normed_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   521
  shows "[|a: HFinite; b: HFinite; c: HFinite|]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   522
      ==> a*a + b*b + c*c \<in> HFinite"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   523
by (auto intro: HFinite_mult HFinite_add)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   524
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   525
lemma not_Infinitesimal_not_zero: "x \<notin> Infinitesimal ==> x \<noteq> 0"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   526
by auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   527
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   528
lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   529
by auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   530
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   531
lemma Infinitesimal_hrabs_iff [iff]:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   532
     "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14653
diff changeset
   533
by (auto simp add: abs_if)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   534
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   535
lemma HFinite_diff_Infinitesimal_hrabs:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   536
  "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   537
by blast
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   538
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   539
lemma hrabs_less_Infinitesimal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   540
      "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   541
by (auto simp add: Infinitesimal_def abs_less_iff)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   542
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   543
lemma hrabs_le_Infinitesimal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   544
     "[| e \<in> Infinitesimal; abs (x::hypreal) \<le> e |] ==> x \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   545
by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   546
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   547
lemma Infinitesimal_interval:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   548
      "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |] 
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   549
       ==> (x::hypreal) \<in> Infinitesimal"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   550
by (auto simp add: Infinitesimal_def abs_less_iff)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   551
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   552
lemma Infinitesimal_interval2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   553
     "[| e \<in> Infinitesimal; e' \<in> Infinitesimal;
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   554
         e' \<le> x ; x \<le> e |] ==> (x::hypreal) \<in> Infinitesimal"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   555
by (auto intro: Infinitesimal_interval simp add: order_le_less)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   556
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   557
lemma not_Infinitesimal_mult:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   558
  fixes x y :: "'a::real_normed_div_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   559
  shows "[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   560
apply (unfold Infinitesimal_def, clarify, rename_tac r s)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   561
apply (simp only: linorder_not_less hnorm_mult)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   562
apply (drule_tac x = "r * s" in bspec)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   563
apply (fast intro: SReal_mult)
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   564
apply (drule mp, blast intro: mult_pos_pos)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   565
apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
20407
93a34d5d1dc5 speed up some proofs
huffman
parents: 20254
diff changeset
   566
apply (simp_all (no_asm_simp))
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   567
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   568
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   569
lemma Infinitesimal_mult_disj:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   570
  fixes x y :: "'a::real_normed_div_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   571
  shows "x*y \<in> Infinitesimal ==> x \<in> Infinitesimal | y \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   572
apply (rule ccontr)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   573
apply (drule de_Morgan_disj [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   574
apply (fast dest: not_Infinitesimal_mult)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   575
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   576
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   577
lemma HFinite_Infinitesimal_not_zero: "x \<in> HFinite-Infinitesimal ==> x \<noteq> 0"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   578
by blast
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   579
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   580
lemma HFinite_Infinitesimal_diff_mult:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   581
  fixes x y :: "'a::real_normed_div_algebra star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   582
  shows "[| x \<in> HFinite - Infinitesimal;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   583
                   y \<in> HFinite - Infinitesimal
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   584
                |] ==> (x*y) \<in> HFinite - Infinitesimal"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   585
apply clarify
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   586
apply (blast dest: HFinite_mult not_Infinitesimal_mult)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   587
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   588
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   589
lemma Infinitesimal_subset_HFinite:
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   590
      "Infinitesimal \<subseteq> HFinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   591
apply (simp add: Infinitesimal_def HFinite_def, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   592
apply (rule_tac x = 1 in bexI, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   593
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   594
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   595
lemma Infinitesimal_hypreal_of_real_mult:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   596
     "x \<in> Infinitesimal ==> x * hypreal_of_real r \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   597
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   598
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   599
lemma Infinitesimal_hypreal_of_real_mult2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   600
     "x \<in> Infinitesimal ==> hypreal_of_real r * x \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   601
by (erule HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult2])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   602
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   603
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   604
subsection{*The Infinitely Close Relation*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   605
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   606
lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   607
by (simp add: Infinitesimal_def approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   608
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   609
lemma approx_minus_iff: " (x @= y) = (x + -y @= 0)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   610
by (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   611
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   612
lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   613
by (simp add: approx_def add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   614
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   615
lemma approx_refl [iff]: "x @= x"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   616
by (simp add: approx_def Infinitesimal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   617
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   618
lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   619
by (simp add: add_commute)
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14468
diff changeset
   620
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   621
lemma approx_sym: "x @= y ==> y @= x"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   622
apply (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   623
apply (rule hypreal_minus_distrib1 [THEN subst])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   624
apply (erule Infinitesimal_minus_iff [THEN iffD2])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   625
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   626
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   627
lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   628
apply (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   629
apply (drule Infinitesimal_add, assumption, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   630
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   631
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   632
lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   633
by (blast intro: approx_sym approx_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   634
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   635
lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   636
by (blast intro: approx_sym approx_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   637
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   638
lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   639
by (blast intro: approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   640
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   641
lemma zero_approx_reorient: "(0 @= x) = (x @= 0)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   642
by (blast intro: approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   643
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   644
lemma one_approx_reorient: "(1 @= x) = (x @= 1)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   645
by (blast intro: approx_sym)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   646
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   647
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   648
ML {*
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   649
local
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   650
(*** re-orientation, following HOL/Integ/Bin.ML
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   651
     We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   652
 ***)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   653
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   654
(*reorientation simprules using ==, for the following simproc*)
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   655
val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   656
val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   657
val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   658
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   659
(*reorientation simplification procedure: reorients (polymorphic)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   660
  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   661
fun reorient_proc sg _ (_ $ t $ u) =
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   662
  case u of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15251
diff changeset
   663
      Const("0", _) => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15251
diff changeset
   664
    | Const("1", _) => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15251
diff changeset
   665
    | Const("Numeral.number_of", _) $ _ => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15251
diff changeset
   666
    | _ => SOME (case t of
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   667
                Const("0", _) => meta_zero_approx_reorient
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   668
              | Const("1", _) => meta_one_approx_reorient
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   669
              | Const("Numeral.number_of", _) $ _ =>
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   670
                                 meta_number_of_approx_reorient);
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   671
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   672
in
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   673
val approx_reorient_simproc =
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20432
diff changeset
   674
  Int_Numeral_Base_Simprocs.prep_simproc
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   675
    ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
19765
dfe940911617 misc cleanup;
wenzelm
parents: 17431
diff changeset
   676
end;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   677
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   678
Addsimprocs [approx_reorient_simproc];
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   679
*}
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   680
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   681
lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   682
by (auto simp add: diff_def approx_minus_iff [symmetric] mem_infmal_iff)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   683
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   684
lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   685
apply (simp add: monad_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   686
apply (auto dest: approx_sym elim!: approx_trans equalityCE)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   687
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   688
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   689
lemma Infinitesimal_approx:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   690
     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   691
apply (simp add: mem_infmal_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   692
apply (blast intro: approx_trans approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   693
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   694
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   695
lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   696
proof (unfold approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   697
  assume inf: "a + - b \<in> Infinitesimal" "c + - d \<in> Infinitesimal"
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   698
  have "a + c + - (b + d) = (a + - b) + (c + - d)" by simp
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   699
  also have "... \<in> Infinitesimal" using inf by (rule Infinitesimal_add)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   700
  finally show "a + c + - (b + d) \<in> Infinitesimal" .
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   701
qed
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   702
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   703
lemma approx_minus: "a @= b ==> -a @= -b"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   704
apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   705
apply (drule approx_minus_iff [THEN iffD1])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   706
apply (simp (no_asm) add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   707
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   708
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   709
lemma approx_minus2: "-a @= -b ==> a @= b"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   710
by (auto dest: approx_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   711
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   712
lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   713
by (blast intro: approx_minus approx_minus2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   714
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   715
lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   716
by (blast intro!: approx_add approx_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   717
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   718
lemma approx_mult1:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   719
  fixes a b c :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   720
  shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   721
by (simp add: approx_def Infinitesimal_HFinite_mult minus_mult_left 
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   722
              left_distrib [symmetric] 
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   723
         del: minus_mult_left [symmetric])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   724
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   725
lemma approx_mult2:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   726
  fixes a b c :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   727
  shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   728
by (simp add: approx_def Infinitesimal_HFinite_mult2 minus_mult_right 
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   729
              right_distrib [symmetric] 
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   730
         del: minus_mult_right [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   731
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   732
lemma approx_mult_subst:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   733
  fixes u v x y :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   734
  shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   735
by (blast intro: approx_mult2 approx_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   736
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   737
lemma approx_mult_subst2:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   738
  fixes u v x y :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   739
  shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   740
by (blast intro: approx_mult1 approx_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   741
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   742
lemma approx_mult_subst_star_of:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   743
  fixes u x y :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   744
  shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   745
by (auto intro: approx_mult_subst2)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   746
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   747
lemma approx_mult_subst_SReal:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   748
     "[| u @= x*hypreal_of_real v; x @= y |] ==> u @= y*hypreal_of_real v"
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   749
by (rule approx_mult_subst_star_of)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   750
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   751
lemma approx_eq_imp: "a = b ==> a @= b"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   752
by (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   753
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   754
lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   755
by (blast intro: Infinitesimal_minus_iff [THEN iffD2] 
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   756
                    mem_infmal_iff [THEN iffD1] approx_trans2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   757
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   758
lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x + -z = y) = (x @= z)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   759
by (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   760
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   761
lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   762
by (force simp add: bex_Infinitesimal_iff [symmetric])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   763
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   764
lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   765
apply (rule bex_Infinitesimal_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   766
apply (drule Infinitesimal_minus_iff [THEN iffD2])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   767
apply (auto simp add: add_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   768
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   769
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   770
lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   771
apply (rule bex_Infinitesimal_iff [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   772
apply (drule Infinitesimal_minus_iff [THEN iffD2])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   773
apply (auto simp add: add_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   774
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   775
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   776
lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   777
by (auto dest: Infinitesimal_add_approx_self simp add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   778
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   779
lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   780
by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   781
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   782
lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   783
apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   784
apply (erule approx_trans3 [THEN approx_sym], assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   785
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   786
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   787
lemma Infinitesimal_add_right_cancel:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   788
     "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   789
apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   790
apply (erule approx_trans3 [THEN approx_sym])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   791
apply (simp add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   792
apply (erule approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   793
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   794
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   795
lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   796
apply (drule approx_minus_iff [THEN iffD1])
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15531
diff changeset
   797
apply (simp add: approx_minus_iff [symmetric] add_ac)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   798
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   799
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   800
lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   801
apply (rule approx_add_left_cancel)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   802
apply (simp add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   803
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   804
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   805
lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   806
apply (rule approx_minus_iff [THEN iffD2])
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15531
diff changeset
   807
apply (simp add: approx_minus_iff [symmetric] add_ac)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   808
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   809
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   810
lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   811
by (simp add: add_commute approx_add_mono1)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   812
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   813
lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   814
by (fast elim: approx_add_left_cancel approx_add_mono1)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   815
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   816
lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   817
by (simp add: add_commute)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   818
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   819
lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   820
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   821
apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   822
apply (drule HFinite_add)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   823
apply (auto simp add: add_assoc)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   824
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   825
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   826
lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   827
by (rule approx_sym [THEN [2] approx_HFinite], auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   828
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   829
lemma approx_hypreal_of_real_HFinite: "x @= hypreal_of_real D ==> x \<in> HFinite"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   830
by (rule approx_star_of_HFinite)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   831
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   832
lemma approx_mult_HFinite:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   833
  fixes a b c d :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   834
  shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   835
apply (rule approx_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   836
apply (rule_tac [2] approx_mult2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   837
apply (rule approx_mult1)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   838
prefer 2 apply (blast intro: approx_HFinite approx_sym, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   839
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   840
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   841
lemma approx_mult_star_of:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   842
  fixes a c :: "'a::real_normed_algebra star"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   843
  shows "[|a @= star_of b; c @= star_of d |]
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   844
      ==> a*c @= star_of b*star_of d"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   845
by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   846
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   847
lemma approx_mult_hypreal_of_real:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   848
     "[|a @= hypreal_of_real b; c @= hypreal_of_real d |]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   849
      ==> a*c @= hypreal_of_real b*hypreal_of_real d"
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   850
by (rule approx_mult_star_of)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   851
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   852
lemma approx_SReal_mult_cancel_zero:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   853
     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   854
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   855
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   856
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   857
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   858
lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   859
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   860
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   861
lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   862
by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   863
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   864
lemma approx_mult_SReal_zero_cancel_iff [simp]:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   865
     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   866
by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   867
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   868
lemma approx_SReal_mult_cancel:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   869
     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   870
apply (drule SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   871
apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   872
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   873
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   874
lemma approx_SReal_mult_cancel_iff1 [simp]:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   875
     "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   876
by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   877
         intro: approx_SReal_mult_cancel)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   878
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   879
lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   880
apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   881
apply (rule_tac x = "g+y-z" in bexI)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   882
apply (simp (no_asm))
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   883
apply (rule Infinitesimal_interval2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   884
apply (rule_tac [2] Infinitesimal_zero, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   885
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   886
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   887
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15531
diff changeset
   888
subsection{* Zero is the Only Infinitesimal that is also a Real*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   889
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   890
lemma Infinitesimal_less_SReal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   891
     "[| (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   892
apply (simp add: Infinitesimal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   893
apply (rule abs_ge_self [THEN order_le_less_trans], auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   894
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   895
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   896
lemma Infinitesimal_less_SReal2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   897
     "(y::hypreal) \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> y < r"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   898
by (blast intro: Infinitesimal_less_SReal)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   899
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   900
lemma SReal_not_Infinitesimal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   901
     "[| 0 < y;  (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   902
apply (simp add: Infinitesimal_def)
15003
6145dd7538d7 replaced monomorphic abs definitions by abs_if
paulson
parents: 14653
diff changeset
   903
apply (auto simp add: abs_if)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   904
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   905
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   906
lemma SReal_minus_not_Infinitesimal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   907
     "[| y < 0;  (y::hypreal) \<in> Reals |] ==> y \<notin> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   908
apply (subst Infinitesimal_minus_iff [symmetric])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   909
apply (rule SReal_not_Infinitesimal, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   910
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   911
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   912
lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   913
apply auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   914
apply (cut_tac x = x and y = 0 in linorder_less_linear)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   915
apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   916
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   917
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   918
lemma SReal_Infinitesimal_zero:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   919
  "[| (x::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   920
by (cut_tac SReal_Int_Infinitesimal_zero, blast)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   921
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   922
lemma SReal_HFinite_diff_Infinitesimal:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   923
     "[| (x::hypreal) \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   924
by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   925
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   926
lemma hypreal_of_real_HFinite_diff_Infinitesimal:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   927
     "hypreal_of_real x \<noteq> 0 ==> hypreal_of_real x \<in> HFinite - Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   928
by (rule SReal_HFinite_diff_Infinitesimal, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   929
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   930
lemma star_of_Infinitesimal_iff_0 [iff]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   931
  "(star_of x \<in> Infinitesimal) = (x = 0)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   932
apply (auto simp add: Infinitesimal_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   933
apply (drule_tac x="hnorm (star_of x)" in bspec)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   934
apply (simp add: hnorm_def)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   935
apply simp
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   936
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   937
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   938
lemma star_of_HFinite_diff_Infinitesimal:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   939
     "x \<noteq> 0 ==> star_of x \<in> HFinite - Infinitesimal"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   940
by simp
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   941
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   942
lemma hypreal_of_real_Infinitesimal_iff_0:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   943
     "(hypreal_of_real x \<in> Infinitesimal) = (x=0)"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   944
by (rule star_of_Infinitesimal_iff_0)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   945
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
   946
lemma number_of_not_Infinitesimal [simp]:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   947
     "number_of w \<noteq> (0::hypreal) ==> (number_of w :: hypreal) \<notin> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   948
by (fast dest: SReal_number_of [THEN SReal_Infinitesimal_zero])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   949
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   950
(*again: 1 is a special case, but not 0 this time*)
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   951
lemma one_not_Infinitesimal [simp]:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   952
  "(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> Infinitesimal"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   953
apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   954
apply simp
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   955
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   956
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   957
lemma approx_SReal_not_zero:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   958
  "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   959
apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   960
apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   961
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   962
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   963
lemma HFinite_diff_Infinitesimal_approx:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   964
     "[| x @= y; y \<in> HFinite - Infinitesimal |]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   965
      ==> x \<in> HFinite - Infinitesimal"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   966
apply (auto intro: approx_sym [THEN [2] approx_HFinite]
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   967
            simp add: mem_infmal_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   968
apply (drule approx_trans3, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   969
apply (blast dest: approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   970
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   971
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   972
(*The premise y\<noteq>0 is essential; otherwise x/y =0 and we lose the
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   973
  HFinite premise.*)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   974
lemma Infinitesimal_ratio:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   975
  fixes x y :: "'a::{real_normed_div_algebra,field} star"
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   976
  shows "[| y \<noteq> 0;  y \<in> Infinitesimal;  x/y \<in> HFinite |]
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   977
         ==> x \<in> Infinitesimal"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   978
apply (drule Infinitesimal_HFinite_mult2, assumption)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
   979
apply (simp add: divide_inverse mult_assoc)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   980
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   981
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   982
lemma Infinitesimal_SReal_divide: 
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
   983
  "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   984
apply (simp add: divide_inverse)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   985
apply (auto intro!: Infinitesimal_HFinite_mult 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   986
            dest!: SReal_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   987
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   988
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   989
(*------------------------------------------------------------------
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   990
       Standard Part Theorem: Every finite x: R* is infinitely
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   991
       close to a unique real number (i.e a member of Reals)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   992
 ------------------------------------------------------------------*)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   993
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
   994
subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
   995
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   996
lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   997
apply safe
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   998
apply (simp add: approx_def)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
   999
apply (simp only: star_of_minus [symmetric] star_of_add [symmetric])
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1000
apply (simp only: star_of_Infinitesimal_iff_0)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1001
apply (simp only: diff_minus [symmetric] right_minus_eq)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1002
done
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1003
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1004
lemma SReal_approx_iff:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1005
  "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1006
apply auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1007
apply (simp add: approx_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1008
apply (drule_tac x = y in SReal_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1009
apply (drule SReal_add, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1010
apply (drule SReal_Infinitesimal_zero, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1011
apply (drule sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1012
apply (simp add: hypreal_eq_minus_iff [symmetric])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1013
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1014
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1015
lemma number_of_approx_iff [simp]:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1016
     "(number_of v @= (number_of w :: 'a::{number,real_normed_vector} star)) =
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1017
      (number_of v = (number_of w :: 'a))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1018
apply (unfold star_number_def)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1019
apply (rule star_of_approx_iff)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1020
done
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1021
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1022
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1023
lemma [simp]:
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1024
  "(number_of w @= (0::'a::{number,real_normed_vector} star)) =
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1025
   (number_of w = (0::'a))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1026
  "((0::'a::{number,real_normed_vector} star) @= number_of w) =
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1027
   (number_of w = (0::'a))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1028
  "(number_of w @= (1::'b::{number,one,real_normed_vector} star)) =
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1029
   (number_of w = (1::'b))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1030
  "((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1031
   (number_of w = (1::'b))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1032
  "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1033
  "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1034
apply (unfold star_number_def star_zero_def star_one_def)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1035
apply (unfold star_of_approx_iff)
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1036
by (auto intro: sym)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1037
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1038
lemma hypreal_of_real_approx_iff:
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1039
     "(hypreal_of_real k @= hypreal_of_real m) = (k = m)"
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1040
by (rule star_of_approx_iff)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1041
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1042
lemma hypreal_of_real_approx_number_of_iff [simp]:
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1043
     "(hypreal_of_real k @= number_of w) = (k = number_of w)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1044
by (subst hypreal_of_real_approx_iff [symmetric], auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1045
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1046
(*And also for 0 and 1.*)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1047
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1048
lemma [simp]: "(hypreal_of_real k @= 0) = (k = 0)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1049
              "(hypreal_of_real k @= 1) = (k = 1)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1050
  by (simp_all add:  hypreal_of_real_approx_iff [symmetric])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1051
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1052
lemma approx_unique_real:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1053
     "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1054
by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1055
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1056
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1057
subsection{* Existence of Unique Real Infinitely Close*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1058
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1059
(* lemma about lubs *)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1060
lemma hypreal_isLub_unique:
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1061
     "[| isLub R S x; isLub R S y |] ==> x = (y::hypreal)"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1062
apply (frule isLub_isUb)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1063
apply (frule_tac x = y in isLub_isUb)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
  1064
apply (blast intro!: order_antisym dest!: isLub_le_isUb)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1065
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1066
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1067
lemma lemma_st_part_ub:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1068
     "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1069
apply (drule HFiniteD, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1070
apply (rule exI, rule isUbI)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1071
apply (auto intro: setleI isUbI simp add: abs_less_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1072
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1073
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1074
lemma lemma_st_part_nonempty:
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1075
  "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1076
apply (drule HFiniteD, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1077
apply (drule SReal_minus)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1078
apply (rule_tac x = "-t" in exI)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1079
apply (auto simp add: abs_less_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1080
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1081
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1082
lemma lemma_st_part_subset: "{s. s \<in> Reals & s < x} \<subseteq> Reals"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1083
by auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1084
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1085
lemma lemma_st_part_lub:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1086
     "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1087
by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty lemma_st_part_subset)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1088
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1089
lemma lemma_hypreal_le_left_cancel: "((t::hypreal) + r \<le> t) = (r \<le> 0)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1090
apply safe
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1091
apply (drule_tac c = "-t" in add_left_mono)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1092
apply (drule_tac [2] c = t in add_left_mono)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
  1093
apply (auto simp add: add_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1094
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1095
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1096
lemma lemma_st_part_le1:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1097
     "[| (x::hypreal) \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1098
         r \<in> Reals;  0 < r |] ==> x \<le> t + r"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1099
apply (frule isLubD1a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1100
apply (rule ccontr, drule linorder_not_le [THEN iffD2])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1101
apply (drule_tac x = t in SReal_add, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1102
apply (drule_tac y = "t + r" in isLubD1 [THEN setleD], auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1103
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1104
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1105
lemma hypreal_setle_less_trans:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1106
     "[| S *<= (x::hypreal); x < y |] ==> S *<= y"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1107
apply (simp add: setle_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1108
apply (auto dest!: bspec order_le_less_trans intro: order_less_imp_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1109
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1110
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1111
lemma hypreal_gt_isUb:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1112
     "[| isUb R S (x::hypreal); x < y; y \<in> R |] ==> isUb R S y"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1113
apply (simp add: isUb_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1114
apply (blast intro: hypreal_setle_less_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1115
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1116
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1117
lemma lemma_st_part_gt_ub:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1118
     "[| (x::hypreal) \<in> HFinite; x < y; y \<in> Reals |]
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1119
      ==> isUb Reals {s. s \<in> Reals & s < x} y"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1120
by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1121
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1122
lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1123
apply (drule_tac c = "-t" in add_left_mono)
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 17298
diff changeset
  1124
apply (auto simp add: add_assoc [symmetric])
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1125
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1126
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1127
lemma lemma_st_part_le2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1128
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1129
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1130
         r \<in> Reals; 0 < r |]
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1131
      ==> t + -r \<le> x"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1132
apply (frule isLubD1a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1133
apply (rule ccontr, drule linorder_not_le [THEN iffD1])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1134
apply (drule SReal_minus, drule_tac x = t in SReal_add, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1135
apply (drule lemma_st_part_gt_ub, assumption+)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1136
apply (drule isLub_le_isUb, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1137
apply (drule lemma_minus_le_zero)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1138
apply (auto dest: order_less_le_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1139
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1140
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1141
lemma lemma_st_part1a:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1142
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1143
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1144
         r \<in> Reals; 0 < r |]
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1145
      ==> x + -t \<le> r"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1146
apply (subgoal_tac "x \<le> t+r") 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1147
apply (auto intro: lemma_st_part_le1)
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1148
done
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1149
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1150
lemma lemma_st_part2a:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1151
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1152
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1153
         r \<in> Reals;  0 < r |]
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1154
      ==> -(x + -t) \<le> r"
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1155
apply (subgoal_tac "(t + -r \<le> x)") 
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1156
apply (auto intro: lemma_st_part_le2)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1157
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1158
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1159
lemma lemma_SReal_ub:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1160
     "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1161
by (auto intro: isUbI setleI order_less_imp_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1162
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1163
lemma lemma_SReal_lub:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1164
     "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1165
apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1166
apply (frule isUbD2a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1167
apply (rule_tac x = x and y = y in linorder_cases)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1168
apply (auto intro!: order_less_imp_le)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1169
apply (drule SReal_dense, assumption, assumption, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1170
apply (drule_tac y = r in isUbD)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1171
apply (auto dest: order_less_le_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1172
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1173
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1174
lemma lemma_st_part_not_eq1:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1175
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1176
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1177
         r \<in> Reals; 0 < r |]
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1178
      ==> x + -t \<noteq> r"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1179
apply auto
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1180
apply (frule isLubD1a [THEN SReal_minus])
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1181
apply (drule SReal_add_cancel, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1182
apply (drule_tac x = x in lemma_SReal_lub)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1183
apply (drule hypreal_isLub_unique, assumption, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1184
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1185
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1186
lemma lemma_st_part_not_eq2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1187
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1188
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1189
         r \<in> Reals; 0 < r |]
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1190
      ==> -(x + -t) \<noteq> r"
15539
333a88244569 comprehensive cleanup, replacing sumr by setsum
nipkow
parents: 15531
diff changeset
  1191
apply (auto)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1192
apply (frule isLubD1a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1193
apply (drule SReal_add_cancel, assumption)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1194
apply (drule_tac x = "-x" in SReal_minus, simp)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1195
apply (drule_tac x = x in lemma_SReal_lub)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1196
apply (drule hypreal_isLub_unique, assumption, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1197
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1198
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1199
lemma lemma_st_part_major:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1200
     "[| (x::hypreal) \<in> HFinite;
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1201
         isLub Reals {s. s \<in> Reals & s < x} t;
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1202
         r \<in> Reals; 0 < r |]
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1203
      ==> abs (x + -t) < r"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1204
apply (frule lemma_st_part1a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1205
apply (frule_tac [4] lemma_st_part2a, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1206
apply (drule order_le_imp_less_or_eq)+
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1207
apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1208
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1209
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1210
lemma lemma_st_part_major2:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1211
     "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1212
      ==> \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1213
by (blast dest!: lemma_st_part_major)
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1214
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1215
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1216
text{*Existence of real and Standard Part Theorem*}
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1217
lemma lemma_st_part_Ex:
20541
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1218
     "(x::hypreal) \<in> HFinite
f614c619b1e1 generalized types of Infinitesimal, HFinite, and HInfinite to work over nonstandard extensions of any real normed vector space
huffman
parents: 20485
diff changeset
  1219
       ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> abs (x + -t) < r"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1220
apply (frule lemma_st_part_lub, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1221
apply (frule isLubD1a)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1222
apply (blast dest: lemma_st_part_major2)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1223
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1224
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1225
lemma st_part_Ex:
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1226
     "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1227
apply (simp add: approx_def Infinitesimal_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1228
apply (drule lemma_st_part_Ex, auto)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1229
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1230
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1231
text{*There is a unique real infinitely close*}
20552
2c31dd358c21 generalized types of many constants to work over arbitrary vector spaces;
huffman
parents: 20541
diff changeset
  1232
lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1233
apply (drule st_part_Ex, safe)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1234
apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1235
apply (auto intro!: approx_unique_real)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1236
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1237
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 14387
diff changeset
  1238
subsection{* Finite, Infinite and Infinitesimal*}
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1239
15229
1eb23f805c06 new simprules for abs and for things like a/b<1
paulson
parents: 15140
diff changeset
  1240
lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
14370
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1241
apply (simp add: HFinite_def HInfinite_def)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1242
apply (auto dest: order_less_trans)
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1243
done
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1244
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1245
lemma HFinite_not_HInfinite: 
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1246
  assumes x: "x \<in> HFinite" shows "x \<notin> HInfinite"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1247
proof
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1248
  assume x': "x \<in> HInfinite"
b0064703967b simplifications in the hyperreals
paulson
parents: 12114
diff changeset
  1249
  with x have "x \<in> HFinite \<inter> HInfinite" by blast