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"