src/HOL/ex/Reflected_Presburger.thy

-(* A formalization of quantifier elimination for Presburger arithmetic*)
-(* based on a generic quantifier elimination algorithm and 
-   cooper's methos to eliminate on \<exists> *)
+(*  Title:      HOL/ex/PresburgerEx.thy
+    ID:         $Id$
+    Author:     Amine Chaieb, TU Muenchen
+
+A formalization of quantifier elimination for Presburger arithmetic
+based on a generic quantifier elimination algorithm and Cooper's
+methos to eliminate on \<exists>. *)
+
+header {* Quantifier elimination for Presburger arithmetic *}
 
 theory Reflected_Presburger
 imports Main
-(* uses ("rcooper.ML") ("rpresbtac.ML") *)
 begin
 
 (* Shadow syntax for integer terms *)
 datatype intterm =
     Cst int

   assumes lpos: "(0::int) < l"
   and inz: "i \<noteq> 0"
   and dvd: "i dvd l"
   shows "(i*x + r = 0) = (l*x + ((l div i)*r) = 0)"
 proof-
-  thm dvd_div_pos[OF lpos inz dvd]
   have ldvdii: "(l div i)*i = l" by (rule dvd_div_pos[OF lpos inz dvd])
   have ldivinz: "l div i \<noteq> 0" using inz ldvdii lpos by auto
   have "(i*x + r = 0) = ((l div i)*(i*x + r) = (l div i)*0)"
     using ldivinz by arith
   also have "\<dots> = (((l div i)*i)*x + (l div i)*r = 0)"

 	  moreover
 	  {
 	    assume nz: "n=0"
 	    from prems have inz: "i \<noteq> 0" by auto
 	    from prems nz have idvdl: "i dvd l" by simp
-	    thm adjustcoeff_eq_corr[OF lpos inz idvdl]
 	    have "(i * a + (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0) =
 	      (l * a + l div i * (i' * (a # ats) ! n' + I_intterm (a # ats) r) = 0)"
 	      by (rule adjustcoeff_eq_corr[OF lpos inz idvdl])
 	    then 
 	    have ?thesis using prems linr linr2

 (* divlcm is correct *)
 lemma divlcm_corr:
   assumes 
   linp: "islinform p"
   shows "alldivide (divlcm p,p)"
-thm nz_le[OF divlcm_pos[OF linp]]
   using linp divlcm_pos
 proof (induct p rule: divlcm.induct,simp_all add: zdvd_refl_abs,clarsimp simp add: Nat.gr0_conv_Suc)
   case (goal1 f)
   have "islinform f" using prems  
     by (cases f, auto) (case_tac "intterm2", auto,case_tac "intterm1", auto)

 use "rcooper.ML"
 oracle rpresburger_oracle ("term") = RCooper.rpresburger_oracle
 use "rpresbtac.ML"
 setup RPresburger.setup
 *)
+
 end