src/HOL/Real/RealArith.ML
author paulson
Thu, 14 Dec 2000 10:30:11 +0100
changeset 10669 3e4f5ae4faa6
parent 10660 a196b944569b
child 10677 36625483213f
permissions -rw-r--r--
new theorem real_lbound_gt_zero
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10648
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     1
(*  Title:      HOL/Real/RealArith.ML
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     2
    ID:         $Id$
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     4
    Copyright   1999  University of Cambridge
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     5
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     6
Assorted facts that need binary literals and the arithmetic decision procedure
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     7
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     8
Also, common factor cancellation
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
     9
*)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    10
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    11
(** Division and inverse **)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    12
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    13
Goal "((#0::real) < inverse x) = (#0 < x)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    14
by (case_tac "x=#0" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    15
by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    16
by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    17
              simpset() addsimps [linorder_neq_iff, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    18
                                  rename_numerals real_inverse_gt_zero]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    19
qed "real_0_less_inverse_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    20
AddIffs [real_0_less_inverse_iff];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    21
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    22
Goal "(inverse x < (#0::real)) = (x < #0)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    23
by (case_tac "x=#0" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    24
by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    25
by (auto_tac (claset() addDs [rename_numerals real_inverse_less_zero], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    26
              simpset() addsimps [linorder_neq_iff, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    27
                                  rename_numerals real_inverse_gt_zero]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    28
qed "real_inverse_less_0_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    29
AddIffs [real_inverse_less_0_iff];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    30
10660
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    31
Goal "((#0::real) <= inverse x) = (#0 <= x)";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    32
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    33
qed "real_0_le_inverse_iff";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    34
AddIffs [real_0_le_inverse_iff];
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    35
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    36
Goal "(inverse x <= (#0::real)) = (x <= #0)";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    37
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    38
qed "real_inverse_le_0_iff";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    39
AddIffs [real_inverse_le_0_iff];
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    40
10648
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    41
Goalw [real_divide_def] "x/(#0::real) = #0";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    42
by (stac (rename_numerals INVERSE_ZERO) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    43
by (Simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    44
qed "REAL_DIVIDE_ZERO";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    45
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    46
(*generalize?*)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    47
Goal "((#0::real) < #1/x) = (#0 < x)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    48
by (simp_tac (simpset() addsimps [real_divide_def]) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    49
qed "real_0_less_recip_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    50
AddIffs [real_0_less_recip_iff];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    51
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    52
Goal "(#1/x < (#0::real)) = (x < #0)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    53
by (simp_tac (simpset() addsimps [real_divide_def]) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    54
qed "real_recip_less_0_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    55
AddIffs [real_recip_less_0_iff];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    56
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    57
Goal "inverse (x::real) = #1/x";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    58
by (simp_tac (simpset() addsimps [real_divide_def]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    59
qed "real_inverse_eq_divide";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    60
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    61
Goal "(x::real)/#1 = x";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    62
by (simp_tac (simpset() addsimps [real_divide_def]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    63
qed "real_divide_1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    64
Addsimps [real_divide_1];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    65
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    66
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    67
(**** Factor cancellation theorems for "real" ****)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    68
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    69
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    70
    but not (yet?) for k*m < n*k. **)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    71
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    72
bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    73
10660
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    74
Goal "(-y < -x) = ((x::real) < y)";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    75
by (arith_tac 1);
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    76
qed "real_minus_less_minus";
a196b944569b another round of tidying-up
paulson
parents: 10648
diff changeset
    77
10648
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    78
Goal "[| i<j;  k < (0::real) |] ==> j*k < i*k";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    79
by (rtac (real_minus_less_minus RS iffD1) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    80
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    81
              simpset() delsimps [real_minus_mult_eq2 RS sym]
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    82
                        addsimps [real_minus_mult_eq2])); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    83
qed "real_mult_less_mono1_neg";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    84
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    85
Goal "[| i<j;  k < (0::real) |] ==> k*j < k*i";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    86
by (rtac (real_minus_less_minus RS iffD1) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    87
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    88
              simpset() delsimps [real_minus_mult_eq1 RS sym]
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    89
                            addsimps [real_minus_mult_eq1]));;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    90
qed "real_mult_less_mono2_neg";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    91
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    92
Goal "[| i <= j;  (0::real) <= k |] ==> i*k <= j*k";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    93
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    94
              simpset() addsimps [order_le_less, real_mult_less_mono1]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    95
qed "real_mult_le_mono1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    96
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    97
Goal "[| i <= j;  k <= (0::real) |] ==> j*k <= i*k";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    98
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
    99
              simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   100
qed "real_mult_le_mono1_neg";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   101
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   102
Goal "[| i <= j;  (0::real) <= k |] ==> k*i <= k*j";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   103
by (dtac real_mult_le_mono1 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   104
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   105
qed "real_mult_le_mono2";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   106
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   107
Goal "[| i <= j;  k <= (0::real) |] ==> k*j <= k*i";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   108
by (dtac real_mult_le_mono1_neg 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   109
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute])));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   110
qed "real_mult_le_mono2_neg";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   111
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   112
Goal "(m*k < n*k) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   113
by (case_tac "k = (0::real)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   114
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   115
              simpset() addsimps [linorder_neq_iff, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   116
                          real_mult_less_mono1, real_mult_less_mono1_neg]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   117
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   118
              simpset() addsimps [linorder_not_less,
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   119
				  inst "y1" "m*k" (linorder_not_le RS sym),
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   120
                                  inst "y1" "m" (linorder_not_le RS sym)]));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   121
by (TRYALL (etac notE));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   122
by (auto_tac (claset(), 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   123
              simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   124
                                            real_mult_le_mono1_neg]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   125
qed "real_mult_less_cancel2";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   126
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   127
Goal "(m*k <= n*k) = (((#0::real) < k --> m<=n) & (k < #0 --> n<=m))";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   128
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   129
                                  real_mult_less_cancel2]) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   130
qed "real_mult_le_cancel2";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   131
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   132
Goal "(k*m < k*n) = (((#0::real) < k & m<n) | (k < #0 & n<m))";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   133
by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   134
                                  real_mult_less_cancel2]) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   135
qed "real_mult_less_cancel1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   136
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   137
Goal "!!k::real. (k*m <= k*n) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   138
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   139
                                  real_mult_less_cancel1]) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   140
qed "real_mult_le_cancel1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   141
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   142
Goal "!!k::real. (k*m = k*n) = (k = #0 | m=n)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   143
by (case_tac "k=0" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   144
by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   145
qed "real_mult_eq_cancel1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   146
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   147
Goal "!!k::real. (m*k = n*k) = (k = #0 | m=n)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   148
by (case_tac "k=0" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   149
by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));  
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   150
qed "real_mult_eq_cancel2";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   151
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   152
Goal "!!k::real. k~=#0 ==> (k*m) / (k*n) = (m/n)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   153
by (asm_simp_tac
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   154
    (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   155
by (subgoal_tac "k * m * (inverse k * inverse n) = \
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   156
\                (k * inverse k) * (m * inverse n)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   157
by (asm_full_simp_tac (simpset() addsimps []) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   158
by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   159
qed "real_mult_div_cancel1";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   160
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   161
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   162
local
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   163
  open Real_Numeral_Simprocs
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   164
in
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   165
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   166
val rel_real_number_of = [eq_real_number_of, less_real_number_of, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   167
                          le_real_number_of_eq_not_less];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   168
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   169
structure CancelNumeralFactorCommon =
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   170
  struct
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   171
  val mk_coeff		= mk_coeff
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   172
  val dest_coeff	= dest_coeff 1
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   173
  val trans_tac         = trans_tac
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   174
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_plus_1s))
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   175
            THEN ALLGOALS
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   176
                 (simp_tac 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   177
                  (HOL_ss addsimps [eq_real_number_of, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   178
                                    real_mult_minus_right RS sym]@
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   179
    [mult_real_number_of, real_mult_number_of_left]@bin_simps@real_mult_ac))
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   180
  val numeral_simp_tac	= 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   181
         ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   182
  val simplify_meta_eq  = simplify_meta_eq
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   183
  end
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   184
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   185
structure DivCancelNumeralFactor = CancelNumeralFactorFun
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   186
 (open CancelNumeralFactorCommon
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   187
  val prove_conv = prove_conv "realdiv_cancel_numeral_factor"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   188
  val mk_bal   = HOLogic.mk_binop "HOL.divide"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   189
  val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   190
  val cancel = real_mult_div_cancel1 RS trans
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   191
  val neg_exchanges = false
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   192
)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   193
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   194
structure EqCancelNumeralFactor = CancelNumeralFactorFun
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   195
 (open CancelNumeralFactorCommon
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   196
  val prove_conv = prove_conv "realeq_cancel_numeral_factor"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   197
  val mk_bal   = HOLogic.mk_eq
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   198
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   199
  val cancel = real_mult_eq_cancel1 RS trans
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   200
  val neg_exchanges = false
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   201
)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   202
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   203
structure LessCancelNumeralFactor = CancelNumeralFactorFun
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   204
 (open CancelNumeralFactorCommon
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   205
  val prove_conv = prove_conv "realless_cancel_numeral_factor"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   206
  val mk_bal   = HOLogic.mk_binrel "op <"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   207
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   208
  val cancel = real_mult_less_cancel1 RS trans
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   209
  val neg_exchanges = true
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   210
)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   211
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   212
structure LeCancelNumeralFactor = CancelNumeralFactorFun
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   213
 (open CancelNumeralFactorCommon
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   214
  val prove_conv = prove_conv "realle_cancel_numeral_factor"
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   215
  val mk_bal   = HOLogic.mk_binrel "op <="
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   216
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   217
  val cancel = real_mult_le_cancel1 RS trans
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   218
  val neg_exchanges = true
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   219
)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   220
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   221
val real_cancel_numeral_factors = 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   222
  map prep_simproc
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   223
   [("realeq_cancel_numeral_factors",
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   224
     prep_pats ["(l::real) * m = n", "(l::real) = m * n"], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   225
     EqCancelNumeralFactor.proc),
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   226
    ("realless_cancel_numeral_factors", 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   227
     prep_pats ["(l::real) * m < n", "(l::real) < m * n"], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   228
     LessCancelNumeralFactor.proc),
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   229
    ("realle_cancel_numeral_factors", 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   230
     prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   231
     LeCancelNumeralFactor.proc),
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   232
    ("realdiv_cancel_numeral_factors", 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   233
     prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   234
     DivCancelNumeralFactor.proc)];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   235
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   236
end;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   237
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   238
Addsimprocs real_cancel_numeral_factors;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   239
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   240
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   241
(*examples:
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   242
print_depth 22;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   243
set timing;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   244
set trace_simp;
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   245
fun test s = (Goal s; by (Simp_tac 1)); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   246
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   247
test "#0 <= (y::real) * #-2";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   248
test "#9*x = #12 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   249
test "(#9*x) / (#12 * (y::real)) = z";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   250
test "#9*x < #12 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   251
test "#9*x <= #12 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   252
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   253
test "#-99*x = #132 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   254
test "(#-99*x) / (#132 * (y::real)) = z";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   255
test "#-99*x < #132 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   256
test "#-99*x <= #132 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   257
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   258
test "#999*x = #-396 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   259
test "(#999*x) / (#-396 * (y::real)) = z";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   260
test "#999*x < #-396 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   261
test "#999*x <= #-396 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   262
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   263
test "#-99*x = #-81 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   264
test "(#-99*x) / (#-81 * (y::real)) = z";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   265
test "#-99*x <= #-81 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   266
test "#-99*x < #-81 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   267
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   268
test "#-2 * x = #-1 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   269
test "#-2 * x = -(y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   270
test "(#-2 * x) / (#-1 * (y::real)) = z";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   271
test "#-2 * x < -(y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   272
test "#-2 * x <= #-1 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   273
test "-x < #-23 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   274
test "-x <= #-23 * (y::real)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   275
*)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   276
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   277
(*** Simplification of inequalities involving literal divisors ***)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   278
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   279
Goal "#0<z ==> ((x::real) <= y/z) = (x*z <= y)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   280
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   281
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   282
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   283
by (stac real_mult_le_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   284
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   285
qed "pos_real_le_divide_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   286
Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   287
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   288
Goal "z<#0 ==> ((x::real) <= y/z) = (y <= x*z)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   289
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   290
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   291
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   292
by (stac real_mult_le_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   293
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   294
qed "neg_real_le_divide_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   295
Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   296
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   297
Goal "#0<z ==> (y/z <= (x::real)) = (y <= x*z)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   298
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   299
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   300
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   301
by (stac real_mult_le_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   302
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   303
qed "pos_real_divide_le_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   304
Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   305
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   306
Goal "z<#0 ==> (y/z <= (x::real)) = (x*z <= y)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   307
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   308
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   309
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   310
by (stac real_mult_le_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   311
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   312
qed "neg_real_divide_le_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   313
Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   314
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   315
Goal "#0<z ==> ((x::real) < y/z) = (x*z < y)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   316
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   317
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   318
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   319
by (stac real_mult_less_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   320
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   321
qed "pos_real_less_divide_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   322
Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   323
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   324
Goal "z<#0 ==> ((x::real) < y/z) = (y < x*z)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   325
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   326
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   327
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   328
by (stac real_mult_less_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   329
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   330
qed "neg_real_less_divide_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   331
Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   332
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   333
Goal "#0<z ==> (y/z < (x::real)) = (y < x*z)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   334
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   335
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   336
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   337
by (stac real_mult_less_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   338
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   339
qed "pos_real_divide_less_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   340
Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   341
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   342
Goal "z<#0 ==> (y/z < (x::real)) = (x*z < y)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   343
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   344
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   345
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   346
by (stac real_mult_less_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   347
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   348
qed "neg_real_divide_less_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   349
Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   350
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   351
Goal "z~=#0 ==> ((x::real) = y/z) = (x*z = y)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   352
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   353
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   354
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   355
by (stac real_mult_eq_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   356
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   357
qed "real_eq_divide_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   358
Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   359
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   360
Goal "z~=#0 ==> (y/z = (x::real)) = (y = x*z)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   361
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   362
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   363
by (etac ssubst 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   364
by (stac real_mult_eq_cancel2 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   365
by (Asm_simp_tac 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   366
qed "real_divide_eq_eq";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   367
Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   368
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   369
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   370
(** Moved from RealOrd.ML to use #0 **)
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   371
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   372
Goal "[| #0 < r; #0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   373
by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   374
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   375
by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   376
by (auto_tac (claset() addIs [real_inverse_less_swap],
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   377
	      simpset() delsimps [real_inverse_inverse]
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   378
			addsimps [real_inverse_gt_zero]));
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   379
qed "real_inverse_less_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   380
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   381
Goal "[| #0 < r; #0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   382
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   383
                                      real_inverse_less_iff]) 1); 
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   384
qed "real_inverse_le_iff";
a8c647cfa31f first stage in tidying up Real and Hyperreal.
paulson
parents: 10574
diff changeset
   385
10669
3e4f5ae4faa6 new theorem real_lbound_gt_zero
paulson
parents: 10660
diff changeset
   386
Goal "[| (#0::real) < d1; #0 < d2 |] ==> EX e. #0 < e & e < d1 & e < d2";
3e4f5ae4faa6 new theorem real_lbound_gt_zero
paulson
parents: 10660
diff changeset
   387
by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1); 
3e4f5ae4faa6 new theorem real_lbound_gt_zero
paulson
parents: 10660
diff changeset
   388
by (asm_simp_tac (simpset() addsimps [min_def]) 1); 
3e4f5ae4faa6 new theorem real_lbound_gt_zero
paulson
parents: 10660
diff changeset
   389
qed "real_lbound_gt_zero";