products/sources/formale Sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: abstract_max.prf   Sprache: Lisp

Untersuchung 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
keywords "try0" :: diag
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
  by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastforce)+) simp_all

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"
  by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastforce)+) simp_all

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"
  {fix x assume H: "d dvd x + t" with d have "d dvd (x + D) + t"
      by (clarsimp simp add: dvd_def,rule_tac x= "ka + k" in exI,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 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\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)"
  apply (rule eq_reflection [symmetric])
  apply (rule iffI)
  defer
  apply (erule exE)
  apply (rule_tac x = "l * x" in exI)
  apply (simp add: dvd_def)
  apply (rule_tac x = x in exI, simp)
  apply (erule exE)
  apply (erule conjE)
  apply simp
  apply (erule dvdE)
  apply (rule_tac x = k in exI)
  apply simp
  done

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


subsection \<open>Try0\<close>

ML_file \<open>Tools/try0.ML\<close>

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.44Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff