src/HOL/Presburger.thy
 changeset 35216 7641e8d831d2 parent 35050 9f841f20dca6 child 36749 a8dc19a352e6
equal 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 `