(* Title: HOL/Tools/svc_funcs.ML ID: $Id: svc_funcs.ML,v 1.9 2005/09/17 16:11:25 wenzelm Exp $ Author: Lawrence C Paulson Copyright 1999 University of Cambridge Translation functions for the interface to SVC Based upon the work of Søren T. Heilmann Integers and naturals are translated as follows: In a positive context, replace x<y by x+1<=y In a negative context, replace x<=y by x<y+1 In a negative context, replace x=y by x<y+1 & y<x+1 Biconditionals (if-and-only-iff) are expanded if they require such translations in either operand. For each variable of type nat, an assumption is added that it is non-negative. *) structure Svc = struct val trace = ref false; datatype expr = Buildin of string * expr list | Interp of string * expr list | UnInterp of string * expr list | FalseExpr | TrueExpr | Int of IntInf.int | Rat of IntInf.int * IntInf.int; fun signedInt i = if i < 0 then "-" ^ IntInf.toString (~i) else IntInf.toString i; fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT; fun is_numeric T = is_intnat T orelse T = HOLogic.realT; fun is_numeric_op T = is_numeric (domain_type T); fun toString t = let fun ue (Buildin(s, l)) = "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " | ue (Interp(s, l)) = "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} " | ue (UnInterp(s, l)) = "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " | ue (FalseExpr) = "FALSE " | ue (TrueExpr) = "TRUE " | ue (Int i) = (signedInt i) ^ " " | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " " in ue t end; fun valid e = let val svc_home = getenv "SVC_HOME" val svc_machine = getenv "SVC_MACHINE" val check_valid = if svc_home = "" then error "Environment variable SVC_HOME not set" else if svc_machine = "" then error "Environment variable SVC_MACHINE not set" else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid" val svc_input = toString e val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else () val svc_input_file = File.tmp_path (Path.basic "SVM_in"); val svc_output_file = File.tmp_path (Path.basic "SVM_out"); val _ = (File.write svc_input_file svc_input; execute (check_valid ^ " -dump-result " ^ File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^ ">/dev/null 2>&1")) val svc_output = (case Library.try File.read svc_output_file of SOME out => out | NONE => error "SVC returned no output"); in if ! trace then tracing ("SVC Returns:\n" ^ svc_output) else (File.rm svc_input_file; File.rm svc_output_file); String.isPrefix "VALID" svc_output end fun fail t = raise TERM ("SVC oracle", [t]); fun apply c args = let val (ts, bs) = ListPair.unzip args in (list_comb(c,ts), exists I bs) end; (*Determining whether the biconditionals must be unfolded: if there are int or nat comparisons below*) val iff_tag = let fun tag t = let val (c,ts) = strip_comb t in case c of Const("op &", _) => apply c (map tag ts) | Const("op |", _) => apply c (map tag ts) | Const("op -->", _) => apply c (map tag ts) | Const("Not", _) => apply c (map tag ts) | Const("True", _) => (c, false) | Const("False", _) => (c, false) | Const("op =", Type ("fun", [T,_])) => if T = HOLogic.boolT then (*biconditional: with int/nat comparisons below?*) let val [t1,t2] = ts val (u1,b1) = tag t1 and (u2,b2) = tag t2 val cname = if b1 orelse b2 then "unfold" else "keep" in (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2, b1 orelse b2) end else (*might be numeric equality*) (t, is_intnat T) | Const("op <", Type ("fun", [T,_])) => (t, is_intnat T) | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T) | _ => (t, false) end in #1 o tag end; (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*) fun add_nat_var (a, e) = Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]), e]); fun param_string [] = "" | param_string is = "_" ^ space_implode "_" (map string_of_int is) (*Translate an Isabelle formula into an SVC expression pos ["positive"]: true if an assumption, false if a goal*) fun expr_of pos t = let val params = rev (rename_wrt_term t (Term.strip_all_vars t)) and body = Term.strip_all_body t val nat_vars = ref ([] : string list) (*translation of a variable: record all natural numbers*) fun trans_var (a,T,is) = (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars)) else (); UnInterp (a ^ param_string is, [])) (*A variable, perhaps applied to a series of parameters*) fun var (Free(a,T), is) = trans_var ("F_" ^ a, T, is) | var (Var((a, 0), T), is) = trans_var (a, T, is) | var (Bound i, is) = let val (a,T) = List.nth (params, i) in trans_var ("B_" ^ a, T, is) end | var (t $ Bound i, is) = var(t,i::is) (*removing a parameter from a Var: the bound var index will become part of the Var's name*) | var (t,_) = fail t; (*translation of a literal*) fun lit (Const("Numeral.number_of", _) $ w) = (HOLogic.dest_binum w handle TERM _ => raise Match) | lit (Const("0", _)) = 0 | lit (Const("1", _)) = 1 (*translation of a literal expression [no variables]*) fun litExp (Const("op +", T) $ x $ y) = if is_numeric_op T then (litExp x) + (litExp y) else fail t | litExp (Const("op -", T) $ x $ y) = if is_numeric_op T then (litExp x) - (litExp y) else fail t | litExp (Const("op *", T) $ x $ y) = if is_numeric_op T then (litExp x) * (litExp y) else fail t | litExp (Const("uminus", T) $ x) = if is_numeric_op T then ~(litExp x) else fail t | litExp t = lit t handle Match => fail t (*translation of a real/rational expression*) fun suc t = Interp("+", [Int 1, t]) fun tm (Const("Suc", T) $ x) = suc (tm x) | tm (Const("op +", T) $ x $ y) = if is_numeric_op T then Interp("+", [tm x, tm y]) else fail t | tm (Const("op -", T) $ x $ y) = if is_numeric_op T then Interp("+", [tm x, Interp("*", [Int ~1, tm y])]) else fail t | tm (Const("op *", T) $ x $ y) = if is_numeric_op T then Interp("*", [tm x, tm y]) else fail t | tm (Const("RealDef.rinv", T) $ x) = if domain_type T = HOLogic.realT then Rat(1, litExp x) else fail t | tm (Const("uminus", T) $ x) = if is_numeric_op T then Interp("*", [Int ~1, tm x]) else fail t | tm t = Int (lit t) handle Match => var (t,[]) (*translation of a formula*) and fm pos (Const("op &", _) $ p $ q) = Buildin("AND", [fm pos p, fm pos q]) | fm pos (Const("op |", _) $ p $ q) = Buildin("OR", [fm pos p, fm pos q]) | fm pos (Const("op -->", _) $ p $ q) = Buildin("=>", [fm (not pos) p, fm pos q]) | fm pos (Const("Not", _) $ p) = Buildin("NOT", [fm (not pos) p]) | fm pos (Const("True", _)) = TrueExpr | fm pos (Const("False", _)) = FalseExpr | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = (*polarity doesn't matter*) Buildin("=", [fm pos p, fm pos q]) | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = Buildin("AND", (*unfolding uses both polarities*) [Buildin("=>", [fm (not pos) p, fm pos q]), Buildin("=>", [fm (not pos) q, fm pos p])]) | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = let val tx = tm x and ty = tm y in if pos orelse T = HOLogic.realT then Buildin("=", [tx, ty]) else if is_intnat T then Buildin("AND", [Buildin("<", [tx, suc ty]), Buildin("<", [ty, suc tx])]) else fail t end (*inequalities: possible types are nat, int, real*) | fm pos (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = if not pos orelse T = HOLogic.realT then Buildin("<", [tm x, tm y]) else if is_intnat T then Buildin("<=", [suc (tm x), tm y]) else fail t | fm pos (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = if pos orelse T = HOLogic.realT then Buildin("<=", [tm x, tm y]) else if is_intnat T then Buildin("<", [tm x, suc (tm y)]) else fail t | fm pos t = var(t,[]); (*entry point, and translation of a meta-formula*) fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p) | mt pos ((c as Const("==>", _)) $ p $ q) = Buildin("=>", [mt (not pos) p, mt pos q]) | mt pos t = fm pos (iff_tag t) (*it might be a formula*) val body_e = mt pos body (*evaluate now to assign into !nat_vars*) in foldr add_nat_var body_e (!nat_vars) end; (*The oracle proves the given formula t, if possible*) fun oracle thy t = (conditional (! trace) (fn () => tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t)); if valid (expr_of false t) then t else fail t); end;