src/HOL/Library/positivstellensatz.ML
changeset 51717 9e7d1c139569
parent 46594 f11f332b964f
child 52049 156e12d5cb92
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -358,15 +358,15 @@
     1.4         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
     1.5         absconv1,absconv2,prover) =
     1.6    let
     1.7 -    val pre_ss = HOL_basic_ss addsimps
     1.8 +    val pre_ss = put_simpset HOL_basic_ss ctxt addsimps
     1.9        @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
    1.10 -    val prenex_ss = HOL_basic_ss addsimps prenex_simps
    1.11 -    val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
    1.12 -    val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
    1.13 -    val prenex_conv = Simplifier.rewrite (Simplifier.context ctxt prenex_ss)
    1.14 -    val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
    1.15 -    val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
    1.16 -    val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
    1.17 +    val prenex_ss = put_simpset HOL_basic_ss ctxt addsimps prenex_simps
    1.18 +    val skolemize_ss = put_simpset HOL_basic_ss ctxt addsimps [choice_iff]
    1.19 +    val presimp_conv = Simplifier.rewrite pre_ss
    1.20 +    val prenex_conv = Simplifier.rewrite prenex_ss
    1.21 +    val skolemize_conv = Simplifier.rewrite skolemize_ss
    1.22 +    val weak_dnf_ss = put_simpset HOL_basic_ss ctxt addsimps weak_dnf_simps
    1.23 +    val weak_dnf_conv = Simplifier.rewrite weak_dnf_ss
    1.24      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
    1.25      fun oprconv cv ct =
    1.26        let val g = Thm.dest_fun2 ct
    1.27 @@ -423,7 +423,7 @@
    1.28        end
    1.29  
    1.30      val init_conv = presimp_conv then_conv
    1.31 -        nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv
    1.32 +        nnf_conv ctxt then_conv skolemize_conv then_conv prenex_conv then_conv
    1.33          weak_dnf_conv
    1.34  
    1.35      val concl = Thm.dest_arg o cprop_of
    1.36 @@ -540,7 +540,7 @@
    1.37      fun f ct =
    1.38        let
    1.39          val nnf_norm_conv' =
    1.40 -          nnf_conv then_conv
    1.41 +          nnf_conv ctxt then_conv
    1.42            literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
    1.43            (Conv.cache_conv
    1.44              (first_conv [real_lt_conv, real_le_conv,
    1.45 @@ -701,9 +701,10 @@
    1.46  (* A less general generic arithmetic prover dealing with abs,max and min*)
    1.47  
    1.48  local
    1.49 -  val absmaxmin_elim_ss1 = HOL_basic_ss addsimps real_abs_thms1
    1.50 +  val absmaxmin_elim_ss1 =
    1.51 +    simpset_of (put_simpset HOL_basic_ss @{context} addsimps real_abs_thms1)
    1.52    fun absmaxmin_elim_conv1 ctxt =
    1.53 -    Simplifier.rewrite (Simplifier.context ctxt absmaxmin_elim_ss1)
    1.54 +    Simplifier.rewrite (put_simpset absmaxmin_elim_ss1 ctxt)
    1.55  
    1.56    val absmaxmin_elim_conv2 =
    1.57      let
    1.58 @@ -758,8 +759,11 @@
    1.59          (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    1.60          simple_cterm_ord
    1.61    in gen_real_arith ctxt
    1.62 -     (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
    1.63 -      main,neg,add,mul, prover)
    1.64 +     (cterm_of_rat,
    1.65 +      Numeral_Simprocs.field_comp_conv ctxt,
    1.66 +      Numeral_Simprocs.field_comp_conv ctxt,
    1.67 +      Numeral_Simprocs.field_comp_conv ctxt,
    1.68 +      main ctxt, neg ctxt, add ctxt, mul ctxt, prover)
    1.69    end;
    1.70  
    1.71  end