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