src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 70334 bba46912379e
parent 69064 5840724b1d71
equal deleted inserted replaced
70333:0f7edf0853df 70334:bba46912379e
  1004         lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
  1004         lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
  1005     | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
  1005     | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
  1006     | _ => NONE)
  1006     | _ => NONE)
  1007 end;
  1007 end;
  1008 
  1008 
       
  1009 val sos_ss = @{context}
       
  1010   |> fold Simplifier.add_simp @{thms field_simps}
       
  1011   |> Simplifier.del_simp @{thm mult_nonneg_nonneg}
       
  1012   |> Simplifier.simpset_of;
       
  1013 
  1009 fun elim_one_denom_tac ctxt = CSUBGOAL (fn (P, i) =>
  1014 fun elim_one_denom_tac ctxt = CSUBGOAL (fn (P, i) =>
  1010   (case get_denom false P of
  1015   (case get_denom false P of
  1011     NONE => no_tac
  1016     NONE => no_tac
  1012   | SOME (d, ord) =>
  1017   | SOME (d, ord) =>
  1013       let
  1018       let
  1014         val simp_ctxt =
  1019         val simp_ctxt = ctxt
  1015           ctxt addsimps @{thms field_simps}
  1020           |> Simplifier.put_simpset sos_ss
  1016           addsimps [@{thm power_divide}]
       
  1017         val th =
  1021         val th =
  1018           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
  1022           Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
  1019             (if ord then @{lemma "(d=0 \<longrightarrow> P) \<and> (d>0 \<longrightarrow> P) \<and> (d<(0::real) \<longrightarrow> P) \<Longrightarrow> P" by auto}
  1023             (if ord then @{lemma "(d=0 \<longrightarrow> P) \<and> (d>0 \<longrightarrow> P) \<and> (d<(0::real) \<longrightarrow> P) \<Longrightarrow> P" by auto}
  1020              else @{lemma "(d=0 \<longrightarrow> P) \<and> (d \<noteq> (0::real) \<longrightarrow> P) \<Longrightarrow> P" by blast})
  1024              else @{lemma "(d=0 \<longrightarrow> P) \<and> (d \<noteq> (0::real) \<longrightarrow> P) \<Longrightarrow> P" by blast})
  1021       in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
  1025       in resolve_tac ctxt [th] i THEN Simplifier.asm_full_simp_tac simp_ctxt i end));
  1022 
  1026 
  1023 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
  1027 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
  1024 
  1028 
  1025 fun sos_tac print_cert prover ctxt =
  1029 fun sos_tac print_cert prover ctxt =
  1026   (* The SOS prover breaks if mult_nonneg_nonneg is in the simpset *)
  1030   Object_Logic.full_atomize_tac ctxt THEN'
  1027   let val ctxt' = Context_Position.set_visible false ctxt delsimps @{thms mult_nonneg_nonneg}
  1031   elim_denom_tac ctxt THEN'
  1028   in Object_Logic.full_atomize_tac ctxt' THEN'
  1032   core_sos_tac print_cert prover ctxt;
  1029      elim_denom_tac ctxt' THEN'
       
  1030      core_sos_tac print_cert prover ctxt'
       
  1031   end;
       
  1032 
  1033 
  1033 end;
  1034 end;