# HG changeset patch
# User haftmann
# Date 1273496106 -7200
# Node ID 5f9fe7b3295d749bd6faee8a4cd8739e9786a643
# Parent  3560de0fe851e05bc674c43cfd41e3e7a379f9f3
only one module fpr presburger method

diff -r 3560de0fe851 -r 5f9fe7b3295d src/HOL/Presburger.thy
--- 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"
 by(induct rule: int_gr_induct, simp_all add:int_distrib)
 
-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 addN = "add"
- 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] 
diff -r 3560de0fe851 -r 5f9fe7b3295d src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:55:04 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:55:06 2010 +0200
@@ -1,5 +1,7 @@
 (*  Title:      HOL/Tools/Qelim/cooper.ML
     Author:     Amine Chaieb, TU Muenchen
+
+Presburger arithmetic by Cooper's algorithm.
 *)
 
 signature COOPER =
@@ -8,10 +10,12 @@
   val get: Proof.context -> entry
   val del: term list -> attribute
   val add: term list -> attribute 
+  val cooper_conv: Proof.context -> conv
+  val cooper_oracle: cterm -> thm
+  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
+  val cooper_method: (Proof.context -> Method.method) context_parser
+  exception COOPER of string * exn
   val setup: theory -> theory
-  val cooper_conv: Proof.context -> conv
-  val cooper_oracle: cterm -> cterm
-  exception COOPER of string * exn
 end;
 
 structure Cooper: COOPER =
@@ -25,7 +29,6 @@
    @{term "op * :: int => _"}, @{term "op * :: nat => _"},
    @{term "op div :: int => _"}, @{term "op div :: nat => _"},
    @{term "op mod :: int => _"}, @{term "op mod :: nat => _"},
