Functionality for sum of squares to call a remote csdp prover
authorPhilipp Meyer
Fri Jul 24 13:56:02 2009 +0200 (2009-07-24)
changeset 32268d50f0cb67578
parent 32166 95ffc6e2a0ea
child 32269 b642e4813e53
Functionality for sum of squares to call a remote csdp prover
CONTRIBUTORS
lib/scripts/neos/NeosCSDPClient.py
lib/scripts/neos/config.py
src/HOL/Library/Sum_Of_Squares.thy
src/HOL/Library/sos_wrapper.ML
src/HOL/Library/sum_of_squares.ML
     1.1 --- a/CONTRIBUTORS	Fri Jul 24 11:31:22 2009 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Jul 24 13:56:02 2009 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* July 2009: Philipp Meyer, TUM
     1.8 +  HOL/Library/Sum_of_Squares: functionality to call a remote csdp prover
     1.9 +
    1.10  * July 2009: Florian Haftmann, TUM
    1.11    New quickcheck implementation using new code generator
    1.12  
    1.13 @@ -19,6 +22,9 @@
    1.14  * June 2009: Florian Haftmann, TUM
    1.15    HOL/Library/Tree: searchtrees implementing mappings, ready to use for code generation
    1.16  
    1.17 +* March 2009: Philipp Meyer, TUM
    1.18 +  minimalization algorithm for results from sledgehammer call
    1.19 +
    1.20  Contributions to Isabelle2009
    1.21  -----------------------------
    1.22  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/scripts/neos/NeosCSDPClient.py	Fri Jul 24 13:56:02 2009 +0200
     2.3 @@ -0,0 +1,56 @@
     2.4 +#!/usr/bin/env python
     2.5 +import sys
     2.6 +import xmlrpclib
     2.7 +import time
     2.8 +import re
     2.9 +
    2.10 +from config import Variables
    2.11 +
    2.12 +if len(sys.argv) < 3 or len(sys.argv) > 3:
    2.13 +  sys.stderr.write("Usage: NeosCSDPClient <input_filename> <output_filename>\n")
    2.14 +  sys.exit(1)
    2.15 +
    2.16 +neos=xmlrpclib.Server("http://%s:%d" % (Variables.NEOS_HOST, Variables.NEOS_PORT))
    2.17 +
    2.18 +xmlfile = open(sys.argv[1],"r")
    2.19 +xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
    2.20 +xml_post = "]]></dat>\n</document>\n"
    2.21 +xml = xml_pre
    2.22 +buffer = 1
    2.23 +while buffer:
    2.24 +  buffer = xmlfile.read()
    2.25 +  xml += buffer
    2.26 +xmlfile.close()
    2.27 +xml += xml_post
    2.28 +
    2.29 +(jobNumber,password) = neos.submitJob(xml)
    2.30 +
    2.31 +if jobNumber == 0:
    2.32 +  sys.stdout.write("error submitting job: %s" % password)
    2.33 +  sys.exit(-1)
    2.34 +else:
    2.35 +  sys.stdout.write("jobNumber = %d\tpassword = %s\n" % (jobNumber,password))
    2.36 +
    2.37 +offset=0
    2.38 +status="Waiting"
    2.39 +while status == "Running" or status=="Waiting":
    2.40 +  time.sleep(1)
    2.41 +  (msg,offset) = neos.getIntermediateResults(jobNumber,password,offset)
    2.42 +  sys.stdout.write(msg.data)
    2.43 +  status = neos.getJobStatus(jobNumber, password)
    2.44 +
    2.45 +msg = neos.getFinalResults(jobNumber, password).data
    2.46 +result = msg.split("Solution:")
    2.47 +
    2.48 +sys.stdout.write(result[0])
    2.49 +if len(result) > 1:
    2.50 +  plain_msg = result[1].strip()
    2.51 +  if plain_msg != "":
    2.52 +    output = open(sys.argv[2],"w")
    2.53 +    output.write(plain_msg)
    2.54 +    output.close()
    2.55 +    sys.exit(0)
    2.56 +
    2.57 +sys.exit(2)
    2.58 +
    2.59 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/scripts/neos/config.py	Fri Jul 24 13:56:02 2009 +0200
     3.3 @@ -0,0 +1,3 @@
     3.4 +class Variables:
     3.5 +  NEOS_HOST="neos.mcs.anl.gov"
     3.6 +  NEOS_PORT=3332
     4.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Fri Jul 24 11:31:22 2009 +0200
     4.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Fri Jul 24 13:56:02 2009 +0200
     4.3 @@ -6,19 +6,22 @@
     4.4            multiplication and ordering using semidefinite programming*}
     4.5  theory Sum_Of_Squares
     4.6    imports Complex_Main (* "~~/src/HOL/Decision_Procs/Dense_Linear_Order" *)
     4.7 -  uses "positivstellensatz.ML" "sum_of_squares.ML"
     4.8 +  uses "positivstellensatz.ML" "sum_of_squares.ML" "sos_wrapper.ML"
     4.9    begin
    4.10  
    4.11  (* Note: 
    4.12  
    4.13 -In order to use the method sos, install CSDP (https://projects.coin-or.org/Csdp/) and put the executable csdp on your path. 
    4.14 +In order to use the method sos, call it with (sos remote_csdp) to use the remote solver
    4.15 +or install CSDP (https://projects.coin-or.org/Csdp/), put the executable csdp on your path,
    4.16 +and call it with (sos csdp)
    4.17  
    4.18  *)
    4.19  
    4.20 -method_setup sos = {* Scan.succeed (SIMPLE_METHOD' o Sos.sos_tac) *} 
    4.21 -  "Prove universal problems over the reals using sums of squares"
    4.22 +(* setup sos tactic *)
    4.23 +setup SosWrapper.setup
    4.24  
    4.25 -text{* Tests -- commented since they work only when csdp is installed -- see above *}
    4.26 +text{* Tests -- commented since they work only when csdp is installed  or take too long with remote csdps *}
    4.27 +
    4.28  (*
    4.29  lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
    4.30  
    4.31 @@ -115,3 +118,4 @@
    4.32  *)
    4.33  
    4.34  end
    4.35 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/sos_wrapper.ML	Fri Jul 24 13:56:02 2009 +0200
     5.3 @@ -0,0 +1,158 @@
     5.4 +(* Title:      sos_wrapper.ML
     5.5 +   Author:     Philipp Meyer, TU Muenchen
     5.6 +
     5.7 +Added functionality for sums of squares, e.g. calling a remote prover
     5.8 +*)
     5.9 +
    5.10 +signature SOS_WRAPPER =
    5.11 +sig
    5.12 +
    5.13 +  datatype prover_result = Success | PartialSuccess | Failure | Error
    5.14 +  type prover = string * (int -> string -> prover_result * string)
    5.15 +
    5.16 +  val setup: theory -> theory
    5.17 +end
    5.18 +
    5.19 +structure SosWrapper : SOS_WRAPPER=
    5.20 +struct
    5.21 +
    5.22 +datatype prover_result = Success | PartialSuccess | Failure | Error
    5.23 +type prover =
    5.24 +  string *                           (* command name *)
    5.25 +  (int -> string ->prover_result * string)   (* function to find failure from return value and output *)
    5.26 +
    5.27 +
    5.28 +(*** output control ***)
    5.29 +
    5.30 +fun debug s = Output.debug (fn () => s)
    5.31 +val answer = Output.priority
    5.32 +val write = Output.writeln
    5.33 +
    5.34 +(*** calling provers ***)
    5.35 +
    5.36 +val destdir = ref ""
    5.37 +
    5.38 +fun filename dir name =
    5.39 +  let
    5.40 +    val probfile = Path.basic (name ^ serial_string ())
    5.41 +  in
    5.42 +    if dir = "" then
    5.43 +      File.tmp_path probfile
    5.44 +    else
    5.45 +      if File.exists (Path.explode dir) then
    5.46 +        Path.append  (Path.explode dir) probfile
    5.47 +      else
    5.48 +        error ("No such directory: " ^ dir)
    5.49 +  end
    5.50 +
    5.51 +fun is_success Success = true
    5.52 +  | is_success PartialSuccess = true
    5.53 +  | is_success _ = false
    5.54 +fun str_of_status Success = "Success"
    5.55 +  | str_of_status PartialSuccess = "Partial Success"
    5.56 +  | str_of_status Failure= "Failure"
    5.57 +  | str_of_status Error= "Error"
    5.58 +
    5.59 +fun run_solver name (cmd, find_failure) input =
    5.60 +  let
    5.61 +    val _ = answer ("Calling solver: " ^ name)
    5.62 +
    5.63 +    (* create input file *)
    5.64 +    val dir = ! destdir
    5.65 +    val input_file = filename dir "sos_in" 
    5.66 +    val _ = File.write input_file input
    5.67 +
    5.68 +    val _ = debug "Solver input:"
    5.69 +    val _ = debug input
    5.70 +
    5.71 +    (* call solver *)
    5.72 +    val output_file = filename dir "sos_out"
    5.73 +    val (output, rv) = system_out (cmd ^ " " ^ (Path.implode input_file) ^
    5.74 +                         " " ^ (Path.implode output_file))
    5.75 + 
    5.76 +    (* read and analysize output *)
    5.77 +    val (res, res_msg) = find_failure rv output
    5.78 +    val result = if is_success res then File.read output_file else ""
    5.79 +
    5.80 +    (* remove temporary files *)
    5.81 +    val _ = if dir = "" then (File.rm input_file ; if File.exists output_file then File.rm output_file else ()) else ()
    5.82 +
    5.83 +    val _ = debug "Solver output:"
    5.84 +    val _ = debug output
    5.85 +    val _ = debug "Solver result:"
    5.86 +    val _ = debug result
    5.87 +
    5.88 +    val _ = answer (str_of_status res ^ ": " ^ res_msg)
    5.89 +
    5.90 +  in
    5.91 +    if is_success res then
    5.92 +      result
    5.93 +    else
    5.94 +      error ("Prover failed: " ^ res_msg)
    5.95 +  end
    5.96 +
    5.97 +(*** various provers ***)
    5.98 +
    5.99 +(* local csdp client *)
   5.100 +
   5.101 +fun find_csdp_run_failure rv _ =
   5.102 +  case rv of
   5.103 +    0 => (Success, "SDP solved")
   5.104 +  | 1 => (Failure, "SDP is primal infeasible")
   5.105 +  | 2 => (Failure, "SDP is dual infeasible")
   5.106 +  | 3 => (PartialSuccess, "SDP solved with reduced accuracy")
   5.107 +  | _ => (Failure, "return code is " ^ string_of_int rv)
   5.108 +
   5.109 +val csdp = ("csdp", find_csdp_run_failure)
   5.110 +
   5.111 +(* remote neos server *)
   5.112 +
   5.113 +fun find_neos_failure rv output =
   5.114 +  if rv = 2 then (Failure, "no solution") else
   5.115 +  if rv <> 0 then (Error, "return code is " ^ string_of_int rv) else
   5.116 +  let
   5.117 +    fun find_success str =
   5.118 +      if String.isPrefix "Success: " str then
   5.119 +        SOME (Success, unprefix "Success: " str)
   5.120 +      else if String.isPrefix "Partial Success: " str then
   5.121 +        SOME (PartialSuccess, unprefix "Partial Success: " str)
   5.122 +      else if String.isPrefix "Failure: " str then
   5.123 +        SOME (Failure, unprefix "Failure: " str)
   5.124 +      else
   5.125 +        NONE 
   5.126 +    val exit_line = get_first find_success (split_lines output)
   5.127 +  in
   5.128 +    case exit_line of
   5.129 +      SOME (status, msg) =>
   5.130 +        if String.isPrefix "SDP solved" msg then
   5.131 +          (status, msg)
   5.132 +        else (Failure, msg)
   5.133 +    | NONE => (Failure, "no success")
   5.134 +  end
   5.135 +
   5.136 +val neos_csdp = ("$ISABELLE_HOME/lib/scripts/neos/NeosCSDPClient.py", find_neos_failure)
   5.137 +
   5.138 +(* save provers in table *)
   5.139 +
   5.140 +val provers =
   5.141 +     Symtab.make [("remote_csdp", neos_csdp),("csdp", csdp)]
   5.142 +
   5.143 +fun get_prover name =
   5.144 +  case Symtab.lookup provers name of
   5.145 +    SOME prover => prover
   5.146 +  | NONE => error ("unknown prover: " ^ name)
   5.147 +
   5.148 +fun call_solver name =
   5.149 +    run_solver name (get_prover name)
   5.150 +
   5.151 +(* setup tactic *)
   5.152 +
   5.153 +val def_solver = "remote_csdp"
   5.154 +
   5.155 +fun sos_solver name = (SIMPLE_METHOD' o (Sos.sos_tac (call_solver name))) 
   5.156 +
   5.157 +val sos_method = Scan.optional (Scan.lift OuterParse.xname) def_solver >> sos_solver
   5.158 +
   5.159 +val setup = Method.setup @{binding sos} sos_method "Prove universal problems over the reals using sums of squares"
   5.160 +
   5.161 +end
     6.1 --- a/src/HOL/Library/sum_of_squares.ML	Fri Jul 24 11:31:22 2009 +0200
     6.2 +++ b/src/HOL/Library/sum_of_squares.ML	Fri Jul 24 13:56:02 2009 +0200
     6.3 @@ -1,6 +1,21 @@
     6.4 -structure Sos = 
     6.5 +(* Title:      sum_of_squares.ML
     6.6 +   Authors:    Amine Chaieb, University of Cambridge
     6.7 +               Philipp Meyer, TU Muenchen
     6.8 +
     6.9 +A tactic for proving nonlinear inequalities
    6.10 +*)
    6.11 +
    6.12 +signature SOS =
    6.13 +sig
    6.14 +
    6.15 +  val sos_tac : (string -> string) -> Proof.context -> int -> Tactical.tactic
    6.16 +
    6.17 +end
    6.18 +
    6.19 +structure Sos : SOS = 
    6.20  struct
    6.21  
    6.22 +
    6.23  val rat_0 = Rat.zero;
    6.24  val rat_1 = Rat.one;
    6.25  val rat_2 = Rat.two;
    6.26 @@ -500,11 +515,11 @@
    6.27  (*    Minimize obj_1 * v_1 + ... obj_m * v_m                                 *)
    6.28  (* ------------------------------------------------------------------------- *)
    6.29  
    6.30 -fun sdpa_of_problem comment obj mats =
    6.31 +fun sdpa_of_problem obj mats =
    6.32   let 
    6.33    val m = length mats - 1
    6.34    val (n,_) = dimensions (hd mats) 
    6.35 - in "\"" ^ comment ^ "\"\n" ^
    6.36 + in
    6.37    string_of_int m ^ "\n" ^
    6.38    "1\n" ^
    6.39    string_of_int n ^ "\n" ^
    6.40 @@ -587,6 +602,14 @@
    6.41   val parse_sdpaoutput = mkparser sdpaoutput
    6.42   val parse_csdpoutput = mkparser csdpoutput
    6.43  
    6.44 +(* Run prover on a problem in linear form.                       *)
    6.45 +
    6.46 +fun run_problem prover obj mats =
    6.47 +  parse_csdpoutput (prover (sdpa_of_problem obj mats))
    6.48 +
    6.49 +(*
    6.50 +UNUSED
    6.51 +
    6.52  (* Also parse the SDPA output to test success (CSDP yields a return code).   *)
    6.53  
    6.54  local
    6.55 @@ -687,6 +710,8 @@
    6.56     res)
    6.57   end;
    6.58  
    6.59 +*)
    6.60 +
    6.61  (* Try some apparently sensible scaling first. Note that this is purely to   *)
    6.62  (* get a cleaner translation to floating-point, and doesn't affect any of    *)
    6.63  (* the results, in principle. In practice it seems a lot better when there   *)
    6.64 @@ -761,6 +786,8 @@
    6.65     in if c =/ rat_0 then a 
    6.66        else Intfunc.update (i,y) a end) v Intfunc.undefined):vector
    6.67  
    6.68 +(*
    6.69 +UNUSED
    6.70  
    6.71  (* Reduce linear program to SDP (diagonal matrices) and test with CSDP. This *)
    6.72  (* one tests A [-1;x1;..;xn] >= 0 (i.e. left column is negated constants).   *)
    6.73 @@ -823,8 +850,12 @@
    6.74   end
    6.75  end;
    6.76  
    6.77 +*)
    6.78 +
    6.79  fun dest_ord f x = is_equal (f x);
    6.80  
    6.81 +
    6.82 +
    6.83  (* Stuff for "equations" ((int*int*int)->num functions).                         *)
    6.84  
    6.85  fun tri_equation_cmul c eq =
    6.86 @@ -1072,6 +1103,9 @@
    6.87  (* constant monomial is last; this gives an order in diagonalization of the  *)
    6.88  (* quadratic form that will tend to display constants.                       *)
    6.89  
    6.90 +(*
    6.91 +UNUSED
    6.92 +
    6.93  fun newton_polytope pol =
    6.94   let 
    6.95    val vars = poly_variables pol
    6.96 @@ -1086,6 +1120,8 @@
    6.97                          vars m monomial_1) (rev all')
    6.98   end;
    6.99  
   6.100 +*)
   6.101 +
   6.102  (* Diagonalize (Cholesky/LDU) the matrix corresponding to a quadratic form.  *)
   6.103  
   6.104  local
   6.105 @@ -1204,9 +1240,9 @@
   6.106  
   6.107  (* SDPA for problem using block diagonal (i.e. multiple SDPs)                *)
   6.108  
   6.109 -fun sdpa_of_blockproblem comment nblocks blocksizes obj mats =
   6.110 +fun sdpa_of_blockproblem nblocks blocksizes obj mats =
   6.111   let val m = length mats - 1 
   6.112 - in  "\"" ^ comment ^ "\"\n" ^
   6.113 + in
   6.114    string_of_int m ^ "\n" ^
   6.115    string_of_int nblocks ^ "\n" ^
   6.116    (fold1 (fn s => fn t => s^" "^t) (map string_of_int blocksizes)) ^
   6.117 @@ -1216,6 +1252,14 @@
   6.118      (1 upto length mats) mats ""
   6.119   end;
   6.120  
   6.121 +(* Run prover on a problem in block diagonal form.                       *)
   6.122 +
   6.123 +fun run_blockproblem prover nblocks blocksizes obj mats=
   6.124 +  parse_csdpoutput (prover (sdpa_of_blockproblem nblocks blocksizes obj mats))
   6.125 +
   6.126 +(*
   6.127 +UNUSED
   6.128 +
   6.129  (* Hence run CSDP on a problem in block diagonal form.                       *)
   6.130  
   6.131  fun run_csdp dbg nblocks blocksizes obj mats =
   6.132 @@ -1248,6 +1292,7 @@
   6.133       else ());
   6.134       res)
   6.135   end;
   6.136 +*)
   6.137  
   6.138  (* 3D versions of matrix operations to consider blocks separately.           *)
   6.139  
   6.140 @@ -1270,17 +1315,25 @@
   6.141   (blocksizes ~~ (1 upto length blocksizes));;
   6.142  
   6.143  (* FIXME : Get rid of this !!!*)
   6.144 +local
   6.145 +  fun tryfind_with msg f [] = error msg
   6.146 +    | tryfind_with msg f (x::xs) = (f x handle ERROR s => tryfind_with s f xs);
   6.147 +in 
   6.148 +  fun tryfind f = tryfind_with "tryfind" f
   6.149 +end
   6.150 +
   6.151 +(*
   6.152  fun tryfind f [] = error "tryfind"
   6.153    | tryfind f (x::xs) = (f x handle ERROR _ => tryfind f xs);
   6.154 -
   6.155 +*)
   6.156  
   6.157  (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
   6.158  
   6.159 -
   6.160 + 
   6.161  local
   6.162   open RealArith
   6.163  in
   6.164 -fun real_positivnullstellensatz_general linf d eqs leqs pol =
   6.165 +fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
   6.166  let 
   6.167   val vars = fold_rev (curry (gen_union (op aconvc)) o poly_variables) 
   6.168                (pol::eqs @ map fst leqs) []
   6.169 @@ -1344,7 +1397,7 @@
   6.170              itern 1 pvs (fn v => fn i => Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
   6.171                          Intfunc.undefined)
   6.172    val raw_vec = if null pvs then vector_0 0
   6.173 -                else tri_scale_then (csdp nblocks blocksizes) obj mats
   6.174 +                else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
   6.175    fun int_element (d,v) i = Intfunc.tryapplyd v i rat_0
   6.176    fun cterm_element (d,v) i = Ctermfunc.tryapplyd v i rat_0
   6.177  
   6.178 @@ -1464,7 +1517,7 @@
   6.179    fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
   6.180  in
   6.181    (* FIXME: Replace tryfind by get_first !! *)
   6.182 -fun real_nonlinear_prover ctxt =
   6.183 +fun real_nonlinear_prover prover ctxt =
   6.184   let 
   6.185    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
   6.186        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
   6.187 @@ -1502,7 +1555,7 @@
   6.188        let val e = multidegree pol
   6.189            val k = if e = 0 then 0 else d div e
   6.190            val eq' = map fst eq 
   6.191 -      in tryfind (fn i => (d,i,real_positivnullstellensatz_general false d eq' leq
   6.192 +      in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
   6.193                              (poly_neg(poly_pow pol i))))
   6.194                (0 upto k)
   6.195        end
   6.196 @@ -1563,7 +1616,7 @@
   6.197     end 
   6.198  in
   6.199  
   6.200 -fun real_nonlinear_subst_prover ctxt =
   6.201 +fun real_nonlinear_subst_prover prover ctxt =
   6.202   let 
   6.203    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
   6.204        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
   6.205 @@ -1596,7 +1649,7 @@
   6.206                                     aconvc @{cterm "0::real"}) (map modify eqs),
   6.207                                     map modify les,map modify lts)
   6.208         end)
   6.209 -       handle ERROR  _ => real_nonlinear_prover ctxt translator (rev eqs, rev les, rev lts))
   6.210 +       handle ERROR  _ => real_nonlinear_prover prover ctxt translator (rev eqs, rev les, rev lts))
   6.211      in substfirst
   6.212     end
   6.213  
   6.214 @@ -1606,7 +1659,7 @@
   6.215  
   6.216  (* Overall function. *)
   6.217  
   6.218 -fun real_sos ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover ctxt) t;
   6.219 +fun real_sos prover ctxt t = gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt) t;
   6.220  end;
   6.221  
   6.222  (* A tactic *)
   6.223 @@ -1618,7 +1671,7 @@
   6.224     end
   6.225  | _ => ([],ct)
   6.226  
   6.227 -fun core_sos_conv ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
   6.228 +fun core_sos_conv prover ctxt t = Drule.arg_cong_rule @{cterm Trueprop} (real_sos prover ctxt (Thm.dest_arg t) RS @{thm Eq_TrueI})
   6.229  
   6.230  val known_sos_constants = 
   6.231    [@{term "op ==>"}, @{term "Trueprop"}, 
   6.232 @@ -1654,10 +1707,10 @@
   6.233                else error ("SOSO: Unknown constants in Subgoal:" ^ commas (map fst ukcs))
   6.234  in () end
   6.235  
   6.236 -fun core_sos_tac ctxt = CSUBGOAL (fn (ct, i) => 
   6.237 +fun core_sos_tac prover ctxt = CSUBGOAL (fn (ct, i) => 
   6.238    let val _ = check_sos known_sos_constants ct
   6.239        val (avs, p) = strip_all ct
   6.240 -      val th = standard (fold_rev forall_intr avs (real_sos ctxt (Thm.dest_arg p)))
   6.241 +      val th = standard (fold_rev forall_intr avs (real_sos prover ctxt (Thm.dest_arg p)))
   6.242    in rtac th i end);
   6.243  
   6.244  fun default_SOME f NONE v = SOME v
   6.245 @@ -1695,7 +1748,7 @@
   6.246  
   6.247  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
   6.248  
   6.249 -fun sos_tac ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac ctxt
   6.250 +fun sos_tac prover ctxt = ObjectLogic.full_atomize_tac THEN' elim_denom_tac ctxt THEN' core_sos_tac prover ctxt
   6.251  
   6.252  
   6.253  end;