src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 67091 1393c2340eec
parent 63523 54e932f0c30a
child 67271 48ef58c6cf4c
equal deleted inserted replaced
67090:0ec94bb9cec4 67091:1393c2340eec
  1016         val simp_ctxt =
  1016         val simp_ctxt =
  1017           ctxt addsimps @{thms field_simps}
  1017           ctxt addsimps @{thms field_simps}
  1018           addsimps [@{thm power_divide}]
  1018           addsimps [@{thm power_divide}]
  1019         val th =
  1019         val th =
  1020           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
  1020           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
  1021             (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
  1021             (if ord then @{lemma "(d=0 \<longrightarrow> P) \<and> (d>0 \<longrightarrow> P) \<and> (d<(0::real) \<longrightarrow> P) \<Longrightarrow> P" by auto}
  1022              else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
  1022              else @{lemma "(d=0 \<longrightarrow> P) \<and> (d \<noteq> (0::real) \<longrightarrow> P) \<Longrightarrow> P" by blast})
  1023       in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
  1023       in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
  1024 
  1024 
  1025 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
  1025 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
  1026 
  1026 
  1027 fun sos_tac print_cert prover ctxt =
  1027 fun sos_tac print_cert prover ctxt =