author chaieb Tue, 09 Jun 2009 11:10:33 +0200 changeset 31512 27118561c2e0 parent 31510 e0f2bb4b0021 child 31513 3625c39e2eff
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;```