src/HOL/Presburger.thy
 changeset 36802 5f9fe7b3295d parent 36800 59b50c691b75 child 36803 2cad8904c4ff
```     1.1 --- a/src/HOL/Presburger.thy	Mon May 10 14:55:04 2010 +0200
1.2 +++ b/src/HOL/Presburger.thy	Mon May 10 14:55:06 2010 +0200
1.3 @@ -218,16 +218,6 @@
1.4  lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
1.5  by(induct rule: int_gr_induct, simp_all add:int_distrib)
1.6
1.7 -theorem int_induct[case_names base step1 step2]:
1.8 -  assumes
1.9 -  base: "P(k::int)" and step1: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)" and
1.10 -  step2: "\<And>i. \<lbrakk>k \<ge> i; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
1.11 -  shows "P i"
1.12 -proof -
1.13 -  have "i \<le> k \<or> i\<ge> k" by arith
1.14 -  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
1.15 -qed
1.16 -
1.17  lemma decr_mult_lemma:
1.18    assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
1.19    shows "ALL x. P x \<longrightarrow> P(x - k*d)"
1.20 @@ -402,29 +392,8 @@
1.21  use "Tools/Qelim/cooper.ML"
1.22
1.23  setup Cooper.setup
1.24 -oracle linzqe_oracle = Cooper.cooper_oracle
1.25
1.26 -use "Tools/Qelim/presburger.ML"
1.27 -
1.28 -setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
1.29 -
1.30 -method_setup presburger = {*
1.31 -let
1.32 - fun keyword k = Scan.lift (Args.\$\$\$ k -- Args.colon) >> K ()
1.33 - fun simple_keyword k = Scan.lift (Args.\$\$\$ k) >> K ()
1.35 - val delN = "del"
1.36 - val elimN = "elim"
1.37 - val any_keyword = keyword addN || keyword delN || simple_keyword elimN
1.38 - val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
1.39 -in
1.40 -  Scan.optional (simple_keyword elimN >> K false) true --
1.41 -  Scan.optional (keyword addN |-- thms) [] --
1.42 -  Scan.optional (keyword delN |-- thms) [] >>
1.43 -  (fn ((elim, add_ths), del_ths) => fn ctxt =>
1.44 -    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
1.45 -end
1.46 -*} "Cooper's algorithm for Presburger arithmetic"
1.47 +method_setup presburger = "Cooper.cooper_method" "Cooper's algorithm for Presburger arithmetic"
1.48
1.49  declare dvd_eq_mod_eq_0[symmetric, presburger]
1.50  declare mod_1[presburger]
```