prefer fixed simpset for proof procedure
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (4 weeks ago)
changeset 70334bba46912379e
parent 70333 0f7edf0853df
child 70335 9bd8c16b6627
prefer fixed simpset for proof procedure
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -1006,14 +1006,18 @@
     1.4      | _ => NONE)
     1.5  end;
     1.6  
     1.7 +val sos_ss = @{context}
     1.8 +  |> fold Simplifier.add_simp @{thms field_simps}
     1.9 +  |> Simplifier.del_simp @{thm mult_nonneg_nonneg}
    1.10 +  |> Simplifier.simpset_of;
    1.11 +
    1.12  fun elim_one_denom_tac ctxt = CSUBGOAL (fn (P, i) =>
    1.13    (case get_denom false P of
    1.14      NONE => no_tac
    1.15    | SOME (d, ord) =>
    1.16        let
    1.17 -        val simp_ctxt =
    1.18 -          ctxt addsimps @{thms field_simps}
    1.19 -          addsimps [@{thm power_divide}]
    1.20 +        val simp_ctxt = ctxt
    1.21 +          |> Simplifier.put_simpset sos_ss
    1.22          val th =
    1.23            Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
    1.24              (if ord then @{lemma "(d=0 \<longrightarrow> P) \<and> (d>0 \<longrightarrow> P) \<and> (d<(0::real) \<longrightarrow> P) \<Longrightarrow> P" by auto}
    1.25 @@ -1023,11 +1027,8 @@
    1.26  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
    1.27  
    1.28  fun sos_tac print_cert prover ctxt =
    1.29 -  (* The SOS prover breaks if mult_nonneg_nonneg is in the simpset *)
    1.30 -  let val ctxt' = Context_Position.set_visible false ctxt delsimps @{thms mult_nonneg_nonneg}
    1.31 -  in Object_Logic.full_atomize_tac ctxt' THEN'
    1.32 -     elim_denom_tac ctxt' THEN'
    1.33 -     core_sos_tac print_cert prover ctxt'
    1.34 -  end;
    1.35 +  Object_Logic.full_atomize_tac ctxt THEN'
    1.36 +  elim_denom_tac ctxt THEN'
    1.37 +  core_sos_tac print_cert prover ctxt;
    1.38  
    1.39  end;