Quelle Presburger.thy Sprache: Isabelle

(* Title:      HOL/Presburger.thy
   Author:     Amine Chaieb, TU Muenchen
*)

section \<open>Decision Procedure for Presburger Arithmetic\<close>

theory Presburger
imports Groebner_Basis Set_Interval
begin

ML_file \<open>Tools/Qelim/qelim.ML\<close>
ML_file \<open>Tools/Qelim/cooper_procedure.ML\<close>

subsection\<open>The \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Properties\<close>

lemma minf:
  "\\(z ::'a::linorder).\xz.\x
     \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
  "\\(z ::'a::linorder).\xz.\x
     \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<or> Q x) = (P' x \<or> Q' x)"
  "\(z ::'a::{linorder}).\x
  "\(z ::'a::{linorder}).\x t) = True"
  "\(z ::'a::{linorder}).\x
  "\(z ::'a::{linorder}).\x t) = True"
  "\(z ::'a::{linorder}).\x t) = False"
  "\(z ::'a::{linorder}).\x t) = False"
  "\z.\(x::'b::{linorder,plus,Rings.dvd})
  "\z.\(x::'b::{linorder,plus,Rings.dvd}) d dvd x + s) = (\ d dvd x + s)"
  "\z.\x
proof safe
  fix z1 z2
  assume "\xx
  then have "\x < min z1 z2. (P x \ Q x) = (P' x \ Q' x)"
    by simp
  then show "\z. \x Q x) = (P' x \ Q' x)"
    by blast
next
  fix z1 z2
  assume "\xx
  then have "\x < min z1 z2. (P x \ Q x) = (P' x \ Q' x)"
    by simp
  then show "\z. \x Q x) = (P' x \ Q' x)"
    by blast
next
  have "\x t"
    by fastforce
  then show "\z. \x t) = True"
    by auto
next
  have "\x t < x"
    by fastforce
  then show "\z. \x
    by auto
next
  have "\x t \ x"
    by fastforce
  then show "\z. \x x) = False"
    by auto
qed auto

lemma pinf:
  "\\(z ::'a::linorder).\x>z. P x = P' x; \z.\x>z. Q x = Q' x\
     \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<and> Q x) = (P' x \<and> Q' x)"
  "\\(z ::'a::linorder).\x>z. P x = P' x; \z.\x>z. Q x = Q' x\
     \<Longrightarrow> \<exists>z.\<forall>x>z. (P x \<or> Q x) = (P' x \<or> Q' x)"
  "\(z ::'a::{linorder}).\x>z.(x = t) = False"
  "\(z ::'a::{linorder}).\x>z.(x \ t) = True"
  "\(z ::'a::{linorder}).\x>z.(x < t) = False"
  "\(z ::'a::{linorder}).\x>z.(x \ t) = False"
  "\(z ::'a::{linorder}).\x>z.(x > t) = True"
  "\(z ::'a::{linorder}).\x>z.(x \ t) = True"
  "\z.\(x::'b::{linorder,plus,Rings.dvd})>z. (d dvd x + s) = (d dvd x + s)"
  "\z.\(x::'b::{linorder,plus,Rings.dvd})>z. (\ d dvd x + s) = (\ d dvd x + s)"
  "\z.\x>z. F = F"
proof safe
  fix z1 z2
  assume "\x>z1. P x = P' x" and "\x>z2. Q x = Q' x"
  then have "\x > max z1 z2. (P x \ Q x) = (P' x \ Q' x)"
    by simp
  then show "\z. \x>z. (P x \ Q x) = (P' x \ Q' x)"
    by blast
next
  fix z1 z2
  assume "\x>z1. P x = P' x" and "\x>z2. Q x = Q' x"
  then have "\x > max z1 z2. (P x \ Q x) = (P' x \ Q' x)"
    by simp
  then show "\z. \x>z. (P x \ Q x) = (P' x \ Q' x)"
    by blast
next
  have "\x>t. \ x < t"
    by fastforce
  then show "\z. \x>z. x < t = False"
    by blast
next
  have "\x>t. \ x \ t"
    by fastforce
  then show "\z. \x>z. x \ t = False"
    by blast
next
  have "\x>t. t \ x"
    by fastforce
  then show "\z. \x>z. t \ x = True"
    by blast
