src/HOL/Decision_Procs/MIR.thy
changeset 30649 57753e0ec1d4
parent 30439 57c68b3af2ea
child 31706 1db0c8f235fb
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Mar 21 12:37:13 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun Mar 22 19:36:04 2009 +0100
     1.3 @@ -3783,8 +3783,7 @@
     1.4      also from mult_left_mono[OF xp] np have "?N s \<le> real n * x + ?N s" by simp
     1.5      finally have "?N (Floor s) \<le> real n * x + ?N s" .
     1.6      moreover
     1.7 -    {from mult_strict_left_mono[OF x1] np 
     1.8 -      have "real n *x + ?N s < real n + ?N s" by simp
     1.9 +    {from x1 np have "real n *x + ?N s < real n + ?N s" by simp
    1.10        also from real_of_int_floor_add_one_gt[where r="?N s"] 
    1.11        have "\<dots> < real n + ?N (Floor s) + 1" by simp
    1.12        finally have "real n *x + ?N s < ?N (Floor s) + real (n+1)" by simp}
    1.13 @@ -3809,8 +3808,7 @@
    1.14      moreover from mult_left_mono_neg[OF xp] nn have "?N s \<ge> real n * x + ?N s" by simp
    1.15      ultimately have "?N (Floor s) + 1 > real n * x + ?N s" by arith 
    1.16      moreover
    1.17 -    {from mult_strict_left_mono_neg[OF x1, where c="real n"] nn
    1.18 -      have "real n *x + ?N s \<ge> real n + ?N s" by simp 
    1.19 +    {from x1 nn have "real n *x + ?N s \<ge> real n + ?N s" by simp
    1.20        moreover from real_of_int_floor_le[where r="?N s"]  have "real n + ?N s \<ge> real n + ?N (Floor s)" by simp
    1.21        ultimately have "real n *x + ?N s \<ge> ?N (Floor s) + real n" 
    1.22  	by (simp only: algebra_simps)}