summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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