src/HOL/NSA/Star.thy
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 39302 d7728f65b353
child 58878 f962e42e324d
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     1
(*  Title       : Star.thy
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     5
*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     6
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     7
header{*Star-Transforms in Non-Standard Analysis*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     8
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     9
theory Star
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    10
imports NSA
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    11
begin
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    12
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    13
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    14
    (* internal sets *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    15
  starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    16
  "*sn* As = Iset (star_n As)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    17
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    18
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    19
  InternalSets :: "'a star set set" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 28562
diff changeset
    20
  "InternalSets = {X. \<exists>As. X = *sn* As}"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    21
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    22
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    23
  (* nonstandard extension of function *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    24
  is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 28562
diff changeset
    25
  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    26
                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    27
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    28
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    29
  (* internal functions *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    30
  starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star"   ("*fn* _" [80] 80) where
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    31
  "*fn* F = Ifun (star_n F)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    32
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    33
definition
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    34
  InternalFuns :: "('a star => 'b star) set" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 28562
diff changeset
    35
  "InternalFuns = {X. \<exists>F. X = *fn* F}"
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    36
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    37
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    38
(*--------------------------------------------------------
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    39
   Preamble - Pulling "EX" over "ALL"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    40
 ---------------------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    41
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    42
(* This proof does not need AC and was suggested by the
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    43
   referee for the JCM Paper: let f(x) be least y such
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    44
   that  Q(x,y)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    45
*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    46
lemma no_choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>(f :: 'a => nat). \<forall>x. Q x (f x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    47
apply (rule_tac x = "%x. LEAST y. Q x y" in exI)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    48
apply (blast intro: LeastI)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    49
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    50
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    51
subsection{*Properties of the Star-transform Applied to Sets of Reals*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    52
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    53
lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    54
by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    55
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    56
lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    57
by (auto simp add: SReal_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    58
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    59
lemma STAR_star_of_Int: "*s* X Int Standard = star_of ` X"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    60
by (auto simp add: Standard_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    61
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    62
lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> \<forall>y \<in> A. x \<noteq> hypreal_of_real y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    63
by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    64
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    65
lemma lemma_not_starA: "x \<notin> star_of ` A ==> \<forall>y \<in> A. x \<noteq> star_of y"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    66
by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    67
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    68
lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    69
by auto
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    70
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    71
lemma STAR_real_seq_to_hypreal:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    72
    "\<forall>n. (X n) \<notin> M ==> star_n X \<notin> *s* M"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    73
apply (unfold starset_def star_of_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    74
apply (simp add: Iset_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    75
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    76
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    77
lemma STAR_singleton: "*s* {x} = {star_of x}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    78
by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    79
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    80
lemma STAR_not_mem: "x \<notin> F ==> star_of x \<notin> *s* F"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    81
by transfer
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    82
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    83
lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    84
by (erule rev_subsetD, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    85
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    86
text{*Nonstandard extension of a set (defined using a constant
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    87
   sequence) as a special case of an internal set*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    88
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    89
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    90
apply (drule fun_eq_iff [THEN iffD2])
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    91
apply (simp add: starset_n_def starset_def star_of_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    92
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    93
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    94
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    95
(*----------------------------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    96
(* Theorems about nonstandard extensions of functions             *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    97
(*----------------------------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    98
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    99
(*----------------------------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   100
(* Nonstandard extension of a function (defined using a           *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   101
(* constant sequence) as a special case of an internal function   *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   102
(*----------------------------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   103
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   104
lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   105
apply (drule fun_eq_iff [THEN iffD2])
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   106
apply (simp add: starfun_n_def starfun_def star_of_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   107
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   108
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   109
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   110
(*
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   111
   Prove that abs for hypreal is a nonstandard extension of abs for real w/o
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   112
   use of congruence property (proved after this for general
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   113
   nonstandard extensions of real valued functions). 
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   114
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   115
   Proof now Uses the ultrafilter tactic!
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   116
*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   117
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   118
lemma hrabs_is_starext_rabs: "is_starext abs abs"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   119
apply (simp add: is_starext_def, safe)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   120
apply (rule_tac x=x in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   121
apply (rule_tac x=y in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   122
apply (unfold star_n_def, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   123
apply (rule bexI, rule_tac [2] lemma_starrel_refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   124
apply (rule bexI, rule_tac [2] lemma_starrel_refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   125
apply (fold star_n_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   126
apply (unfold star_abs_def starfun_def star_of_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   127
apply (simp add: Ifun_star_n star_n_eq_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   128
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   129
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   130
text{*Nonstandard extension of functions*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   131
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   132
lemma starfun:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   133
      "( *f* f) (star_n X) = star_n (%n. f (X n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   134
by (rule starfun_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   135
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   136
lemma starfun_if_eq:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   137
     "!!w. w \<noteq> star_of x
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   138
       ==> ( *f* (\<lambda>z. if z = x then a else g z)) w = ( *f* g) w"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   139
by (transfer, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   140
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   141
(*-------------------------------------------
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   142
  multiplication: ( *f) x ( *g) = *(f x g)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   143
 ------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   144
lemma starfun_mult: "!!x. ( *f* f) x * ( *f* g) x = ( *f* (%x. f x * g x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   145
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   146
declare starfun_mult [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   147
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   148
(*---------------------------------------
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   149
  addition: ( *f) + ( *g) = *(f + g)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   150
 ---------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   151
lemma starfun_add: "!!x. ( *f* f) x + ( *f* g) x = ( *f* (%x. f x + g x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   152
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   153
declare starfun_add [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   154
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   155
(*--------------------------------------------
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   156
  subtraction: ( *f) + -( *g) = *(f + -g)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   157
 -------------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   158
lemma starfun_minus: "!!x. - ( *f* f) x = ( *f* (%x. - f x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   159
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   160
declare starfun_minus [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   161
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   162
(*FIXME: delete*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   163
lemma starfun_add_minus: "!!x. ( *f* f) x + -( *f* g) x = ( *f* (%x. f x + -g x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   164
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   165
declare starfun_add_minus [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   166
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   167
lemma starfun_diff: "!!x. ( *f* f) x  - ( *f* g) x = ( *f* (%x. f x - g x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   168
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   169
declare starfun_diff [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   170
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   171
(*--------------------------------------
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   172
  composition: ( *f) o ( *g) = *(f o g)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   173
 ---------------------------------------*)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   174
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   175
lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   176
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   177
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   178
lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   179
by (transfer o_def, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   180
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   181
text{*NS extension of constant function*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   182
lemma starfun_const_fun [simp]: "!!x. ( *f* (%x. k)) x = star_of k"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   183
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   184
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   185
text{*the NS extension of the identity function*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   186
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   187
lemma starfun_Id [simp]: "!!x. ( *f* (%x. x)) x = x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   188
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   189
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   190
(* this is trivial, given starfun_Id *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   191
lemma starfun_Idfun_approx:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   192
  "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   193
by (simp only: starfun_Id)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   194
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   195
text{*The Star-function is a (nonstandard) extension of the function*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   196
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   197
lemma is_starext_starfun: "is_starext ( *f* f) f"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   198
apply (simp add: is_starext_def, auto)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   199
apply (rule_tac x = x in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   200
apply (rule_tac x = y in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   201
apply (auto intro!: bexI [OF _ Rep_star_star_n]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   202
            simp add: starfun star_n_eq_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   203
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   204
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   205
text{*Any nonstandard extension is in fact the Star-function*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   206
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   207
lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   208
apply (simp add: is_starext_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   209
apply (rule ext)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   210
apply (rule_tac x = x in star_cases)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   211
apply (drule_tac x = x in spec)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   212
apply (drule_tac x = "( *f* f) x" in spec)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   213
apply (auto simp add: starfun_star_n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   214
apply (simp add: star_n_eq_iff [symmetric])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   215
apply (simp add: starfun_star_n [of f, symmetric])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   216
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   217
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   218
lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   219
by (blast intro: is_starfun_starext is_starext_starfun)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   220
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   221
text{*extented function has same solution as its standard
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   222
   version for real arguments. i.e they are the same
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   223
   for all real arguments*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   224
lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   225
by (rule starfun_star_of)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   226
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   227
lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   228
by simp
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   229
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   230
(* useful for NS definition of derivatives *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   231
lemma starfun_lambda_cancel:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   232
  "!!x'. ( *f* (%h. f (x + h))) x'  = ( *f* f) (star_of x + x')"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   233
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   234
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   235
lemma starfun_lambda_cancel2:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   236
  "( *f* (%h. f(g(x + h)))) x' = ( *f* (f o g)) (star_of x + x')"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   237
by (unfold o_def, rule starfun_lambda_cancel)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   238
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   239
lemma starfun_mult_HFinite_approx:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   240
  fixes l m :: "'a::real_normed_algebra star"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   241
  shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   242
                  l: HFinite; m: HFinite
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   243
               |] ==>  ( *f* (%x. f x * g x)) x @= l * m"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   244
apply (drule (3) approx_mult_HFinite)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   245
apply (auto intro: approx_HFinite [OF _ approx_sym])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   246
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   247
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   248
lemma starfun_add_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   249
               |] ==>  ( *f* (%x. f x + g x)) x @= l + m"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   250
by (auto intro: approx_add)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   251
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   252
text{*Examples: hrabs is nonstandard extension of rabs
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   253
              inverse is nonstandard extension of inverse*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   254
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   255
(* can be proved easily using theorem "starfun" and *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   256
(* properties of ultrafilter as for inverse below we  *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   257
(* use the theorem we proved above instead          *)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   258
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   259
lemma starfun_rabs_hrabs: "*f* abs = abs"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   260
by (simp only: star_abs_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   261
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   262
lemma starfun_inverse_inverse [simp]: "( *f* inverse) x = inverse(x)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   263
by (simp only: star_inverse_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   264
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   265
lemma starfun_inverse: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   266
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   267
declare starfun_inverse [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   268
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   269
lemma starfun_divide: "!!x. ( *f* f) x / ( *f* g) x = ( *f* (%x. f x / g x)) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   270
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   271
declare starfun_divide [symmetric, simp]
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   272
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   273
lemma starfun_inverse2: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   274
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   275
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   276
text{*General lemma/theorem needed for proofs in elementary
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   277
    topology of the reals*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   278
lemma starfun_mem_starset:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   279
      "!!x. ( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   280
by (transfer, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   281
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   282
text{*Alternative definition for hrabs with rabs function
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   283
   applied entrywise to equivalence class representative.
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   284
   This is easily proved using starfun and ns extension thm*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   285
lemma hypreal_hrabs:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   286
     "abs (star_n X) = star_n (%n. abs (X n))"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   287
by (simp only: starfun_rabs_hrabs [symmetric] starfun)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   288
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   289
text{*nonstandard extension of set through nonstandard extension
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   290
   of rabs function i.e hrabs. A more general result should be
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   291
   where we replace rabs by some arbitrary function f and hrabs
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   292
   by its NS extenson. See second NS set extension below.*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   293
lemma STAR_rabs_add_minus:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   294
   "*s* {x. abs (x + - y) < r} =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   295
     {x. abs(x + -star_of y) < star_of r}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   296
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   297
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   298
lemma STAR_starfun_rabs_add_minus:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   299
  "*s* {x. abs (f x + - y) < r} =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   300
       {x. abs(( *f* f) x + -star_of y) < star_of r}"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   301
by (transfer, rule refl)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   302
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   303
text{*Another characterization of Infinitesimal and one of @= relation.
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   304
   In this theory since @{text hypreal_hrabs} proved here. Maybe
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   305
   move both theorems??*}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   306
lemma Infinitesimal_FreeUltrafilterNat_iff2:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   307
     "(star_n X \<in> Infinitesimal) =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   308
      (\<forall>m. {n. norm(X n) < inverse(real(Suc m))}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   309
                \<in>  FreeUltrafilterNat)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   310
by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   311
     hnorm_def star_of_nat_def starfun_star_n
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   312
     star_n_inverse star_n_less real_of_nat_def)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   313
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   314
lemma HNatInfinite_inverse_Infinitesimal [simp]:
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   315
     "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   316
apply (cases n)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   317
apply (auto simp add: of_hypnat_def starfun_star_n real_of_nat_def [symmetric] star_n_inverse real_norm_def
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   318
      HNatInfinite_FreeUltrafilterNat_iff
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   319
      Infinitesimal_FreeUltrafilterNat_iff2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   320
apply (drule_tac x="Suc m" in spec)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   321
apply (erule ultra, simp)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   322
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   323
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   324
lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   325
      (\<forall>r>0. {n. norm (X n - Y n) < r} : FreeUltrafilterNat)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   326
apply (subst approx_minus_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   327
apply (rule mem_infmal_iff [THEN subst])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   328
apply (simp add: star_n_diff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   329
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   330
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   331
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   332
lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   333
      (\<forall>m. {n. norm (X n - Y n) <
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   334
                  inverse(real(Suc m))} : FreeUltrafilterNat)"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   335
apply (subst approx_minus_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   336
apply (rule mem_infmal_iff [THEN subst])
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   337
apply (simp add: star_n_diff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   338
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff2)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   339
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   340
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   341
lemma inj_starfun: "inj starfun"
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   342
apply (rule inj_onI)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   343
apply (rule ext, rule ccontr)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   344
apply (drule_tac x = "star_n (%n. xa)" in fun_cong)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   345
apply (auto simp add: starfun star_n_eq_iff)
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   346
done
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   347
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
   348
end