src/HOL/ex/svc_funcs.ML
changeset 12869 f362c0323d92
child 14982 ff1c919f4982
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/svc_funcs.ML	Tue Feb 05 23:18:08 2002 +0100
     1.3 @@ -0,0 +1,260 @@
     1.4 +(*  Title:      HOL/Tools/svc_funcs.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Translation functions for the interface to SVC
    1.10 +
    1.11 +Based upon the work of Søren T. Heilmann
    1.12 +
    1.13 +Integers and naturals are translated as follows:
    1.14 +  In a positive context, replace x<y by x+1<=y
    1.15 +  In a negative context, replace x<=y by x<y+1
    1.16 +  In a negative context, replace x=y by x<y+1 & y<x+1
    1.17 +Biconditionals (if-and-only-iff) are expanded if they require such translations
    1.18 +  in either operand.
    1.19 +
    1.20 +For each variable of type nat, an assumption is added that it is non-negative.
    1.21 +*)
    1.22 +
    1.23 +structure Svc =
    1.24 +struct
    1.25 + val trace = ref false;
    1.26 +
    1.27 + datatype expr =
    1.28 +     Buildin of string * expr list
    1.29 +   | Interp of string * expr list
    1.30 +   | UnInterp of string * expr list
    1.31 +   | FalseExpr 
    1.32 +   | TrueExpr
    1.33 +   | Int of int
    1.34 +   | Rat of int * int;
    1.35 +
    1.36 + open BasisLibrary
    1.37 +
    1.38 + fun signedInt i = 
    1.39 +     if i < 0 then "-" ^ Int.toString (~i)
    1.40 +     else Int.toString i;
    1.41 +	 
    1.42 + fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    1.43 + 
    1.44 + fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    1.45 + 
    1.46 + fun is_numeric_op T = is_numeric (domain_type T);
    1.47 +
    1.48 + fun toString t =
    1.49 +     let fun ue (Buildin(s, l)) = 
    1.50 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.51 +	   | ue (Interp(s, l)) = 
    1.52 +	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.53 +	   | ue (UnInterp(s, l)) = 
    1.54 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.55 +	   | ue (FalseExpr) = "FALSE "
    1.56 +	   | ue (TrueExpr)  = "TRUE "
    1.57 +	   | ue (Int i)     = (signedInt i) ^ " "
    1.58 +	   | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    1.59 +     in
    1.60 +	 ue t
    1.61 +     end;
    1.62 +
    1.63 + fun valid e = 
    1.64 +  let val svc_home = getenv "SVC_HOME" 
    1.65 +      val svc_machine = getenv "SVC_MACHINE"
    1.66 +      val check_valid = if svc_home = ""
    1.67 +	                then error "Environment variable SVC_HOME not set"
    1.68 +			else if svc_machine = ""
    1.69 +	                then error "Environment variable SVC_MACHINE not set"
    1.70 +			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    1.71 +      val svc_input = toString e
    1.72 +      val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    1.73 +      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    1.74 +      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    1.75 +      val _ = (File.write svc_input_file svc_input;
    1.76 +	       execute (check_valid ^ " -dump-result " ^ 
    1.77 +			File.sysify_path svc_output_file ^
    1.78 +			" " ^ File.sysify_path svc_input_file ^ 
    1.79 +			"> /dev/null 2>&1"))
    1.80 +      val svc_output =
    1.81 +        (case Library.try File.read svc_output_file of
    1.82 +          Some out => out
    1.83 +        | None => error "SVC returned no output");
    1.84 +  in
    1.85 +      if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    1.86 +      else (File.rm svc_input_file; File.rm svc_output_file);
    1.87 +      String.isPrefix "VALID" svc_output
    1.88 +  end
    1.89 +
    1.90 + (*New exception constructor for passing arguments to the oracle*)
    1.91 + exception OracleExn of term;
    1.92 +
    1.93 + fun apply c args =
    1.94 +     let val (ts, bs) = ListPair.unzip args
    1.95 +     in  (list_comb(c,ts), exists I bs)  end;
    1.96 +
    1.97 + (*Determining whether the biconditionals must be unfolded: if there are
    1.98 +   int or nat comparisons below*)
    1.99 + val iff_tag =
   1.100 +   let fun tag t =
   1.101 +	 let val (c,ts) = strip_comb t
   1.102 +	 in  case c of
   1.103 +	     Const("op &", _)   => apply c (map tag ts)
   1.104 +	   | Const("op |", _)   => apply c (map tag ts)
   1.105 +	   | Const("op -->", _) => apply c (map tag ts)
   1.106 +	   | Const("Not", _)    => apply c (map tag ts)
   1.107 +	   | Const("True", _)   => (c, false)
   1.108 +	   | Const("False", _)  => (c, false)
   1.109 +	   | Const("op =", Type ("fun", [T,_])) => 
   1.110 +		 if T = HOLogic.boolT then
   1.111 +		     (*biconditional: with int/nat comparisons below?*)
   1.112 +		     let val [t1,t2] = ts
   1.113 +			 val (u1,b1) = tag t1
   1.114 +			 and (u2,b2) = tag t2
   1.115 +			 val cname = if b1 orelse b2 then "unfold" else "keep"
   1.116 +		     in 
   1.117 +			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   1.118 +			 b1 orelse b2)
   1.119 +		     end
   1.120 +		 else (*might be numeric equality*) (t, is_intnat T)
   1.121 +	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   1.122 +	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   1.123 +	   | _ => (t, false)
   1.124 +	 end
   1.125 +   in #1 o tag end;
   1.126 +
   1.127 + (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   1.128 + fun add_nat_var (a, e) = 
   1.129 +     Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   1.130 +		    e]);
   1.131 +
   1.132 + fun param_string [] = ""
   1.133 +   | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   1.134 +
   1.135 + (*Translate an Isabelle formula into an SVC expression
   1.136 +   pos ["positive"]: true if an assumption, false if a goal*)
   1.137 + fun expr_of pos t =
   1.138 +  let
   1.139 +    val params = rev (rename_wrt_term t (Term.strip_all_vars t))
   1.140 +    and body   = Term.strip_all_body t
   1.141 +    val nat_vars = ref ([] : string list)
   1.142 +    (*translation of a variable: record all natural numbers*)
   1.143 +    fun trans_var (a,T,is) =
   1.144 +	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   1.145 +	                     else ();
   1.146 +         UnInterp (a ^ param_string is, []))
   1.147 +    (*A variable, perhaps applied to a series of parameters*)
   1.148 +    fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   1.149 +      | var (Var((a, 0), T), is) = trans_var (a, T, is)
   1.150 +      | var (Bound i, is)        = 
   1.151 +          let val (a,T) = List.nth (params, i)
   1.152 +	  in  trans_var ("B_" ^ a, T, is)  end
   1.153 +      | var (t $ Bound i, is)    = var(t,i::is)
   1.154 +            (*removing a parameter from a Var: the bound var index will
   1.155 +               become part of the Var's name*)
   1.156 +      | var (t,_) = raise OracleExn t;
   1.157 +    (*translation of a literal*)
   1.158 +    fun lit (Const("Numeral.number_of", _) $ w) =
   1.159 +          (HOLogic.dest_binum w handle TERM _ => raise Match)
   1.160 +      | lit (Const("0", _)) = 0
   1.161 +      | lit (Const("1", _)) = 1
   1.162 +    (*translation of a literal expression [no variables]*)
   1.163 +    fun litExp (Const("op +", T) $ x $ y) = 
   1.164 +	  if is_numeric_op T then (litExp x) + (litExp y)
   1.165 +          else raise OracleExn t
   1.166 +      | litExp (Const("op -", T) $ x $ y) = 
   1.167 +	  if is_numeric_op T then (litExp x) - (litExp y)
   1.168 +          else raise OracleExn t
   1.169 +      | litExp (Const("op *", T) $ x $ y) = 
   1.170 +	  if is_numeric_op T then (litExp x) * (litExp y)
   1.171 +          else raise OracleExn t
   1.172 +      | litExp (Const("uminus", T) $ x)   = 
   1.173 +	  if is_numeric_op T then ~(litExp x)
   1.174 +          else raise OracleExn t
   1.175 +      | litExp t = lit t 
   1.176 +		   handle Match => raise OracleExn t
   1.177 +    (*translation of a real/rational expression*)
   1.178 +    fun suc t = Interp("+", [Int 1, t])
   1.179 +    fun tm (Const("Suc", T) $ x) = suc (tm x)
   1.180 +      | tm (Const("op +", T) $ x $ y) = 
   1.181 +	  if is_numeric_op T then Interp("+", [tm x, tm y])
   1.182 +          else raise OracleExn t
   1.183 +      | tm (Const("op -", T) $ x $ y) = 
   1.184 +	  if is_numeric_op T then 
   1.185 +	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   1.186 +          else raise OracleExn t
   1.187 +      | tm (Const("op *", T) $ x $ y) = 
   1.188 +	  if is_numeric_op T then Interp("*", [tm x, tm y])
   1.189 +          else raise OracleExn t
   1.190 +      | tm (Const("RealDef.rinv", T) $ x) = 
   1.191 +	  if domain_type T = HOLogic.realT then 
   1.192 +	      Rat(1, litExp x)
   1.193 +          else raise OracleExn t
   1.194 +      | tm (Const("uminus", T) $ x) = 
   1.195 +	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   1.196 +          else raise OracleExn t
   1.197 +      | tm t = Int (lit t) 
   1.198 +	       handle Match => var (t,[])
   1.199 +    (*translation of a formula*)
   1.200 +    and fm pos (Const("op &", _) $ p $ q) =  
   1.201 +	    Buildin("AND", [fm pos p, fm pos q])
   1.202 +      | fm pos (Const("op |", _) $ p $ q) =  
   1.203 +	    Buildin("OR", [fm pos p, fm pos q])
   1.204 +      | fm pos (Const("op -->", _) $ p $ q) =  
   1.205 +	    Buildin("=>", [fm (not pos) p, fm pos q])
   1.206 +      | fm pos (Const("Not", _) $ p) =  
   1.207 +	    Buildin("NOT", [fm (not pos) p])
   1.208 +      | fm pos (Const("True", _)) = TrueExpr
   1.209 +      | fm pos (Const("False", _)) = FalseExpr
   1.210 +      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   1.211 +	     (*polarity doesn't matter*)
   1.212 +	    Buildin("=", [fm pos p, fm pos q]) 
   1.213 +      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   1.214 +	    Buildin("AND",   (*unfolding uses both polarities*)
   1.215 +			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   1.216 +			  Buildin("=>", [fm (not pos) q, fm pos p])])
   1.217 +      | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   1.218 +	    let val tx = tm x and ty = tm y
   1.219 +		in if pos orelse T = HOLogic.realT then
   1.220 +		       Buildin("=", [tx, ty])
   1.221 +		   else if is_intnat T then
   1.222 +		       Buildin("AND", 
   1.223 +				    [Buildin("<", [tx, suc ty]), 
   1.224 +				     Buildin("<", [ty, suc tx])])
   1.225 +		   else raise OracleExn t
   1.226 +	    end
   1.227 +	(*inequalities: possible types are nat, int, real*)
   1.228 +      | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   1.229 +	    if not pos orelse T = HOLogic.realT then
   1.230 +		Buildin("<", [tm x, tm y])
   1.231 +	    else if is_intnat T then
   1.232 +		Buildin("<=", [suc (tm x), tm y])
   1.233 +	    else raise OracleExn t
   1.234 +      | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   1.235 +	    if pos orelse T = HOLogic.realT then
   1.236 +		Buildin("<=", [tm x, tm y])
   1.237 +	    else if is_intnat T then
   1.238 +		Buildin("<", [tm x, suc (tm y)])
   1.239 +	    else raise OracleExn t
   1.240 +      | fm pos t = var(t,[]);
   1.241 +      (*entry point, and translation of a meta-formula*)
   1.242 +      fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   1.243 +	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   1.244 +	    Buildin("=>", [mt (not pos) p, mt pos q])
   1.245 +	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   1.246 +
   1.247 +      val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   1.248 +  in 
   1.249 +     foldr add_nat_var (!nat_vars, body_e) 
   1.250 +  end;
   1.251 +
   1.252 +
   1.253 + (*The oracle proves the given formula t, if possible*)
   1.254 + fun oracle (sign, OracleExn t) = 
   1.255 +   let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   1.256 +					   Sign.string_of_term sign t)
   1.257 +                   else ()
   1.258 +   in
   1.259 +       if valid (expr_of false t) then t
   1.260 +       else raise OracleExn t
   1.261 +   end;
   1.262 +
   1.263 +end;