# HG changeset patch
# User wenzelm
# Date 1255633683 -7200
# Node ID aa6c470a962a95c83dd6c9ca6191d95d3c681a11
# Parent  e95a4be101a891893421fe85b6ba5e773011dd27
eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
eliminated aliases of Output operations;
print_cert: use warning for increased chance that the user actually sees the output;
misc tuning and simplification;

diff -r e95a4be101a8 -r aa6c470a962a src/HOL/Library/Sum_Of_Squares.thy
--- a/src/HOL/Library/Sum_Of_Squares.thy	Thu Oct 15 17:49:30 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Thu Oct 15 21:08:03 2009 +0200
@@ -1,5 +1,6 @@
-(* Title:      HOL/Library/Sum_Of_Squares.thy
-   Author:     Amine Chaieb, University of Cambridge
+(*  Title:      HOL/Library/Sum_Of_Squares.thy
+    Author:     Amine Chaieb, University of Cambridge
+    Author:     Philipp Meyer, TU Muenchen
 *)
 
 header {* A decision method for universal multivariate real arithmetic with addition, 
@@ -34,7 +35,7 @@
 use "Sum_Of_Squares/sum_of_squares.ML"
 use "Sum_Of_Squares/sos_wrapper.ML"
 
-setup SosWrapper.setup
+setup SOS_Wrapper.setup
 
 text {* Tests *}
 
diff -r e95a4be101a8 -r aa6c470a962a src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Oct 15 17:49:30 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Thu Oct 15 21:08:03 2009 +0200
@@ -1,32 +1,31 @@
-(* Title:      sos_wrapper.ML
-   Author:     Philipp Meyer, TU Muenchen
+(*  Title:      HOL/Library/Sum_Of_Squares/sos_wrapper.ML
+    Author:     Philipp Meyer, TU Muenchen
 
-Added functionality for sums of squares, e.g. calling a remote prover
+Added functionality for sums of squares, e.g. calling a remote prover.
 *)
 
 signature SOS_WRAPPER =
 sig
-
   datatype prover_result = Success | Failure | Error
-
   val setup: theory -> theory
   val destdir: string Unsynchronized.ref
-  val get_prover_name: unit -> string
-  val set_prover_name: string -> unit
+  val prover_name: string Unsynchronized.ref
 end
 
-structure SosWrapper : SOS_WRAPPER=
+structure SOS_Wrapper: SOS_WRAPPER =
 struct
 
 datatype prover_result = Success | Failure | Error
+
 fun str_of_result Success = "Success"
   | str_of_result Failure = "Failure"
   | str_of_result Error = "Error"
 
+
 (*** output control ***)
 
-fun debug s = if ! Sos.debugging then Output.writeln s else ()
-val write = Output.warning
+fun debug s = if ! Sum_Of_Squares.debugging then writeln s else ()
+
 
 (*** calling provers ***)
 
@@ -39,20 +38,18 @@
   in
     if dir = "" then
       File.tmp_path probfile
-    else
-      if File.exists dir_path then
-        Path.append dir_path probfile
-      else
-        error ("No such directory: " ^ dir)
+    else if File.exists dir_path then
+      Path.append dir_path probfile
+    else error ("No such directory: " ^ dir)
   end
 
 fun run_solver name cmd find_failure input =
   let
-    val _ = write ("Calling solver: " ^ name)
+    val _ = warning ("Calling solver: " ^ name)
 
     (* create input file *)
     val dir = ! destdir
-    val input_file = filename dir "sos_in" 
+    val input_file = filename dir "sos_in"
     val _ = File.write input_file input
 
     (* call solver *)
@@ -61,26 +58,28 @@
       if File.exists cmd then space_implode " "
         [File.shell_path cmd, File.shell_path input_file, File.shell_path output_file]
       else error ("Bad executable: " ^ File.platform_path cmd))
- 
-    (* read and analysize output *)
+
+    (* read and analyze output *)
     val (res, res_msg) = find_failure rv
     val result = if File.exists output_file then File.read output_file else ""
 
     (* remove temporary files *)
-    val _ = if dir = "" then
-        (File.rm input_file ; if File.exists output_file then File.rm output_file else ())
-        else ()
+    val _ =
+      if dir = "" then
+        (File.rm input_file; if File.exists output_file then File.rm output_file else ())
+      else ()
 
     val _ = debug ("Solver output:\n" ^ output)
 
-    val _ = write (str_of_result res ^ ": " ^ res_msg)
+    val _ = warning (str_of_result res ^ ": " ^ res_msg)
   in
-    case res of
+    (case res of
       Success => result
-    | Failure => raise Sos.Failure res_msg
-    | Error => error ("Prover failed: " ^ res_msg)
+    | Failure => raise Sum_Of_Squares.Failure res_msg
+    | Error => error ("Prover failed: " ^ res_msg))
   end
 
+
 (*** various provers ***)
 
 (* local csdp client *)
@@ -101,6 +100,7 @@
 
 val csdp = ("$CSDP_EXE", find_csdp_failure)
 
+
 (* remote neos server *)
 
 fun find_neos_failure rv =
@@ -111,57 +111,45 @@
 
 val neos_csdp = ("$ISABELLE_SUM_OF_SQUARES/neos_csdp_client", find_neos_failure)
 
-(* default prover *)
+
+(* named provers *)
+
+fun prover "remote_csdp" = neos_csdp
+  | prover "csdp" = csdp
+  | prover name = error ("Unknown prover: " ^ name)
 
 val prover_name = Unsynchronized.ref "remote_csdp"
 
-fun get_prover_name () = CRITICAL (fn () => ! prover_name);
-fun set_prover_name str = CRITICAL (fn () => prover_name := str);
-
-(* save provers in table *)
-
-val provers =
-     Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)]
+fun call_solver opt_name =
+  let
+    val name = the_default (! prover_name) opt_name
+    val (cmd, find_failure) = prover name
+  in run_solver name (Path.explode cmd) find_failure end
 
