--- a/src/HOL/ex/svc_funcs.ML Thu Jul 14 19:28:17 2005 +0200
+++ b/src/HOL/ex/svc_funcs.ML Thu Jul 14 19:28:18 2005 +0200
@@ -25,55 +25,55 @@
Buildin of string * expr list
| Interp of string * expr list
| UnInterp of string * expr list
- | FalseExpr
+ | FalseExpr
| TrueExpr
| Int of IntInf.int
| Rat of IntInf.int * IntInf.int;
open BasisLibrary
- fun signedInt i =
+ 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) ^ " "
+ 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
+ ue t
end;
- fun valid e =
- let val svc_home = getenv "SVC_HOME"
+ 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"
+ 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"))
+ 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
@@ -84,8 +84,7 @@
String.isPrefix "VALID" svc_output
end
- (*New exception constructor for passing arguments to the oracle*)
- exception OracleExn of term;
+ fun fail t = raise TERM ("SVC oracle", [t]);
fun apply c args =
let val (ts, bs) = ListPair.unzip args
@@ -95,36 +94,36 @@
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
+ 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) =
+ fun add_nat_var (a, e) =
Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
- e]);
+ e]);
fun param_string [] = ""
| param_string is = "_" ^ space_implode "_" (map string_of_int is)
@@ -138,123 +137,119 @@
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 ();
+ (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) =
+ | var (Bound i, is) =
let val (a,T) = List.nth (params, i)
- in trans_var ("B_" ^ a, T, is) end
+ 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,_) = raise OracleExn t;
+ | 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 raise OracleExn t
- | litExp (Const("op -", T) $ x $ y) =
- if is_numeric_op T then (litExp x) - (litExp y)
- else raise OracleExn t
- | litExp (Const("op *", T) $ x $ y) =
- if is_numeric_op T then (litExp x) * (litExp y)
- else raise OracleExn t
- | litExp (Const("uminus", T) $ x) =
- if is_numeric_op T then ~(litExp x)
- else raise OracleExn t
- | litExp t = lit t
- handle Match => raise OracleExn t
+ 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 raise OracleExn t
- | tm (Const("op -", T) $ x $ y) =
- if is_numeric_op T then
- Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
- else raise OracleExn t
- | tm (Const("op *", T) $ x $ y) =
- if is_numeric_op T then Interp("*", [tm x, tm y])
- else raise OracleExn t
- | tm (Const("RealDef.rinv", T) $ x) =
- if domain_type T = HOLogic.realT then
- Rat(1, litExp x)
- else raise OracleExn t
- | tm (Const("uminus", T) $ x) =
- if is_numeric_op T then Interp("*", [Int ~1, tm x])
- else raise OracleExn t
- | tm t = Int (lit t)
- handle Match => var (t,[])
+ | 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])
+ 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 raise OracleExn 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 raise OracleExn 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 raise OracleExn t
+ | 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*)
+ | 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)
+ in
+ foldr add_nat_var body_e (!nat_vars)
end;
(*The oracle proves the given formula t, if possible*)
- fun oracle (sign, OracleExn t) =
- let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
- Sign.string_of_term sign t)
- else ()
- in
- if valid (expr_of false t) then t
- else raise OracleExn t
- end;
+ 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;