# HG changeset patch
# User chaieb
# Date 1242231213 -3600
# Node ID d9752181691aede31b090d9646d34b66de0d93e5
# Parent  94cb206f8f6a3d927e5b3f3ac94209d890c69c25
Now deals with division

diff -r 94cb206f8f6a -r d9752181691a src/HOL/Library/Sum_Of_Squares.thy
--- 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
diff -r 94cb206f8f6a -r d9752181691a src/HOL/Library/sum_of_squares.ML
--- 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