# HG changeset patch
# User haftmann
# Date 1273493510 -7200
# Node ID 628fe06cbeffa96e0498eafe21d49591144c0e64
# Parent  3981db1621313b094687449d366c80ad29f5a64d
one structure is better than three

diff -r 3981db162131 -r 628fe06cbeff src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon May 10 13:58:18 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 14:11:50 2010 +0200
@@ -398,14 +398,15 @@
 
 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
   by (simp cong: conj_cong)
+
 lemma int_eq_number_of_eq:
   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by (rule eq_number_of_eq)
 
 use "Tools/Qelim/cooper.ML"
 
-setup CooperData.setup
-oracle linzqe_oracle = Coopereif.cooper_oracle
+setup Cooper.setup
+oracle linzqe_oracle = Cooper.cooper_oracle
 
 use "Tools/Qelim/presburger.ML"
 
diff -r 3981db162131 -r 628fe06cbeff src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 13:58:18 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:11:50 2010 +0200
@@ -2,30 +2,22 @@
     Author:     Amine Chaieb, TU Muenchen
 *)
 
-signature COOPER_DATA =
+signature COOPER =
 sig
   type entry
   val get: Proof.context -> entry
   val del: term list -> attribute
   val add: term list -> attribute 
   val setup: theory -> theory
-end;
-
-signature COOPER =
-sig
   val cooper_conv: Proof.context -> conv
+  val cooper_oracle: cterm -> cterm
   exception COOPER of string * exn
 end;
 
-signature COOPER_REIFY =
-sig
-  val cooper_oracle: cterm -> cterm
-end;
-
-structure CooperData : COOPER_DATA =
+structure Cooper: COOPER =
 struct
 
-type entry = simpset * (term list);
+type entry = simpset * term list;
 
 val allowed_consts = 
   [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
@@ -95,11 +87,6 @@
 
 end;
 
-end;
-
-structure Cooper: COOPER =
-struct
-
 exception COOPER of string * exn;
 fun simp_thms_conv ctxt =
   Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
@@ -606,12 +593,8 @@
         | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
 in val cooper_conv = conv
 end;
-end;
 
-structure Coopereif : COOPER_REIFY =
-struct
-
-fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
+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!"
diff -r 3981db162131 -r 628fe06cbeff src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 13:58:18 2010 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 14:11:50 2010 +0200
@@ -83,13 +83,13 @@
  in h [] end;
 in 
 fun is_relevant ctxt ct = 
- subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
+ 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 (CooperData.get ctxt)
+  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)
@@ -161,7 +161,7 @@
   (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 (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
+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