qed auto

lemma inf_period:
  "\\x k. P x = P (x - k*D); \x k. Q x = Q (x - k*D)\
    \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
  "\\x k. P x = P (x - k*D); \x k. Q x = Q (x - k*D)\
    \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
  "(d::'a::{comm_ring,Rings.dvd}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
  "(d::'a::{comm_ring,Rings.dvd}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)"
  "\x k. F = F"
apply (auto elim!: dvdE simp add: algebra_simps)
unfolding mult.assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
unfolding dvd_def mult.commute [of d]
by auto

subsection\<open>The A and B sets\<close>
lemma bset:
  "\\x.(\j \ {1 .. D}. \b\B. x \ b + j)\ P x \ P(x - D) ;
     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow>
  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x - D) \<and> Q (x - D))"
  "\\x.(\j\{1 .. D}. \b\B. x \ b + j)\ P x \ P(x - D) ;
     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow>
  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x - D) \<or> Q (x - D))"
  "\D>0; t - 1\ B\ \ (\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x = t) \ (x - D = t))"
  "\D>0 ; t \ B\ \(\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t))"
  "D>0 \ (\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (x < t) \ (x - D < t))"
  "D>0 \ (\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t))"
  "\D>0 ; t \ B\ \(\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (x > t) \ (x - D > t))"
  "\D>0 ; t - 1 \ B\ \(\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t))"
  "d dvd D \(\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (d dvd x+t) \ (d dvd (x - D) + t))"
  "d dvd D \(\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (\d dvd x+t) \ (\ d dvd (x - D) + t))"
  "\x.(\j\{1 .. D}. \b\B. x \ b + j) \ F \ F"
proof (blast, blast)
  assume dp: "D > 0" and tB: "t - 1\ B"
  show "(\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x = t) \ (x - D = t))"
    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t - 1"])
    apply algebra using dp tB by simp_all
next
  assume dp: "D > 0" and tB: "t \ B"
  show "(\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t))"
    apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
    apply algebra
    using dp tB by simp_all
next
  assume dp: "D > 0" thus "(\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x < t) \ (x - D < t))" by arith
next
  assume dp: "D > 0" thus "\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t)" by arith
next
  assume dp: "D > 0" and tB:"t \ B"
  {fix x assume nob: "\j\{1 .. D}. \b\B. x \ b + j" and g: "x > t" and ng: "\ (x - D) > t"
    hence "x -t \ D" and "1 \ x - t" by simp+
      hence "\j \ {1 .. D}. x - t = j" by auto
      hence "\j \ {1 .. D}. x = t + j" by (simp add: algebra_simps)
      with nob tB have "False" by simp}
  thus "\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x > t) \ (x - D > t)" by blast
next
  assume dp: "D > 0" and tB:"t - 1\ B"
  {fix x assume nob: "\j\{1 .. D}. \b\B. x \ b + j" and g: "x \ t" and ng: "\ (x - D) \ t"
    hence "x - (t - 1) \ D" and "1 \ x - (t - 1)" by simp+
      hence "\j \ {1 .. D}. x - (t - 1) = j" by auto
      hence "\j \ {1 .. D}. x = (t - 1) + j" by (simp add: algebra_simps)
      with nob tB have "False" by simp}
  thus "\x.(\j\{1 .. D}. \b\B. x \ b + j)\ (x \ t) \ (x - D \ t)" by blast
next
  assume d: "d dvd D"
  {fix x assume H: "d dvd x + t" with d have "d dvd (x - D) + t" by algebra}
  thus "\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (d dvd x+t) \ (d dvd (x - D) + t)" by simp
next
  assume d: "d dvd D"
  {fix x assume H: "\(d dvd x + t)" with d have "\ d dvd (x - D) + t"
      by (clarsimp simp add: dvd_def,erule_tac x= "ka + k" in allE,simp add: algebra_simps)}
  thus "\(x::int).(\j\{1 .. D}. \b\B. x \ b + j)\ (\d dvd x+t) \ (\d dvd (x - D) + t)" by auto
qed blast

