Tuned sos tactic to reject non SOS goals

--- a/src/HOL/Library/Sum_Of_Squares.thy	Mon Jun 08 22:29:37 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Tue Jun 09 11:10:33 2009 +0200
@@ -15,12 +15,10 @@
 
 *)
 
-
 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 -- see above *}
-
 (*
 lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
 
@@ -59,8 +57,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").                  *)
 (* ------------------------------------------------------------------------- *)

--- a/src/HOL/Library/sum_of_squares.ML	Mon Jun 08 22:29:37 2009 +0200
+++ b/src/HOL/Library/sum_of_squares.ML	Tue Jun 09 11:10:33 2009 +0200
@@ -1619,8 +1619,44 @@
 | _ => ([],ct)
 
 fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
+
+val known_sos_constants = 
+  [@{term "op ==>"}, @{term "Trueprop"}, 
+   @{term "op -->"}, @{term "op &"}, @{term "op |"}, 
+   @{term "Not"}, @{term "op = :: bool => _"}, 
+   @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, 
+   @{term "op = :: real => _"}, @{term "op < :: real => _"}, 
+   @{term "op <= :: real => _"}, 
+   @{term "op + :: real => _"}, @{term "op - :: real => _"}, 
+   @{term "op * :: real => _"}, @{term "uminus :: real => _"}, 
+   @{term "op / :: real => _"}, @{term "inverse :: real => _"},
+   @{term "op ^ :: real => _"}, @{term "abs :: real => _"}, 
+   @{term "min :: real => _"}, @{term "max :: real => _"},
+   @{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"},
+   @{term "number_of :: int => nat"},
+   @{term "Int.Bit0"}, @{term "Int.Bit1"}, 
+   @{term "Int.Pls"}, @{term "Int.Min"}];
+
+fun check_sos kcts ct = 
+ let
+  val t = term_of ct
+  val _ = if not (null (Term.add_tfrees t []) 
+                  andalso null (Term.add_tvars t [])) 
+          then error "SOS: not sos. Additional type varables" else ()
+  val fs = Term.add_frees t []
+  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
+          then error "SOS: not sos. Variables with type not real" else ()
+  val vs = Term.add_vars t []
+  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
+          then error "SOS: not sos. Variables with type not real" else ()
+  val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
+  val _ = if  null ukcs then () 
+              else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
+in () end
+
 fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) => 
-  let val (avs, p) = strip_all ct
+  let val _ = check_sos known_sos_constants ct
+      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);
 
@@ -1662,4 +1698,4 @@
 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
+end;