src/HOL/Presburger.thy
changeset 35216 7641e8d831d2
parent 35050 9f841f20dca6
child 36749 a8dc19a352e6
equal deleted inserted replaced
35215:a03462cbf86f 35216:7641e8d831d2
   197   proof (cases)
   197   proof (cases)
   198     assume "x mod d = 0"
   198     assume "x mod d = 0"
   199     hence "P 0" using P Pmod by simp
   199     hence "P 0" using P Pmod by simp
   200     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
   200     moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
   201     ultimately have "P d" by simp
   201     ultimately have "P d" by simp
   202     moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
   202     moreover have "d : {1..d}" using dpos by simp
   203     ultimately show ?RHS ..
   203     ultimately show ?RHS ..
   204   next
   204   next
   205     assume not0: "x mod d \<noteq> 0"
   205     assume not0: "x mod d \<noteq> 0"
   206     have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
   206     have "P(x mod d)" using dpos P Pmod by simp
   207     moreover have "x mod d : {1..d}"
   207     moreover have "x mod d : {1..d}"
   208     proof -
   208     proof -
   209       from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
   209       from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
   210       moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
   210       moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
   211       ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
   211       ultimately show ?thesis using not0 by simp
   212     qed
   212     qed
   213     ultimately show ?RHS ..
   213     ultimately show ?RHS ..
   214   qed
   214   qed
   215 qed auto
   215 qed auto
   216 
   216