lemma aset:
  "\\x.(\j\{1 .. D}. \b\A. x \ b - j)\ P x \ P(x + D) ;
     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow>
  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j) \<longrightarrow> (P x \<and> Q x) \<longrightarrow> (P(x + D) \<and> Q (x + D))"
  "\\x.(\j\{1 .. D}. \b\A. x \ b - j)\ P x \ P(x + D) ;
     \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> Q x \<longrightarrow> Q(x + D)\<rbrakk> \<Longrightarrow>
  \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (P x \<or> Q x) \<longrightarrow> (P(x + D) \<or> Q (x + D))"
  "\D>0; t + 1\ A\ \ (\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x = t) \ (x + D = t))"
  "\D>0 ; t \ A\ \(\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t))"
  "\D>0; t\ A\ \(\(x::int). (\j\{1 .. D}. \b\A. x \ b - j)\ (x < t) \ (x + D < t))"
  "\D>0; t + 1 \ A\ \ (\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t))"
  "D>0 \(\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (x > t) \ (x + D > t))"
  "D>0 \(\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t))"
  "d dvd D \(\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (d dvd x+t) \ (d dvd (x + D) + t))"
  "d dvd D \(\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (\d dvd x+t) \ (\ d dvd (x + D) + t))"
  "\x.(\j\{1 .. D}. \b\A. x \ b - j) \ F \ F"
proof (blast, blast)
  assume dp: "D > 0" and tA: "t + 1 \ A"
  show "(\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x = t) \ (x + D = t))"
    apply (rule allI, rule impI,erule ballE[where x="1"],erule ballE[where x="t + 1"])
    using dp tA by simp_all
next
  assume dp: "D > 0" and tA: "t \ A"
  show "(\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t))"
    apply (rule allI, rule impI,erule ballE[where x="D"],erule ballE[where x="t"])
    using dp tA by simp_all
next
  assume dp: "D > 0" thus "(\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x > t) \ (x + D > t))" by arith
next
  assume dp: "D > 0" thus "\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t)" by arith
next
  assume dp: "D > 0" and tA:"t \ A"
  {fix x assume nob: "\j\{1 .. D}. \b\A. x \ b - j" and g: "x < t" and ng: "\ (x + D) < t"
    hence "t - x \ D" and "1 \ t - x" by simp+
      hence "\j \ {1 .. D}. t - x = j" by auto
      hence "\j \ {1 .. D}. x = t - j" by (auto simp add: algebra_simps)
      with nob tA have "False" by simp}
  thus "\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x < t) \ (x + D < t)" by blast
next
  assume dp: "D > 0" and tA:"t + 1\ A"
  {fix x assume nob: "\j\{1 .. D}. \b\A. x \ b - j" and g: "x \ t" and ng: "\ (x + D) \ t"
    hence "(t + 1) - x \ D" and "1 \ (t + 1) - x" by (simp_all add: algebra_simps)
      hence "\j \ {1 .. D}. (t + 1) - x = j" by auto
      hence "\j \ {1 .. D}. x = (t + 1) - j" by (auto simp add: algebra_simps)
      with nob tA have "False" by simp}
  thus "\x.(\j\{1 .. D}. \b\A. x \ b - j)\ (x \ t) \ (x + D \ t)" by blast
next
  assume d: "d dvd D"
  have "\x. d dvd x + t \ d dvd x + D + t"
  proof -
    fix x
    assume H: "d dvd x + t"
    then obtain ka where "x + t = d * ka"
      unfolding dvd_def by blast
    moreover from d obtain k where *:"D = d * k"
      unfolding dvd_def by blast
    ultimately have "x + d * k + t = d * (ka + k)"
      by (simp add: algebra_simps)
    then show "d dvd (x + D) + t"
      using * unfolding dvd_def by blast
  qed
  thus "\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (d dvd x+t) \ (d dvd (x + D) + t)" by simp
next
  assume d: "d dvd D"
  {fix x assume H: "\(d dvd x + t)" with d have "\d dvd (x + D) + t"
      using dvd_add_left_iff[OF d, of "x+t"] by (simp add: algebra_simps)}
  thus "\(x::int).(\j\{1 .. D}. \b\A. x \ b - j)\ (\d dvd x+t) \ (\d dvd (x + D) + t)" by auto
qed blast

