--- a/src/HOL/Library/Sum_Of_Squares.thy Tue May 12 21:39:19 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed May 13 17:13:33 2009 +0100
@@ -9,30 +9,20 @@
uses "positivstellensatz.ML" "sum_of_squares.ML"
begin
-method_setup sos = {*
-let
- fun strip_all ct =
- case term_of ct of
- Const("all",_) $ Abs (xn,xT,p) =>
- let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
- in apfst (cons v) (strip_all t')
- end
- | _ => ([],ct)
+(* Note:
+
+In order to use the method sos, install CSDP (https://projects.coin-or.org/Csdp/) and put the executable csdp on your path.
+
+*)
- fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (Sos.real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
- fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) =>
- let val (avs, p) = strip_all ct
- val th = standard (fold_rev forall_intr avs (Sos.real_sos ctxt (Thm.dest_arg p)))
- in rtac th i end) (* CONVERSION o core_sos_conv *)
-in Scan.succeed (SIMPLE_METHOD' o core_sos_tac)
-end
-*} "Prove universal problems over the reals using sums of squares"
+method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *}
+ "Prove universal problems over the reals using sums of squares"
-text{* Tests -- commented since they work only when csdp is installed *}
+text{* Tests -- commented since they work only when csdp is installed -- see above *}
(*
-lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" by sos
+lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" by sos
@@ -69,8 +59,8 @@
(* ------------------------------------------------------------------------- *)
(*
lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+
*)
-
(* ------------------------------------------------------------------------- *)
(* Inequality from sci.math (see "Leon-Sotelo, por favor"). *)
(* ------------------------------------------------------------------------- *)
@@ -110,5 +100,20 @@
*)
(*
lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*)
+(*
+lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x"
+apply sos
+done
+
+lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)"
+apply sos
+done
+
+lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)"
+apply sos
+done
+
+lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" by sos
+*)
end
--- a/src/HOL/Library/sum_of_squares.ML Tue May 12 21:39:19 2009 +0200
+++ b/src/HOL/Library/sum_of_squares.ML Wed May 13 17:13:33 2009 +0100
@@ -1609,4 +1609,57 @@
fun real_sos ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover ctxt) t;
end;
+(* A tactic *)
+fun strip_all ct =
+ case term_of ct of
+ Const("all",_) $ Abs (xn,xT,p) =>
+ let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct
+ in apfst (cons v) (strip_all t')
+ end
+| _ => ([],ct)
+
+fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
+fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) =>
+ let val (avs, p) = strip_all ct
+ val th = standard (fold_rev forall_intr avs (real_sos ctxt (Thm.dest_arg p)))
+ in rtac th i end);
+
+fun default_SOME f NONE v = SOME v
+ | default_SOME f (SOME v) _ = SOME v;
+
+fun lift_SOME f NONE a = f a
+ | lift_SOME f (SOME a) _ = SOME a;
+
+
+local
+ val is_numeral = can (HOLogic.dest_number o term_of)
+in
+fun get_denom b ct = case term_of ct of
+ @{term "op / :: real => _"} $ _ $ _ =>
+ if is_numeral (Thm.dest_arg ct) then get_denom b (Thm.dest_arg1 ct)
+ else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b)
+ | @{term "op < :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ | @{term "op <= :: real => _"} $ _ $ _ => lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
+ | _ => NONE
+end;
+
+fun elim_one_denom_tac ctxt =
+CSUBGOAL (fn (P,i) =>
+ case get_denom false P of
+ NONE => no_tac
+ | SOME (d,ord) =>
+ let
+ val ss = simpset_of (ProofContext.theory_of ctxt) addsimps @{thms field_simps}
+ addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
+ val th = instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
+ (if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
+ else @{lemma "(d=0 --> P) & (d ~= (0::real) --> P) ==> P" by blast})
+ in (rtac th i THEN Simplifier.asm_full_simp_tac ss i) end);
+
+fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
+
+fun sos_tac ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac ctxt
+
+
end;
\ No newline at end of file