src/HOL/Hyperreal/HyperPow.ML
author paulson
Wed, 10 Jan 2001 17:21:31 +0100
changeset 10857 47b1f34ddd09
parent 10834 a7897aebbffc
child 10919 144ede948e58
permissions -rw-r--r--
revisions e.g. images, transitive closure...
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : HyperPow.ML
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Description : Natural Powers of hyperreals theory
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
     6
Exponentials on the hyperreals
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
Goal "(#0::hypreal) ^ (Suc n) = 0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
qed "hrealpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
Addsimps [hrealpow_zero];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    13
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    14
Goal "r ~= (#0::hypreal) --> r ^ n ~= 0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    16
by Auto_tac;
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    17
qed_spec_mp "hrealpow_not_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    18
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    19
Goal "r ~= (#0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
by (forw_inst_tac [("n","n")] hrealpow_not_zero 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    23
by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_distrib]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
qed_spec_mp "hrealpow_inverse";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
by (auto_tac (claset(), simpset() addsimps [hrabs_mult]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
qed "hrealpow_hrabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    31
Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    32
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    33
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    34
qed "hrealpow_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
Goal "(r::hypreal) ^ 1 = r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    37
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    38
qed "hrealpow_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    39
Addsimps [hrealpow_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    40
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    41
Goal "(r::hypreal) ^ 2 = r * r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    42
by (Simp_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    43
qed "hrealpow_two";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    44
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
Goal "(#0::hypreal) <= r --> #0 <= r ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    47
by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    48
qed_spec_mp "hrealpow_ge_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    49
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    50
Goal "(#0::hypreal) < r --> #0 < r ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    51
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    52
by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    53
qed_spec_mp "hrealpow_gt_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    54
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    55
Goal "x <= y & (#0::hypreal) < x --> x ^ n <= y ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    56
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    57
by (auto_tac (claset() addSIs [hypreal_mult_le_mono], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    58
by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    59
qed_spec_mp "hrealpow_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    60
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    61
Goal "x < y & (#0::hypreal) < x & 0 < n --> x ^ n < y ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    62
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    63
by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    64
              simpset() addsimps [hrealpow_gt_zero]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    65
qed "hrealpow_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    66
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    67
Goal "#1 ^ n = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    68
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    69
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    70
qed "hrealpow_eq_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    71
Addsimps [hrealpow_eq_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    72
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    73
Goal "abs(-(#1 ^ n)) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    74
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    75
qed "hrabs_minus_hrealpow_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    76
Addsimps [hrabs_minus_hrealpow_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    77
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    78
Goal "abs(#-1 ^ n) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    79
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    80
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    81
qed "hrabs_hrealpow_minus_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    82
Addsimps [hrabs_hrealpow_minus_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    83
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    84
Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    85
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    86
by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    87
qed "hrealpow_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    88
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    89
Goal "(#0::hypreal) <= r ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    90
by (auto_tac (claset(), simpset() addsimps [hypreal_0_le_mult_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    91
qed "hrealpow_two_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    92
Addsimps [hrealpow_two_le];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    93
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    94
Goal "(#0::hypreal) <= u ^ 2 + v ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    95
by (simp_tac (HOL_ss addsimps [hrealpow_two_le, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    96
                    rename_numerals hypreal_le_add_order]) 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    97
qed "hrealpow_two_le_add_order";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    98
Addsimps [hrealpow_two_le_add_order];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    99
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   100
Goal "(#0::hypreal) <= u ^ 2 + v ^ 2 + w ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   101
by (simp_tac (HOL_ss addsimps [hrealpow_two_le, 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   102
                    rename_numerals hypreal_le_add_order]) 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   103
qed "hrealpow_two_le_add_order2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   104
Addsimps [hrealpow_two_le_add_order2];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   105
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   106
Goal "(x ^ 2 + y ^ 2 + z ^ 2 = (#0::hypreal)) = (x = #0 & y = #0 & z = #0)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   107
by (simp_tac (HOL_ss addsimps
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   108
      [rename_numerals hypreal_three_squares_add_zero_iff, hrealpow_two]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   109
qed "hrealpow_three_squares_add_zero_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   110
Addsimps [hrealpow_three_squares_add_zero_iff];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   111
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   112
Goal "abs(x ^ 2) = (x::hypreal) ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   113
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   114
     simpset() addsimps [hrabs_def, hypreal_0_le_mult_iff])); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   115
qed "hrabs_hrealpow_two";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   116
Addsimps [hrabs_hrealpow_two];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   117
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   118
Goal "abs(x) ^ 2 = (x::hypreal) ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   119
by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   120
                        delsimps [hpowr_Suc]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   121
qed "hrealpow_two_hrabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   122
Addsimps [hrealpow_two_hrabs];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   123
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   124
Goal "(#1::hypreal) < r ==> #1 < r ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   125
by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   126
by (res_inst_tac [("y","#1*#1")] order_le_less_trans 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   127
by (rtac hypreal_mult_less_mono 2); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   128
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   129
qed "hrealpow_two_gt_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   130
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   131
Goal "(#1::hypreal) <= r ==> #1 <= r ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   132
by (etac (order_le_imp_less_or_eq RS disjE) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   133
by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   134
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   135
qed "hrealpow_two_ge_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   136
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   137
Goal "(#1::hypreal) <= #2 ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   138
by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   139
by (rtac hrealpow_le 2);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   140
by Auto_tac;
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   141
qed "two_hrealpow_ge_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   142
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   143
Goal "hypreal_of_nat n < #2 ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   144
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   145
by (auto_tac (claset(),
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   146
        simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   147
by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   148
by (arith_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   149
qed "two_hrealpow_gt";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   150
Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   151
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   152
Goal "#-1 ^ (2*n) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   153
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   154
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   155
qed "hrealpow_minus_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   156
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   157
Goal "#-1 ^ (n + n) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   158
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   159
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   160
qed "hrealpow_minus_one2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   161
Addsimps [hrealpow_minus_one2];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   162
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   163
Goal "(-(x::hypreal)) ^ 2 = x ^ 2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   164
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   165
qed "hrealpow_minus_two";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   166
Addsimps [hrealpow_minus_two];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   167
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   168
Goal "(#0::hypreal) < r & r < #1 --> r ^ Suc n < r ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   169
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   170
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   171
              simpset() addsimps [hypreal_mult_less_mono2]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   172
qed_spec_mp "hrealpow_Suc_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   173
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   174
Goal "(#0::hypreal) <= r & r < #1 --> r ^ Suc n <= r ^ n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   175
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   176
by (auto_tac (claset() addIs [order_less_imp_le]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   177
                       addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   178
              simpset() addsimps [hypreal_mult_less_mono2]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   179
qed_spec_mp "hrealpow_Suc_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   180
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   181
Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   182
by (induct_tac "m" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   183
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   184
              simpset() delsimps [one_eq_numeral_1]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   185
			addsimps [hypreal_one_def, hypreal_mult,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   186
                                  one_eq_numeral_1 RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   187
qed "hrealpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   188
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   189
Goal "(x + (y::hypreal)) ^ 2 = \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   190
\     x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y";
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   191
by (simp_tac (simpset() addsimps
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   192
              [hypreal_add_mult_distrib2, hypreal_add_mult_distrib, 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   193
               hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   194
qed "hrealpow_sum_square_expand";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   195
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   196
(*---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   197
   we'll prove the following theorem by going down to the
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   198
   level of the ultrafilter and relying on the analogous
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   199
   property for the real rather than prove it directly 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   200
   using induction: proof is much simpler this way!
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   201
 ---------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   202
Goal "[|(#0::hypreal) <= x; #0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   203
by (full_simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   204
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   205
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   206
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   207
              simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   208
by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   209
qed "hrealpow_increasing";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   210
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   211
(*By antisymmetry with the above we conclude x=y, replacing the deleted 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   212
  theorem hrealpow_Suc_cancel_eq*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   213
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   214
Goal "x : HFinite --> x ^ n : HFinite";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   215
by (induct_tac "n" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   216
by (auto_tac (claset() addIs [HFinite_mult], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   217
qed_spec_mp "hrealpow_HFinite";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   218
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   219
(*---------------------------------------------------------------
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   220
                  Hypernaturals Powers
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   221
 --------------------------------------------------------------*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   222
Goalw [congruent_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   223
     "congruent hyprel \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   224
\    (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   225
by (safe_tac (claset() addSIs [ext]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   226
by (ALLGOALS(Fuf_tac));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   227
qed "hyperpow_congruent";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   228
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   229
Goalw [hyperpow_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   230
  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \
a7897aebbffc *** empty log message ***
nipkow
parents: 10797
diff changeset
   231
\  Abs_hypreal(hyprel``{%n. X n ^ Y n})";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   232
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   233
by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   234
    simpset() addsimps [hyprel_in_hypreal RS 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   235
    Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   236
by (Fuf_tac 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   237
qed "hyperpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   238
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   239
Goalw [hypnat_one_def] "(#0::hypreal) pow (n + 1hn) = #0";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   240
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   241
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   242
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   243
qed "hyperpow_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   244
Addsimps [hyperpow_zero];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   245
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   246
Goal "r ~= (#0::hypreal) --> r pow n ~= #0";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   247
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   248
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   249
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   250
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   251
by (dtac FreeUltrafilterNat_Compl_mem 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   252
by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   253
    simpset()) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   254
qed_spec_mp "hyperpow_not_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   255
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   256
Goal "r ~= (#0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   257
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   258
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   259
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   260
by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   261
              simpset() addsimps [hypreal_inverse,hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   262
by (rtac FreeUltrafilterNat_subset 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   263
by (auto_tac (claset() addDs [realpow_not_zero] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   264
                       addIs [realpow_inverse], 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   265
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   266
qed "hyperpow_inverse";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   267
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   268
Goal "abs r pow n = abs (r pow n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   269
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   270
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   271
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   272
              simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   273
qed "hyperpow_hrabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   274
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   275
Goal "r pow (n + m) = (r pow n) * (r pow m)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   276
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   277
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   278
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   279
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   280
          simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   281
qed "hyperpow_add";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   282
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   283
Goalw [hypnat_one_def] "r pow 1hn = r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   284
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   285
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   286
qed "hyperpow_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   287
Addsimps [hyperpow_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   288
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   289
Goalw [hypnat_one_def] 
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   290
     "r pow (1hn + 1hn) = r * r";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   291
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   292
by (auto_tac (claset(),
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   293
              simpset() addsimps [hyperpow,hypnat_add, hypreal_mult]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   294
qed "hyperpow_two";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   295
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   296
Goal "(#0::hypreal) < r --> #0 < r pow n";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   297
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   298
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   299
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   300
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   301
              simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   302
qed_spec_mp "hyperpow_gt_zero";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   303
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   304
Goal "(#0::hypreal) <= r --> #0 <= r pow n";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   305
by (simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   306
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   307
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   308
by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero],
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   309
              simpset() addsimps [hyperpow,hypreal_le]));
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   310
qed "hyperpow_ge_zero";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   311
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   312
Goal "(#0::hypreal) < x & x <= y --> x pow n <= y pow n";
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   313
by (full_simp_tac (simpset() addsimps [rename_numerals hypreal_zero_def]) 1);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   314
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   315
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   316
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
10784
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   317
by (auto_tac (claset(),
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   318
              simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   319
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   320
    THEN assume_tac 1);
27e4d90b35b5 more removal of obsolete rules
paulson
parents: 10778
diff changeset
   321
by (auto_tac (claset() addIs [realpow_le], simpset()));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   322
qed_spec_mp "hyperpow_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   323
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   324
Goal "#1 pow n = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   325
by (simp_tac (HOL_ss addsimps [one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   326
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   327
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   328
qed "hyperpow_eq_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   329
Addsimps [hyperpow_eq_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   330
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   331
Goal "abs(-(#1 pow n)) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   332
by (simp_tac (HOL_ss addsimps [one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   333
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   334
by (auto_tac (claset(), simpset() addsimps [hyperpow,hypreal_hrabs]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   335
qed "hrabs_minus_hyperpow_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   336
Addsimps [hrabs_minus_hyperpow_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   337
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   338
Goal "abs(#-1 pow n) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   339
by (subgoal_tac "abs((-1hr) pow n) = 1hr" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   340
by (Asm_full_simp_tac 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   341
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   342
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   343
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   344
       simpset() addsimps [hyperpow,hypreal_minus,hypreal_hrabs]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   345
qed "hrabs_hyperpow_minus_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   346
Addsimps [hrabs_hyperpow_minus_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   347
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   348
Goal "(r * s) pow n = (r pow n) * (s pow n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   349
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   350
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   351
by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   352
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   353
       simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   354
qed "hyperpow_mult";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   355
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   356
Goal "(#0::hypreal) <= r pow (1hn + 1hn)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   357
by (auto_tac (claset(), 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   358
              simpset() addsimps [hyperpow_two, hypreal_0_le_mult_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   359
qed "hyperpow_two_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   360
Addsimps [hyperpow_two_le];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   361
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   362
Goal "abs(x pow (1hn + 1hn)) = x pow (1hn + 1hn)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   363
by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   364
qed "hrabs_hyperpow_two";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   365
Addsimps [hrabs_hyperpow_two];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   366
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   367
Goal "abs(x) pow (1hn + 1hn)  = x pow (1hn + 1hn)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   368
by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   369
qed "hyperpow_two_hrabs";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   370
Addsimps [hyperpow_two_hrabs];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   371
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   372
(*? very similar to hrealpow_two_gt_one *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   373
Goal "(#1::hypreal) < r ==> #1 < r pow (1hn + 1hn)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   374
by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   375
by (res_inst_tac [("y","#1*#1")] order_le_less_trans 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   376
by (rtac hypreal_mult_less_mono 2); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   377
by Auto_tac;  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   378
qed "hyperpow_two_gt_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   379
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   380
Goal "(#1::hypreal) <= r ==> #1 <= r pow (1hn + 1hn)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   381
by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   382
                       addIs [hyperpow_two_gt_one,order_less_imp_le],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   383
              simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   384
qed "hyperpow_two_ge_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   385
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   386
Goal "(#1::hypreal) <= #2 pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   387
by (res_inst_tac [("y","#1 pow n")] order_trans 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   388
by (rtac hyperpow_le 2);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   389
by Auto_tac;
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   390
qed "two_hyperpow_ge_one";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   391
Addsimps [two_hyperpow_ge_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   392
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   393
Addsimps [simplify (simpset()) realpow_minus_one];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   394
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   395
Goal "#-1 pow ((1hn + 1hn)*n) = (#1::hypreal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   396
by (subgoal_tac "(-(1hr)) pow ((1hn + 1hn)*n) = 1hr" 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   397
by (Asm_full_simp_tac 1); 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   398
by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   399
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   400
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   401
              simpset() addsimps [hyperpow, hypnat_add,hypreal_minus]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   402
qed "hyperpow_minus_one2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   403
Addsimps [hyperpow_minus_one2];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   404
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   405
Goalw [hypnat_one_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   406
     "(#0::hypreal) < r & r < #1 --> r pow (n + 1hn) < r pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   407
by (full_simp_tac
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   408
    (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   409
                      one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   410
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   411
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   412
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   413
                  addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   414
              simpset() addsimps [hyperpow,hypreal_less,hypnat_add]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   415
qed_spec_mp "hyperpow_Suc_less";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   416
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   417
Goalw [hypnat_one_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   418
     "#0 <= r & r < (#1::hypreal) --> r pow (n + 1hn) <= r pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   419
by (full_simp_tac
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   420
    (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   421
                      one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   422
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   423
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   424
by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] addEs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   425
    [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset ],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   426
    simpset() addsimps [hyperpow,hypreal_le,hypnat_add,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   427
    hypreal_less]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   428
qed_spec_mp "hyperpow_Suc_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   429
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   430
Goalw [hypnat_one_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   431
     "(#0::hypreal) <= r & r < #1 & n < N --> r pow N <= r pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   432
by (full_simp_tac
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   433
    (HOL_ss addsimps [zero_eq_numeral_0 RS sym, hypreal_zero_def,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   434
                      one_eq_numeral_1 RS sym, hypreal_one_def]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   435
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   436
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   437
by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   438
by (auto_tac (claset(),
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   439
        simpset() addsimps [hyperpow, hypreal_le,hypreal_less,hypnat_less]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   440
by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   441
by (etac FreeUltrafilterNat_Int 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   442
by (auto_tac (claset() addSDs [conjI RS realpow_less_le],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   443
    simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   444
qed_spec_mp "hyperpow_less_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   445
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   446
Goal "[| (#0::hypreal) <= r; r < #1 |]  \
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   447
\     ==> ALL N n. n < N --> r pow N <= r pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   448
by (blast_tac (claset() addSIs [hyperpow_less_le]) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   449
qed "hyperpow_less_le2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   450
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   451
Goal "[| #0 <= r;  r < (#1::hypreal);  N : HNatInfinite |]  \
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   452
\     ==> ALL n: SNat. r pow N <= r pow n";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   453
by (auto_tac (claset() addSIs [hyperpow_less_le],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   454
              simpset() addsimps [HNatInfinite_iff]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   455
qed "hyperpow_SHNat_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   456
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   457
Goalw [hypreal_of_real_def,hypnat_of_nat_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   458
      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   459
by (auto_tac (claset(), simpset() addsimps [hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   460
qed "hyperpow_realpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   461
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   462
Goalw [SReal_def]
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   463
     "(hypreal_of_real r) pow (hypnat_of_nat n) : SReal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   464
by (auto_tac (claset(), simpset() addsimps [hyperpow_realpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   465
qed "hyperpow_SReal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   466
Addsimps [hyperpow_SReal];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   467
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   468
Goal "N : HNatInfinite ==> (#0::hypreal) pow N = 0";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   469
by (dtac HNatInfinite_is_Suc 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   470
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   471
qed "hyperpow_zero_HNatInfinite";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   472
Addsimps [hyperpow_zero_HNatInfinite];
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   473
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   474
Goal "[| (#0::hypreal) <= r; r < #1; n <= N |] ==> r pow N <= r pow n";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   475
by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   476
by (auto_tac (claset() addIs [hyperpow_less_le], simpset()));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   477
qed "hyperpow_le_le";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   478
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   479
Goal "[| (#0::hypreal) < r; r < #1 |] ==> r pow (n + 1hn) <= r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   480
by (dres_inst_tac [("n","1hn")] (order_less_imp_le RS hyperpow_le_le) 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   481
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   482
qed "hyperpow_Suc_le_self";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   483
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   484
Goal "[| (#0::hypreal) <= r; r < #1 |] ==> r pow (n + 1hn) <= r";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   485
by (dres_inst_tac [("n","1hn")] hyperpow_le_le 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   486
by (Auto_tac);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   487
qed "hyperpow_Suc_le_self2";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   488
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   489
Goalw [Infinitesimal_def]
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   490
     "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   491
by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   492
              simpset() addsimps [hyperpow_hrabs RS sym,
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   493
                                  hypnat_gt_zero_iff2, hrabs_ge_zero]));
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   494
qed "lemma_Infinitesimal_hyperpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   495
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   496
Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   497
by (rtac hrabs_le_Infinitesimal 1);
10778
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   498
by (rtac lemma_Infinitesimal_hyperpow 2); 
2c6605049646 more tidying, especially to remove real_of_posnat
paulson
parents: 10751
diff changeset
   499
by Auto_tac;  
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   500
qed "Infinitesimal_hyperpow";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   501
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   502
Goalw [hypnat_of_nat_def] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   503
     "(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   504
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   505
by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   506
qed "hrealpow_hyperpow_Infinitesimal_iff";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   507
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   508
Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal";
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   509
by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   510
    simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   511
                        hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   512
              delsimps [hypnat_of_nat_less_iff RS sym]));
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
   513
qed "Infinitesimal_hrealpow";