shorten names
authorhaftmann
Mon May 10 15:00:53 2010 +0200 (2010-05-10)
changeset 36804f4ad04780669
parent 36803 2cad8904c4ff
child 36805 929b23461a14
shorten names
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Presburger.thy	Mon May 10 14:57:04 2010 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Mon May 10 15:00:53 2010 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4  
     1.5  setup Cooper.setup
     1.6  
     1.7 -method_setup presburger = "Cooper.cooper_method" "Cooper's algorithm for Presburger arithmetic"
     1.8 +method_setup presburger = "Cooper.method" "Cooper's algorithm for Presburger arithmetic"
     1.9  
    1.10  declare dvd_eq_mod_eq_0[symmetric, presburger]
    1.11  declare mod_1[presburger] 
     2.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 14:57:04 2010 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 10 15:00:53 2010 +0200
     2.3 @@ -10,10 +10,10 @@
     2.4    val get: Proof.context -> entry
     2.5    val del: term list -> attribute
     2.6    val add: term list -> attribute 
     2.7 -  val cooper_conv: Proof.context -> conv
     2.8 -  val cooper_oracle: cterm -> thm
     2.9 -  val cooper_tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    2.10 -  val cooper_method: (Proof.context -> Method.method) context_parser
    2.11 +  val conv: Proof.context -> conv
    2.12 +  val oracle: cterm -> thm
    2.13 +  val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
    2.14 +  val method: (Proof.context -> Method.method) context_parser
    2.15    exception COOPER of string * exn
    2.16    val setup: theory -> theory
    2.17  end;
    2.18 @@ -573,7 +573,7 @@
    2.19    handle  CTERM s => raise COOPER ("Cooper Failed", CTERM s)
    2.20          | THM s => raise COOPER ("Cooper Failed", THM s)
    2.21          | TYPE s => raise COOPER ("Cooper Failed", TYPE s)
    2.22 -in val cooper_conv = conv
    2.23 +in val conv = conv
    2.24  end;
    2.25  
    2.26  fun i_of_term vs t = case t
    2.27 @@ -676,7 +676,7 @@
    2.28   | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n))
    2.29   | _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!";
    2.30  
    2.31 -fun raw_cooper_oracle ct =
    2.32 +fun raw_oracle ct =
    2.33    let
    2.34      val thy = Thm.theory_of_cterm ct;
    2.35      val t = Thm.term_of ct;
    2.36 @@ -686,8 +686,8 @@
    2.37        HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))))
    2.38    end;
    2.39  
    2.40 -val (_, cooper_oracle) = Context.>>> (Context.map_theory_result
    2.41 -  (Thm.add_oracle (Binding.name "cooper", raw_cooper_oracle)));
    2.42 +val (_, oracle) = Context.>>> (Context.map_theory_result
    2.43 +  (Thm.add_oracle (Binding.name "cooper", raw_oracle)));
    2.44  
    2.45  val comp_ss = HOL_ss addsimps @{thms semiring_norm};
    2.46  
    2.47 @@ -823,13 +823,13 @@
    2.48  fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i;
    2.49  end;
    2.50  
    2.51 -fun core_cooper_tac ctxt = CSUBGOAL (fn (p, i) =>
    2.52 +fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    2.53     let 
    2.54      val cpth = 
    2.55         if !quick_and_dirty 
    2.56 -       then cooper_oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
    2.57 +       then oracle (Thm.cterm_of (ProofContext.theory_of ctxt)
    2.58               (Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))))
    2.59 -       else Conv.arg_conv (cooper_conv ctxt) p
    2.60 +       else Conv.arg_conv (conv ctxt) p
    2.61      val p' = Thm.rhs_of cpth
    2.62      val th = implies_intr p' (equal_elim (symmetric cpth) (assume p'))
    2.63     in rtac th i end
    2.64 @@ -838,7 +838,7 @@
    2.65  fun finish_tac q = SUBGOAL (fn (_, i) =>
    2.66    (if q then I else TRY) (rtac TrueI i));
    2.67  
    2.68 -fun cooper_tac elim add_ths del_ths ctxt =
    2.69 +fun tac elim add_ths del_ths ctxt =
    2.70  let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths
    2.71      val aprems = Arith_Data.get_arith_facts ctxt
    2.72  in
    2.73 @@ -855,11 +855,11 @@
    2.74    THEN_ALL_NEW simp_tac ss
    2.75    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    2.76    THEN_ALL_NEW nat_to_int_tac ctxt
    2.77 -  THEN_ALL_NEW (core_cooper_tac ctxt)
    2.78 +  THEN_ALL_NEW (core_tac ctxt)
    2.79    THEN_ALL_NEW finish_tac elim
    2.80  end;
    2.81  
    2.82 -val cooper_method =
    2.83 +val method =
    2.84    let
    2.85      fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    2.86      fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
    2.87 @@ -873,7 +873,7 @@
    2.88      Scan.optional (keyword addN |-- thms) [] --
    2.89      Scan.optional (keyword delN |-- thms) [] >>
    2.90      (fn ((elim, add_ths), del_ths) => fn ctxt =>
    2.91 -      SIMPLE_METHOD' (cooper_tac elim add_ths del_ths ctxt))
    2.92 +      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
    2.93    end;
    2.94  
    2.95  
    2.96 @@ -896,7 +896,7 @@
    2.97    Attrib.setup @{binding presburger}
    2.98      ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    2.99        optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
   2.100 -  #> Arith_Data.add_tactic "Presburger arithmetic" (K (cooper_tac true [] []));
   2.101 +  #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
   2.102  
   2.103  end;
   2.104