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
```