src/HOL/Decision_Procs/MIR.thy
 changeset 56479 91958d4b30f7 parent 56410 a14831ac3023 child 56544 b60d5d119489
```     1.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Apr 08 23:16:00 2014 +0200
1.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Wed Apr 09 09:37:47 2014 +0200
1.3 @@ -2068,7 +2068,7 @@
1.4    from 3 have nbe: "numbound0 e" by simp
1.5    fix y
1.6    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"
1.7 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.8 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.9      fix x :: int
1.10      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.11      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.12 @@ -2085,7 +2085,7 @@
1.13    from 4 have nbe: "numbound0 e" by simp
1.14    fix y
1.15    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"
1.16 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.17 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.18      fix x :: int
1.19      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.20      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.21 @@ -2102,7 +2102,7 @@
1.22    from 5 have nbe: "numbound0 e" by simp
1.23    fix y
1.24    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"
1.25 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.26 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.27      fix x :: int
1.28      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.29      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.30 @@ -2118,7 +2118,7 @@
1.31    from 6 have nbe: "numbound0 e" by simp
1.32    fix y
1.33    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"
1.34 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.35 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.36      fix x :: int
1.37      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.38      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.39 @@ -2134,7 +2134,7 @@
1.40    from 7 have nbe: "numbound0 e" by simp
1.41    fix y
1.42    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"
1.43 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.44 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.45      fix x :: int
1.46      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.47      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.48 @@ -2150,7 +2150,7 @@
1.49    from 8 have nbe: "numbound0 e" by simp
1.50    fix y
1.51    have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"
1.52 -  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
1.53 +  proof (simp add: less_floor_eq , rule allI, rule impI)
1.54      fix x :: int
1.55      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
1.56      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
1.57 @@ -4267,7 +4267,7 @@
1.58    {fix x
1.59      assume xz: "x > ?z"
1.60      with mult_strict_right_mono [OF xz cp] cp
1.61 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.62 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.63      hence "real c * x + ?e > 0" by arith
1.64      hence "real c * x + ?e \<noteq> 0" by simp
1.65      with xz have "?P ?z x (Eq (CN 0 c e))"
1.66 @@ -4284,7 +4284,7 @@
1.67    {fix x
1.68      assume xz: "x > ?z"
1.69      with mult_strict_right_mono [OF xz cp] cp
1.70 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.71 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.72      hence "real c * x + ?e > 0" by arith
1.73      hence "real c * x + ?e \<noteq> 0" by simp
1.74      with xz have "?P ?z x (NEq (CN 0 c e))"
1.75 @@ -4301,7 +4301,7 @@
1.76    {fix x
1.77      assume xz: "x > ?z"
1.78      with mult_strict_right_mono [OF xz cp] cp
1.79 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.80 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.81      hence "real c * x + ?e > 0" by arith
1.82      with xz have "?P ?z x (Lt (CN 0 c e))"
1.83        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
1.84 @@ -4317,7 +4317,7 @@
1.85    {fix x
1.86      assume xz: "x > ?z"
1.87      with mult_strict_right_mono [OF xz cp] cp
1.88 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.89 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.90      hence "real c * x + ?e > 0" by arith
1.91      with xz have "?P ?z x (Le (CN 0 c e))"
1.92        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
1.93 @@ -4333,7 +4333,7 @@
1.94    {fix x
1.95      assume xz: "x > ?z"
1.96      with mult_strict_right_mono [OF xz cp] cp
1.97 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.98 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.99      hence "real c * x + ?e > 0" by arith
1.100      with xz have "?P ?z x (Gt (CN 0 c e))"
1.101        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
1.102 @@ -4349,7 +4349,7 @@
1.103    {fix x
1.104      assume xz: "x > ?z"
1.105      with mult_strict_right_mono [OF xz cp] cp
1.106 -    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
1.107 +    have "(real c * x > - ?e)" by (simp add: mult_ac)
1.108      hence "real c * x + ?e > 0" by arith
1.109      with xz have "?P ?z x (Ge (CN 0 c e))"
1.110        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
```