src/HOL/Decision_Procs/ferrack_tac.ML

     Author:     Amine Chaieb, TU Muenchen
 *)
 
 signature FERRACK_TAC =
 sig
-  val trace: bool Unsynchronized.ref
   val linr_tac: Proof.context -> bool -> int -> tactic
 end
 
-structure Ferrack_Tac =
+structure Ferrack_Tac: FERRACK_TAC =
 struct
-
-val trace = Unsynchronized.ref false;
-fun trace_msg s = if !trace then tracing s else ();
 
 val ferrack_ss = let val ths = [@{thm real_of_int_inject}, @{thm real_of_int_less_iff}, 
                                 @{thm real_of_int_le_iff}]
              in @{context} delsimps ths addsimps (map (fn th => th RS sym) ths)
              end |> simpset_of;
 
 val binarith = @{thms arith_simps}
 val comp_arith = binarith @ @{thms simp_thms}
 
-val zdvd_int = @{thm zdvd_int};
-val zdiff_int_split = @{thm zdiff_int_split};
-val all_nat = @{thm all_nat};
-val ex_nat = @{thm ex_nat};
-val split_zdiv = @{thm split_zdiv};
-val split_zmod = @{thm split_zmod};
-val mod_div_equality' = @{thm mod_div_equality'};
-val split_div' = @{thm split_div'};
-val Suc_eq_plus1 = @{thm Suc_eq_plus1};
-val imp_le_cong = @{thm imp_le_cong};
-val conj_le_cong = @{thm conj_le_cong};
-val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
-val mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val nat_div_add_eq = @{thm div_add1_eq} RS sym;
-val int_div_add_eq = @{thm zdiv_zadd1_eq} RS sym;
-
-fun prepare_for_linr sg q fm = 
+fun prepare_for_linr q fm = 
   let
     val ps = Logic.strip_params fm
     val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
     val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
     fun mk_all ((s, T), (P,n)) =

         THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let
     val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
-    val (t,np,nh) = prepare_for_linr thy q g
+    val (t,np,nh) = prepare_for_linr q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val simpset0 = put_simpset HOL_basic_ss ctxt addsimps comp_arith
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     (* Theorem for the nat --> int transformation *)
    val pre_thm = Seq.hd (EVERY

     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
     in 
-          (trace_msg ("calling procedure with term:\n" ^
-             Syntax.string_of_term ctxt t1);
-           ((pth RS iffD2) RS pre_thm,
-            assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
+       ((pth RS iffD2) RS pre_thm,
+        assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     end
       | _ => (pre_thm, assm_tac i)
   in rtac ((mp_step nh o spec_step np) th) i THEN tac end);
 
 end