subsection\<open>Cooper's Theorem \<open>-\<infinity>\<close> and \<open>+\<infinity>\<close> Version\<close>

subsubsection\<open>First some trivial facts about periodic sets or predicates\<close>
lemma periodic_finite_ex:
  assumes dpos: "(0::int) < d" and modd: "\x k. P x = P(x - k*d)"
  shows "(\x. P x) = (\j \ {1..d}. P j)"
  (is "?LHS = ?RHS")
proof
  assume ?LHS
  then obtain x where P: "P x" ..
  have "x mod d = x - (x div d)*d" by(simp add:mult_div_mod_eq [symmetric] ac_simps eq_diff_eq)
  hence Pmod: "P x = P(x mod d)" using modd by simp
  show ?RHS
  proof (cases)
    assume "x mod d = 0"
    hence "P 0" using P Pmod by simp
    moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
    ultimately have "P d" by simp
    moreover have "d \ {1..d}" using dpos by simp
    ultimately show ?RHS ..
  next
    assume not0: "x mod d \ 0"
    have "P(x mod d)" using dpos P Pmod by simp
    moreover have "x mod d \ {1..d}"
    proof -
      from dpos have "0 \ x mod d" by(rule pos_mod_sign)
      moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
      ultimately show ?thesis using not0 by simp
    qed
    ultimately show ?RHS ..
  qed
qed auto

subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>

lemma decr_lemma: "0 < (d::int) \ x - (\x - z\ + 1) * d < z"
  by (induct rule: int_gr_induct) (simp_all add: int_distrib)

lemma incr_lemma: "0 < (d::int) \ z < x + (\x - z\ + 1) * d"
  by (induct rule: int_gr_induct) (simp_all add: int_distrib)

lemma decr_mult_lemma:
  assumes dpos: "(0::int) < d" and minus: "\x. P x \ P(x - d)" and knneg: "0 <= k"
  shows "\x. P x \ P(x - k*d)"
using knneg
proof (induct rule:int_ge_induct)
  case base thus ?case by simp
next
  case (step i)
  {fix x
    have "P x \ P (x - i * d)" using step.hyps by blast
    also have "\ \ P(x - (i + 1) * d)" using minus[THEN spec, of "x - i * d"]
      by (simp add: algebra_simps)
    ultimately have "P x \ P(x - (i + 1) * d)" by blast}
  thus ?case ..
qed

lemma  minusinfinity:
  assumes dpos: "0 < d" and
    P1eqP1: "\x k. P1 x = P1(x - k*d)" and ePeqP1: "\z::int. \x. x < z \ (P x = P1 x)"
  shows "(\x. P1 x) \ (\x. P x)"
proof
  assume eP1: "\x. P1 x"
  then obtain x where P1: "P1 x" ..
  from ePeqP1 obtain z where P1eqP: "\x. x < z \ (P x = P1 x)" ..
  let ?w = "x - (\x - z\ + 1) * d"
  from dpos have w: "?w < z" by(rule decr_lemma)
  have "P1 x = P1 ?w" using P1eqP1 by blast
  also have "\ = P(?w)" using w P1eqP by blast
  finally have "P ?w" using P1 by blast
  thus "\x. P x" ..
qed

lemma cpmi:
  assumes dp: "0 < D" and p1:"\z. \ x< z. P x = P' x"
  and nb:"\x.(\ j\ {1..D}. \(b::int) \ B. x \ b+j) \ P (x) \ P (x - D)"
  and pd: "\ x k. P' x = P' (x-k*D)"
  shows "(\x. P x) = ((\j \ {1..D} . P' j) \ (\j \ {1..D}. \ b \ B. P (b+j)))"
         (is "?L = (?R1 \ ?R2)")
