# HG changeset patch
# User huffman
# Date 1182308816 -7200
# Node ID 771117253634ba292630d3088f26a69dc69da766
# Parent  5a55a9409e573301994f92871cc8d20c831d3e4c
section headings

diff -r 5a55a9409e57 -r 771117253634 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Jun 20 05:06:16 2007 +0200
+++ b/src/HOL/Presburger.thy	Wed Jun 20 05:06:56 2007 +0200
@@ -3,6 +3,8 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
+header {* Decision Procedure for Presburger Arithmetic *}
+
 theory Presburger
 imports NatSimprocs SetInterval
   uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim" 
@@ -12,7 +14,7 @@
 begin
 setup {* Cooper_Data.setup*}
 
-section{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
+subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
 
 lemma minf:
   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
@@ -175,9 +177,9 @@
   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
 qed blast
 
-section{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
+subsection{* Cooper's Theorem @{text "-\<infinity>"} and @{text "+\<infinity>"} Version *}
 
-subsection{* First some trivial facts about periodic sets or predicates *}
+subsubsection{* First some trivial facts about periodic sets or predicates *}
 lemma periodic_finite_ex:
   assumes dpos: "(0::int) < d" and modd: "ALL x k. P x = P(x - k*d)"
   shows "(EX x. P x) = (EX j : {1..d}. P j)"
@@ -208,7 +210,7 @@
   qed
 qed auto
 
-subsection{* The @{text "-\<infinity>"} Version*}
+subsubsection{* The @{text "-\<infinity>"} Version*}
 
 lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
 by(induct rule: int_gr_induct,simp_all add:int_distrib)
@@ -286,7 +288,7 @@
  ultimately show ?thesis by blast
 qed
 
-subsection {* The @{text "+\<infinity>"} Version*}
+subsubsection {* The @{text "+\<infinity>"} Version*}
 
 lemma  plusinfinity:
   assumes dpos: "(0::int) < d" and