src/HOL/Hyperreal/SEQ.ML
author paulson
Wed, 10 Jan 2001 17:21:31 +0100
changeset 10857 47b1f34ddd09
parent 10834 a7897aebbffc
child 10919 144ede948e58
permissions -rw-r--r--
revisions e.g. images, transitive closure...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : SEQ.ML
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Description : Theory of sequence and series of real numbers
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
*) 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
(*---------------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
   Example of an hypersequence (i.e. an extended standard sequence) 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
   whose term with an hypernatural suffix is an infinitesimal i.e. 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
   the whn'nth term of the hypersequence is a member of Infinitesimal 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
 -------------------------------------------------------------------------- *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
Goalw [hypnat_omega_def] 
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
    14
      "(*fNat* (%n::nat. inverse(real_of_nat(Suc n)))) whn : Infinitesimal";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    16
      simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    17
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    18
by (auto_tac (claset(),
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
    19
              simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2,
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
    20
                            FreeUltrafilterNat_inverse_real_of_posnat]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
qed "SEQ_Infinitesimal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    23
(*--------------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
                  Rules for LIMSEQ and NSLIMSEQ etc.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
 --------------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
(*** LIMSEQ ***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
      "X ----> L ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
\      ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    31
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    32
qed "LIMSEQD1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    33
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    34
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
      "[| X ----> L; #0 < r|] ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
\      EX no. ALL n. no <= n --> abs(X n + -L) < r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    37
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    38
qed "LIMSEQD2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    39
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    40
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    41
      "ALL r. #0 < r --> (EX no. ALL n. \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    42
\      no <= n --> abs(X n + -L) < r) ==> X ----> L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    43
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    44
qed "LIMSEQI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    47
      "(X ----> L) = \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    48
\      (ALL r. #0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    49
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    50
qed "LIMSEQ_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    51
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    52
(*** NSLIMSEQ ***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    53
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    54
     "X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    55
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    56
qed "NSLIMSEQD1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    57
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    58
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    59
    "[| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    60
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    61
qed "NSLIMSEQD2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    62
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    63
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    64
     "ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    65
by (Asm_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    66
qed "NSLIMSEQI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    67
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    68
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    69
    "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    70
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    71
qed "NSLIMSEQ_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    72
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    73
(*----------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    74
          LIMSEQ ==> NSLIMSEQ
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    75
 ---------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    76
Goalw [LIMSEQ_def,NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    77
      "X ----> L ==> X ----NS> L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    78
by (auto_tac (claset(),simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    79
    [HNatInfinite_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    80
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    81
by (rtac (inf_close_minus_iff RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    82
by (auto_tac (claset(),simpset() addsimps [starfunNat,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    83
    mem_infmal_iff RS sym,hypreal_of_real_def,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    84
    hypreal_minus,hypreal_add,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    85
    Infinitesimal_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    86
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    87
by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    88
by (dres_inst_tac [("x","no")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    89
by (Fuf_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    90
by (blast_tac (claset() addDs [less_imp_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    91
qed "LIMSEQ_NSLIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    92
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    93
(*-------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    94
          NSLIMSEQ ==> LIMSEQ
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    95
    proving NS def ==> Standard def is trickier as usual 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    96
 -------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    97
(* the following sequence f(n) defines a hypernatural *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    98
(* lemmas etc. first *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    99
Goal "!!(f::nat=>nat). ALL n. n <= f n \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   100
\          ==> {n. f n = 0} = {0} | {n. f n = 0} = {}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   101
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   102
by (dres_inst_tac [("x","xa")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   103
by (dres_inst_tac [("x","x")] spec 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   104
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   105
val lemma_NSLIMSEQ1 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   106
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   107
Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   108
by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   109
val lemma_NSLIMSEQ2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   110
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   111
Goal "!!(f::nat=>nat). ALL n. n <= f n \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   112
\          ==> {n. f n = Suc u} <= {n. n <= Suc u}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   113
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   114
by (dres_inst_tac [("x","x")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   115
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   116
val lemma_NSLIMSEQ3 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   117
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   118
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   119
\         ==> finite {n. f n <= u}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   120
by (induct_tac "u" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   121
by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   122
by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   123
    finite_nat_le_segment], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   124
by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   125
by (ALLGOALS(Asm_simp_tac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   126
qed "NSLIMSEQ_finite_set";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   127
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   128
Goal "- {n. u < (f::nat=>nat) n} = {n. f n <= u}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   129
by (auto_tac (claset() addDs [less_le_trans],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   130
    simpset() addsimps [le_def]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   131
qed "Compl_less_set";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   132
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   133
(* the index set is in the free ultrafilter *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   134
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   135
\         ==> {n. u < f n} : FreeUltrafilterNat";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   136
by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   137
by (rtac FreeUltrafilterNat_finite 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   138
by (auto_tac (claset() addDs [NSLIMSEQ_finite_set],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   139
    simpset() addsimps [Compl_less_set]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   140
qed "FreeUltrafilterNat_NSLIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   141
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   142
(* thus, the sequence defines an infinite hypernatural! *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   143
Goal "ALL n. n <= f n \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   144
\         ==> Abs_hypnat (hypnatrel `` {f}) : HNatInfinite";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   145
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   146
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   147
by (etac FreeUltrafilterNat_NSLIMSEQ 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   148
qed "HNatInfinite_NSLIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   149
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   150
val lemmaLIM = CLAIM  "{n. X (f n) + - L = Y n} Int {n. abs (Y n) < r} <= \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   151
\         {n. abs (X (f n) + - L) < r}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   152
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   153
Goal "{n. abs (X (f n) + - L) < r} Int {n. r <= abs (X (f n) + - (L::real))} \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   154
\     = {}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   155
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   156
val lemmaLIM2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   157
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   158
Goal "[| #0 < r; ALL n. r <= abs (X (f n) + - L); \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   159
\          (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   160
\          - hypreal_of_real  L @= 0 |] ==> False";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   161
by (auto_tac (claset(),simpset() addsimps [starfunNat,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   162
    mem_infmal_iff RS sym,hypreal_of_real_def,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   163
    hypreal_minus,hypreal_add,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   164
    Infinitesimal_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   165
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   166
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   167
by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   168
by (dtac FreeUltrafilterNat_all 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   169
by (thin_tac "{n. abs (Y n) < r} : FreeUltrafilterNat" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   170
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   171
by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   172
                                  FreeUltrafilterNat_empty]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   173
val lemmaLIM3 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   174
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   175
Goalw [LIMSEQ_def,NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   176
      "X ----NS> L ==> X ----> L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   177
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   178
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   179
(* skolemization step *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   180
by (dtac choice 1 THEN Step_tac 1);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   181
by (dres_inst_tac [("x","Abs_hypnat(hypnatrel``{f})")] bspec 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   182
by (dtac (inf_close_minus_iff RS iffD1) 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   183
by (fold_tac [real_le_def]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   184
by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   185
by (blast_tac (claset() addIs [rename_numerals lemmaLIM3]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   186
qed "NSLIMSEQ_LIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   187
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   188
(* Now the all important result is trivially proved! *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   189
Goal "(f ----> L) = (f ----NS> L)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   190
by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   191
qed "LIMSEQ_NSLIMSEQ_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   192
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   193
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   194
                   Theorems about sequences
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   195
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   196
Goalw [NSLIMSEQ_def] "(%n. k) ----NS> k";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   197
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   198
qed "NSLIMSEQ_const";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   199
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   200
Goalw [LIMSEQ_def] "(%n. k) ----> k";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   201
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   202
qed "LIMSEQ_const";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   203
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   204
Goalw [NSLIMSEQ_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   205
      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n + Y n) ----NS> a + b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   206
by (auto_tac (claset() addIs [inf_close_add],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   207
    simpset() addsimps [starfunNat_add RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   208
qed "NSLIMSEQ_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   209
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   210
Goal "[| X ----> a; Y ----> b |] ==> (%n. X n + Y n) ----> a + b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   211
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   212
                                           NSLIMSEQ_add]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   213
qed "LIMSEQ_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   214
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   215
Goalw [NSLIMSEQ_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   216
      "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   217
by (auto_tac (claset() addSIs [inf_close_mult_HFinite],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   218
    simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   219
qed "NSLIMSEQ_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   220
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   221
Goal "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   222
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   223
                                           NSLIMSEQ_mult]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   224
qed "LIMSEQ_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   225
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   226
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   227
     "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   228
by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   229
qed "NSLIMSEQ_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   230
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   231
Goal "X ----> a ==> (%n. -(X n)) ----> -a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   232
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   233
                                           NSLIMSEQ_minus]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   234
qed "LIMSEQ_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   235
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   236
Goal "(%n. -(X n)) ----> -a ==> X ----> a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   237
by (dtac LIMSEQ_minus 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   238
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   239
qed "LIMSEQ_minus_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   240
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   241
Goal "(%n. -(X n)) ----NS> -a ==> X ----NS> a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   242
by (dtac NSLIMSEQ_minus 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   243
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   244
qed "NSLIMSEQ_minus_cancel";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   245
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   246
Goal "[| X ----NS> a; Y ----NS> b |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   247
\               ==> (%n. X n + -Y n) ----NS> a + -b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   248
by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   249
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   250
qed "NSLIMSEQ_add_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   251
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   252
Goal "[| X ----> a; Y ----> b |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   253
\               ==> (%n. X n + -Y n) ----> a + -b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   254
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   255
    NSLIMSEQ_add_minus]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   256
qed "LIMSEQ_add_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   257
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   258
Goalw [real_diff_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   259
     "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   260
by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   261
qed "LIMSEQ_diff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   262
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   263
Goalw [real_diff_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   264
     "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   265
by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   266
qed "NSLIMSEQ_diff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   267
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   268
(*---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   269
    Proof is like that of NSLIM_inverse.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   270
 --------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   271
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   272
     "[| X ----NS> a;  a ~= #0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   273
by (Clarify_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   274
by (dtac bspec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   275
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   276
              simpset() addsimps [starfunNat_inverse RS sym, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   277
                                  hypreal_of_real_inf_close_inverse]));  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   278
qed "NSLIMSEQ_inverse";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   279
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   280
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   281
(*------ Standard version of theorem -------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   282
Goal "[| X ----> a; a ~= #0 |] ==> (%n. inverse(X n)) ----> inverse(a)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   283
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   284
    LIMSEQ_NSLIMSEQ_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   285
qed "LIMSEQ_inverse";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   286
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   287
Goal "[| X ----NS> a;  Y ----NS> b;  b ~= #0 |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   288
\     ==> (%n. X n / Y n) ----NS> a/b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   289
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   290
                                           real_divide_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   291
qed "NSLIMSEQ_mult_inverse";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   292
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   293
Goal "[| X ----> a;  Y ----> b;  b ~= #0 |] ==> (%n. X n / Y n) ----> a/b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   294
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   295
                                           real_divide_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   296
qed "LIMSEQ_divide";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   297
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   298
(*-----------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   299
            Uniqueness of limit
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   300
 ----------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   301
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   302
     "[| X ----NS> a; X ----NS> b |] ==> a = b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   303
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   304
by (auto_tac (claset() addDs [inf_close_trans3], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   305
qed "NSLIMSEQ_unique";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   306
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   307
Goal "[| X ----> a; X ----> b |] ==> a = b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   308
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   309
    NSLIMSEQ_unique]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   310
qed "LIMSEQ_unique";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   311
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   312
(*-----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   313
    theorems about nslim and lim
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   314
 ----------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   315
Goalw [lim_def] "X ----> L ==> lim X = L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   316
by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   317
qed "limI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   318
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   319
Goalw [nslim_def] "X ----NS> L ==> nslim X = L";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   320
by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   321
qed "nslimI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   322
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   323
Goalw [lim_def,nslim_def] "lim X = nslim X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   324
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   325
qed "lim_nslim_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   326
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   327
(*------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   328
                      Convergence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   329
 -----------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   330
Goalw [convergent_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   331
     "convergent X ==> EX L. (X ----> L)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   332
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   333
qed "convergentD";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   334
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   335
Goalw [convergent_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   336
     "(X ----> L) ==> convergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   337
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   338
qed "convergentI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   339
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   340
Goalw [NSconvergent_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   341
     "NSconvergent X ==> EX L. (X ----NS> L)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   342
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   343
qed "NSconvergentD";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   344
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   345
Goalw [NSconvergent_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   346
     "(X ----NS> L) ==> NSconvergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   347
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   348
qed "NSconvergentI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   349
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   350
Goalw [convergent_def,NSconvergent_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   351
     "convergent X = NSconvergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   352
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   353
qed "convergent_NSconvergent_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   354
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   355
Goalw [NSconvergent_def,nslim_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   356
     "NSconvergent X = (X ----NS> nslim X)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   357
by (auto_tac (claset() addIs [someI], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   358
qed "NSconvergent_NSLIMSEQ_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   359
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   360
Goalw [convergent_def,lim_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   361
     "convergent X = (X ----> lim X)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   362
by (auto_tac (claset() addIs [someI], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   363
qed "convergent_LIMSEQ_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   364
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   365
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   366
         Subsequence (alternative definition) (e.g. Hoskins)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   367
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   368
Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   369
by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   370
by (nat_ind_tac "k" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   371
by (auto_tac (claset() addIs [less_trans], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   372
qed "subseq_Suc_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   373
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   374
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   375
                   Monotonicity
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   376
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   377
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   378
Goalw [monoseq_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   379
   "monoseq X = ((ALL n. X n <= X (Suc n)) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   380
\                | (ALL n. X (Suc n) <= X n))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   381
by (auto_tac (claset () addSDs [le_imp_less_or_eq], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   382
by (auto_tac (claset() addSIs [lessI RS less_imp_le]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   383
                       addSDs [less_imp_Suc_add], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   384
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   385
by (induct_tac "ka" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   386
by (auto_tac (claset() addIs [order_trans], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   387
by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   388
by (induct_tac "k" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   389
by (auto_tac (claset() addIs [order_trans], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   390
qed "monoseq_Suc";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   391
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   392
Goalw [monoseq_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   393
       "ALL m n. m <= n --> X m <= X n ==> monoseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   394
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   395
qed "monoI1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   396
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   397
Goalw [monoseq_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   398
       "ALL m n. m <= n --> X n <= X m ==> monoseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   399
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   400
qed "monoI2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   401
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   402
Goal "ALL n. X n <= X (Suc n) ==> monoseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   403
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   404
qed "mono_SucI1";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   405
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   406
Goal "ALL n. X (Suc n) <= X n ==> monoseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   407
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   408
qed "mono_SucI2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   409
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   410
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   411
                  Bounded Sequence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   412
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   413
Goalw [Bseq_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   414
      "Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   415
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   416
qed "BseqD";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   417
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   418
Goalw [Bseq_def]
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   419
      "[| #0 < K; ALL n. abs(X n) <= K |] ==> Bseq X";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   420
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   421
qed "BseqI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   422
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   423
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   424
\     (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   425
by Auto_tac;
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   426
by (cut_inst_tac [("x","K")] reals_Archimedean2 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   427
by (Clarify_tac 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   428
by (res_inst_tac [("x","n")] exI 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   429
by (Clarify_tac 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   430
by (dres_inst_tac [("x","na")] spec 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   431
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   432
qed "lemma_NBseq_def";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   433
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   434
(* alternative definition for Bseq *)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   435
Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   436
by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   437
qed "Bseq_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   438
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   439
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   440
\     (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   441
by (stac lemma_NBseq_def 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   442
by Auto_tac;
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   443
by (res_inst_tac [("x","Suc N")] exI 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   444
by (res_inst_tac [("x","N")] exI 2); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   445
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   446
by (blast_tac (claset() addIs [order_less_imp_le]) 2);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   447
by (dres_inst_tac [("x","n")] spec 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   448
by (Asm_simp_tac 1); 
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   449
qed "lemma_NBseq_def2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   450
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   451
(* yet another definition for Bseq *)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   452
Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real_of_nat(Suc N))";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   453
by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   454
qed "Bseq_iff1a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   455
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   456
Goalw [NSBseq_def]
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   457
     "[| NSBseq X;  N: HNatInfinite |] ==> (*fNat* X) N : HFinite";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   458
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   459
qed "NSBseqD";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   460
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   461
Goalw [NSBseq_def]
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   462
     "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   463
by (assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   464
qed "NSBseqI";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   465
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   466
(*-----------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   467
       Standard definition ==> NS definition
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   468
 ----------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   469
(* a few lemmas *)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   470
Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   471
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   472
val lemma_Bseq = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   473
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   474
Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   475
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   476
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   477
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   478
              simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff,
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   479
                                  HNatInfinite_FreeUltrafilterNat_iff]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   480
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   481
by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   482
by (res_inst_tac [("x","K+#1")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   483
by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   484
by (Ultra_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   485
qed "Bseq_NSBseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   486
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   487
(*---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   488
       NS  definition ==> Standard definition
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   489
 ---------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   490
(* similar to NSLIM proof in REALTOPOS *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   491
(*------------------------------------------------------------------- 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   492
   We need to get rid of the real variable and do so by proving the
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   493
   following which relies on the Archimedean property of the reals
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   494
   When we skolemize we then get the required function f::nat=>nat 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   495
   o/w we would be stuck with a skolem function f :: real=>nat which
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   496
   is not what we want (read useless!)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   497
 -------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   498
 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   499
Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   500
\          ==> ALL N. EX n. real_of_nat(Suc N) < abs (X n)";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   501
by (Step_tac 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   502
by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   503
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   504
val lemmaNSBseq = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   505
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   506
Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   507
\         ==> EX f. ALL N. real_of_nat(Suc N) < abs (X (f N))";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   508
by (dtac lemmaNSBseq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   509
by (dtac choice 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   510
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   511
val lemmaNSBseq2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   512
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   513
Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   514
\         ==>  Abs_hypreal(hyprel``{X o f}) : HInfinite";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   515
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   516
              simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   517
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   518
by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   519
by (dtac FreeUltrafilterNat_all 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   520
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   521
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   522
qed "real_seq_to_hypreal_HInfinite";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   523
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   524
(*-----------------------------------------------------------------------------
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   525
     Now prove that we can get out an infinite hypernatural as well 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   526
     defined using the skolem function f::nat=>nat above
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   527
 ----------------------------------------------------------------------------*)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   528
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   529
Goal "{n. f n <= Suc u & real_of_nat(Suc n) < abs (X (f n))} <= \
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   530
\         {n. f n <= u & real_of_nat(Suc n) < abs (X (f n))} \
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   531
\         Un {n. real_of_nat(Suc n) < abs (X (Suc u))}";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   532
by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset()));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   533
val lemma_finite_NSBseq = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   534
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   535
Goal "finite {n. f n <= (u::nat) &  real_of_nat(Suc n) < abs(X(f n))}";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   536
by (induct_tac "u" 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   537
by (res_inst_tac [("B","{n. real_of_nat(Suc n) < abs(X 0)}")] finite_subset 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   538
by (Force_tac 1); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   539
by (rtac (lemma_finite_NSBseq RS finite_subset) 2);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   540
by (auto_tac (claset() addIs [finite_real_of_nat_less_real], 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   541
              simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   542
val lemma_finite_NSBseq2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   543
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   544
Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   545
\     ==> Abs_hypnat(hypnatrel``{f}) : HNatInfinite";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   546
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   547
              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   548
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   549
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   550
by (asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   551
   [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   552
\   = {n. f n <= u}" [le_def]]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   553
by (dtac FreeUltrafilterNat_all 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   554
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   555
by (auto_tac (claset(), 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   556
     simpset() addsimps 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   557
    [CLAIM "({n. f n <= u} Int {n. real_of_nat(Suc n) < abs(X(f n))}) = \
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   558
\          {n. f n <= (u::nat) &  real_of_nat(Suc n) < abs(X(f n))}",
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   559
     lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   560
qed "HNatInfinite_skolem_f";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   561
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   562
Goalw [Bseq_def,NSBseq_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   563
      "NSBseq X ==> Bseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   564
by (rtac ccontr 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   565
by (auto_tac (claset(), simpset() addsimps [real_le_def]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   566
by (dtac lemmaNSBseq2 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   567
by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   568
by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   569
by (auto_tac (claset(), 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   570
              simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   571
qed "NSBseq_Bseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   572
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   573
(*----------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   574
  Equivalence of nonstandard and standard definitions 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   575
  for a bounded sequence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   576
 -----------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   577
Goal "(Bseq X) = (NSBseq X)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   578
by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   579
qed "Bseq_NSBseq_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   580
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   581
(*----------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   582
   A convergent sequence is bounded
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   583
   (Boundedness as a necessary condition for convergence)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   584
 -----------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   585
(* easier --- nonstandard version - no existential as usual *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   586
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   587
          "NSconvergent X ==> NSBseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   588
by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   589
               (inf_close_sym RSN (2,inf_close_HFinite))]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   590
qed "NSconvergent_NSBseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   591
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   592
(* standard version - easily now proved using *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   593
(* equivalence of NS and standard definitions *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   594
Goal "convergent X ==> Bseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   595
by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   596
    convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   597
qed "convergent_Bseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   598
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   599
(*----------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   600
             Results about Ubs and Lubs of bounded sequences
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   601
 -----------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   602
Goalw [Bseq_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   603
  "!!(X::nat=>real). Bseq X ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   604
\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   605
by (auto_tac (claset() addIs [isUbI,setleI],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   606
    simpset() addsimps [abs_le_interval_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   607
qed "Bseq_isUb";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   608
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   609
(*----------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   610
   Use completeness of reals (supremum property) 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   611
   to show that any bounded sequence has a lub 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   612
-----------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   613
Goal
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   614
  "!!(X::nat=>real). Bseq X ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   615
\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   616
by (blast_tac (claset() addIs [reals_complete,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   617
    Bseq_isUb]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   618
qed "Bseq_isLub";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   619
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   620
(* nonstandard version of premise will be *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   621
(* handy when we work in NS universe      *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   622
Goal   "NSBseq X ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   623
\  EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   624
by (asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   625
    [Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   626
qed "NSBseq_isUb";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   627
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   628
Goal
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   629
  "NSBseq X ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   630
\  EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   631
by (asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   632
    [Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   633
qed "NSBseq_isLub";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   634
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   635
(*--------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   636
             Bounded and monotonic sequence converges              
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   637
 --------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   638
(* lemmas *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   639
Goal 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   640
     "!!(X::nat=>real). [| ALL m n. m <= n -->  X m <= X n; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   641
\                 isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   642
\              |] ==> ALL n. ma <= n --> X n = X ma";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   643
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   644
by (dres_inst_tac [("y","X n")] isLubD2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   645
by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym])));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   646
val lemma_converg1 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   647
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   648
(*------------------------------------------------------------------- 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   649
   The best of both world: Easier to prove this result as a standard
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   650
   theorem and then use equivalence to "transfer" it into the
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   651
   equivalent nonstandard form if needed!
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   652
 -------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   653
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   654
         "ALL n. m <= n --> X n = X m \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   655
\         ==> EX L. (X ----> L)";  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   656
by (res_inst_tac [("x","X m")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   657
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   658
by (res_inst_tac [("x","m")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   659
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   660
by (dtac spec 1 THEN etac impE 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   661
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   662
qed "Bmonoseq_LIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   663
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   664
(* Now same theorem in terms of NS limit *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   665
Goal "ALL n. m <= n --> X n = X m \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   666
\         ==> EX L. (X ----NS> L)";  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   667
by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   668
    simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   669
qed "Bmonoseq_NSLIMSEQ";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   670
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   671
(* a few more lemmas *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   672
Goal "!!(X::nat=>real). \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   673
\ [| ALL m. X m ~= U;  isLub UNIV {x. EX n. X n = x} U |] ==> ALL m. X m < U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   674
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   675
by (dres_inst_tac [("y","X m")] isLubD2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   676
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   677
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   678
val lemma_converg2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   679
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   680
Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   681
\         isUb UNIV {x. EX n. X n = x} U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   682
by (rtac (setleI RS isUbI) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   683
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   684
val lemma_converg3 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   685
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   686
(* FIXME: U - T < U redundant *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   687
Goal "!!(X::nat=> real). \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   688
\              [| ALL m. X m ~= U; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   689
\                 isLub UNIV {x. EX n. X n = x} U; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   690
\                 #0 < T; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   691
\                 U + - T < U \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   692
\              |] ==> EX m. U + -T < X m & X m < U";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   693
by (dtac lemma_converg2 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   694
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   695
by (fold_tac [real_le_def]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   696
by (dtac lemma_converg3 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   697
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   698
by (auto_tac (claset() addDs [order_less_le_trans],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   699
              simpset() addsimps [real_minus_zero_le_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   700
val lemma_converg4 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   701
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   702
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   703
  A standard proof of the theorem for monotone increasing sequence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   704
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   705
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   706
Goalw [convergent_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   707
     "[| Bseq X; ALL m n. m <= n --> X m <= X n |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   708
\                ==> convergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   709
by (forward_tac [Bseq_isLub] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   710
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   711
by (case_tac "EX m. X m = U" 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   712
by (blast_tac (claset() addDs [lemma_converg1,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   713
    Bmonoseq_LIMSEQ]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   714
(* second case *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   715
by (res_inst_tac [("x","U")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   716
by (rtac LIMSEQI 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   717
by (forward_tac [lemma_converg2] 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   718
by (dtac lemma_converg4 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   719
by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   720
by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   721
by (rotate_tac 3 1 THEN dres_inst_tac [("x","n")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   722
by (arith_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   723
qed "Bseq_mono_convergent";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   724
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   725
(* NS version of theorem *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   726
Goalw [convergent_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   727
     "[| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   728
\                ==> NSconvergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   729
by (auto_tac (claset() addIs [Bseq_mono_convergent], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   730
    simpset() addsimps [convergent_NSconvergent_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   731
    Bseq_NSBseq_iff RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   732
qed "NSBseq_mono_NSconvergent";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   733
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   734
Goalw [convergent_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   735
      "(convergent X) = (convergent (%n. -(X n)))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   736
by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   737
by (dtac LIMSEQ_minus 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   738
qed "convergent_minus_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   739
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   740
Goalw [Bseq_def] "Bseq (%n. -(X n)) = Bseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   741
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   742
qed "Bseq_minus_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   743
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   744
(*--------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   745
   **** main mono theorem ****
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   746
 -------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   747
Goalw [monoseq_def] "[| Bseq X; monoseq X |] ==> convergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   748
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   749
by (rtac (convergent_minus_iff RS ssubst) 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   750
by (dtac (Bseq_minus_iff RS ssubst) 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   751
by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   752
qed "Bseq_monoseq_convergent";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   753
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   754
(*----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   755
          A few more equivalence theorems for boundedness 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   756
 ---------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   757
 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   758
(***--- alternative formulation for boundedness---***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   759
Goalw [Bseq_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   760
   "Bseq X = (EX k x. #0 < k & (ALL n. abs(X(n) + -x) <= k))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   761
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   762
by (res_inst_tac [("x","k + abs(x)")] exI 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   763
by (res_inst_tac [("x","K")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   764
by (res_inst_tac [("x","0")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   765
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   766
by (ALLGOALS (dres_inst_tac [("x","n")] spec));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   767
by (ALLGOALS arith_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   768
qed "Bseq_iff2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   769
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   770
(***--- alternative formulation for boundedness ---***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   771
Goal "Bseq X = (EX k N. #0 < k & (ALL n. abs(X(n) + -X(N)) <= k))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   772
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   773
by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   774
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   775
by (res_inst_tac [("x","K + abs(X N)")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   776
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   777
by (arith_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   778
by (res_inst_tac [("x","N")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   779
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   780
by (dres_inst_tac [("x","n")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   781
by (arith_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   782
by (auto_tac (claset(), simpset() addsimps [Bseq_iff2]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   783
qed "Bseq_iff3";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   784
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   785
Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   786
by (res_inst_tac [("x","(abs(k) + abs(K)) + #1")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   787
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   788
by (dres_inst_tac [("x","n")] spec 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   789
by (ALLGOALS arith_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   790
qed "BseqI2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   791
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   792
(*-------------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   793
   Equivalence between NS and standard definitions of Cauchy seqs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   794
 ------------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   795
(*-------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   796
      Standard def => NS def
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   797
 -------------------------------*)
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   798
Goal "Abs_hypnat (hypnatrel `` {x}) : HNatInfinite \
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   799
\         ==> {n. M <= x n} : FreeUltrafilterNat";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   800
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   801
              simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   802
by (dres_inst_tac [("x","M")] spec 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   803
by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   804
val lemmaCauchy1 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   805
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   806
Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   807
\     {n. M <= xa n} Int {n. M <= x n} <= \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   808
\     {n. abs (X (xa n) + - X (x n)) < u}";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   809
by (Blast_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   810
val lemmaCauchy2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   811
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   812
Goalw [Cauchy_def,NSCauchy_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   813
      "Cauchy X ==> NSCauchy X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   814
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   815
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   816
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   817
by (rtac (inf_close_minus_iff RS iffD2) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   818
by (rtac (mem_infmal_iff RS iffD1) 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   819
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   820
              simpset() addsimps [starfunNat, hypreal_minus,hypreal_add,
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   821
                                  Infinitesimal_FreeUltrafilterNat_iff]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   822
by (EVERY[rtac bexI 1, Auto_tac]);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   823
by (dtac spec 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   824
by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   825
by (dres_inst_tac [("M","M")] lemmaCauchy1 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   826
by (res_inst_tac [("x1","xa")] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   827
    (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   828
by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   829
by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   830
        FreeUltrafilterNat_Nat_set], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   831
qed "Cauchy_NSCauchy";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   832
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   833
(*-----------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   834
     NS def => Standard def -- rather long but 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   835
     straightforward proof in this case
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   836
 ---------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   837
Goalw [Cauchy_def,NSCauchy_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   838
      "NSCauchy X ==> Cauchy X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   839
by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   840
by (dtac choice 1 THEN 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   841
    auto_tac (claset(), simpset() addsimps [all_conj_distrib]));
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   842
by (dtac choice 1 THEN 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   843
    step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   844
by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   845
by (dtac bspec 1 THEN assume_tac 1);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   846
by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {fa})")] bspec 1 
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   847
    THEN auto_tac (claset(), simpset() addsimps [starfunNat]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   848
by (dtac (inf_close_minus_iff RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   849
by (dtac (mem_infmal_iff RS iffD2) 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   850
by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   851
    hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   852
by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   853
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   854
by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   855
\         {n. abs (Y n) < e} <= \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   856
\         {n. abs (X (f n) + - X (fa n)) < e}" RSN 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   857
          (2,FreeUltrafilterNat_subset)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   858
by (thin_tac "{n. abs (Y n) < e} : FreeUltrafilterNat" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   859
by (dtac FreeUltrafilterNat_all 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   860
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   861
by (asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   862
    [CLAIM "{n. abs (X (f n) + - X (fa n)) < e} Int \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   863
\         {M. ~ abs (X (f M) + - X (fa M)) < e} = {}",
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   864
     FreeUltrafilterNat_empty]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   865
qed "NSCauchy_Cauchy";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   866
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   867
(*----- Equivalence -----*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   868
Goal "NSCauchy X = Cauchy X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   869
by (blast_tac (claset() addSIs[NSCauchy_Cauchy,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   870
    Cauchy_NSCauchy]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   871
qed "NSCauchy_Cauchy_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   872
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   873
(*-------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   874
  Cauchy sequence is bounded -- this is the standard 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   875
  proof mechanization rather than the nonstandard proof 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   876
 -------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   877
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   878
(***-------------  VARIOUS LEMMAS --------------***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   879
Goal "ALL n. M <= n --> abs (X M + - X n) < (#1::real) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   880
\         ==>  ALL n. M <= n --> abs(X n) < #1 + abs(X M)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   881
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   882
by (dtac spec 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   883
by (arith_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   884
val lemmaCauchy = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   885
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   886
Goal "(n < Suc M) = (n <= M)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   887
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   888
qed "less_Suc_cancel_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   889
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   890
(* FIXME: Long. Maximal element in subsequence *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   891
Goal "EX m. m <= M & (ALL n. n <= M --> \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   892
\         abs ((X::nat=> real) n) <= abs (X m))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   893
by (induct_tac "M" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   894
by (res_inst_tac [("x","0")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   895
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   896
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   897
by (cut_inst_tac [("R1.0","abs (X (Suc n))"),("R2.0","abs(X m)")]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   898
        real_linear 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   899
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   900
by (res_inst_tac [("x","m")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   901
by (res_inst_tac [("x","m")] exI 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   902
by (res_inst_tac [("x","Suc n")] exI 3);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   903
by (ALLGOALS(Asm_full_simp_tac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   904
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   905
by (ALLGOALS(eres_inst_tac [("m1","na")] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   906
    (le_imp_less_or_eq RS disjE)));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   907
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   908
    [less_Suc_cancel_iff, order_less_imp_le])));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   909
by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   910
qed "SUP_rabs_subseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   911
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   912
(* lemmas to help proof - mostly trivial *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   913
Goal "[| ALL m::nat. m <= M --> P M m; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   914
\        ALL m. M <= m --> P M m |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   915
\     ==> ALL m. P M m";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   916
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   917
by (REPEAT(dres_inst_tac [("x","m")] spec 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   918
by (auto_tac (claset() addEs [less_asym],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   919
    simpset() addsimps [le_def]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   920
val lemma_Nat_covered = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   921
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   922
Goal "[| ALL n. n <= M --> abs ((X::nat=>real) n) <= a;  a < b |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   923
\     ==> ALL n. n <= M --> abs(X n) <= b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   924
by (blast_tac (claset() addIs [order_le_less_trans RS order_less_imp_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   925
val lemma_trans1 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   926
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   927
Goal "[| ALL n. M <= n --> abs ((X::nat=>real) n) < a; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   928
\        a < b |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   929
\     ==> ALL n. M <= n --> abs(X n)<= b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   930
by (blast_tac (claset() addIs [order_less_trans RS order_less_imp_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   931
val lemma_trans2 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   932
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   933
Goal "[| ALL n. n <= M --> abs (X n) <= a; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   934
\        a = b |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   935
\     ==> ALL n. n <= M --> abs(X n) <= b";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   936
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   937
val lemma_trans3 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   938
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   939
Goal "ALL n. M <= n --> abs ((X::nat=>real) n) < a \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   940
\             ==>  ALL n. M <= n --> abs (X n) <= a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   941
by (blast_tac (claset() addIs [order_less_imp_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   942
val lemma_trans4 = result();
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   943
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   944
(*---------------------------------------------------------- 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   945
   Trickier than expected --- proof is more involved than
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   946
   outlines sketched by various authors would suggest
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   947
 ---------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   948
Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   949
by (dres_inst_tac [("x","#1")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   950
by (etac (rename_numerals real_zero_less_one RSN (2,impE)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   951
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   952
by (dres_inst_tac [("x","M")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   953
by (Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   954
by (dtac lemmaCauchy 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   955
by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   956
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   957
by (cut_inst_tac [("R1.0","abs(X m)"),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   958
     ("R2.0","#1 + abs(X M)")] real_linear 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   959
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   960
by (dtac lemma_trans1 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   961
by (dtac lemma_trans2 3 THEN assume_tac 3);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   962
by (dtac lemma_trans3 2 THEN assume_tac 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   963
by (dtac (abs_add_one_gt_zero RS order_less_trans) 3);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   964
by (dtac lemma_trans4 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   965
by (dtac lemma_trans4 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   966
by (res_inst_tac [("x","#1 + abs(X M)")] exI 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   967
by (res_inst_tac [("x","#1 + abs(X M)")] exI 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   968
by (res_inst_tac [("x","abs(X m)")] exI 3);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   969
by (auto_tac (claset() addSEs [lemma_Nat_covered],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   970
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   971
by (ALLGOALS arith_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   972
qed "Cauchy_Bseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   973
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   974
(*------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   975
  Cauchy sequence is bounded -- NSformulation
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   976
 ------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   977
Goal "NSCauchy X ==> NSBseq X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   978
by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   979
    Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   980
qed "NSCauchy_NSBseq";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   981
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   982
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   983
(*-----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   984
          Equivalence of Cauchy criterion and convergence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   985
  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   986
  We will prove this using our NS formulation which provides a
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   987
  much easier proof than using the standard definition. We do not 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   988
  need to use properties of subsequences such as boundedness, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   989
  monotonicity etc... Compare with Harrison's corresponding proof
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   990
  in HOL which is much longer and more complicated. Of course, we do
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   991
  not have problems which he encountered with guessing the right 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   992
  instantiations for his 'espsilon-delta' proof(s) in this case
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   993
  since the NS formulations do not involve existential quantifiers.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   994
 -----------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   995
Goalw [NSconvergent_def,NSLIMSEQ_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   996
      "NSCauchy X = NSconvergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   997
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   998
by (forward_tac [NSCauchy_NSBseq] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   999
by (auto_tac (claset() addIs [inf_close_trans2], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1000
    simpset() addsimps 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1001
    [NSBseq_def,NSCauchy_def]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1002
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1003
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1004
by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1005
              addsimps [SReal_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1006
by (blast_tac (claset() addIs [inf_close_trans3]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1007
qed "NSCauchy_NSconvergent_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1008
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1009
(* Standard proof for free *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1010
Goal "Cauchy X = convergent X";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1011
by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1012
    convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1013
qed "Cauchy_convergent_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1014
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1015
(*-----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1016
     We can now try and derive a few properties of sequences
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1017
     starting with the limit comparison property for sequences
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1018
 -----------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1019
Goalw [NSLIMSEQ_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1020
       "[| f ----NS> l; g ----NS> m; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1021
\                  EX N. ALL n. N <= n --> f(n) <= g(n) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1022
\               |] ==> l <= m";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1023
by (Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1024
by (dtac starfun_le_mono 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1025
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1026
by (dres_inst_tac [("x","whn")] spec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1027
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1028
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1029
by (auto_tac (claset() addIs 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1030
    [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1031
qed "NSLIMSEQ_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1032
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1033
(* standard version *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1034
Goal "[| f ----> l; g ----> m; \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1035
\        EX N. ALL n. N <= n --> f(n) <= g(n) |] \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1036
\     ==> l <= m";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1037
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1038
    NSLIMSEQ_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1039
qed "LIMSEQ_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1040
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1041
(*---------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1042
    Also...
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1043
 --------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1044
Goal "[| X ----> r; ALL n. a <= X n |] ==> a <= r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1045
by (rtac LIMSEQ_le 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1046
by (rtac LIMSEQ_const 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1047
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1048
qed "LIMSEQ_le_const";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1049
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1050
Goal "[| X ----NS> r; ALL n. a <= X n |] ==> a <= r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1051
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1052
    LIMSEQ_le_const]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1053
qed "NSLIMSEQ_le_const";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1054
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1055
Goal "[| X ----> r; ALL n. X n <= a |] ==> r <= a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1056
by (rtac LIMSEQ_le 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1057
by (rtac LIMSEQ_const 2);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1058
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1059
qed "LIMSEQ_le_const2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1060
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1061
Goal "[| X ----NS> r; ALL n. X n <= a |] ==> r <= a";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1062
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1063
    LIMSEQ_le_const2]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1064
qed "NSLIMSEQ_le_const2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1065
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1066
(*-----------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1067
            Shift a convergent series by 1
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1068
  We use the fact that Cauchyness and convergence
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1069
  are equivalent and also that the successor of an
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1070
  infinite hypernatural is also infinite.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1071
 -----------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1072
Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1073
by (forward_tac [NSconvergentI RS 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1074
    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1075
by (auto_tac (claset(), 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1076
     simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1077
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1078
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1079
by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1080
by (blast_tac (claset() addIs [inf_close_trans3]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1081
qed "NSLIMSEQ_Suc";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1082
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1083
(* standard version *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1084
Goal "f ----> l ==> (%n. f(Suc n)) ----> l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1085
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1086
    NSLIMSEQ_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1087
qed "LIMSEQ_Suc";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1088
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1089
Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1090
by (forward_tac [NSconvergentI RS 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1091
    (NSCauchy_NSconvergent_iff RS iffD2)] 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1092
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1093
      simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1094
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1095
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1096
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1097
by (rotate_tac 2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1098
by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1099
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1100
qed "NSLIMSEQ_imp_Suc";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1101
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1102
Goal "(%n. f(Suc n)) ----> l ==> f ----> l";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1103
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1104
by (etac NSLIMSEQ_imp_Suc 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1105
qed "LIMSEQ_imp_Suc";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1106
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1107
Goal "((%n. f(Suc n)) ----> l) = (f ----> l)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1108
by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1109
qed "LIMSEQ_Suc_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1110
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1111
Goal "((%n. f(Suc n)) ----NS> l) = (f ----NS> l)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1112
by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1113
qed "NSLIMSEQ_Suc_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1114
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1115
(*-----------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1116
       A sequence tends to zero iff its abs does
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1117
 ----------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1118
(* we can prove this directly since proof is trivial *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1119
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1120
      "((%n. abs(f n)) ----> #0) = (f ----> #0)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1121
by (simp_tac (simpset() addsimps [abs_idempotent]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1122
qed "LIMSEQ_rabs_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1123
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1124
(*-----------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1125
(* We prove the NS version from the standard one       *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1126
(* Actually pure NS proof seems more complicated       *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1127
(* than the direct standard one above!                 *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1128
(*-----------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1129
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1130
Goal "((%n. abs(f n)) ----NS> #0) = (f ----NS> #0)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1131
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1132
             LIMSEQ_rabs_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1133
qed "NSLIMSEQ_rabs_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1134
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1135
(*----------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1136
    Also we have for a general limit 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1137
        (NS proof much easier)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1138
 ---------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1139
Goalw [NSLIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1140
       "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1141
by (auto_tac (claset() addIs [inf_close_hrabs], simpset() 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1142
    addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1143
qed "NSLIMSEQ_imp_rabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1144
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1145
(* standard version *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1146
Goal "f ----> l ==> (%n. abs(f n)) ----> abs(l)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1147
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1148
    NSLIMSEQ_imp_rabs]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1149
qed "LIMSEQ_imp_rabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1150
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1151
(*-----------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1152
       An unbounded sequence's inverse tends to 0
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1153
  ----------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1154
(* standard proof seems easier *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1155
Goalw [LIMSEQ_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1156
      "ALL y. EX N. ALL n. N <= n --> y < f(n) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1157
\      ==> (%n. inverse(f n)) ----> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1158
by (Step_tac 1 THEN Asm_full_simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1159
by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1160
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1161
by (dtac spec 1 THEN Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1162
by (forward_tac [real_inverse_gt_0] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1163
by (forward_tac [order_less_trans] 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1164
by (forw_inst_tac [("x","f n")] real_inverse_gt_0 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1165
by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1166
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1167
by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD2], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1168
              simpset() delsimps [real_inverse_inverse]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1169
qed "LIMSEQ_inverse_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1170
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1171
Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1172
\     ==> (%n. inverse(f n)) ----NS> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1173
by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1174
                  LIMSEQ_inverse_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1175
qed "NSLIMSEQ_inverse_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1176
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1177
(*--------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1178
             Sequence  1/n --> 0 as n --> infinity 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1179
 -------------------------------------------------------------*)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1180
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1181
Goal "(%n. inverse(real_of_nat(Suc n))) ----> #0";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1182
by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1183
by (cut_inst_tac [("x","y")] reals_Archimedean2 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1184
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1185
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc]));  
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1186
by (subgoal_tac "y < real_of_nat na" 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1187
by (Asm_simp_tac 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1188
by (blast_tac (claset() addIs [order_less_le_trans]) 1);  
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1189
qed "LIMSEQ_inverse_real_of_nat";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1190
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1191
Goal "(%n. inverse(real_of_nat(Suc n))) ----NS> #0";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1192
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1193
    LIMSEQ_inverse_real_of_nat]) 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1194
qed "NSLIMSEQ_inverse_real_of_nat";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1195
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1196
(*--------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1197
    Sequence  r + 1/n --> r as n --> infinity 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1198
    now easily proved
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1199
 --------------------------------------------*)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1200
Goal "(%n. r + inverse(real_of_nat(Suc n))) ----> r";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1201
by (cut_facts_tac
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1202
    [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1);
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1203
by Auto_tac;
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1204
qed "LIMSEQ_inverse_real_of_posnat_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1205
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1206
Goal "(%n. r + inverse(real_of_nat(Suc n))) ----NS> r";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1207
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1208
    LIMSEQ_inverse_real_of_posnat_add]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1209
qed "NSLIMSEQ_inverse_real_of_posnat_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1210
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1211
(*--------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1212
    Also...
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1213
 --------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1214
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1215
Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----> r";
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1216
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat]
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1217
                   MRS LIMSEQ_add_minus] 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1218
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1219
qed "LIMSEQ_inverse_real_of_posnat_add_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1220
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1221
Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----NS> r";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1222
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1223
    LIMSEQ_inverse_real_of_posnat_add_minus]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1224
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1225
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1226
Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----> r";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1227
by (cut_inst_tac [("b","#1")] ([LIMSEQ_const,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1228
    LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1229
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1230
qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1231
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1232
Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----NS> r";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1233
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1234
    LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1235
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1236
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1237
(*---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1238
                          Real Powers
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1239
 --------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1240
Goal "(X ----NS> a) --> ((%n. (X n) ^ m) ----NS> a ^ m)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1241
by (induct_tac "m" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1242
by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1243
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1244
qed_spec_mp "NSLIMSEQ_pow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1245
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1246
Goal "X ----> a ==> (%n. (X n) ^ m) ----> a ^ m";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1247
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1248
    NSLIMSEQ_pow]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1249
qed "LIMSEQ_pow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1250
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1251
(*----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1252
               0 <= x < #1 ==> (x ^ n ----> 0)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1253
  Proof will use (NS) Cauchy equivalence for convergence and
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1254
  also fact that bounded and monotonic sequence converges.  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1255
 ---------------------------------------------------------------*)
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
  1256
Goalw [Bseq_def] "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1257
by (res_inst_tac [("x","#1")] exI 1);
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
  1258
by (auto_tac (claset() addDs [conjI RS realpow_le] 
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1259
                       addIs [order_less_imp_le], 
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
  1260
              simpset() addsimps [abs_eqI1, realpow_abs RS sym] ));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1261
qed "Bseq_realpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1262
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1263
Goal "[| #0 <= x; x < #1 |] ==> monoseq (%n. x ^ n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1264
by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1265
qed "monoseq_realpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1266
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1267
Goal "[| #0 <= x; x < #1 |] ==> convergent (%n. x ^ n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1268
by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1269
                                Bseq_realpow,monoseq_realpow]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1270
qed "convergent_realpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1271
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1272
(* We now use NS criterion to bring proof of theorem through *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1273
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1274
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1275
Goalw [NSLIMSEQ_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1276
     "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----NS> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1277
by (auto_tac (claset() addSDs [convergent_realpow],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1278
              simpset() addsimps [convergent_NSconvergent_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1279
by (forward_tac [NSconvergentD] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1280
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1281
        simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1282
                            NSCauchy_def, starfunNat_pow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1283
by (forward_tac [HNatInfinite_add_one] 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1284
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1285
by (dtac bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1286
by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1287
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1288
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1289
by (dtac inf_close_trans3 1 THEN assume_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1290
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1291
              simpset() delsimps [hypreal_of_real_mult]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1292
			addsimps [hypreal_of_real_mult RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1293
qed "NSLIMSEQ_realpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1294
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1295
(*---------------  standard version ---------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1296
Goal "[| #0 <= x; x < #1 |] ==> (%n. x ^ n) ----> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1297
by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1298
                                      LIMSEQ_NSLIMSEQ_iff]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1299
qed "LIMSEQ_realpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1300
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1301
Goal "#1 < x ==> (%n. a / (x ^ n)) ----> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1302
by (cut_inst_tac [("a","a"),("x1","inverse x")] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1303
    ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1304
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1305
              simpset() addsimps [real_divide_def, realpow_inverse])); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1306
by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1307
                                      pos_real_divide_less_eq]) 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1308
qed "LIMSEQ_divide_realpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1309
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1310
(*----------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1311
               Limit of c^n for |c| < 1  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1312
 ---------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1313
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) ----> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1314
by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1315
qed "LIMSEQ_rabs_realpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1316
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1317
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) ----NS> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1318
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1319
    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1320
qed "NSLIMSEQ_rabs_realpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1321
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1322
Goal "abs(c) < #1 ==> (%n. c ^ n) ----> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1323
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1324
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1325
              simpset() addsimps [realpow_abs RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1326
qed "LIMSEQ_rabs_realpow_zero2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1327
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1328
Goal "abs(c) < #1 ==> (%n. c ^ n) ----NS> #0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1329
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1330
    LIMSEQ_NSLIMSEQ_iff RS sym]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1331
qed "NSLIMSEQ_rabs_realpow_zero2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1332
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1333
(***---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1334
                 Hyperreals and Sequences
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1335
 ---------------------------------------------------------------***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1336
(*** A bounded sequence is a finite hyperreal ***)
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
  1337
Goal "NSBseq X ==> Abs_hypreal(hyprel``{X}) : HFinite";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1338
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1339
       [FreeUltrafilterNat_all RS FreeUltrafilterNat_subset],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1340
       simpset() addsimps [HFinite_FreeUltrafilterNat_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1341
        Bseq_NSBseq_iff RS sym, Bseq_iff1a]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1342
qed "NSBseq_HFinite_hypreal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1343
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1344
(*** A sequence converging to zero defines an infinitesimal ***)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1345
Goalw [NSLIMSEQ_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
  1346
      "X ----NS> #0 ==> Abs_hypreal(hyprel``{X}) : Infinitesimal";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1347
by (dres_inst_tac [("x","whn")] bspec 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1348
by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1349
by (auto_tac (claset(),
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1350
              simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym,
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1351
                                  starfunNat,hypreal_of_real_zero]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1352
qed "NSLIMSEQ_zero_Infinitesimal_hypreal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1353
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1354
(***---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1355
    Theorems proved by Harrison in HOL that we do not need 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1356
    in order to prove equivalence between Cauchy criterion 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1357
    and convergence:
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1358
 -- Show that every sequence contains a monotonic subsequence   
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1359
Goal "EX f. subseq f & monoseq (%n. s (f n))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1360
 -- Show that a subsequence of a bounded sequence is bounded
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1361
Goal "Bseq X ==> Bseq (%n. X (f n))";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1362
 -- Show we can take subsequential terms arbitrarily far 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1363
    up a sequence       
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1364
Goal "subseq f ==> n <= f(n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1365
Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
  1366
 ---------------------------------------------------------------***)
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1367
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
  1368