proof-
{assume "?R2" hence "?L"  by blast}
moreover
{assume H:"?R1" hence "?L" using minusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
moreover
{ fix x
   assume P: "P x" and H: "\ ?R2"
   {fix y assume "\ (\j\{1..D}. \b\B. P (b + j))" and P: "P y"
     hence "\(\(j::int) \ {1..D}. \(b::int) \ B. y = b+j)" by auto
     with nb P  have "P (y - D)" by auto }
   hence "\x. \(\(j::int) \ {1..D}. \(b::int) \ B. P(b+j)) \ P (x) \ P (x - D)" by blast
   with H P have th: " \x. P x \ P (x - D)" by auto
   from p1 obtain z where z: "\x. x < z \ (P x = P' x)" by blast
   let ?y = "x - (\x - z\ + 1)*D"
   have zp: "0 <= (\x - z\ + 1)" by arith
   from dp have yz: "?y < z" using decr_lemma[OF dp] by simp
   from z[rule_format, OF yz] decr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
   with periodic_finite_ex[OF dp pd]
   have "?R1" by blast}
ultimately show ?thesis by blast
qed

subsubsection \<open>The \<open>+\<infinity>\<close> Version\<close>

lemma  plusinfinity:
  assumes dpos: "(0::int) < d" and
    P1eqP1: "\x k. P' x = P'(x - k*d)" and ePeqP1: "\ z. \ x>z. P x = P' x"
  shows "(\ x. P' x) \ (\ x. P x)"
proof
  assume eP1: "\x. P' x"
  then obtain x where P1: "P' x" ..
  from ePeqP1 obtain z where P1eqP: "\x>z. P x = P' x" ..
  let ?w' = "x + (\x - z\ + 1) * d"
  let ?w = "x - (- (\x - z\ + 1)) * d"
  have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps)
  from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
  hence "P' x = P' ?w" using P1eqP1 by blast
  also have "\ = P(?w)" using w P1eqP by blast
  finally have "P ?w" using P1 by blast
  thus "\x. P x" ..
qed

lemma incr_mult_lemma:
  assumes dpos: "(0::int) < d" and plus: "\x::int. P x \ P(x + d)" and knneg: "0 <= k"
  shows "\x. P x \ P(x + k*d)"
using knneg
proof (induct rule:int_ge_induct)
  case base thus ?case by simp
next
  case (step i)
  {fix x
    have "P x \ P (x + i * d)" using step.hyps by blast
    also have "\ \ P(x + (i + 1) * d)" using plus[THEN spec, of "x + i * d"]
      by (simp add:int_distrib ac_simps)
    ultimately have "P x \ P(x + (i + 1) * d)" by blast}
  thus ?case ..
qed

lemma cppi:
  assumes dp: "0 < D" and p1:"\z. \ x> z. P x = P' x"
  and nb:"\x.(\ j\ {1..D}. \(b::int) \ A. x \ b - j) \ P (x) \ P (x + D)"
  and pd: "\ x k. P' x= P' (x-k*D)"
  shows "(\x. P x) = ((\j \ {1..D} . P' j) \ (\ j \ {1..D}. \ b\ A. P (b - j)))" (is "?L = (?R1 \ ?R2)")
proof-
{assume "?R2" hence "?L"  by blast}
moreover
{assume H:"?R1" hence "?L" using plusinfinity[OF dp pd p1] periodic_finite_ex[OF dp pd] by simp}
moreover
{ fix x
   assume P: "P x" and H: "\ ?R2"
   {fix y assume "\ (\j\{1..D}. \b\A. P (b - j))" and P: "P y"
     hence "\(\(j::int) \ {1..D}. \(b::int) \ A. y = b - j)" by auto
     with nb P  have "P (y + D)" by auto }
   hence "\x. \(\(j::int) \ {1..D}. \(b::int) \ A. P(b-j)) \ P (x) \ P (x + D)" by blast
   with H P have th: " \x. P x \ P (x + D)" by auto
   from p1 obtain z where z: "\x. x > z \ (P x = P' x)" by blast
   let ?y = "x + (\x - z\ + 1)*D"
   have zp: "0 <= (\x - z\ + 1)" by arith
   from dp have yz: "?y > z" using incr_lemma[OF dp] by simp
   from z[rule_format, OF yz] incr_mult_lemma[OF dp th zp, rule_format, OF P] have th2: " P' ?y" by auto
   with periodic_finite_ex[OF dp pd]
   have "?R1" by blast}
ultimately show ?thesis by blast
qed

lemma simp_from_to: "{i..j::int} = (if j < i then {} else insert i {i+1..j})"
apply(simp add:atLeastAtMost_def atLeast_def atMost_def)
apply(fastforce)
done

