src/HOL/Hyperreal/HTranscendental.thy
author paulson
Thu, 01 Jul 2004 12:29:53 +0200
changeset 15013 34264f5e4691
parent 14641 79b7bd936264
child 15077 89840837108e
permissions -rw-r--r--
new treatment of binary numerals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
     1
(*  Title       : HTranscendental.thy
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
     3
    Copyright   : 2001 University of Edinburgh
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
     4
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
     5
Converted to Isar and polished by lcp
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
     6
*)
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
     7
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
     8
header{*Nonstandard Extensions of Transcendental Functions*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
     9
14641
79b7bd936264 moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents: 14477
diff changeset
    10
theory HTranscendental = Transcendental + Integration:
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    11
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    12
text{*really belongs in Transcendental*}
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    13
lemma sqrt_divide_self_eq:
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    14
  assumes nneg: "0 \<le> x"
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    15
  shows "sqrt x / x = inverse (sqrt x)"
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    16
proof cases
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    17
  assume "x=0" thus ?thesis by simp
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    18
next
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    19
  assume nz: "x\<noteq>0" 
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    20
  hence pos: "0<x" using nneg by arith
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    21
  show ?thesis
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    22
  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    23
    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    24
    show "inverse (sqrt x) / (sqrt x / x) = 1"
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    25
      by (simp add: divide_inverse mult_assoc [symmetric] 
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    26
                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    27
  qed
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    28
qed
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    29
34264f5e4691 new treatment of binary numerals
paulson
parents: 14641
diff changeset
    30
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    31
constdefs
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    32
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    33
  exphr :: "real => hypreal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    34
    --{*define exponential function using standard part *}
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    35
    "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    36
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    37
  sinhr :: "real => hypreal"
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    38
    "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    39
             ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    40
  
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    41
  coshr :: "real => hypreal"
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    42
    "coshr x == st(sumhr (0, whn, %n. (if even(n) then
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    43
            ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    44
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    45
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    46
subsection{*Nonstandard Extension of Square Root Function*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    47
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    48
lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    49
by (simp add: starfun hypreal_zero_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    50
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    51
lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    52
by (simp add: starfun hypreal_one_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    53
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    54
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
    55
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    56
apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    57
                      real_sqrt_pow2_iff 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    58
            simp del: hpowr_Suc realpow_Suc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    59
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    60
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    61
lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
    62
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    63
apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    64
            simp add: hypreal_less starfun hrealpow hypreal_zero_num 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    65
            simp del: hpowr_Suc realpow_Suc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    66
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    67
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    68
lemma hypreal_sqrt_pow2_gt_zero: "0 < x ==> 0 < ( *f* sqrt) (x) ^ 2"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    69
by (frule hypreal_sqrt_gt_zero_pow2, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    70
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    71
lemma hypreal_sqrt_not_zero: "0 < x ==> ( *f* sqrt) (x) \<noteq> 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    72
apply (frule hypreal_sqrt_pow2_gt_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    73
apply (auto simp add: numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    74
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    75
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    76
lemma hypreal_inverse_sqrt_pow2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    77
     "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    78
apply (cut_tac n1 = 2 and a1 = "( *f* sqrt) x" in power_inverse [symmetric])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    79
apply (auto dest: hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    80
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    81
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    82
lemma hypreal_sqrt_mult_distrib: 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    83
    "[|0 < x; 0 <y |] ==> ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
    84
apply (cases x, cases y)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    85
apply (simp add: hypreal_zero_def starfun hypreal_mult hypreal_less hypreal_zero_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    86
apply (auto intro: real_sqrt_mult_distrib) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    87
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    88
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    89
lemma hypreal_sqrt_mult_distrib2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    90
     "[|0\<le>x; 0\<le>y |] ==>  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    91
     ( *f* sqrt)(x*y) =  ( *f* sqrt)(x) * ( *f* sqrt)(y)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    92
by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    93
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    94
lemma hypreal_sqrt_approx_zero [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    95
     "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    96
apply (auto simp add: mem_infmal_iff [symmetric])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    97
apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    98
apply (auto intro: Infinitesimal_mult 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
    99
            dest!: hypreal_sqrt_gt_zero_pow2 [THEN ssubst] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   100
            simp add: numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   101
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   102
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   103
lemma hypreal_sqrt_approx_zero2 [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   104
     "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   105
by (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   106
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   107
lemma hypreal_sqrt_sum_squares [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   108
     "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   109
apply (rule hypreal_sqrt_approx_zero2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   110
apply (rule hypreal_le_add_order)+
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   111
apply (auto simp add: zero_le_square)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   112
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   113
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   114
lemma hypreal_sqrt_sum_squares2 [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   115
     "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   116
apply (rule hypreal_sqrt_approx_zero2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   117
apply (rule hypreal_le_add_order)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   118
apply (auto simp add: zero_le_square)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   119
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   120
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   121
lemma hypreal_sqrt_gt_zero: "0 < x ==> 0 < ( *f* sqrt)(x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   122
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   123
apply (auto simp add: starfun hypreal_zero_def hypreal_less hypreal_zero_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   124
apply (auto intro: real_sqrt_gt_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   125
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   126
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   127
lemma hypreal_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> ( *f* sqrt)(x)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   128
by (auto intro: hypreal_sqrt_gt_zero simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   129
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   130
lemma hypreal_sqrt_hrabs [simp]: "( *f* sqrt)(x ^ 2) = abs(x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   131
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   132
apply (simp add: starfun hypreal_hrabs hypreal_mult numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   133
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   134
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   135
lemma hypreal_sqrt_hrabs2 [simp]: "( *f* sqrt)(x*x) = abs(x)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   136
apply (rule hrealpow_two [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   137
apply (rule numeral_2_eq_2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   138
apply (rule hypreal_sqrt_hrabs)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   139
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   140
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   141
lemma hypreal_sqrt_hyperpow_hrabs [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   142
     "( *f* sqrt)(x pow (hypnat_of_nat 2)) = abs(x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   143
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   144
apply (simp add: starfun hypreal_hrabs hypnat_of_nat_eq hyperpow)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   145
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   146
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   147
lemma star_sqrt_HFinite: "\<lbrakk>x \<in> HFinite; 0 \<le> x\<rbrakk> \<Longrightarrow> ( *f* sqrt) x \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   148
apply (rule HFinite_square_iff [THEN iffD1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   149
apply (simp only: hypreal_sqrt_mult_distrib2 [symmetric], simp) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   150
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   151
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   152
lemma st_hypreal_sqrt:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   153
     "[| x \<in> HFinite; 0 \<le> x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   154
apply (rule power_inject_base [where n=1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   155
apply (auto intro!: st_zero_le hypreal_sqrt_ge_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   156
apply (rule st_mult [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   157
apply (rule_tac [3] hypreal_sqrt_mult_distrib2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   158
apply (rule_tac [5] hypreal_sqrt_mult_distrib2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   159
apply (auto simp add: st_hrabs st_zero_le star_sqrt_HFinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   160
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   161
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   162
lemma hypreal_sqrt_sum_squares_ge1 [simp]: "x \<le> ( *f* sqrt)(x ^ 2 + y ^ 2)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   163
apply (cases x, cases y)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   164
apply (simp add: starfun hypreal_add hrealpow hypreal_le 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   165
            del: hpowr_Suc realpow_Suc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   166
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   167
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   168
lemma HFinite_hypreal_sqrt:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   169
     "[| 0 \<le> x; x \<in> HFinite |] ==> ( *f* sqrt) x \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   170
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   171
apply (rule HFinite_square_iff [THEN iffD1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   172
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   173
apply (simp add: numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   174
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   175
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   176
lemma HFinite_hypreal_sqrt_imp_HFinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   177
     "[| 0 \<le> x; ( *f* sqrt) x \<in> HFinite |] ==> x \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   178
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   179
apply (drule HFinite_square_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   180
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   181
apply (simp add: numeral_2_eq_2 del: HFinite_square_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   182
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   183
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   184
lemma HFinite_hypreal_sqrt_iff [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   185
     "0 \<le> x ==> (( *f* sqrt) x \<in> HFinite) = (x \<in> HFinite)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   186
by (blast intro: HFinite_hypreal_sqrt HFinite_hypreal_sqrt_imp_HFinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   187
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   188
lemma HFinite_sqrt_sum_squares [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   189
     "(( *f* sqrt)(x*x + y*y) \<in> HFinite) = (x*x + y*y \<in> HFinite)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   190
apply (rule HFinite_hypreal_sqrt_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   191
apply (rule hypreal_le_add_order)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   192
apply (auto simp add: zero_le_square)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   193
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   194
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   195
lemma Infinitesimal_hypreal_sqrt:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   196
     "[| 0 \<le> x; x \<in> Infinitesimal |] ==> ( *f* sqrt) x \<in> Infinitesimal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   197
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   198
apply (rule Infinitesimal_square_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   199
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   200
apply (simp add: numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   201
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   202
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   203
lemma Infinitesimal_hypreal_sqrt_imp_Infinitesimal:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   204
     "[| 0 \<le> x; ( *f* sqrt) x \<in> Infinitesimal |] ==> x \<in> Infinitesimal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   205
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   206
apply (drule Infinitesimal_square_iff [THEN iffD1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   207
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   208
apply (simp add: numeral_2_eq_2 del: Infinitesimal_square_iff [symmetric])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   209
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   210
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   211
lemma Infinitesimal_hypreal_sqrt_iff [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   212
     "0 \<le> x ==> (( *f* sqrt) x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   213
by (blast intro: Infinitesimal_hypreal_sqrt_imp_Infinitesimal Infinitesimal_hypreal_sqrt)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   214
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   215
lemma Infinitesimal_sqrt_sum_squares [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   216
     "(( *f* sqrt)(x*x + y*y) \<in> Infinitesimal) = (x*x + y*y \<in> Infinitesimal)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   217
apply (rule Infinitesimal_hypreal_sqrt_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   218
apply (rule hypreal_le_add_order)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   219
apply (auto simp add: zero_le_square)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   220
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   221
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   222
lemma HInfinite_hypreal_sqrt:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   223
     "[| 0 \<le> x; x \<in> HInfinite |] ==> ( *f* sqrt) x \<in> HInfinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   224
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   225
apply (rule HInfinite_square_iff [THEN iffD1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   226
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   227
apply (simp add: numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   228
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   229
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   230
lemma HInfinite_hypreal_sqrt_imp_HInfinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   231
     "[| 0 \<le> x; ( *f* sqrt) x \<in> HInfinite |] ==> x \<in> HInfinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   232
apply (auto simp add: order_le_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   233
apply (drule HInfinite_square_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   234
apply (drule hypreal_sqrt_gt_zero_pow2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   235
apply (simp add: numeral_2_eq_2 del: HInfinite_square_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   236
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   237
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   238
lemma HInfinite_hypreal_sqrt_iff [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   239
     "0 \<le> x ==> (( *f* sqrt) x \<in> HInfinite) = (x \<in> HInfinite)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   240
by (blast intro: HInfinite_hypreal_sqrt HInfinite_hypreal_sqrt_imp_HInfinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   241
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   242
lemma HInfinite_sqrt_sum_squares [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   243
     "(( *f* sqrt)(x*x + y*y) \<in> HInfinite) = (x*x + y*y \<in> HInfinite)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   244
apply (rule HInfinite_hypreal_sqrt_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   245
apply (rule hypreal_le_add_order)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   246
apply (auto simp add: zero_le_square)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   247
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   248
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   249
lemma HFinite_exp [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   250
     "sumhr (0, whn, %n. inverse (real (fact n)) * x ^ n) \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   251
by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   252
         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   253
                   convergent_NSconvergent_iff [symmetric] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   254
                   summable_convergent_sumr_iff [symmetric] summable_exp)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   255
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   256
lemma exphr_zero [simp]: "exphr 0 = 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   257
apply (simp add: exphr_def sumhr_split_add
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   258
                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   259
apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def hypnat_add
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   260
                 hypnat_omega_def hypreal_add 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   261
            del: hypnat_add_zero_left)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   262
apply (simp add: hypreal_one_num [symmetric])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   263
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   264
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   265
lemma coshr_zero [simp]: "coshr 0 = 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   266
apply (simp add: coshr_def sumhr_split_add
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   267
                   [OF hypnat_one_less_hypnat_omega, symmetric]) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   268
apply (simp add: sumhr hypnat_zero_def starfunNat hypnat_one_def 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   269
         hypnat_add hypnat_omega_def st_add [symmetric] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   270
         hypreal_one_def [symmetric] hypreal_zero_def [symmetric]
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   271
       del: hypnat_add_zero_left)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   272
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   273
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   274
lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) 0 @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   275
by (simp add: hypreal_zero_def hypreal_one_def starfun hypreal_one_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   276
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   277
lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) x @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   278
apply (case_tac "x = 0")
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   279
apply (cut_tac [2] x = 0 in DERIV_exp)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   280
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   281
apply (drule_tac x = x in bspec, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   282
apply (drule_tac c = x in approx_mult1)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   283
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   284
            simp add: mult_assoc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   285
apply (rule approx_add_right_cancel [where d="-1"])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   286
apply (rule approx_sym [THEN [2] approx_trans2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   287
apply (auto simp add: mem_infmal_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   288
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   289
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   290
lemma STAR_exp_epsilon [simp]: "( *f* exp) epsilon @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   291
by (auto intro: STAR_exp_Infinitesimal)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   292
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   293
lemma STAR_exp_add: "( *f* exp)(x + y) = ( *f* exp) x * ( *f* exp) y"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   294
apply (cases x, cases y)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   295
apply (simp add: starfun hypreal_add hypreal_mult exp_add)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   296
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   297
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   298
lemma exphr_hypreal_of_real_exp_eq: "exphr x = hypreal_of_real (exp x)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   299
apply (simp add: exphr_def)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   300
apply (rule st_hypreal_of_real [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   301
apply (rule approx_st_eq, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   302
apply (rule approx_minus_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   303
apply (auto simp add: mem_infmal_iff [symmetric] hypreal_of_real_def hypnat_zero_def hypnat_omega_def sumhr hypreal_minus hypreal_add)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   304
apply (rule NSLIMSEQ_zero_Infinitesimal_hypreal)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   305
apply (insert exp_converges [of x]) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   306
apply (simp add: sums_def) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   307
apply (drule LIMSEQ_const [THEN [2] LIMSEQ_add, where b = "- exp x"])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   308
apply (simp add: LIMSEQ_NSLIMSEQ_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   309
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   310
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   311
lemma starfun_exp_ge_add_one_self [simp]: "0 \<le> x ==> (1 + x) \<le> ( *f* exp) x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   312
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   313
apply (simp add: starfun hypreal_add hypreal_le hypreal_zero_num hypreal_one_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   314
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   315
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   316
(* exp (oo) is infinite *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   317
lemma starfun_exp_HInfinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   318
     "[| x \<in> HInfinite; 0 \<le> x |] ==> ( *f* exp) x \<in> HInfinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   319
apply (frule starfun_exp_ge_add_one_self)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   320
apply (rule HInfinite_ge_HInfinite, assumption)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   321
apply (rule order_trans [of _ "1+x"], auto) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   322
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   323
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   324
lemma starfun_exp_minus: "( *f* exp) (-x) = inverse(( *f* exp) x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   325
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   326
apply (simp add: starfun hypreal_inverse hypreal_minus exp_minus)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   327
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   328
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   329
(* exp (-oo) is infinitesimal *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   330
lemma starfun_exp_Infinitesimal:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   331
     "[| x \<in> HInfinite; x \<le> 0 |] ==> ( *f* exp) x \<in> Infinitesimal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   332
apply (subgoal_tac "\<exists>y. x = - y")
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   333
apply (rule_tac [2] x = "- x" in exI)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   334
apply (auto intro!: HInfinite_inverse_Infinitesimal starfun_exp_HInfinite
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   335
            simp add: starfun_exp_minus HInfinite_minus_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   336
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   337
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   338
lemma starfun_exp_gt_one [simp]: "0 < x ==> 1 < ( *f* exp) x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   339
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   340
apply (simp add: starfun hypreal_one_num hypreal_zero_num hypreal_less, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   341
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   342
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   343
(* needs derivative of inverse function
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   344
   TRY a NS one today!!!
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   345
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   346
Goal "x @= 1 ==> ( *f* ln) x @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   347
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   348
by (auto_tac (claset(),simpset() addsimps [hypreal_one_def]));
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   349
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   350
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   351
Goalw [nsderiv_def] "0r < x ==> NSDERIV ln x :> inverse x";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   352
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   353
*)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   354
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   355
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   356
lemma starfun_ln_exp [simp]: "( *f* ln) (( *f* exp) x) = x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   357
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   358
apply (simp add: starfun)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   359
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   360
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   361
lemma starfun_exp_ln_iff [simp]: "(( *f* exp)(( *f* ln) x) = x) = (0 < x)"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   362
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   363
apply (simp add: starfun hypreal_zero_num hypreal_less)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   364
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   365
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   366
lemma starfun_exp_ln_eq: "( *f* exp) u = x ==> ( *f* ln) x = u"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   367
by (auto simp add: starfun)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   368
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   369
lemma starfun_ln_less_self [simp]: "0 < x ==> ( *f* ln) x < x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   370
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   371
apply (simp add: starfun hypreal_zero_num hypreal_less, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   372
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   373
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   374
lemma starfun_ln_ge_zero [simp]: "1 \<le> x ==> 0 \<le> ( *f* ln) x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   375
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   376
apply (simp add: starfun hypreal_zero_num hypreal_le hypreal_one_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   377
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   378
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   379
lemma starfun_ln_gt_zero [simp]: "1 < x ==> 0 < ( *f* ln) x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   380
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   381
apply (simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   382
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   383
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   384
lemma starfun_ln_not_eq_zero [simp]: "[| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   385
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   386
apply (auto simp add: starfun hypreal_zero_num hypreal_less hypreal_one_num, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   387
apply (auto dest: ln_not_eq_zero) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   388
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   389
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   390
lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   391
apply (rule HFinite_bounded)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   392
apply (rule_tac [2] order_less_imp_le)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   393
apply (rule_tac [2] starfun_ln_less_self)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   394
apply (rule_tac [2] order_less_le_trans, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   395
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   396
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   397
lemma starfun_ln_inverse: "0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   398
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   399
apply (simp add: starfun hypreal_zero_num hypreal_minus hypreal_inverse hypreal_less, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   400
apply (simp add: ln_inverse)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   401
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   402
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   403
lemma starfun_exp_HFinite: "x \<in> HFinite ==> ( *f* exp) x \<in> HFinite"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   404
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   405
apply (auto simp add: starfun HFinite_FreeUltrafilterNat_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   406
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   407
apply (rule_tac x = "exp u" in exI)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   408
apply (ultra, arith)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   409
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   410
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   411
lemma starfun_exp_add_HFinite_Infinitesimal_approx:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   412
     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x) @= ( *f* exp) z"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   413
apply (simp add: STAR_exp_add)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   414
apply (frule STAR_exp_Infinitesimal)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   415
apply (drule approx_mult2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   416
apply (auto intro: starfun_exp_HFinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   417
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   418
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   419
(* using previous result to get to result *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   420
lemma starfun_ln_HInfinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   421
     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   422
apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   423
apply (drule starfun_exp_HFinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   424
apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   425
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   426
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   427
lemma starfun_exp_HInfinite_Infinitesimal_disj:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   428
 "x \<in> HInfinite ==> ( *f* exp) x \<in> HInfinite | ( *f* exp) x \<in> Infinitesimal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   429
apply (insert linorder_linear [of x 0]) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   430
apply (auto intro: starfun_exp_HInfinite starfun_exp_Infinitesimal)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   431
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   432
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   433
(* check out this proof!!! *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   434
lemma starfun_ln_HFinite_not_Infinitesimal:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   435
     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   436
apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   437
apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   438
apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   439
            del: starfun_exp_ln_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   440
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   441
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   442
(* we do proof by considering ln of 1/x *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   443
lemma starfun_ln_Infinitesimal_HInfinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   444
     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   445
apply (drule Infinitesimal_inverse_HInfinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   446
apply (frule positive_imp_inverse_positive)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   447
apply (drule_tac [2] starfun_ln_HInfinite)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   448
apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   449
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   450
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   451
lemma starfun_ln_less_zero: "[| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
14468
6be497cacab5 heavy tidying
paulson
parents: 14430
diff changeset
   452
apply (cases x)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   453
apply (simp add: hypreal_zero_num hypreal_one_num hypreal_less starfun, ultra)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   454
apply (auto intro: ln_less_zero) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   455
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   456
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   457
lemma starfun_ln_Infinitesimal_less_zero:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   458
     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   459
apply (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   460
apply (drule bspec [where x = 1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   461
apply (auto simp add: abs_if)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   462
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   463
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   464
lemma starfun_ln_HInfinite_gt_zero:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   465
     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   466
apply (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   467
apply (drule bspec [where x = 1])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   468
apply (auto simp add: abs_if)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   469
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   470
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   471
(*
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   472
Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   473
*)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   474
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   475
lemma HFinite_sin [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   476
     "sumhr (0, whn, %n. (if even(n) then 0 else  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   477
              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   478
              \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   479
apply (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   480
            simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   481
                      convergent_NSconvergent_iff [symmetric] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   482
                      summable_convergent_sumr_iff [symmetric])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   483
apply (simp only: One_nat_def summable_sin)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   484
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   485
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   486
lemma STAR_sin_zero [simp]: "( *f* sin) 0 = 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   487
by (simp add: starfun hypreal_zero_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   488
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   489
lemma STAR_sin_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   490
apply (case_tac "x = 0")
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   491
apply (cut_tac [2] x = 0 in DERIV_sin)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   492
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   493
apply (drule bspec [where x = x], auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   494
apply (drule approx_mult1 [where c = x])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   495
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   496
           simp add: mult_assoc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   497
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   498
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   499
lemma HFinite_cos [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   500
     "sumhr (0, whn, %n. (if even(n) then  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   501
            ((- 1) ^ (n div 2))/(real (fact n)) else  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   502
            0) * x ^ n) \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   503
by (auto intro!: NSBseq_HFinite_hypreal NSconvergent_NSBseq 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   504
         simp add: starfunNat_sumr [symmetric] starfunNat hypnat_omega_def
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   505
                   convergent_NSconvergent_iff [symmetric] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   506
                   summable_convergent_sumr_iff [symmetric] summable_cos)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   507
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   508
lemma STAR_cos_zero [simp]: "( *f* cos) 0 = 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   509
by (simp add: starfun hypreal_zero_num hypreal_one_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   510
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   511
lemma STAR_cos_Infinitesimal [simp]: "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   512
apply (case_tac "x = 0")
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   513
apply (cut_tac [2] x = 0 in DERIV_cos)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   514
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   515
apply (drule bspec [where x = x])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   516
apply (auto simp add: hypreal_of_real_zero hypreal_of_real_one)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   517
apply (drule approx_mult1 [where c = x])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   518
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   519
            simp add: mult_assoc hypreal_of_real_one)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   520
apply (rule approx_add_right_cancel [where d = "-1"], auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   521
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   522
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   523
lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   524
by (simp add: starfun hypreal_zero_num)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   525
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   526
lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   527
apply (case_tac "x = 0")
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   528
apply (cut_tac [2] x = 0 in DERIV_tan)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   529
apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   530
apply (drule bspec [where x = x], auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   531
apply (drule approx_mult1 [where c = x])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   532
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   533
             simp add: mult_assoc)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   534
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   535
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   536
lemma STAR_sin_cos_Infinitesimal_mult:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   537
     "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   538
apply (insert approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1]) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   539
apply (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   540
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   541
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   542
lemma HFinite_pi: "hypreal_of_real pi \<in> HFinite"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   543
by simp
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   544
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   545
(* lemmas *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   546
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   547
lemma lemma_split_hypreal_of_real:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   548
     "N \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   549
      ==> hypreal_of_real a =  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   550
          hypreal_of_hypnat N * (inverse(hypreal_of_hypnat N) * hypreal_of_real a)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   551
by (simp add: mult_assoc [symmetric] HNatInfinite_not_eq_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   552
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   553
lemma STAR_sin_Infinitesimal_divide:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   554
     "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   555
apply (cut_tac x = 0 in DERIV_sin)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   556
apply (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def hypreal_of_real_zero hypreal_of_real_one)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   557
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   558
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   559
(*------------------------------------------------------------------------*) 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   560
(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   561
(*------------------------------------------------------------------------*)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   562
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   563
lemma lemma_sin_pi:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   564
     "n \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   565
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   566
apply (rule STAR_sin_Infinitesimal_divide)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   567
apply (auto simp add: HNatInfinite_not_eq_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   568
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   569
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   570
lemma STAR_sin_inverse_HNatInfinite:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   571
     "n \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   572
      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   573
apply (frule lemma_sin_pi)
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   574
apply (simp add: divide_inverse)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   575
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   576
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   577
lemma Infinitesimal_pi_divide_HNatInfinite: 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   578
     "N \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   579
      ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<in> Infinitesimal"
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   580
apply (simp add: divide_inverse)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   581
apply (auto intro: Infinitesimal_HFinite_mult2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   582
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   583
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   584
lemma pi_divide_HNatInfinite_not_zero [simp]:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   585
     "N \<in> HNatInfinite ==> hypreal_of_real pi/(hypreal_of_hypnat N) \<noteq> 0"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   586
by (simp add: HNatInfinite_not_eq_zero)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   587
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   588
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   589
     "n \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   590
      ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   591
          @= hypreal_of_real pi"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   592
apply (frule STAR_sin_Infinitesimal_divide
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   593
               [OF Infinitesimal_pi_divide_HNatInfinite 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   594
                   pi_divide_HNatInfinite_not_zero])
14477
cc61fd03e589 conversion of Hyperreal/Lim to new-style
paulson
parents: 14468
diff changeset
   595
apply (auto simp add: inverse_mult_distrib)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   596
apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   597
apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   598
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   599
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   600
lemma STAR_sin_pi_divide_HNatInfinite_approx_pi2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   601
     "n \<in> HNatInfinite  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   602
      ==> hypreal_of_hypnat n *  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   603
          ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   604
          @= hypreal_of_real pi"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   605
apply (rule mult_commute [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   606
apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   607
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   608
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   609
lemma starfunNat_pi_divide_n_Infinitesimal: 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   610
     "N \<in> HNatInfinite ==> ( *fNat* (%x. pi / real x)) N \<in> Infinitesimal"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   611
by (auto intro!: Infinitesimal_HFinite_mult2 
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   612
         simp add: starfunNat_mult [symmetric] divide_inverse
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   613
                   starfunNat_inverse [symmetric] starfunNat_real_of_nat)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   614
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   615
lemma STAR_sin_pi_divide_n_approx:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   616
     "N \<in> HNatInfinite ==>  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   617
      ( *f* sin) (( *fNat* (%x. pi / real x)) N) @=  
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   618
      hypreal_of_real pi/(hypreal_of_hypnat N)"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   619
by (auto intro!: STAR_sin_Infinitesimal Infinitesimal_HFinite_mult2 
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   620
         simp add: starfunNat_mult [symmetric] divide_inverse
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   621
                   starfunNat_inverse_real_of_nat_eq)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   622
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   623
lemma NSLIMSEQ_sin_pi: "(%n. real n * sin (pi / real n)) ----NS> pi"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   624
apply (auto simp add: NSLIMSEQ_def starfunNat_mult [symmetric] starfunNat_real_of_nat)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   625
apply (rule_tac f1 = sin in starfun_stafunNat_o2 [THEN subst])
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   626
apply (auto simp add: starfunNat_mult [symmetric] starfunNat_real_of_nat divide_inverse)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   627
apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   628
apply (auto dest: STAR_sin_pi_divide_HNatInfinite_approx_pi 
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   629
            simp add: starfunNat_real_of_nat mult_commute divide_inverse)
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   630
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   631
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   632
lemma NSLIMSEQ_cos_one: "(%n. cos (pi / real n))----NS> 1"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   633
apply (simp add: NSLIMSEQ_def, auto)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   634
apply (rule_tac f1 = cos in starfun_stafunNat_o2 [THEN subst])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   635
apply (rule STAR_cos_Infinitesimal)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   636
apply (auto intro!: Infinitesimal_HFinite_mult2 
14430
5cb24165a2e1 new material from Avigad, and simplified treatment of division by 0
paulson
parents: 14420
diff changeset
   637
            simp add: starfunNat_mult [symmetric] divide_inverse
14420
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   638
                      starfunNat_inverse [symmetric] starfunNat_real_of_nat)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   639
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   640
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   641
lemma NSLIMSEQ_sin_cos_pi:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   642
     "(%n. real n * sin (pi / real n) * cos (pi / real n)) ----NS> pi"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   643
by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   644
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   645
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   646
text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   647
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   648
lemma STAR_cos_Infinitesimal_approx:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   649
     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x ^ 2"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   650
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   651
apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   652
            diff_minus add_assoc [symmetric] numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   653
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   654
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   655
lemma STAR_cos_Infinitesimal_approx2:
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   656
     "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x ^ 2)/2"
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   657
apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   658
apply (auto intro: Infinitesimal_SReal_divide 
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   659
            simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   660
done
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   661
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   662
ML
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   663
{*
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   664
val STAR_sqrt_zero = thm "STAR_sqrt_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   665
val STAR_sqrt_one = thm "STAR_sqrt_one";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   666
val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   667
val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   668
val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   669
val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   670
val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   671
val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   672
val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   673
val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   674
val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   675
val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   676
val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   677
val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   678
val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   679
val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   680
val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   681
val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   682
val star_sqrt_HFinite = thm "star_sqrt_HFinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   683
val st_hypreal_sqrt = thm "st_hypreal_sqrt";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   684
val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   685
val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   686
val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   687
val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   688
val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   689
val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   690
val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   691
val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   692
val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   693
val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   694
val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   695
val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   696
val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   697
val HFinite_exp = thm "HFinite_exp";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   698
val exphr_zero = thm "exphr_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   699
val coshr_zero = thm "coshr_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   700
val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   701
val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   702
val STAR_exp_epsilon = thm "STAR_exp_epsilon";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   703
val STAR_exp_add = thm "STAR_exp_add";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   704
val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   705
val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   706
val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   707
val starfun_exp_minus = thm "starfun_exp_minus";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   708
val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   709
val starfun_exp_gt_one = thm "starfun_exp_gt_one";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   710
val starfun_ln_exp = thm "starfun_ln_exp";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   711
val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   712
val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   713
val starfun_ln_less_self = thm "starfun_ln_less_self";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   714
val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   715
val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   716
val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   717
val starfun_ln_HFinite = thm "starfun_ln_HFinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   718
val starfun_ln_inverse = thm "starfun_ln_inverse";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   719
val starfun_exp_HFinite = thm "starfun_exp_HFinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   720
val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   721
val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   722
val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   723
val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   724
val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   725
val starfun_ln_less_zero = thm "starfun_ln_less_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   726
val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   727
val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   728
val HFinite_sin = thm "HFinite_sin";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   729
val STAR_sin_zero = thm "STAR_sin_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   730
val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   731
val HFinite_cos = thm "HFinite_cos";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   732
val STAR_cos_zero = thm "STAR_cos_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   733
val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   734
val STAR_tan_zero = thm "STAR_tan_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   735
val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   736
val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   737
val HFinite_pi = thm "HFinite_pi";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   738
val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   739
val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   740
val lemma_sin_pi = thm "lemma_sin_pi";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   741
val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   742
val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   743
val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   744
val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   745
val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   746
val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   747
val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   748
val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   749
val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   750
val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   751
val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   752
val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   753
*}
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   754
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   755
4e72cd222e0b converted Hyperreal/HTranscendental to Isar script
paulson
parents: 13958
diff changeset
   756
end