--- a/src/HOL/ex/svc_funcs.ML Mon Jun 01 15:06:09 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,255 +0,0 @@
-(* Title: HOL/ex/svc_funcs.ML
- Author: Lawrence C Paulson
- Copyright 1999 University of Cambridge
-
-Translation functions for the interface to SVC.
-
-Based upon the work of Soren 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.
-
-Relevant Isabelle environment settings:
-
- #SVC_HOME=
- #SVC_MACHINE=i386-redhat-linux
- #SVC_MACHINE=sparc-sun-solaris
-*)
-
-structure Svc =
-struct
- val trace = Unsynchronized.ref false;
-
- datatype expr =
- Buildin of string * expr list
- | Interp of string * expr list
- | UnInterp of string * expr list
- | FalseExpr
- | TrueExpr
- | Int of int
- | Rat of int * int;
-
- 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) = signed_string_of_int i ^ " "
- | ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int 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;
- val _ =
- Isabelle_System.bash_output (check_valid ^ " -dump-result " ^
- File.shell_path svc_output_file ^ " " ^ File.shell_path svc_input_file ^
- ">/dev/null 2>&1")
- val svc_output =
- (case 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(@{const_name HOL.conj}, _) => apply c (map tag ts)
- | Const(@{const_name HOL.disj}, _) => apply c (map tag ts)
- | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
- | Const(@{const_name Not}, _) => apply c (map tag ts)
- | Const(@{const_name True}, _) => (c, false)
- | Const(@{const_name False}, _) => (c, false)
- | Const(@{const_name HOL.eq}, 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(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T)
- | Const(@{const_name Orderings.less_eq}, 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 (Term.rename_wrt_term t (Term.strip_all_vars t))
- and body = Term.strip_all_body t
- val nat_vars = Unsynchronized.ref ([] : string list)
- (*translation of a variable: record all natural numbers*)
- fun trans_var (a,T,is) =
- (if T = HOLogic.natT then nat_vars := (insert (op =) a (!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) = 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*)
- val lit = snd o HOLogic.dest_number;
- (*translation of a literal expression [no variables]*)
- fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) =
- if is_numeric_op T then (litExp x) + (litExp y)
- else fail t
- | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) =
- if is_numeric_op T then (litExp x) - (litExp y)
- else fail t
- | litExp (Const(@{const_name Groups.times}, T) $ x $ y) =
- if is_numeric_op T then (litExp x) * (litExp y)
- else fail t
- | litExp (Const(@{const_name Groups.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(@{const_name Suc}, T) $ x) = suc (tm x)
- | tm (Const(@{const_name Groups.plus}, T) $ x $ y) =
- if is_numeric_op T then Interp("+", [tm x, tm y])
- else fail t
- | tm (Const(@{const_name Groups.minus}, T) $ x $ y) =
- if is_numeric_op T then
- Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
- else fail t
- | tm (Const(@{const_name Groups.times}, T) $ x $ y) =
- if is_numeric_op T then Interp("*", [tm x, tm y])
- else fail t
- | tm (Const(@{const_name Fields.inverse}, T) $ x) =
- if domain_type T = HOLogic.realT then
- Rat(1, litExp x)
- else fail t
- | tm (Const(@{const_name Groups.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(@{const_name HOL.conj}, _) $ p $ q) =
- Buildin("AND", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name HOL.disj}, _) $ p $ q) =
- Buildin("OR", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name HOL.implies}, _) $ p $ q) =
- Buildin("=>", [fm (not pos) p, fm pos q])
- | fm pos (Const(@{const_name Not}, _) $ p) =
- Buildin("NOT", [fm (not pos) p])
- | fm pos (Const(@{const_name True}, _)) = TrueExpr
- | fm pos (Const(@{const_name False}, _)) = FalseExpr
- | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
- (*polarity doesn't matter*)
- Buildin("=", [fm pos p, fm pos q])
- | fm pos (Const(@{const_name 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(@{const_name HOL.eq}, 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(@{const_name Orderings.less}, 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(@{const_name Orderings.less_eq}, 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(@{const_name Trueprop}, _)) $ p) = fm pos (iff_tag p)
- | mt pos ((c as Const(@{const_name Pure.imp}, _)) $ 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
- fold_rev add_nat_var (!nat_vars) body_e
- end;
-
-
- (*The oracle proves the given formula, if possible*)
- fun oracle ct =
- let
- val thy = Thm.theory_of_cterm ct;
- val t = Thm.term_of ct;
- val _ =
- if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
- else ();
- in if valid (expr_of false t) then ct else fail t end;
-
-end;