theorem unity_coeff_ex: "(\(x::'a::{semiring_0,Rings.dvd}). P (l * x)) \ (\x. l dvd (x + 0) \ P x)"
  unfolding dvd_def by (rule eq_reflection, rule iffI) auto

lemma zdvd_mono:
  fixes k m t :: int
  assumes "k \ 0"
  shows "m dvd t \ k * m dvd k * t"
  using assms by simp

lemma uminus_dvd_conv:
  fixes d t :: int
  shows "d dvd t \ - d dvd t" and "d dvd t \ d dvd - t"
  by simp_all

text \<open>\bigskip Theorems for transforming predicates on nat to predicates on \<open>int\<close>\<close>

lemma zdiff_int_split: "P (int (x - y)) =
  ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
  by (cases "y \ x") (simp_all add: of_nat_diff)

text \<open>
  \medskip Specific instances of congruence rules, to prevent
  simplifier from looping.\<close>

theorem imp_le_cong:
  "\x = x'; 0 \ x' \ P = P'\ \ (0 \ (x::int) \ P) = (0 \ x' \ P')"
  by simp

theorem conj_le_cong:
  "\x = x'; 0 \ x' \ P = P'\ \ (0 \ (x::int) \ P) = (0 \ x' \ P')"
  by (simp cong: conj_cong)

ML_file \<open>Tools/Qelim/cooper.ML\<close>

method_setup presburger = \<open>
  let
    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
    val addN = "add"
    val delN = "del"
    val elimN = "elim"
    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm)
  in
    Scan.optional (simple_keyword elimN >> K false) true --
    Scan.optional (keyword addN |-- thms) [] --
    Scan.optional (keyword delN |-- thms) [] >>
    (fn ((elim, add_ths), del_ths) => fn ctxt =>
      SIMPLE_METHOD' (Cooper.tac elim add_ths del_ths ctxt))
  end
\<close> "Cooper's algorithm for Presburger arithmetic"

declare mod_eq_0_iff_dvd [presburger]
declare mod_by_Suc_0 [presburger]
declare mod_0 [presburger]
declare mod_by_1 [presburger]
declare mod_self [presburger]
declare div_by_0 [presburger]
declare mod_by_0 [presburger]
declare mod_div_trivial [presburger]
declare mult_div_mod_eq [presburger]
declare div_mult_mod_eq [presburger]
declare mod_mult_self1 [presburger]
declare mod_mult_self2 [presburger]
declare mod2_Suc_Suc [presburger]
declare not_mod_2_eq_0_eq_1 [presburger]
declare nat_zero_less_power_iff [presburger]

lemma [presburger, algebra]: "m mod 2 = (1::nat) \ \ 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = Suc 0 \ \ 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \ \ 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \ \ 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \ \ 2 dvd m " by presburger

context semiring_parity
begin

declare even_mult_iff [presburger]

declare even_power [presburger]

lemma [presburger]:
  "even (a + b) \ even a \ even b \ odd a \ odd b"
  by auto

end

context ring_parity
begin

declare even_minus [presburger]

end

context linordered_idom
begin

declare zero_le_power_eq [presburger]

declare zero_less_power_eq [presburger]

declare power_less_zero_eq [presburger]

declare power_le_zero_eq [presburger]

end

declare even_Suc [presburger]

lemma [presburger]:
  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \ even n"
  by presburger

declare even_diff_nat [presburger]

lemma [presburger]:
  fixes k :: int
  shows "(k + 1) div 2 = k div 2 \ even k"
  by presburger

lemma [presburger]:
  fixes k :: int
  shows "(k + 1) div 2 = k div 2 + 1 \ odd k"
  by presburger

lemma [presburger]:
  "even n \ even (int n)"
  by simp


subsection \<open>Nice facts about division by \<^term>\<open>4\<close>\<close>

lemma even_even_mod_4_iff:
  "even (n::nat) \ even (n mod 4)"
  by presburger

lemma odd_mod_4_div_2:
  "n mod 4 = (3::nat) \ odd ((n - Suc 0) div 2)"
  by presburger

lemma even_mod_4_div_2:
  "n mod 4 = Suc 0 \ even ((n - Suc 0) div 2)"
  by presburger

end

quality99%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.