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 }