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