src/HOL/Presburger.thy
 changeset 23389 aaca6a8e5414 parent 23365 f31794033ae1 child 23390 01ef1135de73
```     1.1 --- a/src/HOL/Presburger.thy	Thu Jun 14 18:33:29 2007 +0200
1.2 +++ b/src/HOL/Presburger.thy	Thu Jun 14 18:33:31 2007 +0200
1.3 @@ -200,8 +200,8 @@
1.4      have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
1.5      moreover have "x mod d : {1..d}"
1.6      proof -
1.7 -      have "0 \<le> x mod d" by(rule pos_mod_sign)
1.8 -      moreover have "x mod d < d" by(rule pos_mod_bound)
1.9 +      from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
1.10 +      moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
1.11        ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
1.12      qed
1.13      ultimately show ?RHS ..
1.14 @@ -243,7 +243,7 @@
1.15  qed
1.16
1.17  lemma  minusinfinity:
1.18 -  assumes "0 < d" and
1.19 +  assumes dpos: "0 < d" and
1.20      P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \<longrightarrow> (P x = P1 x)"
1.21    shows "(EX x. P1 x) \<longrightarrow> (EX x. P x)"
1.22  proof
1.23 @@ -251,7 +251,7 @@
1.24    then obtain x where P1: "P1 x" ..
1.25    from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
1.26    let ?w = "x - (abs(x-z)+1) * d"
1.27 -  have w: "?w < z" by(rule decr_lemma)
1.28 +  from dpos have w: "?w < z" by(rule decr_lemma)
1.29    have "P1 x = P1 ?w" using P1eqP1 by blast
1.30    also have "\<dots> = P(?w)" using w P1eqP by blast
1.31    finally have "P ?w" using P1 by blast
1.32 @@ -289,7 +289,7 @@
1.33  subsection {* The @{text "+\<infinity>"} Version*}
1.34
1.35  lemma  plusinfinity:
1.36 -  assumes "(0::int) < d" and
1.37 +  assumes dpos: "(0::int) < d" and
1.38      P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
1.39    shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
1.40  proof
1.41 @@ -299,7 +299,7 @@
1.42    let ?w' = "x + (abs(x-z)+1) * d"
1.43    let ?w = "x - (-(abs(x-z) + 1))*d"
1.44    have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps)
1.45 -  have w: "?w > z" by(simp only: ww', rule incr_lemma)
1.46 +  from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
1.47    hence "P' x = P' ?w" using P1eqP1 by blast
1.48    also have "\<dots> = P(?w)" using w P1eqP by blast
1.49    finally have "P ?w" using P1 by blast
```