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

src/HOL/Presburger.thy

changeset 35216 | 7641e8d831d2 |

parent 35050 | 9f841f20dca6 |

child 36749 | a8dc19a352e6 |

1.1 --- a/src/HOL/Presburger.thy Thu Feb 18 13:29:59 2010 -0800 1.2 +++ b/src/HOL/Presburger.thy Thu Feb 18 14:21:44 2010 -0800 1.3 @@ -199,16 +199,16 @@ 1.4 hence "P 0" using P Pmod by simp 1.5 moreover have "P 0 = P(0 - (-1)*d)" using modd by blast 1.6 ultimately have "P d" by simp 1.7 - moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff) 1.8 + moreover have "d : {1..d}" using dpos by simp 1.9 ultimately show ?RHS .. 1.10 next 1.11 assume not0: "x mod d \<noteq> 0" 1.12 - have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) 1.13 + have "P(x mod d)" using dpos P Pmod by simp 1.14 moreover have "x mod d : {1..d}" 1.15 proof - 1.16 from dpos have "0 \<le> x mod d" by(rule pos_mod_sign) 1.17 moreover from dpos have "x mod d < d" by(rule pos_mod_bound) 1.18 - ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) 1.19 + ultimately show ?thesis using not0 by simp 1.20 qed 1.21 ultimately show ?RHS .. 1.22 qed