eliminated some old uses of cumulative prems (!) in proof methods;
authorwenzelm
Tue Nov 10 18:29:07 2009 +0100 (2009-11-10)
changeset 33555a0a8a40385a2
parent 33554 4601372337e4
child 33598 d7784ad2680d
eliminated some old uses of cumulative prems (!) in proof methods;
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Library/Float.thy	Tue Nov 10 18:11:23 2009 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Tue Nov 10 18:29:07 2009 +0100
     1.3 @@ -1378,8 +1378,8 @@
     1.4    assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
     1.5    shows "real (lb_mod prec x ub lb) \<le> ?x - ?k * y"
     1.6  proof -
     1.7 -  have "?lb \<le> ?ub" by (auto!)
     1.8 -  have "0 \<le> ?lb" and "?lb \<noteq> 0" by (auto!)
     1.9 +  have "?lb \<le> ?ub" using assms by auto
    1.10 +  have "0 \<le> ?lb" and "?lb \<noteq> 0" using assms by auto
    1.11    have "?k * y \<le> ?x" using assms by auto
    1.12    also have "\<dots> \<le> ?x / ?lb * ?ub" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?lb` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?lb \<noteq> 0`])
    1.13    also have "\<dots> \<le> real (ceiling_fl (float_divr prec x lb)) * ?ub" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divr ceiling_fl)
    1.14 @@ -1390,8 +1390,8 @@
    1.15    assumes "0 < real lb" "real lb \<le> y" (is "?lb \<le> y") "y \<le> real ub" (is "y \<le> ?ub")
    1.16    shows "?x - ?k * y \<le> real (ub_mod prec x ub lb)"
    1.17  proof -
    1.18 -  have "?lb \<le> ?ub" by (auto!)
    1.19 -  hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" by (auto!)
    1.20 +  have "?lb \<le> ?ub" using assms by auto
    1.21 +  hence "0 \<le> ?lb" and "0 \<le> ?ub" and "?ub \<noteq> 0" using assms by auto
    1.22    have "real (floor_fl (float_divl prec x ub)) * ?lb \<le> ?x / ?ub * ?lb" by (metis mult_right_mono order_trans `0 \<le> ?lb` `?lb \<le> ?ub` float_divl floor_fl)
    1.23    also have "\<dots> \<le> ?x" by (metis mult_left_mono[OF `?lb \<le> ?ub` `0 \<le> ?x`] divide_right_mono[OF _ `0 \<le> ?ub` ] times_divide_eq_left nonzero_mult_divide_cancel_right[OF `?ub \<noteq> 0`])
    1.24    also have "\<dots> \<le> ?k * y" using assms by auto