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

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 }