src/HOL/Presburger.thy
 changeset 36802 5f9fe7b3295d parent 36800 59b50c691b75 child 36803 2cad8904c4ff
```--- a/src/HOL/Presburger.thy	Mon May 10 14:55:04 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 14:55:06 2010 +0200
@@ -218,16 +218,6 @@
lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"

-theorem int_induct[case_names base step1 step2]:
-  assumes
-  base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and
-  step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
-  shows "P i"
-proof -
-  have "i \<le> k \<or> i\<ge> k" by arith
-  thus ?thesis using prems int_ge_induct[where P="P" and k="k" and i="i"] int_le_induct[where P="P" and k="k" and i="i"] by blast
-qed
-
lemma decr_mult_lemma:
assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
shows "ALL x. P x \<longrightarrow> P(x - k*d)"
@@ -402,29 +392,8 @@
use "Tools/Qelim/cooper.ML"

setup Cooper.setup
-oracle linzqe_oracle = Cooper.cooper_oracle

-use "Tools/Qelim/presburger.ML"
-
-setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
-
-method_setup presburger = {*
-let
- fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
- fun simple_keyword k = Scan.lift (Args.\$\$\$ k) >> K ()
- val delN = "del"
- val elimN = "elim"
- val any_keyword = keyword addN || keyword delN || simple_keyword elimN
- val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-in
-  Scan.optional (simple_keyword elimN >> K false) true --
-  Scan.optional (keyword addN |-- thms) [] --
-  Scan.optional (keyword delN |-- thms) [] >>
-  (fn ((elim, add_ths), del_ths) => fn ctxt =>
-    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
-end
-*} "Cooper's algorithm for Presburger arithmetic"
+method_setup presburger = "Cooper.cooper_method" "Cooper's algorithm for Presburger arithmetic"

declare dvd_eq_mod_eq_0[symmetric, presburger]
declare mod_1[presburger] ```