-   @{term "Int.Bit0"}, @{term "Int.Bit1"},
    @{term "op &"}, @{term "op |"}, @{term "op -->"}, 
    @{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"},
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
@@ -64,30 +67,6 @@
   context |> Data.map (fn (ss,ts') => 
      (ss delsimps [th], subtract (op aconv) ts' ts ))) 
 
-
-(* theory setup *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
-
-val constsN = "consts";
-val any_keyword = keyword constsN
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-val terms = thms >> map (term_of o Drule.dest_term);
-
-fun optional scan = Scan.optional scan [];
-
-in
-
-val setup =
-  Attrib.setup @{binding presburger}
-    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
-      optional (keyword constsN |-- terms) >> add) "Cooper data";
-
-end;
-
-exception COOPER of string * exn;
 fun simp_thms_conv ctxt =
   Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
 val FWD = Drule.implies_elim_list;
@@ -274,6 +253,9 @@
 fun linear_neg tm = linear_cmul ~1 tm;
 fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
 
+exception COOPER of string * exn;
+
+fun cooper s = raise COOPER ("Cooper failed", ERROR s);
 
 fun lint vars tm =  if is_numeral tm then tm  else case tm of
   Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
@@ -594,7 +576,6 @@
 in val cooper_conv = conv
 end;
 
-fun cooper s = raise COOPER ("Cooper oracle failed", ERROR s);
 fun i_of_term vs t = case t
  of Free (xn, xT) => (case AList.lookup (op aconv) vs t
      of NONE   => cooper "Variable not found in the list!"
@@ -619,7 +600,7 @@
   | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Rings.dvd},_)$t1$t2 =>
-      (Cooper_Procedure.Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
+      (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle TERM _ => cooper "Reification: unsupported dvd")
   | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
   | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
@@ -695,7 +676,7 @@
  | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
  | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
 
-fun cooper_oracle ct =
+fun raw_cooper_oracle ct =
   let
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
@@ -705,4 +686,218 @@
       HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
   end;
 
+val (_, cooper_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (Binding.name "cooper", raw_cooper_oracle)));
+
+val comp_ss = HOL_ss addsimps @{thms semiring_norm};
+
+fun strip_objimp ct =
+  (case Thm.term_of ct of
+    Const ("op -->", _) $ _ $ _ =>
+      let val (A, B) = Thm.dest_binop ct
+      in A :: strip_objimp B end
+  | _ => [ct]);
+
+fun strip_objall ct = 
+ case term_of ct of 
+  Const ("All", _) $ Abs (xn,xT,p) => 
+   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
+   in apfst (cons (a,v)) (strip_objall t')
+   end
+| _ => ([],ct);
+
+local
+  val all_maxscope_ss = 
+     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
+in
+fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
+  CSUBGOAL (fn (p', i) =>
+    let
+     val (qvs, p) = strip_objall (Thm.dest_arg p')
+     val (ps, c) = split_last (strip_objimp p)
+     val qs = filter P ps
+     val q = if P c then c else @{cterm "False"}
+     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
+         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
+     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
+     val ntac = (case qs of [] => q aconvc @{cterm "False"}
+                         | _ => false)
+    in 
+    if ntac then no_tac
+      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
+    end)
 end;
+
+local
+ fun isnum t = case t of 
+   Const(@{const_name Groups.zero},_) => true
+ | Const(@{const_name Groups.one},_) => true
+ | @{term "Suc"}$s => isnum s
+ | @{term "nat"}$s => isnum s
+ | @{term "int"}$s => isnum s
+ | Const(@{const_name Groups.uminus},_)$s => isnum s
+ | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
+ | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
+
+ fun ty cts t = 
+ if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
+    else case term_of t of 
+      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
+               then not (isnum l orelse isnum r)
+               else not (member (op aconv) cts c)
+    | c$_ => not (member (op aconv) cts c)
+    | c => not (member (op aconv) cts c)
+
+ val term_constants =
+  let fun h acc t = case t of
+    Const _ => insert (op aconv) t acc
+  | a$b => h (h acc a) b
+  | Abs (_,_,t) => h acc t
+  | _ => acc
+ in h [] end;
+in 
+fun is_relevant ctxt ct = 
+ subset (op aconv) (term_constants (term_of ct) , snd (get ctxt))
+ andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
+ andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
+
+fun int_nat_terms ctxt ct =
+ let 
+  val cts = snd (get ctxt)
+  fun h acc t = if ty cts t then insert (op aconvc) t acc else
+   case (term_of t) of
+    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+  | _ => acc
+ in h [] ct end
+end;
+
+fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
+ let 
+   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
+   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
+   val p' = fold_rev gen ts p
+ in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
+
+local
+val ss1 = comp_ss
+  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
+      @ map (fn r => r RS sym) 
+        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
+         @{thm "zmult_int"}]
+    addsplits [@{thm "zdiff_int_split"}]
+
+val ss2 = HOL_basic_ss
+  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
+            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
+            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
+  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
+val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
+  @ map (symmetric o mk_meta_eq) 
+    [@{thm "dvd_eq_mod_eq_0"},
+     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
+     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
+  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
+     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
+     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
+     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
+     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
+  @ @{thms add_ac}
+ addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+ val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
+     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
+      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
+in
+fun nat_to_int_tac ctxt = 
+  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
+  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
+  simp_tac (Simplifier.context ctxt comp_ss);
+
+fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
+fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
+end;
+
+fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
+   let 
+    val cpth = 
+       if !quick_and_dirty 
+       then cooper_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
+             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
+       else Conv.arg_conv (cooper_conv ctxt) p
+    val p' = Thm.rhs_of cpth
+    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
+   in rtac th i end
+   handle COOPER _ => no_tac);
+
+fun finish_tac q = SUBGOAL (fn (_, i) =>
+  (if q then I else TRY) (rtac TrueI i));
+
+fun cooper_tac elim add_ths del_ths ctxt =
+let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
+    val aprems = Arith_Data.get_arith_facts ctxt
+in
+  Method.insert_tac aprems
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
+  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
+  THEN_ALL_NEW simp_tac ss
+  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
+  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
+  THEN_ALL_NEW div_mod_tac ctxt
+  THEN_ALL_NEW splits_tac ctxt
+  THEN_ALL_NEW simp_tac ss
+  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
+  THEN_ALL_NEW nat_to_int_tac ctxt
+  THEN_ALL_NEW (core_cooper_tac ctxt)
+  THEN_ALL_NEW finish_tac elim
+end;
+
+val cooper_method =
+  let
+    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
+    val addN = "add"
+    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' (cooper_tac elim add_ths del_ths ctxt))
+  end;
+
+
+(* theory setup *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
+
+val constsN = "consts";
+val any_keyword = keyword constsN
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+val terms = thms >> map (term_of o Drule.dest_term);
+
+fun optional scan = Scan.optional scan [];
+
+in
+
+val setup =
+  Attrib.setup @{binding presburger}
+    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+      optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
+  #> Arith_Data.add_tactic "Presburger arithmetic" (K (cooper_tac true [] []));
+
+end;
+
+end;
diff -r 3560de0fe851 -r 5f9fe7b3295d src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 14:55:04 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,184 +0,0 @@
-(*  Title:      HOL/Tools/Qelim/presburger.ML
-    Author:     Amine Chaieb, TU Muenchen
-*)
-
-signature PRESBURGER =
-sig
-  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
-end;
-
-structure Presburger : PRESBURGER = 
-struct
-
-val comp_ss = HOL_ss addsimps @{thms semiring_norm};
-
-fun strip_objimp ct =
-  (case Thm.term_of ct of
-    Const ("op -->", _) $ _ $ _ =>
-      let val (A, B) = Thm.dest_binop ct
-      in A :: strip_objimp B end
-  | _ => [ct]);
-
-fun strip_objall ct = 
- case term_of ct of 
-  Const ("All", _) $ Abs (xn,xT,p) => 
-   let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
-   in apfst (cons (a,v)) (strip_objall t')
-   end
-| _ => ([],ct);
-
-local
-  val all_maxscope_ss = 
-     HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"}
-in
-fun thin_prems_tac P = simp_tac all_maxscope_ss THEN'
-  CSUBGOAL (fn (p', i) =>
-    let
-     val (qvs, p) = strip_objall (Thm.dest_arg p')
-     val (ps, c) = split_last (strip_objimp p)
-     val qs = filter P ps
-     val q = if P c then c else @{cterm "False"}
-     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
-         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q)
-     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
-     val ntac = (case qs of [] => q aconvc @{cterm "False"}
-                         | _ => false)
-    in 
-    if ntac then no_tac
-      else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i
-    end)
-end;
-
-local
- fun isnum t = case t of 
-   Const(@{const_name Groups.zero},_) => true
- | Const(@{const_name Groups.one},_) => true
- | @{term "Suc"}$s => isnum s
- | @{term "nat"}$s => isnum s
- | @{term "int"}$s => isnum s
- | Const(@{const_name Groups.uminus},_)$s => isnum s
- | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
- | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
-
- fun ty cts t = 
- if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
-    else case term_of t of 
-      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
-               then not (isnum l orelse isnum r)
-               else not (member (op aconv) cts c)
-    | c$_ => not (member (op aconv) cts c)
-    | c => not (member (op aconv) cts c)
-
- val term_constants =
-  let fun h acc t = case t of
-    Const _ => insert (op aconv) t acc
-  | a$b => h (h acc a) b
-  | Abs (_,_,t) => h acc t
-  | _ => acc
- in h [] end;
-in 
-fun is_relevant ctxt ct = 
- subset (op aconv) (term_constants (term_of ct) , snd (Cooper.get ctxt))
- andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
- andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
-
-fun int_nat_terms ctxt ct =
- let 
-  val cts = snd (Cooper.get ctxt)
-  fun h acc t = if ty cts t then insert (op aconvc) t acc else
-   case (term_of t) of
-    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
-  | _ => acc
- in h [] ct end
-end;
-
-fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
- let 
-   fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
-   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
-   val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
-   val p' = fold_rev gen ts p
- in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end));
-
-local
-val ss1 = comp_ss
-  addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] 
-      @ map (fn r => r RS sym) 
-        [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, 
-         @{thm "zmult_int"}]
-    addsplits [@{thm "zdiff_int_split"}]
-
-val ss2 = HOL_basic_ss
-  addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
-            @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
-            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
-  addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
-val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms}
-  @ map (symmetric o mk_meta_eq) 
-    [@{thm "dvd_eq_mod_eq_0"},
-     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
-     @{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
-  @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, 
-     @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
-     @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
-     @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
-     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
-  @ @{thms add_ac}
- addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
- val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
-     [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
-      @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
-in
-fun nat_to_int_tac ctxt = 
-  simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW
-  simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW
-  simp_tac (Simplifier.context ctxt comp_ss);
-
-fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i;
-fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
-end;
-
-
-fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
-   let 
-    val cpth = 
-       if !quick_and_dirty 
-       then linzqe_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
-             (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
-       else Conv.arg_conv (Cooper.cooper_conv ctxt) p
-    val p' = Thm.rhs_of cpth
-    val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
-   in rtac th i end
-   handle Cooper.COOPER _ => no_tac);
-
-fun finish_tac q = SUBGOAL (fn (_, i) =>
-  (if q then I else TRY) (rtac TrueI i));
-
-fun cooper_tac elim add_ths del_ths ctxt =
-let val ss = Simplifier.context ctxt (fst (Cooper.get ctxt)) delsimps del_ths addsimps add_ths
-    val aprems = Arith_Data.get_arith_facts ctxt
-in
-  Method.insert_tac aprems
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
-  THEN_ALL_NEW simp_tac ss
-  THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
-  THEN_ALL_NEW Object_Logic.full_atomize_tac
-  THEN_ALL_NEW div_mod_tac ctxt
-  THEN_ALL_NEW splits_tac ctxt
-  THEN_ALL_NEW simp_tac ss
-  THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
-  THEN_ALL_NEW nat_to_int_tac ctxt
-  THEN_ALL_NEW (core_cooper_tac ctxt)
-  THEN_ALL_NEW finish_tac elim
-end;
-
-end;