--- a/src/HOL/Tools/svc_funcs.ML Tue Aug 03 13:15:20 1999 +0200
+++ b/src/HOL/Tools/svc_funcs.ML Tue Aug 03 13:15:36 1999 +0200
@@ -6,15 +6,16 @@
Translation and abstraction functions for the interface to SVC
Based upon the work of Søren T. Heilmann
-*)
-(**TODO
- change Path.pack to File.sysify_path
- move realT to hologic.ML**)
+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.
-val realT = Type("RealDef.real",[]);
-
-
+For each variable of type nat, an assumption is added that it is non-negative.
+*)
structure Svc =
struct
@@ -84,8 +85,8 @@
val svc_output_file = File.tmp_path (Path.basic "SVM_out");
val _ = (File.write svc_input_file svc_input;
execute (check_valid ^ " -dump-result " ^
- Path.pack svc_output_file ^
- " " ^ Path.pack svc_input_file ^
+ File.sysify_path svc_output_file ^
+ " " ^ File.sysify_path svc_input_file ^
"> /dev/null 2>&1"))
val svc_output = File.read svc_output_file
handle _ => error "SVC returned no output"
@@ -97,160 +98,229 @@
(*New exception constructor for passing arguments to the oracle*)
exception OracleExn of term;
+ fun apply c args =
+ let val (ts, bs) = ListPair.unzip args
+ in (list_comb(c,ts), exists I bs) end;
+
+ fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
+
+ (*Determining whether the biconditionals must be unfoled: 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 (*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_expr("=>", [buildin_expr("<=", [int_expr 0,
+ uninterp_expr (a, [])]),
+ e]);
+
(*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 = rename_wrt_term t (Term.strip_all_vars t)
- and body = Term.strip_all_body t
- val parNames = rev (map #1 params)
- (*translation of a variable*)
- fun var (Free(a, _)) = uninterp_expr("F_" ^ a, [])
- | var (Var((a, 0), _)) = uninterp_expr(a, [])
- | var (Bound i) = uninterp_expr("B_" ^ List.nth (parNames,i), [])
- | var (t $ Bound _) = var t (*removing a parameter from a Var*)
- | var t = raise OracleExn t;
- (*translation of a literal*)
- fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
- | lit (Const("0", _)) = 0
- | lit (Const("0r", _)) = 0
- | lit (Const("1r", _)) = 1
- (*translation of a literal expression [no variables]*)
- fun litExp (Const("op +", T) $ x $ y) = (litExp x) + (litExp y)
- | litExp (Const("op -", T) $ x $ y) = (litExp x) - (litExp y)
- | litExp (Const("op *", T) $ x $ y) = (litExp x) * (litExp y)
- | litExp (Const("uminus", _) $ x) = ~(litExp x)
- | litExp t = lit t
- handle Match => raise OracleExn t
- (*translation of a real/rational expression*)
- fun suc t = interp_expr("+", [int_expr 1, t])
- fun tm (Const("Suc", T) $ x) = suc (tm x)
- | tm (Const("op +", T) $ x $ y) = interp_expr("+", [tm x, tm y])
- | tm (Const("op -", _) $ x $ y) =
- interp_expr("+", [tm x, interp_expr("*", [int_expr ~1, tm y])])
- | tm (Const("op *", _) $ x $ y) = interp_expr("*", [tm x, tm y])
- | tm (Const("op /", _) $ x $ y) =
- interp_expr("*", [tm x, rat_expr(1, litExp y)])
- | tm (Const("uminus", _) $ x) = interp_expr("*", [int_expr ~1, tm x])
- | tm t = int_expr (lit t)
- handle Match => var t
- (*translation of a formula*)
- and fm pos (Const("op &", _) $ p $ q) =
- buildin_expr("AND", [fm pos p, fm pos q])
- | fm pos (Const("op |", _) $ p $ q) =
- buildin_expr("OR", [fm pos p, fm pos q])
- | fm pos (Const("op -->", _) $ p $ q) =
- buildin_expr("=>", [fm (not pos) p, fm pos q])
- | fm pos (Const("Not", _) $ p) =
- buildin_expr("NOT", [fm (not pos) p])
- | fm pos (Const("True", _)) = true_expr
- | fm pos (Const("False", _)) = false_expr
- | fm pos (Const("op =", Type ("fun", [T,_])) $ x $ y) =
- if T = HOLogic.boolT then buildin_expr("=", [fm pos x, fm pos y])
- else
- let val tx = tm x and ty = tm y
- in if pos orelse T = realT then
- buildin_expr("=", [tx, ty])
- else
- buildin_expr("AND",
- [buildin_expr("<", [tx, suc ty]),
- buildin_expr("<", [ty, suc tx])])
- end
- (*inequalities: possible types are nat, int, real*)
- | fm pos (Const("op <", Type ("fun", [T,_])) $ x $ y) =
- if not pos orelse T = realT then
- buildin_expr("<", [tm x, tm y])
- else buildin_expr("<=", [suc (tm x), tm y])
- | fm pos (Const("op <=", Type ("fun", [T,_])) $ x $ y) =
- if pos orelse T = realT then
- buildin_expr("<=", [tm x, tm y])
- else buildin_expr("<", [tm x, suc (tm y)])
- | fm pos t = var t;
- (*entry point, and translation of a meta-formula*)
- fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos p
- | mt pos ((c as Const("==>", _)) $ p $ q) =
- buildin_expr("=>", [mt (not pos) p, mt pos q])
- | mt pos t = fm pos t (*it might be a formula*)
+ 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) =
+ (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
+ else ();
+ uninterp_expr (a, []))
+ fun var (Free(a,T)) = trans_var ("F_" ^ a, T)
+ | var (Var((a, 0), T)) = trans_var (a, T)
+ | var (Bound i) =
+ let val (a,T) = List.nth (params, i)
+ in trans_var ("B_" ^ a, T) end
+ | var (t $ Bound _) = var t (*removing a parameter from a Var*)
+ | var t = raise OracleExn t;
+ (*translation of a literal*)
+ fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
+ | lit (Const("0", _)) = 0
+ | lit (Const("RealDef.0r", _)) = 0
+ | lit (Const("RealDef.1r", _)) = 1
+ (*translation of a literal expression [no variables]*)
+ fun litExp (Const("op +", T) $ x $ y) = (litExp x) + (litExp y)
+ | litExp (Const("op -", T) $ x $ y) = (litExp x) - (litExp y)
+ | litExp (Const("op *", T) $ x $ y) = (litExp x) * (litExp y)
+ | litExp (Const("uminus", _) $ x) = ~(litExp x)
+ | litExp t = lit t
+ handle Match => raise OracleExn t
+ (*translation of a real/rational expression*)
+ fun suc t = interp_expr("+", [int_expr 1, t])
+ fun tm (Const("Suc", T) $ x) = suc (tm x)
+ | tm (Const("op +", T) $ x $ y) = interp_expr("+", [tm x, tm y])
+ | tm (Const("op -", _) $ x $ y) =
+ interp_expr("+", [tm x, interp_expr("*", [int_expr ~1, tm y])])
+ | tm (Const("op *", _) $ x $ y) = interp_expr("*", [tm x, tm y])
+ | tm (Const("op /", _) $ x $ y) =
+ interp_expr("*", [tm x, rat_expr(1, litExp y)])
+ | tm (Const("uminus", _) $ x) = interp_expr("*", [int_expr ~1, tm x])
+ | tm t = int_expr (lit t)
+ handle Match => var t
+ (*translation of a formula*)
+ and fm pos (Const("op &", _) $ p $ q) =
+ buildin_expr("AND", [fm pos p, fm pos q])
+ | fm pos (Const("op |", _) $ p $ q) =
+ buildin_expr("OR", [fm pos p, fm pos q])
+ | fm pos (Const("op -->", _) $ p $ q) =
+ buildin_expr("=>", [fm (not pos) p, fm pos q])
+ | fm pos (Const("Not", _) $ p) =
+ buildin_expr("NOT", [fm (not pos) p])
+ | fm pos (Const("True", _)) = true_expr
+ | fm pos (Const("False", _)) = false_expr
+ | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
+ (*polarity doesn't matter*)
+ buildin_expr("=", [fm pos p, fm pos q])
+ | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
+ buildin_expr("AND", (*unfolding uses both polarities*)
+ [buildin_expr("=>", [fm (not pos) p, fm pos q]),
+ buildin_expr("=>", [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_expr("=", [tx, ty])
+ else if is_intnat T then
+ buildin_expr("AND",
+ [buildin_expr("<", [tx, suc ty]),
+ buildin_expr("<", [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_expr("<", [tm x, tm y])
+ else if is_intnat T then
+ buildin_expr("<=", [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_expr("<=", [tm x, tm y])
+ else if is_intnat T then
+ buildin_expr("<", [tm x, suc (tm y)])
+ else raise OracleExn 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_expr("=>", [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
- mt pos body
+ foldr add_nat_var (!nat_vars, body_e)
end;
(*Generalize an Isabelle formula, replacing by Vars
- all subterms not intelligible to SVC. *)
+ all subterms not intelligible to SVC.
+ Do not present "raw" terms to expr_of; the translation could be unsound!*)
fun abstract t =
let
- val params = Term.strip_all_vars t
- and body = Term.strip_all_body t
- val Us = map #2 params
- val nPar = length params
- val vname = ref "V_a"
- val pairs = ref ([] : (term*term) list)
- fun insert t =
- let val T = fastype_of t
- val v = Unify.combound (Var ((!vname,0), Us--->T),
- 0, nPar)
- in vname := bump_string (!vname);
- pairs := (t, v) :: !pairs;
- v
- end;
- fun replace t =
- case t of
- Free _ => t (*but not existing Vars, lest the names clash*)
- | Bound _ => t
- | _ => (case gen_assoc (op aconv) (!pairs, t) of
- Some v => v
- | None => insert t)
- (*abstraction of a real/rational expression*)
- fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
- | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
- | rat ((c as Const("0r", _))) = c
- | rat ((c as Const("1r", _))) = c
- | rat (t as Const("Numeral.number_of", _) $ w) = t
- | rat t = replace t
- (*abstraction of an integer expression: no div, mod*)
- fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
- | int ((c as Const("uminus", _)) $ x) = c $ (int x)
- | int (t as Const("Numeral.number_of", _) $ w) = t
- | int t = replace t
- (*abstraction of a natural number expression: no minus*)
- fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
- | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
- | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
- | nat (t as Const("0", _)) = t
- | nat (t as Const("Numeral.number_of", _) $ w) = t
- | nat t = replace t
- (*abstraction of a relation: =, <, <=*)
- fun rel (T, c $ x $ y) =
- if T = realT then c $ (rat x) $ (rat y)
- else if T = HOLogic.intT then c $ (int x) $ (int y)
- else if T = HOLogic.natT then c $ (nat x) $ (nat y)
- else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
- else replace (c $ x $ y) (*non-numeric comparison*)
- (*abstraction of a formula*)
- and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
- | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
- | fm ((c as Const("True", _))) = c
- | fm ((c as Const("False", _))) = c
- | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
- | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
- | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
- | fm t = replace t
- (*entry point, and abstraction of a meta-formula*)
- fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
- | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
- | mt t = fm t (*it might be a formula*)
+ val params = Term.strip_all_vars t
+ and body = Term.strip_all_body t
+ val Us = map #2 params
+ val nPar = length params
+ val vname = ref "V_a"
+ val pairs = ref ([] : (term*term) list)
+ fun insert t =
+ let val T = fastype_of t
+ val v = Unify.combound (Var ((!vname,0), Us--->T),
+ 0, nPar)
+ in vname := bump_string (!vname);
+ pairs := (t, v) :: !pairs;
+ v
+ end;
+ fun replace t =
+ case t of
+ Free _ => t (*but not existing Vars, lest the names clash*)
+ | Bound _ => t
+ | _ => (case gen_assoc (op aconv) (!pairs, t) of
+ Some v => v
+ | None => insert t)
+ (*abstraction of a real/rational expression*)
+ fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
+ | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
+ | rat ((c as Const("RealDef.0r", _))) = c
+ | rat ((c as Const("RealDef.1r", _))) = c
+ | rat (t as Const("Numeral.number_of", _) $ w) = t
+ | rat t = replace t
+ (*abstraction of an integer expression: no div, mod*)
+ fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
+ | int ((c as Const("uminus", _)) $ x) = c $ (int x)
+ | int (t as Const("Numeral.number_of", _) $ w) = t
+ | int t = replace t
+ (*abstraction of a natural number expression: no minus*)
+ fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
+ | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
+ | nat (t as Const("0", _)) = t
+ | nat (t as Const("Numeral.number_of", _) $ w) = t
+ | nat t = replace t
+ (*abstraction of a relation: =, <, <=*)
+ fun rel (T, c $ x $ y) =
+ if T = HOLogic.realT then c $ (rat x) $ (rat y)
+ else if T = HOLogic.intT then c $ (int x) $ (int y)
+ else if T = HOLogic.natT then c $ (nat x) $ (nat y)
+ else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
+ else replace (c $ x $ y) (*non-numeric comparison*)
+ (*abstraction of a formula*)
+ and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
+ | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
+ | fm ((c as Const("True", _))) = c
+ | fm ((c as Const("False", _))) = c
+ | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+ | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+ | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+ | fm t = replace t
+ (*entry point, and abstraction of a meta-formula*)
+ fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
+ | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
+ | mt t = fm t (*it might be a formula*)
in (list_all (params, mt body), !pairs) end;
- fun oracle (sign, OracleExn svc_form) =
- if valid (expr_of false svc_form) then svc_form
- else raise OracleExn svc_form;
+ (*The oracle proves not the original formula but the abstracted version*)
+ fun oracle (sign, OracleExn P) =
+ let val (absP, _) = abstract P
+ val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^
+ Sign.string_of_term sign absP)
+ else ()
+ in
+ if valid (expr_of false absP) then absP
+ else raise OracleExn P
+ end;
end;