# HG changeset patch
# User haftmann
# Date 1273496453 -7200
# Node ID f4ad04780669984c9b62b3e1eca60cace880e828
# Parent  2cad8904c4ff0a863825f442505301736c4af15e
shorten names

diff -r 2cad8904c4ff -r f4ad04780669 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Mon May 10 14:57:04 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 15:00:53 2010 +0200
@@ -392,7 +392,7 @@
 
 setup Cooper.setup
 
-method_setup presburger = "Cooper.cooper_method" "Cooper's algorithm for Presburger arithmetic"
+method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic"
 
 declare dvd_eq_mod_eq_0[symmetric, presburger]
 declare mod_1[presburger] 
diff -r 2cad8904c4ff -r f4ad04780669 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:57:04 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:00:53 2010 +0200
@@ -10,10 +10,10 @@
   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
+  val conv: Proof.context -> conv
+  val oracle: cterm -> thm
+  val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
+  val method: (Proof.context -> Method.method) context_parser
   exception COOPER of string * exn
   val setup: theory -> theory
 end;
@@ -573,7 +573,7 @@
   handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
         | THM s => raise COOPER ("Cooper Failed", THM s)
         | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
-in val cooper_conv = conv
+in val conv = conv
 end;
 
 fun i_of_term vs t = case t
@@ -676,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 raw_cooper_oracle ct =
+fun raw_oracle ct =
   let
     val thy = Thm.theory_of_cterm ct;
     val t = Thm.term_of ct;
@@ -686,8 +686,8 @@
       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 (_, oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (Binding.name "cooper", raw_oracle)));
 
 val comp_ss = HOL_ss addsimps @{thms semiring_norm};
 
@@ -823,13 +823,13 @@
 fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
 end;
 
-fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
+fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    let 
     val cpth = 
        if !quick_and_dirty 
-       then cooper_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
+       then 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
+       else Conv.arg_conv (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
@@ -838,7 +838,7 @@
 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 =
+fun 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
@@ -855,11 +855,11 @@
   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 (core_tac ctxt)
   THEN_ALL_NEW finish_tac elim
 end;
 
-val cooper_method =
+val method =
   let
     fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
     fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
@@ -873,7 +873,7 @@
     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))
+      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
   end;
 
 
@@ -896,7 +896,7 @@
   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 [] []));
+  #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
 
 end;