section headings
authorhuffman
Thu Jun 21 23:49:26 2007 +0200 (2007-06-21)
changeset 2347202099ea56555
parent 23471 08e6c03b2a72
child 23473 997bca36d4fe
section headings
src/HOL/Presburger.thy
     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>