src/HOL/Presburger.thy
changeset 23430 771117253634
parent 23405 8993b3144358
child 23438 dd824e86fa8a
equal deleted inserted replaced
23429:5a55a9409e57 23430:771117253634
     1 (*  Title:      HOL/Presburger.thy
     1 (*  Title:      HOL/Presburger.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Amine Chaieb, TU Muenchen
     3     Author:     Amine Chaieb, TU Muenchen
     4 *)
     4 *)
       
     5 
       
     6 header {* Decision Procedure for Presburger Arithmetic *}
     5 
     7 
     6 theory Presburger
     8 theory Presburger
     7 imports NatSimprocs SetInterval
     9 imports NatSimprocs SetInterval
     8   uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" 
    10   uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" 
     9        "Tools/Presburger/generated_cooper.ML"
    11        "Tools/Presburger/generated_cooper.ML"
    10        ("Tools/Presburger/cooper.ML") ("Tools/Presburger/presburger.ML") 
    12        ("Tools/Presburger/cooper.ML") ("Tools/Presburger/presburger.ML") 
    11        
    13        
    12 begin
    14 begin
    13 setup {* Cooper_Data.setup*}
    15 setup {* Cooper_Data.setup*}
    14 
    16 
    15 section{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    17 subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    16 
    18 
    17 lemma minf:
    19 lemma minf:
    18   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    20   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    19      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
    21      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
    20   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    22   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
   173   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
   175   {fix x assume H: "\<not>(d dvd x + t)" with d have "\<not>d dvd (x + D) + t"
   174       by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
   176       by (clarsimp simp add: dvd_def,erule_tac x= "ka - k" in allE,simp add: ring_eq_simps)}
   175   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
   177   thus "\<forall>(x::int).(\<forall>j\<in>{1 .. D}. \<forall>b\<in>A. x \<noteq> b - j)\<longrightarrow> (\<not>d dvd x+t) \<longrightarrow> (\<not>d dvd (x + D) + t)" by auto
   176 qed blast
   178 qed blast
   177 
   179 
   178 section{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
   180 subsection{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
   179 
   181 
   180 subsection{* First some trivial facts about periodic sets or predicates *}
   182 subsubsection{* First some trivial facts about periodic sets or predicates *}
   181 lemma periodic_finite_ex:
   183 lemma periodic_finite_ex:
   182   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   184   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   183   shows "(EX x. P x) = (EX j : {1..d}. P j)"
   185   shows "(EX x. P x) = (EX j : {1..d}. P j)"
   184   (is "?LHS = ?RHS")
   186   (is "?LHS = ?RHS")
   185 proof
   187 proof
   206     qed
   208     qed
   207     ultimately show ?RHS ..
   209     ultimately show ?RHS ..
   208   qed
   210   qed
   209 qed auto
   211 qed auto
   210 
   212 
   211 subsection{* The @{text "-\<infinity>"} Version*}
   213 subsubsection{* The @{text "-\<infinity>"} Version*}
   212 
   214 
   213 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   215 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
   214 by(induct rule: int_gr_induct,simp_all add:int_distrib)
   216 by(induct rule: int_gr_induct,simp_all add:int_distrib)
   215 
   217 
   216 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   218 lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   284    with periodic_finite_ex[OF dp pd]
   286    with periodic_finite_ex[OF dp pd]
   285    have "?R1" by blast}
   287    have "?R1" by blast}
   286  ultimately show ?thesis by blast
   288  ultimately show ?thesis by blast
   287 qed
   289 qed
   288 
   290 
   289 subsection {* The @{text "+\<infinity>"} Version*}
   291 subsubsection {* The @{text "+\<infinity>"} Version*}
   290 
   292 
   291 lemma  plusinfinity:
   293 lemma  plusinfinity:
   292   assumes dpos: "(0::int) < d" and
   294   assumes dpos: "(0::int) < d" and
   293     P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   295     P1eqP1: "\<forall>x k. P' x = P'(x - k*d)" and ePeqP1: "\<exists> z. \<forall> x>z. P x = P' x"
   294   shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"
   296   shows "(\<exists> x. P' x) \<longrightarrow> (\<exists> x. P x)"