Restructured lin.arith.package and fixed a proof in RComplete.
authornipkow
Thu Sep 23 09:05:44 1999 +0200 (1999-09-23 ago)
changeset 7583d1b40e0464b1
parent 7582 2650c9c2ab7f
child 7584 5be4bb8e4e3f
Restructured lin.arith.package and fixed a proof in RComplete.
src/HOL/Real/RComplete.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/RealBin.ML
     1.1 --- a/src/HOL/Real/RComplete.ML	Thu Sep 23 09:04:36 1999 +0200
     1.2 +++ b/src/HOL/Real/RComplete.ML	Thu Sep 23 09:05:44 1999 +0200
     1.3 @@ -138,7 +138,6 @@
     1.4  by (asm_full_simp_tac
     1.5      (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym,
     1.6  			 real_add_minus_left,real_add_zero_left]) 1);
     1.7 -by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
     1.8  qed "lemma_real_complete1";
     1.9  
    1.10  Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S";
     2.1 --- a/src/HOL/Real/ROOT.ML	Thu Sep 23 09:04:36 1999 +0200
     2.2 +++ b/src/HOL/Real/ROOT.ML	Thu Sep 23 09:05:44 1999 +0200
     2.3 @@ -4,6 +4,8 @@
     2.4      Copyright   1998  University of Cambridge
     2.5  
     2.6  Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
     2.7 +
     2.8 +Linear real arithmetic is installed in RealBin.ML.
     2.9  *)
    2.10  
    2.11  writeln"Root file for HOL/Real";
     3.1 --- a/src/HOL/Real/RealBin.ML	Thu Sep 23 09:04:36 1999 +0200
     3.2 +++ b/src/HOL/Real/RealBin.ML	Thu Sep 23 09:05:44 1999 +0200
     3.3 @@ -151,3 +151,350 @@
     3.4  (*Perhaps add some theorems that aren't in the default simpset, as
     3.5    done in Integ/NatBin.ML*)
     3.6  
     3.7 +
     3.8 +(*  Author:     Tobias Nipkow, TU Muenchen
     3.9 +    Copyright   1999 TU Muenchen
    3.10 +
    3.11 +Instantiate linear arithmetic decision procedure for the reals.
    3.12 +FIXME: multiplication with constants (eg #2 * x) does not work yet.
    3.13 +Solution: there should be a simproc for combining coefficients.
    3.14 +*)
    3.15 +
    3.16 +let
    3.17 +
    3.18 +(* reduce contradictory <= to False *)
    3.19 +val simps = [order_less_irrefl,zero_eq_numeral_0,one_eq_numeral_1,
    3.20 +  add_real_number_of,minus_real_number_of,diff_real_number_of,
    3.21 +  mult_real_number_of,eq_real_number_of,less_real_number_of,
    3.22 +  le_real_number_of_eq_not_less];
    3.23 +
    3.24 +val simprocs = [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
    3.25 +
    3.26 +val add_mono_thms =
    3.27 +  map (fn s => prove_goal thy s
    3.28 +                 (fn prems => [cut_facts_tac prems 1,
    3.29 +                      asm_simp_tac (simpset() addsimps
    3.30 +     [real_add_le_mono,real_add_less_mono,
    3.31 +      real_add_less_le_mono,real_add_le_less_mono]) 1]))
    3.32 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
    3.33 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
    3.34 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
    3.35 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::real)",
    3.36 +     "(i < j) & (k = l)   ==> i + k < j + (l::real)",
    3.37 +     "(i = j) & (k < l)   ==> i + k < j + (l::real)",
    3.38 +     "(i < j) & (k <= l)  ==> i + k < j + (l::real)",
    3.39 +     "(i <= j) & (k < l)  ==> i + k < j + (l::real)",
    3.40 +     "(i < j) & (k < l)   ==> i + k < j + (l::real)"];
    3.41 +
    3.42 +in
    3.43 +LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
    3.44 +LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps simps
    3.45 +                      addsimprocs simprocs;
    3.46 +LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("RealDef.real",false)]
    3.47 +end;
    3.48 +
    3.49 +let
    3.50 +val real_arith_simproc_pats =
    3.51 +  map (fn s => Thm.read_cterm (Theory.sign_of thy) (s, HOLogic.boolT))
    3.52 +      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
    3.53 +
    3.54 +val fast_real_arith_simproc = mk_simproc
    3.55 +  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
    3.56 +in
    3.57 +Addsimprocs [fast_real_arith_simproc]
    3.58 +end;
    3.59 +
    3.60 +Goalw [rabs_def]
    3.61 +  "P(rabs x) = ((#0 <= x --> P x) & (x < #0 --> P(-x)))";
    3.62 +by(auto_tac (claset(), simpset() addsimps [zero_eq_numeral_0]));
    3.63 +qed "rabs_split";
    3.64 +
    3.65 +arith_tac_split_thms := !arith_tac_split_thms @ [rabs_split];
    3.66 +
    3.67 +(** Tests **)
    3.68 +Goal "(x + y = x) = (y = (#0::real))";
    3.69 +by(arith_tac 1);
    3.70 +
    3.71 +Goal "(x + y = y) = (x = (#0::real))";
    3.72 +by(arith_tac 1);
    3.73 +
    3.74 +Goal "(x + y = (#0::real)) = (x = -y)";
    3.75 +by(arith_tac 1);
    3.76 +
    3.77 +Goal "(x + y = (#0::real)) = (y = -x)";
    3.78 +by(arith_tac 1);
    3.79 +
    3.80 +Goal "((x + y) < (x + z)) = (y < (z::real))";
    3.81 +by(arith_tac 1);
    3.82 +
    3.83 +Goal "((x + z) < (y + z)) = (x < (y::real))";
    3.84 +by(arith_tac 1);
    3.85 +
    3.86 +Goal "(~ x < y) = (y <= (x::real))";
    3.87 +by(arith_tac 1);
    3.88 +
    3.89 +Goal "~(x < y & y < (x::real))";
    3.90 +by(arith_tac 1);
    3.91 +
    3.92 +Goal "(x::real) < y ==> ~ y < x";
    3.93 +by(arith_tac 1);
    3.94 +
    3.95 +Goal "((x::real) ~= y) = (x < y | y < x)";
    3.96 +by(arith_tac 1);
    3.97 +
    3.98 +Goal "(~ x <= y) = (y < (x::real))";
    3.99 +by(arith_tac 1);
   3.100 +
   3.101 +Goal "x <= y | y <= (x::real)";
   3.102 +by(arith_tac 1);
   3.103 +
   3.104 +Goal "x <= y | y < (x::real)";
   3.105 +by(arith_tac 1);
   3.106 +
   3.107 +Goal "x < y | y <= (x::real)";
   3.108 +by(arith_tac 1);
   3.109 +
   3.110 +Goal "x <= (x::real)";
   3.111 +by(arith_tac 1);
   3.112 +
   3.113 +Goal "((x::real) <= y) = (x < y | x = y)";
   3.114 +by(arith_tac 1);
   3.115 +
   3.116 +Goal "((x::real) <= y & y <= x) = (x = y)";
   3.117 +by(arith_tac 1);
   3.118 +
   3.119 +Goal "~(x < y & y <= (x::real))";
   3.120 +by(arith_tac 1);
   3.121 +
   3.122 +Goal "~(x <= y & y < (x::real))";
   3.123 +by(arith_tac 1);
   3.124 +
   3.125 +Goal "(-x < (#0::real)) = (#0 < x)";
   3.126 +by(arith_tac 1);
   3.127 +
   3.128 +Goal "((#0::real) < -x) = (x < #0)";
   3.129 +by(arith_tac 1);
   3.130 +
   3.131 +Goal "(-x <= (#0::real)) = (#0 <= x)";
   3.132 +by(arith_tac 1);
   3.133 +
   3.134 +Goal "((#0::real) <= -x) = (x <= #0)";
   3.135 +by(arith_tac 1);
   3.136 +
   3.137 +Goal "(x::real) = y | x < y | y < x";
   3.138 +by(arith_tac 1);
   3.139 +
   3.140 +Goal "(x::real) = #0 | #0 < x | #0 < -x";
   3.141 +by(arith_tac 1);
   3.142 +
   3.143 +Goal "(#0::real) <= x | #0 <= -x";
   3.144 +by(arith_tac 1);
   3.145 +
   3.146 +Goal "((x::real) + y <= x + z) = (y <= z)";
   3.147 +by(arith_tac 1);
   3.148 +
   3.149 +Goal "((x::real) + z <= y + z) = (x <= y)";
   3.150 +by(arith_tac 1);
   3.151 +
   3.152 +Goal "(w::real) < x & y < z ==> w + y < x + z";
   3.153 +by(arith_tac 1);
   3.154 +
   3.155 +Goal "(w::real) <= x & y <= z ==> w + y <= x + z";
   3.156 +by(arith_tac 1);
   3.157 +
   3.158 +Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y";
   3.159 +by(arith_tac 1);
   3.160 +
   3.161 +Goal "(#0::real) < x & #0 < y ==> #0 < x + y";
   3.162 +by(arith_tac 1);
   3.163 +
   3.164 +Goal "(-x < y) = (#0 < x + (y::real))";
   3.165 +by(arith_tac 1);
   3.166 +
   3.167 +Goal "(x < -y) = (x + y < (#0::real))";
   3.168 +by(arith_tac 1);
   3.169 +
   3.170 +Goal "(y < x + -z) = (y + z < (x::real))";
   3.171 +by(arith_tac 1);
   3.172 +
   3.173 +Goal "(x + -y < z) = (x < z + (y::real))";
   3.174 +by(arith_tac 1);
   3.175 +
   3.176 +Goal "x <= y ==> x < y + (#1::real)";
   3.177 +by(arith_tac 1);
   3.178 +
   3.179 +Goal "(x - y) + y = (x::real)";
   3.180 +by(arith_tac 1);
   3.181 +
   3.182 +Goal "y + (x - y) = (x::real)";
   3.183 +by(arith_tac 1);
   3.184 +
   3.185 +Goal "x - x = (#0::real)";
   3.186 +by(arith_tac 1);
   3.187 +
   3.188 +Goal "(x - y = #0) = (x = (y::real))";
   3.189 +by(arith_tac 1);
   3.190 +
   3.191 +Goal "((#0::real) <= x + x) = (#0 <= x)";
   3.192 +by(arith_tac 1);
   3.193 +
   3.194 +Goal "(-x <= x) = ((#0::real) <= x)";
   3.195 +by(arith_tac 1);
   3.196 +
   3.197 +Goal "(x <= -x) = (x <= (#0::real))";
   3.198 +by(arith_tac 1);
   3.199 +
   3.200 +Goal "(-x = (#0::real)) = (x = #0)";
   3.201 +by(arith_tac 1);
   3.202 +
   3.203 +Goal "-(x - y) = y - (x::real)";
   3.204 +by(arith_tac 1);
   3.205 +
   3.206 +Goal "((#0::real) < x - y) = (y < x)";
   3.207 +by(arith_tac 1);
   3.208 +
   3.209 +Goal "((#0::real) <= x - y) = (y <= x)";
   3.210 +by(arith_tac 1);
   3.211 +
   3.212 +Goal "(x + y) - x = (y::real)";
   3.213 +by(arith_tac 1);
   3.214 +
   3.215 +Goal "(-x = y) = (x = (-y::real))";
   3.216 +by(arith_tac 1);
   3.217 +
   3.218 +Goal "x < (y::real) ==> ~(x = y)";
   3.219 +by(arith_tac 1);
   3.220 +
   3.221 +Goal "(x <= x + y) = ((#0::real) <= y)";
   3.222 +by(arith_tac 1);
   3.223 +
   3.224 +Goal "(y <= x + y) = ((#0::real) <= x)";
   3.225 +by(arith_tac 1);
   3.226 +
   3.227 +Goal "(x < x + y) = ((#0::real) < y)";
   3.228 +by(arith_tac 1);
   3.229 +
   3.230 +Goal "(y < x + y) = ((#0::real) < x)";
   3.231 +by(arith_tac 1);
   3.232 +
   3.233 +Goal "(x - y) - x = (-y::real)";
   3.234 +by(arith_tac 1);
   3.235 +
   3.236 +Goal "(x + y < z) = (x < z - (y::real))";
   3.237 +by(arith_tac 1);
   3.238 +
   3.239 +Goal "(x - y < z) = (x < z + (y::real))";
   3.240 +by(arith_tac 1);
   3.241 +
   3.242 +Goal "(x < y - z) = (x + z < (y::real))";
   3.243 +by(arith_tac 1);
   3.244 +
   3.245 +Goal "(x <= y - z) = (x + z <= (y::real))";
   3.246 +by(arith_tac 1);
   3.247 +
   3.248 +Goal "(x - y <= z) = (x <= z + (y::real))";
   3.249 +by(arith_tac 1);
   3.250 +
   3.251 +Goal "(-x < -y) = (y < (x::real))";
   3.252 +by(arith_tac 1);
   3.253 +
   3.254 +Goal "(-x <= -y) = (y <= (x::real))";
   3.255 +by(arith_tac 1);
   3.256 +
   3.257 +Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))";
   3.258 +by(arith_tac 1);
   3.259 +
   3.260 +Goal "(#0::real) - x = -x";
   3.261 +by(arith_tac 1);
   3.262 +
   3.263 +Goal "x - (#0::real) = x";
   3.264 +by(arith_tac 1);
   3.265 +
   3.266 +Goal "w <= x & y < z ==> w + y < x + (z::real)";
   3.267 +by(arith_tac 1);
   3.268 +
   3.269 +Goal "w < x & y <= z ==> w + y < x + (z::real)";
   3.270 +by(arith_tac 1);
   3.271 +
   3.272 +Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)";
   3.273 +by(arith_tac 1);
   3.274 +
   3.275 +Goal "(#0::real) < x & #0 <= y ==> #0 < x + y";
   3.276 +by(arith_tac 1);
   3.277 +
   3.278 +Goal "-x - y = -(x + (y::real))";
   3.279 +by(arith_tac 1);
   3.280 +
   3.281 +Goal "x - (-y) = x + (y::real)";
   3.282 +by(arith_tac 1);
   3.283 +
   3.284 +Goal "-x - -y = y - (x::real)";
   3.285 +by(arith_tac 1);
   3.286 +
   3.287 +Goal "(a - b) + (b - c) = a - (c::real)";
   3.288 +by(arith_tac 1);
   3.289 +
   3.290 +Goal "(x = y - z) = (x + z = (y::real))";
   3.291 +by(arith_tac 1);
   3.292 +
   3.293 +Goal "(x - y = z) = (x = z + (y::real))";
   3.294 +by(arith_tac 1);
   3.295 +
   3.296 +Goal "x - (x - y) = (y::real)";
   3.297 +by(arith_tac 1);
   3.298 +
   3.299 +Goal "x - (x + y) = -(y::real)";
   3.300 +by(arith_tac 1);
   3.301 +
   3.302 +Goal "x = y ==> x <= (y::real)";
   3.303 +by(arith_tac 1);
   3.304 +
   3.305 +Goal "(#0::real) < x ==> ~(x = #0)";
   3.306 +by(arith_tac 1);
   3.307 +
   3.308 +Goal "(x + y) * (x - y) = (x * x) - (y * y)";
   3.309 +
   3.310 +Goal "(-x = -y) = (x = (y::real))";
   3.311 +by(arith_tac 1);
   3.312 +
   3.313 +Goal "(-x < -y) = (y < (x::real))";
   3.314 +by(arith_tac 1);
   3.315 +
   3.316 +Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   3.317 +by (fast_arith_tac 1);
   3.318 +
   3.319 +Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)";
   3.320 +by (fast_arith_tac 1);
   3.321 +
   3.322 +Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
   3.323 +by (fast_arith_tac 1);
   3.324 +
   3.325 +Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] \
   3.326 +\     ==> a+a <= j+j";
   3.327 +by (fast_arith_tac 1);
   3.328 +
   3.329 +Goal "!!a::real. [| a+b < i+j; a<b; i<j |] \
   3.330 +\     ==> a+a < j+j";
   3.331 +by (fast_arith_tac 1);
   3.332 +
   3.333 +Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   3.334 +by (arith_tac 1);
   3.335 +
   3.336 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   3.337 +\     ==> a <= l";
   3.338 +by (fast_arith_tac 1);
   3.339 +
   3.340 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   3.341 +\     ==> a+a+a+a <= l+l+l+l";
   3.342 +by (fast_arith_tac 1);
   3.343 +
   3.344 +(* Too slow. Needs "combine_coefficients" simproc
   3.345 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   3.346 +\     ==> a+a+a+a+a <= l+l+l+l+i";
   3.347 +by (fast_arith_tac 1);
   3.348 +
   3.349 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   3.350 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   3.351 +by (fast_arith_tac 1);
   3.352 +*)
   3.353 +