src/HOL/Presburger.thy
 changeset 23472 02099ea56555 parent 23465 8f8835aac299 child 23477 f4b83f03cac9
```     1.1 --- a/src/HOL/Presburger.thy	Thu Jun 21 23:33:10 2007 +0200
1.2 +++ b/src/HOL/Presburger.thy	Thu Jun 21 23:49:26 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 Arith_Tools SetInterval
1.11  uses
1.12 @@ -12,8 +14,6 @@
1.13    ("Tools/Qelim/presburger.ML")
1.14  begin
1.15
1.16 -subsection {* Decision Procedure for Presburger Arithmetic *}
1.17 -
1.18  setup CooperData.setup
1.19
1.20  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
1.21 @@ -62,7 +62,7 @@
1.22    (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
1.23      simp add: ring_eq_simps, clarsimp,rule_tac x = "kb + ka*k" in exI,simp add: ring_eq_simps)+
1.24
1.25 -section{* The A and B sets *}
1.26 +subsection{* The A and B sets *}
1.27  lemma bset:
1.28    "\<lbrakk>\<forall>x.(\<forall>j \<in> {1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> P x \<longrightarrow> P(x - D) ;
1.29       \<forall>x.(\<forall>j\<in>{1 .. D}. \<forall>b\<in>B. x \<noteq> b + j)\<longrightarrow> Q x \<longrightarrow> Q(x - D)\<rbrakk> \<Longrightarrow>
```