src/HOL/Decision_Procs/MIR.thy
changeset 36778 739a9379e29b
parent 36531 19f6e3b0d9b6
child 36870 b897bd9ca71b
     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sun May 09 17:47:43 2010 -0700
     1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sun May 09 22:51:11 2010 -0700
     1.3 @@ -2177,7 +2177,7 @@
     1.4      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
     1.5      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
     1.6      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
     1.7 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
     1.8 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
     1.9      hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
    1.10      thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
    1.11        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
    1.12 @@ -2194,7 +2194,7 @@
    1.13      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    1.14      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    1.15      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    1.16 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    1.17 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    1.18      hence "real c * real x + Inum (y # bs) e \<noteq> 0"using rcpos  by simp
    1.19      thus "real c * real x + Inum (real x # bs) e \<noteq> 0" 
    1.20        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"]  by simp
    1.21 @@ -2211,7 +2211,7 @@
    1.22      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    1.23      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    1.24      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    1.25 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    1.26 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    1.27      thus "real c * real x + Inum (real x # bs) e < 0" 
    1.28        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    1.29    qed
    1.30 @@ -2227,7 +2227,7 @@
    1.31      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    1.32      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    1.33      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    1.34 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    1.35 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    1.36      thus "real c * real x + Inum (real x # bs) e \<le> 0" 
    1.37        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    1.38    qed
    1.39 @@ -2243,7 +2243,7 @@
    1.40      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    1.41      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    1.42      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    1.43 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    1.44 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    1.45      thus "\<not> (real c * real x + Inum (real x # bs) e>0)" 
    1.46        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    1.47    qed
    1.48 @@ -2259,7 +2259,7 @@
    1.49      assume A: "real x + (1\<Colon>real) \<le> - (Inum (y # bs) e / real c)"
    1.50      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
    1.51      with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
    1.52 -      by (simp only:  real_mult_less_mono2[OF rcpos th1])
    1.53 +      by (simp only: mult_strict_left_mono [OF th1 rcpos])
    1.54      thus "\<not> real c * real x + Inum (real x # bs) e \<ge> 0" 
    1.55        using numbound0_I[OF nbe, where b="y" and bs="bs" and b'="real x"] rcpos by simp
    1.56    qed