src/HOL/Nonstandard_Analysis/HLim.thy
author wenzelm
Wed, 26 Oct 2016 15:14:17 +0200
changeset 64406 492de9062cd2
parent 63579 73939a9b70a3
child 64435 c93b0e6131c3
permissions -rw-r--r--
more specific hardware information: relevant for ultimate Mac OS X version;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62479
716336f19aa9 clarified session;
wenzelm
parents: 61982
diff changeset
     1
(*  Title:      HOL/Nonstandard_Analysis/HLim.thy
41589
bbd861837ebc tuned headers;
wenzelm
parents: 37887
diff changeset
     2
    Author:     Jacques D. Fleuriot, University of Cambridge
bbd861837ebc tuned headers;
wenzelm
parents: 37887
diff changeset
     3
    Author:     Lawrence C Paulson
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     4
*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     5
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
     6
section\<open>Limits and Continuity (Nonstandard)\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     7
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     8
theory HLim
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63040
diff changeset
     9
  imports Star
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63040
diff changeset
    10
  abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    11
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    12
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
    13
text\<open>Nonstandard Definitions\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    14
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    15
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    16
  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    17
            ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    18
  "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
61982
3af5a06577c7 more symbols;
wenzelm
parents: 61981
diff changeset
    19
    (\<forall>x. (x \<noteq> star_of a & x \<approx> star_of a --> ( *f* f) x \<approx> star_of L))"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    20
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    21
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    22
  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
    23
    \<comment>\<open>NS definition dispenses with limit notions\<close>
61982
3af5a06577c7 more symbols;
wenzelm
parents: 61981
diff changeset
    24
  "isNSCont f a = (\<forall>y. y \<approx> star_of a -->
3af5a06577c7 more symbols;
wenzelm
parents: 61981
diff changeset
    25
         ( *f* f) y \<approx> star_of (f a))"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    26
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    27
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    28
  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
61982
3af5a06577c7 more symbols;
wenzelm
parents: 61981
diff changeset
    29
  "isNSUCont f = (\<forall>x y. x \<approx> y --> ( *f* f) x \<approx> ( *f* f) y)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    30
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    31
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
    32
subsection \<open>Limits of Functions\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    33
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    34
lemma NSLIM_I:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    35
  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    36
   \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    37
