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