src/HOL/Presburger.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Presburger.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -211,11 +211,11 @@
     1.4  
     1.5  subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
     1.6  
     1.7 -lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
     1.8 -by(induct rule: int_gr_induct,simp_all add:int_distrib)
     1.9 +lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (\<bar>x - z\<bar> + 1) * d < z"
    1.10 +  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
    1.11  
    1.12 -lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
    1.13 -by(induct rule: int_gr_induct, simp_all add:int_distrib)
    1.14 +lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (\<bar>x - z\<bar> + 1) * d"
    1.15 +  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
    1.16  
    1.17  lemma decr_mult_lemma:
    1.18    assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
    1.19 @@ -241,7 +241,7 @@
    1.20    assume eP1: "EX x. P1 x"
    1.21    then obtain x where P1: "P1 x" ..
    1.22    from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
    1.23 -  let ?w = "x - (abs(x-z)+1) * d"
    1.24 +  let ?w = "x - (\<bar>x - z\<bar> + 1) * d"
    1.25    from dpos have w: "?w < z" by(rule decr_lemma)
    1.26    have "P1 x = P1 ?w" using P1eqP1 by blast
    1.27    also have "\<dots> = P(?w)" using w P1eqP by blast
    1.28 @@ -287,8 +287,8 @@
    1.29    assume eP1: "EX x. P' x"
    1.30    then obtain x where P1: "P' x" ..
    1.31    from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
    1.32 -  let ?w' = "x + (abs(x-z)+1) * d"
    1.33 -  let ?w = "x - (-(abs(x-z) + 1))*d"
    1.34 +  let ?w' = "x + (\<bar>x - z\<bar> + 1) * d"
    1.35 +  let ?w = "x - (- (\<bar>x - z\<bar> + 1)) * d"
    1.36    have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps)
    1.37    from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
    1.38    hence "P' x = P' ?w" using P1eqP1 by blast