src/HOL/Presburger.thy
changeset 23430 771117253634
parent 23405 8993b3144358
child 23438 dd824e86fa8a
     1.1 --- a/src/HOL/Presburger.thy	Wed Jun 20 05:06:16 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Jun 20 05:06:56 2007 +0200
     1.3 @@ -3,6 +3,8 @@
     1.4      Author:     Amine Chaieb, TU Muenchen
     1.5  *)
     1.6  
     1.7 +header {* Decision Procedure for Presburger Arithmetic *}
     1.8 +
     1.9  theory Presburger
    1.10  imports NatSimprocs SetInterval
    1.11    uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" 
    1.12 @@ -12,7 +14,7 @@
    1.13  begin
    1.14  setup {* Cooper_Data.setup*}
    1.15  
    1.16 -section{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    1.17 +subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
    1.18  
    1.19  lemma minf:
    1.20    "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
    1.21 @@ -175,9 +177,9 @@
    1.22    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
    1.23  qed blast
    1.24  
    1.25 -section{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
    1.26 +subsection{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
    1.27  
    1.28 -subsection{* First some trivial facts about periodic sets or predicates *}
    1.29 +subsubsection{* First some trivial facts about periodic sets or predicates *}
    1.30  lemma periodic_finite_ex:
    1.31    assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
    1.32    shows "(EX x. P x) = (EX j : {1..d}. P j)"
    1.33 @@ -208,7 +210,7 @@
    1.34    qed
    1.35  qed auto
    1.36  
    1.37 -subsection{* The @{text "-\<infinity>"} Version*}
    1.38 +subsubsection{* The @{text "-\<infinity>"} Version*}
    1.39  
    1.40  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
    1.41  by(induct rule: int_gr_induct,simp_all add:int_distrib)
    1.42 @@ -286,7 +288,7 @@
    1.43   ultimately show ?thesis by blast
    1.44  qed
    1.45  
    1.46 -subsection {* The @{text "+\<infinity>"} Version*}
    1.47 +subsubsection {* The @{text "+\<infinity>"} Version*}
    1.48  
    1.49  lemma  plusinfinity:
    1.50    assumes dpos: "(0::int) < d" and