-fun get_prover name =
-  case Symtab.lookup provers name of
-    SOME prover => prover
-  | NONE => error ("unknown prover: " ^ name)
-
-fun call_solver name_option =
-  let
-    val name = the_default (get_prover_name()) name_option
-    val (cmd, find_failure) = get_prover name
-  in
-    run_solver name (Path.explode cmd) find_failure
-  end
 
 (* certificate output *)
 
-fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^
-        (Markup.markup Markup.sendback) ("by (sos_cert \"" ^ cert ^ "\")")
-
-val print_cert = Output.writeln o output_line o PositivstellensatzTools.pss_tree_to_cert
-
-(* setup tactic *)
+fun output_line cert =
+  "To repeat this proof with a certifiate use this command:\n" ^
+    Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
 
-fun parse_cert (input as (ctxt, _)) = 
-  (Scan.lift OuterParse.string >>
-    PositivstellensatzTools.cert_to_pss_tree (Context.proof_of ctxt)) input
+val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
 
-fun sos_solver print method = (SIMPLE_METHOD' o (Sos.sos_tac print method)) 
 
-val sos_method =
-   Scan.lift (Scan.option OuterParse.xname) >> (fn n => Sos.Prover (call_solver n)) >>
-   sos_solver print_cert
+(* method setup *)
 
-val sos_cert_method =
-  parse_cert >> Sos.Certificate >> sos_solver ignore
+fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method
 
 val setup =
-     Method.setup @{binding sos} sos_method
-     "Prove universal problems over the reals using sums of squares"
-  #> Method.setup @{binding sos_cert} sos_cert_method
-     "Prove universal problems over the reals using sums of squares with certificates"
+  Method.setup @{binding sos}
+    (Scan.lift (Scan.option OuterParse.xname)
+      >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
+    "prove universal problems over the reals using sums of squares" #>
+  Method.setup @{binding sos_cert}
+    (Scan.lift OuterParse.string
+      >> (fn cert => fn ctxt =>
+        sos_solver ignore
+          (Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
+    "prove universal problems over the reals using sums of squares with certificates"
 
 end
diff -r e95a4be101a8 -r aa6c470a962a src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 15 17:49:30 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 15 21:08:03 2009 +0200
@@ -1,26 +1,19 @@
-(* Title:      HOL/Library/Sum_Of_Squares/sum_of_squares.ML
-   Author:     Amine Chaieb, University of Cambridge
-   Author:     Philipp Meyer, TU Muenchen
+(*  Title:      HOL/Library/Sum_Of_Squares/sum_of_squares.ML
+    Author:     Amine Chaieb, University of Cambridge
+    Author:     Philipp Meyer, TU Muenchen
 
 A tactic for proving nonlinear inequalities.
 *)
 
-signature SOS =
+signature SUM_OF_SQUARES =
 sig
-
-  datatype proof_method =
-    Certificate of RealArith.pss_tree
-  | Prover of (string -> string)
-
-  val sos_tac : (RealArith.pss_tree -> unit) ->
-    proof_method -> Proof.context -> int -> tactic
-
-  val debugging : bool Unsynchronized.ref;
-
+  datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
+  val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
+  val debugging: bool Unsynchronized.ref
   exception Failure of string;
 end
 
-structure Sos : SOS =
+structure Sum_Of_Squares: SUM_OF_SQUARES =
 struct
 
 val rat_0 = Rat.zero;
@@ -28,8 +21,8 @@
 val rat_2 = Rat.two;
 val rat_10 = Rat.rat_of_int 10;
 val rat_1_2 = rat_1 // rat_2;
-val max = curry IntInf.max;
-val min = curry IntInf.min;
+val max = curry Int.max;
+val min = curry Int.min;
 
 val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
 val numerator_rat = Rat.quotient_of_rat #> fst #> Rat.rat_of_int;
@@ -527,10 +520,10 @@
 fun rat_of_quotient (a,b) = if b = 0 then rat_0 else Rat.rat_of_quotient (a,b);
 fun rat_of_string s =
  let val n = index_char s #"/" 0 in
-  if n = ~1 then s |> IntInf.fromString |> valOf |> Rat.rat_of_int
+  if n = ~1 then s |> Int.fromString |> valOf |> Rat.rat_of_int
   else
-   let val SOME numer = IntInf.fromString(String.substring(s,0,n))
-       val SOME den = IntInf.fromString (String.substring(s,n+1,String.size s - n - 1))
+   let val SOME numer = Int.fromString(String.substring(s,0,n))
+       val SOME den = Int.fromString (String.substring(s,n+1,String.size s - n - 1))
    in rat_of_quotient(numer, den)
    end
  end;
@@ -1130,13 +1123,13 @@
   val raw_vec = if null pvs then vector_0 0
                 else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
   fun int_element (d,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
-  fun cterm_element (d,v) i = FuncUtil.Ctermfunc.tryapplyd v i rat_0
 
   fun find_rounding d =
    let
-    val _ = if !debugging
-          then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
-          else ()
+    val _ =
+      if !debugging
+      then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
+      else ()
     val vec = nice_vector d raw_vec
     val blockmat = iter (1,dim vec)
      (fn i => fn a => bmatrix_add (bmatrix_cmul (int_element vec i) (nth mats i)) a)
@@ -1179,7 +1172,8 @@
 (* Iterative deepening.                                                      *)
 
 fun deepen f n =
-  (writeln ("Searching with depth limit " ^ string_of_int n) ; (f n handle Failure s => (writeln ("failed with message: " ^ s) ; deepen f (n+1))))
+  (writeln ("Searching with depth limit " ^ string_of_int n);
+    (f n handle Failure s => (writeln ("failed with message: " ^ s); deepen f (n + 1))));
 
 
 (* Map back polynomials and their composites to a positivstellensatz.        *)
@@ -1430,11 +1424,13 @@
       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);
+     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 print_cert prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac print_cert prover ctxt
-
+fun sos_tac print_cert prover ctxt =
+  ObjectLogic.full_atomize_tac THEN'
+  elim_denom_tac ctxt THEN'
+  core_sos_tac print_cert prover ctxt;
 
 end;