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.34 - val addN = "add"
    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]