1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Mon Jun 08 22:29:37 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Tue Jun 09 11:10:33 2009 +0200
     1.3 @@ -15,12 +15,10 @@
     1.4  
     1.5  *)
     1.6  
     1.7 -
     1.8  method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *} 
     1.9    "Prove universal problems over the reals using sums of squares"
    1.10  
    1.11  text{* Tests -- commented since they work only when csdp is installed -- see above *}
    1.12 -
    1.13  (*
    1.14  lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
    1.15  
    1.16 @@ -59,8 +57,8 @@
    1.17  (* ------------------------------------------------------------------------- *)
    1.18  (*
    1.19  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
    1.20 +*)
    1.21  
    1.22 -*)
    1.23  (* ------------------------------------------------------------------------- *)
    1.24  (* Inequality from sci.math (see "Leon-Sotelo, por favor").                  *)
    1.25  (* ------------------------------------------------------------------------- *)

     2.1 --- a/src/HOL/Library/sum_of_squares.ML	Mon Jun 08 22:29:37 2009 +0200
     2.2 +++ b/src/HOL/Library/sum_of_squares.ML	Tue Jun 09 11:10:33 2009 +0200
     2.3 @@ -1619,8 +1619,44 @@
     2.4  | _ => ([],ct)
     2.5  
     2.6  fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
     2.7 +
     2.8 +val known_sos_constants = 
     2.9 +  [@{term "op ==>"}, @{term "Trueprop"}, 
    2.10 +   @{term "op -->"}, @{term "op &"}, @{term "op |"}, 
    2.11 +   @{term "Not"}, @{term "op = :: bool => _"}, 
    2.12 +   @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"}, 
    2.13 +   @{term "op = :: real => _"}, @{term "op < :: real => _"}, 
    2.14 +   @{term "op <= :: real => _"}, 
    2.15 +   @{term "op + :: real => _"}, @{term "op - :: real => _"}, 
    2.16 +   @{term "op * :: real => _"}, @{term "uminus :: real => _"}, 
    2.17 +   @{term "op / :: real => _"}, @{term "inverse :: real => _"},
    2.18 +   @{term "op ^ :: real => _"}, @{term "abs :: real => _"}, 
    2.19 +   @{term "min :: real => _"}, @{term "max :: real => _"},
    2.20 +   @{term "0::real"}, @{term "1::real"}, @{term "number_of :: int => real"},
    2.21 +   @{term "number_of :: int => nat"},
    2.22 +   @{term "Int.Bit0"}, @{term "Int.Bit1"}, 
    2.23 +   @{term "Int.Pls"}, @{term "Int.Min"}];
    2.24 +
    2.25 +fun check_sos kcts ct = 
    2.26 + let
    2.27 +  val t = term_of ct
    2.28 +  val _ = if not (null (Term.add_tfrees t []) 
    2.29 +                  andalso null (Term.add_tvars t [])) 
    2.30 +          then error "SOS: not sos. Additional type varables" else ()
    2.31 +  val fs = Term.add_frees t []
    2.32 +  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
    2.33 +          then error "SOS: not sos. Variables with type not real" else ()
    2.34 +  val vs = Term.add_vars t []
    2.35 +  val _ = if exists (fn ((_,T)) => not (T = @{typ "real"})) fs 
    2.36 +          then error "SOS: not sos. Variables with type not real" else ()
    2.37 +  val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
    2.38 +  val _ = if  null ukcs then () 
    2.39 +              else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
    2.40 +in () end
    2.41 +
    2.42  fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) => 
    2.43 -  let val (avs, p) = strip_all ct
    2.44 +  let val _ = check_sos known_sos_constants ct
    2.45 +      val (avs, p) = strip_all ct
    2.46        val th = standard (fold_rev forall_intr avs (real_sos ctxt (Thm.dest_arg p)))
    2.47    in rtac th i end);
    2.48  
    2.49 @@ -1662,4 +1698,4 @@
    2.50  fun sos_tac ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac ctxt
    2.51  
    2.52  
    2.53 -end;
    2.54 \ No newline at end of file
    2.55 +end;