installing the cancel_numerals and combine_numerals simprocs
authorpaulson
Wed Jun 14 18:19:20 2000 +0200 (2000-06-14)
changeset 9068202fdf72cf23
parent 9067 64464b5f6867
child 9069 e8d530582061
installing the cancel_numerals and combine_numerals simprocs
src/HOL/Real/RealBin.ML
     1.1 --- a/src/HOL/Real/RealBin.ML	Wed Jun 14 18:00:46 2000 +0200
     1.2 +++ b/src/HOL/Real/RealBin.ML	Wed Jun 14 18:19:20 2000 +0200
     1.3 @@ -121,7 +121,8 @@
     1.4      HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
     1.5  		     minus_numeral_one];
     1.6  
     1.7 -fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
     1.8 +fun rename_numerals thy th = 
     1.9 +    asm_full_simplify real_numeral_ss (change_theory thy th);
    1.10  
    1.11  
    1.12  (*Now insert some identities previously stated for 0 and 1r*)
    1.13 @@ -138,14 +139,14 @@
    1.14  
    1.15  AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]);
    1.16  
    1.17 -bind_thm ("real_0_less_times_iff", 
    1.18 -	  rename_numerals thy real_zero_less_times_iff);
    1.19 -bind_thm ("real_0_le_times_iff", 
    1.20 -	  rename_numerals thy real_zero_le_times_iff);
    1.21 -bind_thm ("real_times_less_0_iff", 
    1.22 -	  rename_numerals thy real_times_less_zero_iff);
    1.23 -bind_thm ("real_times_le_0_iff", 
    1.24 -	  rename_numerals thy real_times_le_zero_iff);
    1.25 +bind_thm ("real_0_less_mult_iff", 
    1.26 +	  rename_numerals thy real_zero_less_mult_iff);
    1.27 +bind_thm ("real_0_le_mult_iff", 
    1.28 +	  rename_numerals thy real_zero_le_mult_iff);
    1.29 +bind_thm ("real_mult_less_0_iff", 
    1.30 +	  rename_numerals thy real_mult_less_zero_iff);
    1.31 +bind_thm ("real_mult_le_0_iff", 
    1.32 +	  rename_numerals thy real_mult_le_zero_iff);
    1.33  
    1.34  
    1.35  (*Perhaps add some theorems that aren't in the default simpset, as
    1.36 @@ -207,10 +208,6 @@
    1.37  
    1.38  Addsimps [zero_eq_numeral_0,one_eq_numeral_1];
    1.39  
    1.40 -(* added by jdf *)
    1.41 -fun full_rename_numerals thy th = 
    1.42 -    asm_full_simplify real_numeral_ss (change_theory thy th);
    1.43 -
    1.44  
    1.45  (** Simplification of arithmetic when nested to the right **)
    1.46  
    1.47 @@ -236,3 +233,461 @@
    1.48  Addsimps [real_add_number_of_left, real_mult_number_of_left,
    1.49  	  real_add_number_of_diff1, real_add_number_of_diff2]; 
    1.50  
    1.51 +
    1.52 +(*"neg" is used in rewrite rules for binary comparisons*)
    1.53 +Goal "real_of_nat (number_of v :: nat) = \
    1.54 +\        (if neg (number_of v) then #0 \
    1.55 +\         else (number_of v :: real))";
    1.56 +by (simp_tac
    1.57 +    (simpset_of Int.thy addsimps [nat_number_of_def, real_of_nat_real_of_int,
    1.58 +				  real_of_nat_neg_int, real_number_of,
    1.59 +				  zero_eq_numeral_0]) 1);
    1.60 +qed "real_of_nat_number_of";
    1.61 +Addsimps [real_of_nat_number_of];
    1.62 +
    1.63 +
    1.64 +(**** Simprocs for numeric literals ****)
    1.65 +
    1.66 +(** Combining of literal coefficients in sums of products **)
    1.67 +
    1.68 +Goal "(x < y) = (x-y < (#0::real))";
    1.69 +by Auto_tac; 
    1.70 +qed "real_less_iff_diff_less_0";
    1.71 +
    1.72 +Goal "(x = y) = (x-y = (#0::real))";
    1.73 +by Auto_tac; 
    1.74 +qed "real_eq_iff_diff_eq_0";
    1.75 +
    1.76 +Goal "(x <= y) = (x-y <= (#0::real))";
    1.77 +by Auto_tac; 
    1.78 +qed "real_le_iff_diff_le_0";
    1.79 +
    1.80 +
    1.81 +(** For combine_numerals **)
    1.82 +
    1.83 +Goal "i*u + (j*u + k) = (i+j)*u + (k::real)";
    1.84 +by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
    1.85 +qed "left_real_add_mult_distrib";
    1.86 +
    1.87 +
    1.88 +(** For cancel_numerals **)
    1.89 +
    1.90 +val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
    1.91 +                          [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0, 
    1.92 +			   real_le_iff_diff_le_0] @
    1.93 +		        map (inst "y" "n")
    1.94 +                          [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0, 
    1.95 +			   real_le_iff_diff_le_0];
    1.96 +
    1.97 +Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    1.98 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
    1.99 +		                     real_add_ac@rel_iff_rel_0_rls) 1);
   1.100 +qed "real_eq_add_iff1";
   1.101 +
   1.102 +Goal "!!i::real. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
   1.103 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
   1.104 +                                     real_add_ac@rel_iff_rel_0_rls) 1);
   1.105 +qed "real_eq_add_iff2";
   1.106 +
   1.107 +Goal "!!i::real. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
   1.108 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
   1.109 +                                     real_add_ac@rel_iff_rel_0_rls) 1);
   1.110 +qed "real_less_add_iff1";
   1.111 +
   1.112 +Goal "!!i::real. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
   1.113 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
   1.114 +                                     real_add_ac@rel_iff_rel_0_rls) 1);
   1.115 +qed "real_less_add_iff2";
   1.116 +
   1.117 +Goal "!!i::real. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
   1.118 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
   1.119 +                                     real_add_ac@rel_iff_rel_0_rls) 1);
   1.120 +qed "real_le_add_iff1";
   1.121 +
   1.122 +Goal "!!i::real. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
   1.123 +by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]
   1.124 +                                     @real_add_ac@rel_iff_rel_0_rls) 1);
   1.125 +qed "real_le_add_iff2";
   1.126 +
   1.127 +
   1.128 +structure Real_Numeral_Simprocs =
   1.129 +struct
   1.130 +
   1.131 +(*Utilities*)
   1.132 +
   1.133 +fun mk_numeral n = HOLogic.number_of_const HOLogic.realT $ 
   1.134 +                   NumeralSyntax.mk_bin n;
   1.135 +
   1.136 +(*Decodes a binary real constant*)
   1.137 +fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
   1.138 +     (NumeralSyntax.dest_bin w
   1.139 +      handle Match => raise TERM("Real_Numeral_Simprocs.dest_numeral:1", [w]))
   1.140 +  | dest_numeral t = raise TERM("Real_Numeral_Simprocs.dest_numeral:2", [t]);
   1.141 +
   1.142 +fun find_first_numeral past (t::terms) =
   1.143 +	((dest_numeral t, rev past @ terms)
   1.144 +	 handle TERM _ => find_first_numeral (t::past) terms)
   1.145 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
   1.146 +
   1.147 +val zero = mk_numeral 0;
   1.148 +val mk_plus = HOLogic.mk_binop "op +";
   1.149 +
   1.150 +val uminus_const = Const ("uminus", HOLogic.realT --> HOLogic.realT);
   1.151 +
   1.152 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   1.153 +fun mk_sum []        = zero
   1.154 +  | mk_sum [t,u]     = mk_plus (t, u)
   1.155 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.156 +
   1.157 +(*this version ALWAYS includes a trailing zero*)
   1.158 +fun long_mk_sum []        = zero
   1.159 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.160 +
   1.161 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.realT;
   1.162 +
   1.163 +(*decompose additions AND subtractions as a sum*)
   1.164 +fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   1.165 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   1.166 +  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   1.167 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   1.168 +  | dest_summing (pos, t, ts) =
   1.169 +	if pos then t::ts else uminus_const$t :: ts;
   1.170 +
   1.171 +fun dest_sum t = dest_summing (true, t, []);
   1.172 +
   1.173 +val mk_diff = HOLogic.mk_binop "op -";
   1.174 +val dest_diff = HOLogic.dest_bin "op -" HOLogic.realT;
   1.175 +
   1.176 +val one = mk_numeral 1;
   1.177 +val mk_times = HOLogic.mk_binop "op *";
   1.178 +
   1.179 +fun mk_prod [] = one
   1.180 +  | mk_prod [t] = t
   1.181 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   1.182 +                        else mk_times (t, mk_prod ts);
   1.183 +
   1.184 +val dest_times = HOLogic.dest_bin "op *" HOLogic.realT;
   1.185 +
   1.186 +fun dest_prod t =
   1.187 +      let val (t,u) = dest_times t 
   1.188 +      in  dest_prod t @ dest_prod u  end
   1.189 +      handle TERM _ => [t];
   1.190 +
   1.191 +(*DON'T do the obvious simplifications; that would create special cases*) 
   1.192 +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   1.193 +
   1.194 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   1.195 +fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   1.196 +  | dest_coeff sign t =
   1.197 +    let val ts = sort Term.term_ord (dest_prod t)
   1.198 +	val (n, ts') = find_first_numeral [] ts
   1.199 +                          handle TERM _ => (1, ts)
   1.200 +    in (sign*n, mk_prod ts') end;
   1.201 +
   1.202 +(*Find first coefficient-term THAT MATCHES u*)
   1.203 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   1.204 +  | find_first_coeff past u (t::terms) =
   1.205 +	let val (n,u') = dest_coeff 1 t
   1.206 +	in  if u aconv u' then (n, rev past @ terms)
   1.207 +			  else find_first_coeff (t::past) u terms
   1.208 +	end
   1.209 +	handle TERM _ => find_first_coeff (t::past) u terms;
   1.210 +
   1.211 +
   1.212 +(*Simplify #1*n and n*#1 to n*)
   1.213 +val add_0s = map (rename_numerals thy) 
   1.214 +                 [real_add_zero_left, real_add_zero_right];
   1.215 +val mult_1s = map (rename_numerals thy) 
   1.216 +                  [real_mult_1, real_mult_1_right, 
   1.217 +		   real_mult_minus_1, real_mult_minus_1_right];
   1.218 +
   1.219 +(*To perform binary arithmetic*)
   1.220 +val bin_simps = 
   1.221 +    [add_real_number_of, real_add_number_of_left, minus_real_number_of, 
   1.222 +     diff_real_number_of] @ 
   1.223 +    bin_arith_simps @ bin_rel_simps;
   1.224 +
   1.225 +(*To evaluate binary negations of coefficients*)
   1.226 +val real_minus_simps = NCons_simps @
   1.227 +                   [minus_real_number_of, 
   1.228 +		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   1.229 +		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   1.230 +
   1.231 +(*To let us treat subtraction as addition*)
   1.232 +val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus];
   1.233 +
   1.234 +(*Apply the given rewrite (if present) just once*)
   1.235 +fun trans_tac None      = all_tac
   1.236 +  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
   1.237 +
   1.238 +fun prove_conv name tacs sg (t, u) =
   1.239 +  if t aconv u then None
   1.240 +  else
   1.241 +  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
   1.242 +  in Some
   1.243 +     (prove_goalw_cterm [] ct (K tacs)
   1.244 +      handle ERROR => error 
   1.245 +	  ("The error(s) above occurred while trying to prove " ^
   1.246 +	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   1.247 +  end;
   1.248 +
   1.249 +(*Final simplification: cancel + and *  *)
   1.250 +val simplify_meta_eq = 
   1.251 +    Int_Numeral_Simprocs.simplify_meta_eq
   1.252 +         [real_add_zero_left, real_add_zero_right,
   1.253 + 	  real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
   1.254 +
   1.255 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.256 +fun prep_pat s = Thm.read_cterm (Theory.sign_of RealInt.thy) (s, HOLogic.termT);
   1.257 +val prep_pats = map prep_pat;
   1.258 +
   1.259 +structure CancelNumeralsCommon =
   1.260 +  struct
   1.261 +  val mk_sum    	= mk_sum
   1.262 +  val dest_sum		= dest_sum
   1.263 +  val mk_coeff		= mk_coeff
   1.264 +  val dest_coeff	= dest_coeff 1
   1.265 +  val find_first_coeff	= find_first_coeff []
   1.266 +  val trans_tac         = trans_tac
   1.267 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.268 +                                                real_minus_simps@real_add_ac))
   1.269 +                 THEN ALLGOALS
   1.270 +                    (simp_tac (HOL_ss addsimps [real_minus_mult_eq2]@
   1.271 +                                         bin_simps@real_add_ac@real_mult_ac))
   1.272 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.273 +  val simplify_meta_eq  = simplify_meta_eq
   1.274 +  end;
   1.275 +
   1.276 +
   1.277 +structure EqCancelNumerals = CancelNumeralsFun
   1.278 + (open CancelNumeralsCommon
   1.279 +  val prove_conv = prove_conv "realeq_cancel_numerals"
   1.280 +  val mk_bal   = HOLogic.mk_eq
   1.281 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT
   1.282 +  val bal_add1 = real_eq_add_iff1 RS trans
   1.283 +  val bal_add2 = real_eq_add_iff2 RS trans
   1.284 +);
   1.285 +
   1.286 +structure LessCancelNumerals = CancelNumeralsFun
   1.287 + (open CancelNumeralsCommon
   1.288 +  val prove_conv = prove_conv "realless_cancel_numerals"
   1.289 +  val mk_bal   = HOLogic.mk_binrel "op <"
   1.290 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT
   1.291 +  val bal_add1 = real_less_add_iff1 RS trans
   1.292 +  val bal_add2 = real_less_add_iff2 RS trans
   1.293 +);
   1.294 +
   1.295 +structure LeCancelNumerals = CancelNumeralsFun
   1.296 + (open CancelNumeralsCommon
   1.297 +  val prove_conv = prove_conv "realle_cancel_numerals"
   1.298 +  val mk_bal   = HOLogic.mk_binrel "op <="
   1.299 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT
   1.300 +  val bal_add1 = real_le_add_iff1 RS trans
   1.301 +  val bal_add2 = real_le_add_iff2 RS trans
   1.302 +);
   1.303 +
   1.304 +val cancel_numerals = 
   1.305 +  map prep_simproc
   1.306 +   [("realeq_cancel_numerals",
   1.307 +     prep_pats ["(l::real) + m = n", "(l::real) = m + n", 
   1.308 +		"(l::real) - m = n", "(l::real) = m - n", 
   1.309 +		"(l::real) * m = n", "(l::real) = m * n"], 
   1.310 +     EqCancelNumerals.proc),
   1.311 +    ("realless_cancel_numerals", 
   1.312 +     prep_pats ["(l::real) + m < n", "(l::real) < m + n", 
   1.313 +		"(l::real) - m < n", "(l::real) < m - n", 
   1.314 +		"(l::real) * m < n", "(l::real) < m * n"], 
   1.315 +     LessCancelNumerals.proc),
   1.316 +    ("realle_cancel_numerals", 
   1.317 +     prep_pats ["(l::real) + m <= n", "(l::real) <= m + n", 
   1.318 +		"(l::real) - m <= n", "(l::real) <= m - n", 
   1.319 +		"(l::real) * m <= n", "(l::real) <= m * n"], 
   1.320 +     LeCancelNumerals.proc)];
   1.321 +
   1.322 +
   1.323 +structure CombineNumeralsData =
   1.324 +  struct
   1.325 +  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
   1.326 +  val dest_sum		= dest_sum
   1.327 +  val mk_coeff		= mk_coeff
   1.328 +  val dest_coeff	= dest_coeff 1
   1.329 +  val left_distrib	= left_real_add_mult_distrib RS trans
   1.330 +  val prove_conv	= prove_conv "real_combine_numerals"
   1.331 +  val trans_tac          = trans_tac
   1.332 +  val norm_tac = ALLGOALS
   1.333 +                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.334 +                                              real_minus_simps@real_add_ac))
   1.335 +                 THEN ALLGOALS
   1.336 +                    (simp_tac (HOL_ss addsimps [real_minus_mult_eq2]@
   1.337 +                                               bin_simps@real_add_ac@real_mult_ac))
   1.338 +  val numeral_simp_tac	= ALLGOALS 
   1.339 +                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.340 +  val simplify_meta_eq  = simplify_meta_eq
   1.341 +  end;
   1.342 +
   1.343 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.344 +  
   1.345 +val combine_numerals = 
   1.346 +    prep_simproc ("real_combine_numerals",
   1.347 +		  prep_pats ["(i::real) + j", "(i::real) - j"],
   1.348 +		  CombineNumerals.proc);
   1.349 +
   1.350 +end;
   1.351 +
   1.352 +
   1.353 +Addsimprocs Real_Numeral_Simprocs.cancel_numerals;
   1.354 +Addsimprocs [Real_Numeral_Simprocs.combine_numerals];
   1.355 +
   1.356 +(*The Abel_Cancel simprocs are now obsolete*)
   1.357 +Delsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
   1.358 +
   1.359 +(*examples:
   1.360 +print_depth 22;
   1.361 +set timing;
   1.362 +set trace_simp;
   1.363 +fun test s = (Goal s; by (Simp_tac 1)); 
   1.364 +
   1.365 +test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::real)";
   1.366 +
   1.367 +test "#2*u = (u::real)";
   1.368 +test "(i + j + #12 + (k::real)) - #15 = y";
   1.369 +test "(i + j + #12 + (k::real)) - #5 = y";
   1.370 +
   1.371 +test "y - b < (b::real)";
   1.372 +test "y - (#3*b + c) < (b::real) - #2*c";
   1.373 +
   1.374 +test "(#2*x - (u*v) + y) - v*#3*u = (w::real)";
   1.375 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::real)";
   1.376 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::real)";
   1.377 +test "u*v - (x*u*v + (u*v)*#4 + y) = (w::real)";
   1.378 +
   1.379 +test "(i + j + #12 + (k::real)) = u + #15 + y";
   1.380 +test "(i + j*#2 + #12 + (k::real)) = j + #5 + y";
   1.381 +
   1.382 +test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::real)";
   1.383 +
   1.384 +test "a + -(b+c) + b = (d::real)";
   1.385 +test "a + -(b+c) - b = (d::real)";
   1.386 +
   1.387 +(*negative numerals*)
   1.388 +test "(i + j + #-2 + (k::real)) - (u + #5 + y) = zz";
   1.389 +test "(i + j + #-3 + (k::real)) < u + #5 + y";
   1.390 +test "(i + j + #3 + (k::real)) < u + #-6 + y";
   1.391 +test "(i + j + #-12 + (k::real)) - #15 = y";
   1.392 +test "(i + j + #12 + (k::real)) - #-15 = y";
   1.393 +test "(i + j + #-12 + (k::real)) - #-15 = y";
   1.394 +*)
   1.395 +
   1.396 +
   1.397 +(** Constant folding for real plus and times **)
   1.398 +
   1.399 +(*We do not need
   1.400 +    structure Real_Plus_Assoc = Assoc_Fold (Real_Plus_Assoc_Data);
   1.401 +  because combine_numerals does the same thing*)
   1.402 +
   1.403 +structure Real_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.404 +struct
   1.405 +  val ss		= HOL_ss
   1.406 +  val eq_reflection	= eq_reflection
   1.407 +  val thy    = RealBin.thy
   1.408 +  val T	     = HOLogic.realT
   1.409 +  val plus   = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT)
   1.410 +  val add_ac = real_mult_ac
   1.411 +end;
   1.412 +
   1.413 +structure Real_Times_Assoc = Assoc_Fold (Real_Times_Assoc_Data);
   1.414 +
   1.415 +Addsimprocs [Real_Times_Assoc.conv];
   1.416 +
   1.417 +
   1.418 +(*** decision procedure for linear arithmetic ***)
   1.419 +
   1.420 +(*---------------------------------------------------------------------------*)
   1.421 +(* Linear arithmetic                                                         *)
   1.422 +(*---------------------------------------------------------------------------*)
   1.423 +
   1.424 +(*
   1.425 +Instantiation of the generic linear arithmetic package for real.
   1.426 +*)
   1.427 +
   1.428 +(* Update parameters of arithmetic prover *)
   1.429 +let
   1.430 +
   1.431 +(* reduce contradictory <= to False *)
   1.432 +val add_rules =  
   1.433 +    real_diff_def ::
   1.434 +    map (rename_numerals thy) 
   1.435 +        [real_add_zero_left, real_add_zero_right, 
   1.436 +	 real_add_minus, real_add_minus_left, 
   1.437 +	 real_mult_0, real_mult_0_right, 
   1.438 +	 real_mult_1, real_mult_1_right, 
   1.439 +	 real_mult_minus_1, real_mult_minus_1_right];
   1.440 +
   1.441 +val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
   1.442 +               Real_Numeral_Simprocs.cancel_numerals;
   1.443 +
   1.444 +val add_mono_thms =
   1.445 +  map (fn s => prove_goal RealBin.thy s
   1.446 +                 (fn prems => [cut_facts_tac prems 1,
   1.447 +                      asm_simp_tac (simpset() addsimps [real_add_le_mono]) 1]))
   1.448 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
   1.449 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
   1.450 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
   1.451 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::real)"
   1.452 +    ];
   1.453 +
   1.454 +in
   1.455 +LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
   1.456 +(*We don't change LA_Data_Ref.lessD and LA_Data_Ref.discrete
   1.457 + because the real ordering is dense!*)
   1.458 +LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
   1.459 +                      addsimprocs simprocs
   1.460 +                      addcongs [if_weak_cong]
   1.461 +end;
   1.462 +
   1.463 +let
   1.464 +val real_arith_simproc_pats =
   1.465 +  map (fn s => Thm.read_cterm (Theory.sign_of RealDef.thy) (s, HOLogic.boolT))
   1.466 +      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
   1.467 +
   1.468 +val fast_real_arith_simproc = mk_simproc
   1.469 +  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
   1.470 +in
   1.471 +Addsimprocs [fast_real_arith_simproc]
   1.472 +end;
   1.473 +
   1.474 +(* Some test data [omitting examples thet assume the ordering to be discrete!]
   1.475 +Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   1.476 +by (fast_arith_tac 1);
   1.477 +Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
   1.478 +by (fast_arith_tac 1);
   1.479 +Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
   1.480 +by (fast_arith_tac 1);
   1.481 +Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   1.482 +by (arith_tac 1);
   1.483 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.484 +\     ==> a <= l";
   1.485 +by (fast_arith_tac 1);
   1.486 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.487 +\     ==> a+a+a+a <= l+l+l+l";
   1.488 +by (fast_arith_tac 1);
   1.489 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.490 +\     ==> a+a+a+a+a <= l+l+l+l+i";
   1.491 +by (fast_arith_tac 1);
   1.492 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.493 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   1.494 +by (fast_arith_tac 1);
   1.495 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.496 +\     ==> #6*a <= #5*l+i";
   1.497 +by (fast_arith_tac 1);
   1.498 +*)
   1.499 +
   1.500 +(*---------------------------------------------------------------------------*)
   1.501 +(* End of linear arithmetic                                                  *)
   1.502 +(*---------------------------------------------------------------------------*)
   1.503 +
   1.504 +(*useful??*)
   1.505 +Goal "(z = z + w) = (w = (#0::real))";
   1.506 +by Auto_tac;
   1.507 +qed "real_add_left_cancel0";
   1.508 +Addsimps [real_add_left_cancel0];