author | huffman |
Thu, 12 Apr 2007 03:37:30 +0200 | |
changeset 22641 | a5dc96fad632 |
child 23010 | e6b5459f9028 |
permissions | -rw-r--r-- |
22641
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
1 |
(* Title : HLim.thy |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
2 |
ID : $Id$ |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
3 |
Author : Jacques D. Fleuriot |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
4 |
Copyright : 1998 University of Cambridge |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
6 |
*) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
7 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
8 |
header{* Limits and Continuity (Nonstandard) *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
9 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
10 |
theory HLim |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
11 |
imports HSEQ Lim |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
12 |
begin |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
13 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
14 |
text{*Nonstandard Definitions*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
15 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
16 |
definition |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
17 |
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
18 |
("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
19 |
"f -- a --NS> L = |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
20 |
(\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
21 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
22 |
definition |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
23 |
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
24 |
--{*NS definition dispenses with limit notions*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
25 |
"isNSCont f a = (\<forall>y. y @= star_of a --> |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
26 |
( *f* f) y @= star_of (f a))" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
27 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
28 |
definition |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
29 |
isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
30 |
"isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
31 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
32 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
33 |
subsection {* Limits of Functions *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
34 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
35 |
lemma NSLIM_I: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
36 |
"(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
37 |
\<Longrightarrow> f -- a --NS> L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
38 |
by (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
39 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
40 |
lemma NSLIM_D: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
41 |
"\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
42 |
\<Longrightarrow> starfun f x \<approx> star_of L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
43 |
by (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
44 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
45 |
text{*Proving properties of limits using nonstandard definition. |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
46 |
The properties hold for standard limits as well!*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
47 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
48 |
lemma NSLIM_mult: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
49 |
fixes l m :: "'a::real_normed_algebra" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
50 |
shows "[| f -- x --NS> l; g -- x --NS> m |] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
51 |
==> (%x. f(x) * g(x)) -- x --NS> (l * m)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
52 |
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
53 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
54 |
lemma starfun_scaleR [simp]: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
55 |
"starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
56 |
by transfer (rule refl) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
57 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
58 |
lemma NSLIM_scaleR: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
59 |
"[| f -- x --NS> l; g -- x --NS> m |] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
60 |
==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
61 |
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
62 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
63 |
lemma NSLIM_add: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
64 |
"[| f -- x --NS> l; g -- x --NS> m |] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
65 |
==> (%x. f(x) + g(x)) -- x --NS> (l + m)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
66 |
by (auto simp add: NSLIM_def intro!: approx_add) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
67 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
68 |
lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
69 |
by (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
70 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
71 |
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
72 |
by (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
73 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
74 |
lemma NSLIM_diff: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
75 |
"\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
76 |
by (simp only: diff_def NSLIM_add NSLIM_minus) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
77 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
78 |
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
79 |
by (simp only: NSLIM_add NSLIM_minus) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
80 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
81 |
lemma NSLIM_inverse: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
82 |
fixes L :: "'a::real_normed_div_algebra" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
83 |
shows "[| f -- a --NS> L; L \<noteq> 0 |] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
84 |
==> (%x. inverse(f(x))) -- a --NS> (inverse L)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
85 |
apply (simp add: NSLIM_def, clarify) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
86 |
apply (drule spec) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
87 |
apply (auto simp add: star_of_approx_inverse) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
88 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
89 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
90 |
lemma NSLIM_zero: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
91 |
assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
92 |
proof - |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
93 |
have "(\<lambda>x. f x - l) -- a --NS> l - l" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
94 |
by (rule NSLIM_diff [OF f NSLIM_const]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
95 |
thus ?thesis by simp |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
96 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
97 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
98 |
lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
99 |
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
100 |
apply (auto simp add: diff_minus add_assoc) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
101 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
102 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
103 |
lemma NSLIM_const_not_eq: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
104 |
fixes a :: real (*TODO: generalize to real_normed_div_algebra*) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
105 |
shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
106 |
apply (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
107 |
apply (rule_tac x="star_of a + epsilon" in exI) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
108 |
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
109 |
simp add: hypreal_epsilon_not_zero) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
110 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
111 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
112 |
lemma NSLIM_not_zero: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
113 |
fixes a :: real |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
114 |
shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
115 |
by (rule NSLIM_const_not_eq) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
116 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
117 |
lemma NSLIM_const_eq: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
118 |
fixes a :: real |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
119 |
shows "(%x. k) -- a --NS> L ==> k = L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
120 |
apply (rule ccontr) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
121 |
apply (blast dest: NSLIM_const_not_eq) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
122 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
123 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
124 |
text{* can actually be proved more easily by unfolding the definition!*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
125 |
lemma NSLIM_unique: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
126 |
fixes a :: real |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
127 |
shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
128 |
apply (drule NSLIM_minus) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
129 |
apply (drule NSLIM_add, assumption) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
130 |
apply (auto dest!: NSLIM_const_eq [symmetric]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
131 |
apply (simp add: diff_def [symmetric]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
132 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
133 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
134 |
lemma NSLIM_mult_zero: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
135 |
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
136 |
shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
137 |
by (drule NSLIM_mult, auto) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
138 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
139 |
lemma NSLIM_self: "(%x. x) -- a --NS> a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
140 |
by (simp add: NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
141 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
142 |
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
143 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
144 |
lemma LIM_NSLIM: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
145 |
assumes f: "f -- a --> L" shows "f -- a --NS> L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
146 |
proof (rule NSLIM_I) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
147 |
fix x |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
148 |
assume neq: "x \<noteq> star_of a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
149 |
assume approx: "x \<approx> star_of a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
150 |
have "starfun f x - star_of L \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
151 |
proof (rule InfinitesimalI2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
152 |
fix r::real assume r: "0 < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
153 |
from LIM_D [OF f r] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
154 |
obtain s where s: "0 < s" and |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
155 |
less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
156 |
by fast |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
157 |
from less_r have less_r': |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
158 |
"\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk> |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
159 |
\<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
160 |
by transfer |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
161 |
from approx have "x - star_of a \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
162 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
163 |
hence "hnorm (x - star_of a) < star_of s" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
164 |
using s by (rule InfinitesimalD2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
165 |
with neq show "hnorm (starfun f x - star_of L) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
166 |
by (rule less_r') |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
167 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
168 |
thus "starfun f x \<approx> star_of L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
169 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
170 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
171 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
172 |
lemma NSLIM_LIM: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
173 |
assumes f: "f -- a --NS> L" shows "f -- a --> L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
174 |
proof (rule LIM_I) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
175 |
fix r::real assume r: "0 < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
176 |
have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
177 |
\<longrightarrow> hnorm (starfun f x - star_of L) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
178 |
proof (rule exI, safe) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
179 |
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
180 |
next |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
181 |
fix x assume neq: "x \<noteq> star_of a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
182 |
assume "hnorm (x - star_of a) < epsilon" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
183 |
with Infinitesimal_epsilon |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
184 |
have "x - star_of a \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
185 |
by (rule hnorm_less_Infinitesimal) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
186 |
hence "x \<approx> star_of a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
187 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
188 |
with f neq have "starfun f x \<approx> star_of L" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
189 |
by (rule NSLIM_D) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
190 |
hence "starfun f x - star_of L \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
191 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
192 |
thus "hnorm (starfun f x - star_of L) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
193 |
using r by (rule InfinitesimalD2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
194 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
195 |
thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
196 |
by transfer |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
197 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
198 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
199 |
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
200 |
by (blast intro: LIM_NSLIM NSLIM_LIM) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
201 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
202 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
203 |
subsection {* Continuity *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
204 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
205 |
lemma isNSContD: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
206 |
"\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
207 |
by (simp add: isNSCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
208 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
209 |
lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) " |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
210 |
by (simp add: isNSCont_def NSLIM_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
211 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
212 |
lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
213 |
apply (simp add: isNSCont_def NSLIM_def, auto) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
214 |
apply (case_tac "y = star_of a", auto) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
215 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
216 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
217 |
text{*NS continuity can be defined using NS Limit in |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
218 |
similar fashion to standard def of continuity*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
219 |
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
220 |
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
221 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
222 |
text{*Hence, NS continuity can be given |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
223 |
in terms of standard limit*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
224 |
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
225 |
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
226 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
227 |
text{*Moreover, it's trivial now that NS continuity |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
228 |
is equivalent to standard continuity*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
229 |
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
230 |
apply (simp add: isCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
231 |
apply (rule isNSCont_LIM_iff) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
232 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
233 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
234 |
text{*Standard continuity ==> NS continuity*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
235 |
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
236 |
by (erule isNSCont_isCont_iff [THEN iffD2]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
237 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
238 |
text{*NS continuity ==> Standard continuity*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
239 |
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
240 |
by (erule isNSCont_isCont_iff [THEN iffD1]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
241 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
242 |
text{*Alternative definition of continuity*} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
243 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
244 |
(* Prove equivalence between NS limits - *) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
245 |
(* seems easier than using standard def *) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
246 |
lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
247 |
apply (simp add: NSLIM_def, auto) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
248 |
apply (drule_tac x = "star_of a + x" in spec) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
249 |
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
250 |
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
251 |
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
252 |
prefer 2 apply (simp add: add_commute diff_def [symmetric]) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
253 |
apply (rule_tac x = x in star_cases) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
254 |
apply (rule_tac [2] x = x in star_cases) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
255 |
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
256 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
257 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
258 |
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
259 |
by (rule NSLIM_h_iff) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
260 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
261 |
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
262 |
by (simp add: isNSCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
263 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
264 |
lemma isNSCont_inverse: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
265 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
266 |
shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
267 |
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
268 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
269 |
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
270 |
by (simp add: isNSCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
271 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
272 |
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
273 |
apply (simp add: isNSCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
274 |
apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
275 |
done |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
276 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
277 |
(**************************************************************** |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
278 |
(%* Leave as commented until I add topology theory or remove? *%) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
279 |
(%*------------------------------------------------------------ |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
280 |
Elementary topology proof for a characterisation of |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
281 |
continuity now: a function f is continuous if and only |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
282 |
if the inverse image, {x. f(x) \<in> A}, of any open set A |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
283 |
is always an open set |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
284 |
------------------------------------------------------------*%) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
285 |
Goal "[| isNSopen A; \<forall>x. isNSCont f x |] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
286 |
==> isNSopen {x. f x \<in> A}" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
287 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
288 |
by (dtac (mem_monad_approx RS approx_sym); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
289 |
by (dres_inst_tac [("x","a")] spec 1); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
290 |
by (dtac isNSContD 1 THEN assume_tac 1) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
291 |
by (dtac bspec 1 THEN assume_tac 1) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
292 |
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
293 |
by (blast_tac (claset() addIs [starfun_mem_starset]); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
294 |
qed "isNSCont_isNSopen"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
295 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
296 |
Goalw [isNSCont_def] |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
297 |
"\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \ |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
298 |
\ ==> isNSCont f x"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
299 |
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
300 |
(approx_minus_iff RS iffD2)],simpset() addsimps |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
301 |
[Infinitesimal_def,SReal_iff])); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
302 |
by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
303 |
by (etac (isNSopen_open_interval RSN (2,impE)); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
304 |
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
305 |
by (dres_inst_tac [("x","x")] spec 1); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
306 |
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
307 |
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
308 |
qed "isNSopen_isNSCont"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
309 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
310 |
Goal "(\<forall>x. isNSCont f x) = \ |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
311 |
\ (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
312 |
by (blast_tac (claset() addIs [isNSCont_isNSopen, |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
313 |
isNSopen_isNSCont]); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
314 |
qed "isNSCont_isNSopen_iff"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
315 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
316 |
(%*------- Standard version of same theorem --------*%) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
317 |
Goal "(\<forall>x. isCont f x) = \ |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
318 |
\ (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
319 |
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
320 |
simpset() addsimps [isNSopen_isopen_iff RS sym, |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
321 |
isNSCont_isCont_iff RS sym])); |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
322 |
qed "isCont_isopen_iff"; |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
323 |
*******************************************************************) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
324 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
325 |
subsection {* Uniform Continuity *} |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
326 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
327 |
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
328 |
by (simp add: isNSUCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
329 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
330 |
lemma isUCont_isNSUCont: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
331 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
332 |
assumes f: "isUCont f" shows "isNSUCont f" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
333 |
proof (unfold isNSUCont_def, safe) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
334 |
fix x y :: "'a star" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
335 |
assume approx: "x \<approx> y" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
336 |
have "starfun f x - starfun f y \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
337 |
proof (rule InfinitesimalI2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
338 |
fix r::real assume r: "0 < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
339 |
with f obtain s where s: "0 < s" and |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
340 |
less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
341 |
by (auto simp add: isUCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
342 |
from less_r have less_r': |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
343 |
"\<And>x y. hnorm (x - y) < star_of s |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
344 |
\<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
345 |
by transfer |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
346 |
from approx have "x - y \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
347 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
348 |
hence "hnorm (x - y) < star_of s" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
349 |
using s by (rule InfinitesimalD2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
350 |
thus "hnorm (starfun f x - starfun f y) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
351 |
by (rule less_r') |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
352 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
353 |
thus "starfun f x \<approx> starfun f y" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
354 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
355 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
356 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
357 |
lemma isNSUCont_isUCont: |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
358 |
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
359 |
assumes f: "isNSUCont f" shows "isUCont f" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
360 |
proof (unfold isUCont_def, safe) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
361 |
fix r::real assume r: "0 < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
362 |
have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
363 |
\<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
364 |
proof (rule exI, safe) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
365 |
show "0 < epsilon" by (rule hypreal_epsilon_gt_zero) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
366 |
next |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
367 |
fix x y :: "'a star" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
368 |
assume "hnorm (x - y) < epsilon" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
369 |
with Infinitesimal_epsilon |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
370 |
have "x - y \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
371 |
by (rule hnorm_less_Infinitesimal) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
372 |
hence "x \<approx> y" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
373 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
374 |
with f have "starfun f x \<approx> starfun f y" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
375 |
by (simp add: isNSUCont_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
376 |
hence "starfun f x - starfun f y \<in> Infinitesimal" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
377 |
by (unfold approx_def) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
378 |
thus "hnorm (starfun f x - starfun f y) < star_of r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
379 |
using r by (rule InfinitesimalD2) |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
380 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
381 |
thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r" |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
382 |
by transfer |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
383 |
qed |
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
384 |
|
a5dc96fad632
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
huffman
parents:
diff
changeset
|
385 |
end |