one structure is better than three
authorhaftmann
Mon May 10 14:11:50 2010 +0200 (2010-05-10)
changeset 36799628fe06cbeff
parent 36798 3981db162131
child 36800 59b50c691b75
one structure is better than three
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/presburger.ML
     1.1 --- a/src/HOL/Presburger.thy	Mon May 10 13:58:18 2010 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon May 10 14:11:50 2010 +0200
     1.3 @@ -398,14 +398,15 @@
     1.4  
     1.5  theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
     1.6    by (simp cong: conj_cong)
     1.7 +
     1.8  lemma int_eq_number_of_eq:
     1.9    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
    1.10    by (rule eq_number_of_eq)
    1.11  
    1.12  use "Tools/Qelim/cooper.ML"
    1.13  
    1.14 -setup CooperData.setup
    1.15 -oracle linzqe_oracle = Coopereif.cooper_oracle
    1.16 +setup Cooper.setup
    1.17 +oracle linzqe_oracle = Cooper.cooper_oracle
    1.18  
    1.19  use "Tools/Qelim/presburger.ML"
    1.20  
     2.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 13:58:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:11:50 2010 +0200
     2.3 @@ -2,30 +2,22 @@
     2.4      Author:     Amine Chaieb, TU Muenchen
     2.5  *)
     2.6  
     2.7 -signature COOPER_DATA =
     2.8 +signature COOPER =
     2.9  sig
    2.10    type entry
    2.11    val get: Proof.context -> entry
    2.12    val del: term list -> attribute
    2.13    val add: term list -> attribute 
    2.14    val setup: theory -> theory
    2.15 -end;
    2.16 -
    2.17 -signature COOPER =
    2.18 -sig
    2.19    val cooper_conv: Proof.context -> conv
    2.20 +  val cooper_oracle: cterm -> cterm
    2.21    exception COOPER of string * exn
    2.22  end;
    2.23  
    2.24 -signature COOPER_REIFY =
    2.25 -sig
    2.26 -  val cooper_oracle: cterm -> cterm
    2.27 -end;
    2.28 -
    2.29 -structure CooperData : COOPER_DATA =
    2.30 +structure Cooper: COOPER =
    2.31  struct
    2.32  
    2.33 -type entry = simpset * (term list);
    2.34 +type entry = simpset * term list;
    2.35  
    2.36  val allowed_consts = 
    2.37    [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
    2.38 @@ -95,11 +87,6 @@
    2.39  
    2.40  end;
    2.41  
    2.42 -end;
    2.43 -
    2.44 -structure Cooper: COOPER =
    2.45 -struct
    2.46 -
    2.47  exception COOPER of string * exn;
    2.48  fun simp_thms_conv ctxt =
    2.49    Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms});
    2.50 @@ -606,12 +593,8 @@
    2.51          | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
    2.52  in val cooper_conv = conv
    2.53  end;
    2.54 -end;
    2.55  
    2.56 -structure Coopereif : COOPER_REIFY =
    2.57 -struct
    2.58 -
    2.59 -fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
    2.60 +fun cooper s = raise COOPER ("Cooper oracle failed", ERROR s);
    2.61  fun i_of_term vs t = case t
    2.62   of Free (xn, xT) => (case AList.lookup (op aconv) vs t
    2.63       of NONE   => cooper "Variable not found in the list!"
     3.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 13:58:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Mon May 10 14:11:50 2010 +0200
     3.3 @@ -83,13 +83,13 @@
     3.4   in h [] end;
     3.5  in 
     3.6  fun is_relevant ctxt ct = 
     3.7 - subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
     3.8 + subset (op aconv) (term_constants (term_of ct) , snd (Cooper.get ctxt))
     3.9   andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
    3.10   andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
    3.11  
    3.12  fun int_nat_terms ctxt ct =
    3.13   let 
    3.14 -  val cts = snd (CooperData.get ctxt)
    3.15 +  val cts = snd (Cooper.get ctxt)
    3.16    fun h acc t = if ty cts t then insert (op aconvc) t acc else
    3.17     case (term_of t) of
    3.18      _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
    3.19 @@ -161,7 +161,7 @@
    3.20    (if q then I else TRY) (rtac TrueI i));
    3.21  
    3.22  fun cooper_tac elim add_ths del_ths ctxt =
    3.23 -let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
    3.24 +let val ss = Simplifier.context ctxt (fst (Cooper.get ctxt)) delsimps del_ths addsimps add_ths
    3.25      val aprems = Arith_Data.get_arith_facts ctxt
    3.26  in
    3.27    Method.insert_tac aprems