src/HOL/Real/RealAbs.ML
author paulson
Thu Oct 01 18:18:01 1998 +0200 (1998-10-01)
changeset 5588 a3ab526bb891
parent 5459 1dbaf888f4e7
child 7077 60b098bb8b8a
permissions -rw-r--r--
Revised version with Abelian group simprocs
     1 (*  Title       : RealAbs.ML
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Description : Absolute value function for the reals
     5 *) 
     6 
     7 (*----------------------------------------------------------------------------
     8        Properties of the absolute value function over the reals
     9        (adapted version of previously proved theorems about abs)
    10  ----------------------------------------------------------------------------*)
    11 Goalw [rabs_def] "rabs r = (if 0r<=r then r else -r)";
    12 by Auto_tac;
    13 qed "rabs_iff";
    14 
    15 Goalw [rabs_def] "rabs 0r = 0r";
    16 by (rtac (real_le_refl RS if_P) 1);
    17 qed "rabs_zero";
    18 
    19 Addsimps [rabs_zero];
    20 
    21 Goalw [rabs_def] "rabs 0r = -0r";
    22 by (stac real_minus_zero 1);
    23 by (rtac if_cancel 1);
    24 qed "rabs_minus_zero";
    25 
    26 val [prem] = goalw thy [rabs_def] "0r<=x ==> rabs x = x";
    27 by (rtac (prem RS if_P) 1);
    28 qed "rabs_eqI1";
    29 
    30 val [prem] = goalw thy [rabs_def] "0r<x ==> rabs x = x";
    31 by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1);
    32 qed "rabs_eqI2";
    33 
    34 val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
    35 by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
    36 qed "rabs_minus_eqI2";
    37 
    38 Goal "x<=0r ==> rabs x = -x";
    39 by (dtac real_le_imp_less_or_eq 1);
    40 by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
    41 qed "rabs_minus_eqI1";
    42 
    43 Goalw [rabs_def,real_le_def] "0r<= rabs x";
    44 by (Full_simp_tac 1);
    45 by (blast_tac (claset() addDs [real_minus_zero_less_iff RS iffD2,
    46 			       real_less_asym]) 1);
    47 qed "rabs_ge_zero";
    48 
    49 Goal "rabs(rabs x)=rabs x";
    50 by (res_inst_tac [("r1","rabs x")] (rabs_iff RS ssubst) 1);
    51 by (blast_tac (claset() addIs [if_P,rabs_ge_zero]) 1);
    52 qed "rabs_idempotent";
    53 
    54 Goalw [rabs_def] "(x=0r) = (rabs x = 0r)";
    55 by (Full_simp_tac 1);
    56 qed "rabs_zero_iff";
    57 
    58 Goal  "(x ~= 0r) = (rabs x ~= 0r)";
    59 by (full_simp_tac (simpset() addsimps [rabs_zero_iff RS sym]) 1);
    60 qed "rabs_not_zero_iff";
    61 
    62 Goalw [rabs_def] "x<=rabs x";
    63 by (Full_simp_tac 1);
    64 by (auto_tac (claset() addDs [not_real_leE RS real_less_imp_le],
    65 	      simpset() addsimps [real_le_zero_iff]));
    66 qed "rabs_ge_self";
    67 
    68 Goalw [rabs_def] "-x<=rabs x";
    69 by (full_simp_tac (simpset() addsimps [real_ge_zero_iff]) 1);
    70 qed "rabs_ge_minus_self";
    71 
    72 (* case splits nightmare *)
    73 Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)";
    74 by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1,
    75    real_minus_mult_commute,real_minus_mult_eq2]));
    76 by (blast_tac (claset() addDs [real_le_mult_order]) 1);
    77 by (auto_tac (claset() addSDs [not_real_leE],simpset()));
    78 by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
    79 by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
    80 by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
    81 by (auto_tac (claset() addDs [real_less_asym,sym],
    82     simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
    83 qed "rabs_mult";
    84 
    85 Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
    86 by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] 
    87    ));
    88 by (ALLGOALS(dtac not_real_leE));
    89 by (etac real_less_asym 1);
    90 by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
    91           real_rinv_gt_zero]) 1);
    92 by (dtac (rinv_not_zero RS not_sym) 1);
    93 by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1);
    94 by (assume_tac 2);
    95 by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1);
    96 qed "rabs_rinv";
    97 
    98 val [prem] = goal thy "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))";
    99 by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1);
   100 by (simp_tac (simpset() addsimps [(rabs_not_zero_iff RS sym), prem]) 1);
   101 by (simp_tac (simpset() addsimps [(rabs_mult RS sym) ,real_mult_inv_right, 
   102     prem,rabs_not_zero_iff RS sym] @ real_mult_ac) 1);
   103 qed "rabs_mult_rinv";
   104 
   105 Goal "rabs(x+y) <= rabs x + rabs y";
   106 by (EVERY1 [res_inst_tac [("Q1","0r<=x+y")] (expand_if RS ssubst), rtac conjI]);
   107 by (asm_simp_tac
   108     (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
   109 by (asm_simp_tac 
   110     (simpset() addsimps [not_real_leE,rabs_minus_eqI2,real_add_le_mono,
   111 			 rabs_ge_minus_self]) 1);
   112 qed "rabs_triangle_ineq";
   113 
   114 Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)";
   115 by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   116 by (blast_tac (claset() addSIs [(rabs_triangle_ineq RS real_le_trans),
   117 				real_add_left_le_mono1]) 1);
   118 qed "rabs_triangle_ineq_four";
   119 
   120 Goalw [rabs_def] "rabs(-x)=rabs(x)";
   121 by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] addIs [real_le_anti_sym],
   122    simpset() addsimps [real_ge_zero_iff]));
   123 qed "rabs_minus_cancel";
   124 
   125 Goal "rabs(x + -y) <= rabs x + rabs y";
   126 by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
   127 by (rtac rabs_triangle_ineq 1);
   128 qed "rabs_triangle_minus_ineq";
   129 
   130 Goal "rabs (x + y + (-l + -m)) <= rabs(x + -l) + rabs(y + -m)";
   131 by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   132 by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
   133 by (rtac (real_add_assoc RS subst) 1);
   134 by (rtac rabs_triangle_ineq 1);
   135 qed "rabs_sum_triangle_ineq";
   136 
   137 Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
   138 by (rtac real_le_less_trans 1);
   139 by (rtac rabs_triangle_ineq 1);
   140 by (REPEAT (ares_tac [real_add_less_mono] 1));
   141 qed "rabs_add_less";
   142 
   143 Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ -y) < r+s";
   144 by (rotate_tac 1 1);
   145 by (dtac (rabs_minus_cancel RS ssubst) 1);
   146 by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
   147 qed "rabs_add_minus_less";
   148 
   149 (* lemmas manipulating terms *)
   150 Goal "(0r*x<r)=(0r<r)";
   151 by (Simp_tac 1);
   152 qed "real_mult_0_less";
   153 
   154 Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s";
   155 by (blast_tac (claset() addSIs [real_mult_less_mono2]
   156 	                addIs  [real_less_trans]) 1);
   157 qed "real_mult_less_trans";
   158 
   159 Goal "!!(x::real) y.[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
   160 by (dtac real_le_imp_less_or_eq 1);
   161 by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
   162 			    real_mult_less_trans]) 1);
   163 qed "real_mult_le_less_trans";
   164 
   165 (* proofs lifted from previous older version *)
   166 Goal "[| rabs x<r; rabs y<s |] ==> rabs(x*y)<r*s";
   167 by (simp_tac (simpset() addsimps [rabs_mult]) 1);
   168 by (rtac real_mult_le_less_trans 1);
   169 by (rtac rabs_ge_zero 1);
   170 by (assume_tac 1);
   171 by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_less_mono1, 
   172 			     real_le_less_trans]) 1);
   173 by (blast_tac (HOL_cs addIs [rabs_ge_zero, real_mult_order, 
   174 			     real_le_less_trans]) 1);
   175 qed "rabs_mult_less";
   176 
   177 Goal "[| rabs x < r; rabs y < s |] ==> rabs(x)*rabs(y)<r*s";
   178 by (auto_tac (claset() addIs [rabs_mult_less],
   179               simpset() addsimps [rabs_mult RS sym]));
   180 qed "rabs_mult_less2";
   181 
   182 Goal "1r < rabs x ==> rabs y <= rabs(x*y)";
   183 by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
   184 by (EVERY1[etac disjE,rtac real_less_imp_le]);
   185 by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
   186 by (forw_inst_tac [("y","rabs x + -1r")] real_mult_order 1);
   187 by (assume_tac 1);
   188 by (rtac real_sum_gt_zero_less 1);
   189 by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
   190     real_mult_commute, rabs_mult]) 1);
   191 by (dtac sym 1);
   192 by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1);
   193 qed "rabs_mult_le";
   194 
   195 Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
   196 by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
   197 qed "rabs_mult_gt";
   198 
   199 Goal "rabs(x)<r ==> 0r<r";
   200 by (blast_tac (claset() addSIs [real_le_less_trans,rabs_ge_zero]) 1);
   201 qed "rabs_less_gt_zero";
   202 
   203 Goalw [rabs_def] "rabs 1r = 1r";
   204 by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym],
   205    simpset() addsimps [real_zero_less_one]));
   206 qed "rabs_one";
   207 
   208 Goal "[| 0r < x ; x < r |] ==> rabs x < r";
   209 by (asm_simp_tac (simpset() addsimps [rabs_eqI2]) 1);
   210 qed "rabs_lessI";
   211 
   212 Goal "rabs x =x | rabs x = -x";
   213 by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
   214 by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
   215                             rabs_zero,rabs_minus_zero]) 1);
   216 qed "rabs_disj";
   217 
   218 Goal "rabs x = y ==> x = y | -x = y";
   219 by (dtac sym 1);
   220 by (hyp_subst_tac 1);
   221 by (res_inst_tac [("x1","x")] (rabs_disj RS disjE) 1);
   222 by (REPEAT(Asm_simp_tac 1));
   223 qed "rabs_eq_disj";
   224 
   225 Goal "(rabs x < r) = (-r<x & x<r)";
   226 by Safe_tac;
   227 by (rtac (real_less_swap_iff RS iffD2) 1);
   228 by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
   229     RS real_le_less_trans)]) 1);
   230 by (asm_simp_tac (simpset() addsimps [(rabs_ge_self 
   231     RS real_le_less_trans)]) 1);
   232 by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, 
   233             dtac (real_minus_minus RS subst), 
   234             cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]);
   235 by (assume_tac 3 THEN Auto_tac);
   236 qed "rabs_interval_iff";
   237