src/HOL/Presburger.thy
 changeset 23430 771117253634 parent 23405 8993b3144358 child 23438 dd824e86fa8a
equal 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)"`