by (simp add: NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    38
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    39
lemma NSLIM_D:
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    40
  "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    41
   \<Longrightarrow> starfun f x \<approx> star_of L"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    42
by (simp add: NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    43
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
    44
text\<open>Proving properties of limits using nonstandard definition.
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
    45
      The properties hold for standard limits as well!\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    46
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    47
lemma NSLIM_mult:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    48
  fixes l m :: "'a::real_normed_algebra"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    49
  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    50
      ==> (%x. f(x) * g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    51
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    52
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    53
lemma starfun_scaleR [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    54
  "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    55
by transfer (rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    56
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    57
lemma NSLIM_scaleR:
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    58
  "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    59
      ==> (%x. f(x) *\<^sub>R g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    60
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    61
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    62
lemma NSLIM_add:
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    63
     "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    64
      ==> (%x. f(x) + g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    65
by (auto simp add: NSLIM_def intro!: approx_add)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    66
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    67
lemma NSLIM_const [simp]: "(%x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    68
by (simp add: NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    69
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    70
lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. -f(x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    71
by (simp add: NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    72
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    73
lemma NSLIM_diff:
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    74
  "\<lbrakk>f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 51525
diff changeset
    75
  by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    76
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    77
lemma NSLIM_add_minus: "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] ==> (%x. f(x) + -g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    78
by (simp only: NSLIM_add NSLIM_minus)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    79
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    80
lemma NSLIM_inverse:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    81
  fixes L :: "'a::real_normed_div_algebra"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    82
  shows "[| f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L;  L \<noteq> 0 |]
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    83
      ==> (%x. inverse(f(x))) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    84
apply (simp add: NSLIM_def, clarify)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    85
apply (drule spec)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    86
apply (auto simp add: star_of_approx_inverse)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    87
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    88
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    89
lemma NSLIM_zero:
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    90
  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" shows "(%x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    91
proof -
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    92
  have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    93
    by (rule NSLIM_diff [OF f NSLIM_const])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    94
  thus ?thesis by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    95
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    96
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
    97
lemma NSLIM_zero_cancel: "(%x. f(x) - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 ==> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    98
apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54230
diff changeset
    99
apply (auto simp add: add.assoc)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   100
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   101
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   102
lemma NSLIM_const_not_eq:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   103
  fixes a :: "'a::real_normed_algebra_1"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   104
  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   105
apply (simp add: NSLIM_def)
61981
1b5845c62fa0 more symbols;
wenzelm
parents: 61976
diff changeset
   106
apply (rule_tac x="star_of a + of_hypreal \<epsilon>" in exI)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   107
apply (simp add: hypreal_epsilon_not_zero approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   108
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   109
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   110
lemma NSLIM_not_zero:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   111
  fixes a :: "'a::real_normed_algebra_1"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   112
  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   113
by (rule NSLIM_const_not_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   114
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   115
lemma NSLIM_const_eq:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   116
  fixes a :: "'a::real_normed_algebra_1"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   117
  shows "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   118
apply (rule ccontr)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   119
apply (blast dest: NSLIM_const_not_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   120
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   121
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   122
lemma NSLIM_unique:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   123
  fixes a :: "'a::real_normed_algebra_1"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   124
  shows "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M\<rbrakk> \<Longrightarrow> L = M"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   125
apply (drule (1) NSLIM_diff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   126
apply (auto dest!: NSLIM_const_eq)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   127
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   128
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   129
lemma NSLIM_mult_zero:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   130
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   131
  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 |] ==> (%x. f(x)*g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   132
by (drule NSLIM_mult, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   133
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   134
lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   135
by (simp add: NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   136
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   137
subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   138
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   139
lemma LIM_NSLIM:
61976
3a27957ac658 more symbols;
wenzelm
parents: 61975
diff changeset
   140
  assumes f: "f \<midarrow>a\<rightarrow> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   141
proof (rule NSLIM_I)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   142
  fix x
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   143
  assume neq: "x \<noteq> star_of a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   144
  assume approx: "x \<approx> star_of a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   145
  have "starfun f x - star_of L \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   146
  proof (rule InfinitesimalI2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   147
    fix r::real assume r: "0 < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   148
    from LIM_D [OF f r]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   149
    obtain s where s: "0 < s" and
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   150
      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   151
      by fast
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   152
    from less_r have less_r':
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   153
       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   154
        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   155
      by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   156
    from approx have "x - star_of a \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   157
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   158
    hence "hnorm (x - star_of a) < star_of s"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   159
      using s by (rule InfinitesimalD2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   160
    with neq show "hnorm (starfun f x - star_of L) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   161
      by (rule less_r')
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   162
  qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   163
  thus "starfun f x \<approx> star_of L"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   164
    by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   165
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   166
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   167
lemma NSLIM_LIM:
61976
3a27957ac658 more symbols;
wenzelm
parents: 61975
diff changeset
   168
  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f \<midarrow>a\<rightarrow> L"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   169
proof (rule LIM_I)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   170
  fix r::real assume r: "0 < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   171
  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   172
        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   173
  proof (rule exI, safe)
61981
1b5845c62fa0 more symbols;
wenzelm
parents: 61976
diff changeset
   174
    show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   175
  next
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   176
    fix x assume neq: "x \<noteq> star_of a"
61981
1b5845c62fa0 more symbols;
wenzelm
parents: 61976
diff changeset
   177
    assume "hnorm (x - star_of a) < \<epsilon>"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   178
    with Infinitesimal_epsilon
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   179
    have "x - star_of a \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   180
      by (rule hnorm_less_Infinitesimal)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   181
    hence "x \<approx> star_of a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   182
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   183
    with f neq have "starfun f x \<approx> star_of L"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   184
      by (rule NSLIM_D)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   185
    hence "starfun f x - star_of L \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   186
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   187
    thus "hnorm (starfun f x - star_of L) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   188
      using r by (rule InfinitesimalD2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   189
  qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   190
  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   191
    by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   192
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   193
61976
3a27957ac658 more symbols;
wenzelm
parents: 61975
diff changeset
   194
theorem LIM_NSLIM_iff: "(f \<midarrow>x\<rightarrow> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   195
by (blast intro: LIM_NSLIM NSLIM_LIM)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   196
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   197
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   198
subsection \<open>Continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   199
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   200
lemma isNSContD:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   201
  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   202
by (simp add: isNSCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   203
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   204
lemma isNSCont_NSLIM: "isNSCont f a ==> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) "
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   205
by (simp add: isNSCont_def NSLIM_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   206
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   207
lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) ==> isNSCont f a"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   208
apply (simp add: isNSCont_def NSLIM_def, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   209
apply (case_tac "y = star_of a", auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   210
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   211
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   212
text\<open>NS continuity can be defined using NS Limit in
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62479
diff changeset
   213
    similar fashion to standard definition of continuity\<close>
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   214
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   215
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   216
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   217
text\<open>Hence, NS continuity can be given
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   218
  in terms of standard limit\<close>
61976
3a27957ac658 more symbols;
wenzelm
parents: 61975
diff changeset
   219
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   220
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   221
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   222
text\<open>Moreover, it's trivial now that NS continuity
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   223
  is equivalent to standard continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   224
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   225
apply (simp add: isCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   226
apply (rule isNSCont_LIM_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   227
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   228
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   229
text\<open>Standard continuity ==> NS continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   230
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   231
by (erule isNSCont_isCont_iff [THEN iffD2])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   232
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   233
text\<open>NS continuity ==> Standard continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   234
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   235
by (erule isNSCont_isCont_iff [THEN iffD1])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   236
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   237
text\<open>Alternative definition of continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   238
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   239
(* Prove equivalence between NS limits - *)
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62479
diff changeset
   240
(* seems easier than using standard definition  *)
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   241
lemma NSLIM_h_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L)"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   242
apply (simp add: NSLIM_def, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   243
apply (drule_tac x = "star_of a + x" in spec)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   244
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   245
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   246
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54230
diff changeset
   247
 prefer 2 apply (simp add: add.commute)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   248
apply (rule_tac x = x in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   249
apply (rule_tac [2] x = x in star_cases)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 54230
diff changeset
   250
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   251
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   252
61971
720fa884656e more symbols;
wenzelm
parents: 58878
diff changeset
   253
lemma NSLIM_isCont_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
54230
b1d955791529 more simplification rules on unary and binary minus
haftmann
parents: 51525
diff changeset
   254
  by (fact NSLIM_h_iff)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   255
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   256
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   257
by (simp add: isNSCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   258
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   259
lemma isNSCont_inverse:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   260
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   261
  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   262
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   263
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   264
lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   265
by (simp add: isNSCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   266
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   267
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   268
apply (simp add: isNSCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   269
apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   270
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   271
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   272
61975
b4b11391c676 isabelle update_cartouches -c -t;
wenzelm
parents: 61971
diff changeset
   273
subsection \<open>Uniform Continuity\<close>
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   274
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   275
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   276
by (simp add: isNSUCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   277
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   278
lemma isUCont_isNSUCont:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   279
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   280
  assumes f: "isUCont f" shows "isNSUCont f"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   281
proof (unfold isNSUCont_def, safe)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   282
  fix x y :: "'a star"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   283
  assume approx: "x \<approx> y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   284
  have "starfun f x - starfun f y \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   285
  proof (rule InfinitesimalI2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   286
    fix r::real assume r: "0 < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   287
    with f obtain s where s: "0 < s" and
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   288
      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 28562
diff changeset
   289
      by (auto simp add: isUCont_def dist_norm)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   290
    from less_r have less_r':
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   291
       "\<And>x y. hnorm (x - y) < star_of s
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   292
        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   293
      by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   294
    from approx have "x - y \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   295
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   296
    hence "hnorm (x - y) < star_of s"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   297
      using s by (rule InfinitesimalD2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   298
    thus "hnorm (starfun f x - starfun f y) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   299
      by (rule less_r')
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   300
  qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   301
  thus "starfun f x \<approx> starfun f y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   302
    by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   303
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   304
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   305
lemma isNSUCont_isUCont:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   306
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   307
  assumes f: "isNSUCont f" shows "isUCont f"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 28562
diff changeset
   308
proof (unfold isUCont_def dist_norm, safe)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   309
  fix r::real assume r: "0 < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   310
  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   311
        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   312
  proof (rule exI, safe)
61981
1b5845c62fa0 more symbols;
wenzelm
parents: 61976
diff changeset
   313
    show "0 < \<epsilon>" by (rule hypreal_epsilon_gt_zero)
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   314
  next
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   315
    fix x y :: "'a star"
61981
1b5845c62fa0 more symbols;
wenzelm
parents: 61976
diff changeset
   316
    assume "hnorm (x - y) < \<epsilon>"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   317
    with Infinitesimal_epsilon
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   318
    have "x - y \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   319
      by (rule hnorm_less_Infinitesimal)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   320
    hence "x \<approx> y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   321
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   322
    with f have "starfun f x \<approx> starfun f y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   323
      by (simp add: isNSUCont_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   324
    hence "starfun f x - starfun f y \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   325
      by (unfold approx_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   326
    thus "hnorm (starfun f x - starfun f y) < star_of r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   327
      using r by (rule InfinitesimalD2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   328
  qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   329
  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   330
    by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   331
qed
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   332
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   333
end