disposed some old debugging tools;
authorwenzelm
Fri Aug 27 15:46:08 2010 +0200 (2010-08-27)
changeset 38801319a28dd3564
parent 38800 34c84817e39c
child 38802 a925c0ee42f7
disposed some old debugging tools;
src/HOL/Library/positivstellensatz.ML
src/HOL/Tools/TFL/rules.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:07:35 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Aug 27 15:46:08 2010 +0200
     1.3 @@ -164,21 +164,6 @@
     1.4    thm list * thm list * thm list -> thm * pss_tree
     1.5  type cert_conv = cterm -> thm * pss_tree
     1.6  
     1.7 -val my_eqs = Unsynchronized.ref ([] : thm list);
     1.8 -val my_les = Unsynchronized.ref ([] : thm list);
     1.9 -val my_lts = Unsynchronized.ref ([] : thm list);
    1.10 -val my_proof = Unsynchronized.ref (Axiom_eq 0);
    1.11 -val my_context = Unsynchronized.ref @{context};
    1.12 -
    1.13 -val my_mk_numeric = Unsynchronized.ref ((K @{cterm True}) :Rat.rat -> cterm);
    1.14 -val my_numeric_eq_conv = Unsynchronized.ref no_conv;
    1.15 -val my_numeric_ge_conv = Unsynchronized.ref no_conv;
    1.16 -val my_numeric_gt_conv = Unsynchronized.ref no_conv;
    1.17 -val my_poly_conv = Unsynchronized.ref no_conv;
    1.18 -val my_poly_neg_conv = Unsynchronized.ref no_conv;
    1.19 -val my_poly_add_conv = Unsynchronized.ref no_conv;
    1.20 -val my_poly_mul_conv = Unsynchronized.ref no_conv;
    1.21 -
    1.22  
    1.23      (* Some useful derived rules *)
    1.24  fun deduct_antisym_rule tha thb = 
    1.25 @@ -362,11 +347,6 @@
    1.26         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
    1.27         absconv1,absconv2,prover) = 
    1.28  let
    1.29 - val _ = my_context := ctxt 
    1.30 - val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ; 
    1.31 -          my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ;
    1.32 -          my_poly_conv := poly_conv; my_poly_neg_conv := poly_neg_conv; 
    1.33 -          my_poly_add_conv := poly_add_conv; my_poly_mul_conv := poly_mul_conv)
    1.34   val pre_ss = HOL_basic_ss addsimps simp_thms@ ex_simps@ all_simps@[@{thm not_all},@{thm not_ex},ex_disj_distrib, all_conj_distrib, @{thm if_bool_eq_disj}]
    1.35   val prenex_ss = HOL_basic_ss addsimps prenex_simps
    1.36   val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
    1.37 @@ -408,7 +388,6 @@
    1.38  
    1.39    fun hol_of_positivstellensatz(eqs,les,lts) proof =
    1.40     let 
    1.41 -    val _ = (my_eqs := eqs ; my_les := les ; my_lts := lts ; my_proof := proof)
    1.42      fun translate prf = case prf of
    1.43          Axiom_eq n => nth eqs n
    1.44        | Axiom_le n => nth les n
     2.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:07:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Aug 27 15:46:08 2010 +0200
     2.3 @@ -46,10 +46,6 @@
     2.4    val simpl_conv: simpset -> thm list -> cterm -> thm
     2.5  
     2.6    val rbeta: thm -> thm
     2.7 -(* For debugging my isabelle solver in the conditional rewriter *)
     2.8 -  val term_ref: term list Unsynchronized.ref
     2.9 -  val thm_ref: thm list Unsynchronized.ref
    2.10 -  val ss_ref: simpset list Unsynchronized.ref
    2.11    val tracing: bool Unsynchronized.ref
    2.12    val CONTEXT_REWRITE_RULE: term * term list * thm * thm list
    2.13                               -> thm -> thm * term list
    2.14 @@ -542,9 +538,6 @@
    2.15  (*---------------------------------------------------------------------------
    2.16   * Trace information for the rewriter
    2.17   *---------------------------------------------------------------------------*)
    2.18 -val term_ref = Unsynchronized.ref [] : term list Unsynchronized.ref
    2.19 -val ss_ref = Unsynchronized.ref [] : simpset list Unsynchronized.ref;
    2.20 -val thm_ref = Unsynchronized.ref [] : thm list Unsynchronized.ref;
    2.21  val tracing = Unsynchronized.ref false;
    2.22  
    2.23  fun say s = if !tracing then writeln s else ();
    2.24 @@ -665,9 +658,6 @@
    2.25       val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
    2.26       val pbeta_reduce = simpl_conv ss0 [@{thm split_conv} RS eq_reflection];
    2.27       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
    2.28 -     val dummy = term_ref := []
    2.29 -     val dummy = thm_ref  := []
    2.30 -     val dummy = ss_ref  := []
    2.31       val cut_lemma' = cut_lemma RS eq_reflection
    2.32       fun prover used ss thm =
    2.33       let fun cong_prover ss thm =
    2.34 @@ -676,8 +666,6 @@
    2.35               val dummy = print_thms "cntxt:" cntxt
    2.36               val dummy = say "cong rule:"
    2.37               val dummy = say (Display.string_of_thm_without_context thm)
    2.38 -             val dummy = thm_ref := (thm :: !thm_ref)
    2.39 -             val dummy = ss_ref := (ss :: !ss_ref)
    2.40               (* Unquantified eliminate *)
    2.41               fun uq_eliminate (thm,imp,thy) =
    2.42                   let val tych = cterm_of thy
    2.43 @@ -784,7 +772,6 @@
    2.44                val dummy = tc_list := (TC :: !tc_list)
    2.45                val nestedp = is_some (S.find_term is_func TC)
    2.46                val dummy = if nestedp then say "nested" else say "not_nested"
    2.47 -              val dummy = term_ref := ([func,TC]@(!term_ref))
    2.48                val th' = if nestedp then raise RULES_ERR "solver" "nested function"
    2.49                          else let val cTC = cterm_of thy
    2.50                                                (HOLogic.mk_Trueprop TC)