--- a/src/HOL/Tools/svc_funcs.ML Thu Aug 19 15:12:51 1999 +0200
+++ b/src/HOL/Tools/svc_funcs.ML Thu Aug 19 15:13:17 1999 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
-Translation and abstraction functions for the interface to SVC
+Translation functions for the interface to SVC
Based upon the work of Søren T. Heilmann
@@ -22,51 +22,37 @@
val trace = ref false;
datatype expr =
- bracketed_expr of expr
- | ref_def_expr of string * expr
- | ref_expr of string
- | typed_expr of Type * expr
- | buildin_expr of string * expr list
- | interp_expr of string * expr list
- | uninterp_expr of string * expr list
- | false_expr
- | true_expr
- | distinct_expr of string
- | int_expr of int
- | rat_expr of int * int
- and Type =
- simple_type of string
- | array_type of Type * Type
- | record_type of (expr * Type) list
- | bitvec_type of int;
+ Buildin of string * expr list
+ | Interp of string * expr list
+ | UnInterp of string * expr list
+ | FalseExpr
+ | TrueExpr
+ | Int of int
+ | Rat of int * int;
open BasisLibrary
+ fun signedInt i =
+ if i < 0 then "-" ^ Int.toString (~i)
+ else Int.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 signedInt i =
- if i < 0 then "-" ^ Int.toString (~i)
- else Int.toString i
- fun ut(simple_type s) = s ^ " "
- | ut(array_type(t1, t2)) = "ARRAY " ^ (ut t1) ^ (ut t2)
- | ut(record_type fl) =
- "RECORD" ^
- (foldl (fn (a, (d, t)) => a ^ (ue d) ^ (ut t)) (" ", fl))
- | ut(bitvec_type n) = "BITVEC " ^ (Int.toString n) ^ " "
- and ue(bracketed_expr e) = "(" ^ (ue e) ^ ") "
- | ue(ref_def_expr(r, e)) = "$" ^ r ^ ":" ^ (ue e)
- | ue(ref_expr r) = "$" ^ r ^ " "
- | ue(typed_expr(t, e)) = (ut t) ^ (ue e)
- | ue(buildin_expr(s, l)) =
+ let fun ue (Buildin(s, l)) =
"(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
- | ue(interp_expr(s, l)) =
+ | ue (Interp(s, l)) =
"{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
- | ue(uninterp_expr(s, l)) =
+ | ue (UnInterp(s, l)) =
"(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
- | ue(false_expr) = "FALSE "
- | ue(true_expr) = "TRUE "
- | ue(distinct_expr s) = "@" ^ s ^ " "
- | ue(int_expr i) = (signedInt i) ^ " "
- | ue(rat_expr(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
+ | ue (FalseExpr) = "FALSE "
+ | ue (TrueExpr) = "TRUE "
+ | ue (Int i) = (signedInt i) ^ " "
+ | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
in
ue t
end;
@@ -91,8 +77,8 @@
val svc_output = File.read svc_output_file
handle _ => error "SVC returned no output"
in
- if ! trace then writeln ("SVC Returns:\n" ^ svc_output) else ();
- if not (! trace) then (File.rm svc_input_file; File.rm svc_output_file) else ();
+ if ! trace then writeln ("SVC Returns:\n" ^ svc_output)
+ else (File.rm svc_input_file; File.rm svc_output_file);
String.isPrefix "VALID" svc_output
end
@@ -103,9 +89,7 @@
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
+ (*Determining whether the biconditionals must be unfolded: if there are
int or nat comparisons below*)
val iff_tag =
let fun tag t =
@@ -128,19 +112,17 @@
(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
b1 orelse b2)
end
- else (*numeric equality*) (t, is_intnat T)
+ 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_expr("=>", [buildin_expr("<=", [int_expr 0,
- uninterp_expr (a, [])]),
- e]);
+ Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
+ e]);
(*Translate an Isabelle formula into an SVC expression
pos ["positive"]: true if an assumption, false if a goal*)
@@ -153,7 +135,7 @@
fun trans_var (a,T) =
(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
else ();
- uninterp_expr (a, []))
+ UnInterp (a, []))
fun var (Free(a,T)) = trans_var ("F_" ^ a, T)
| var (Var((a, 0), T)) = trans_var (a, T)
| var (Bound i) =
@@ -167,70 +149,88 @@
| 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)
+ 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
+ handle Match => raise OracleExn t
(*translation of a real/rational expression*)
- fun suc t = interp_expr("+", [int_expr 1, t])
+ fun suc t = Interp("+", [Int 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)
+ | 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
(*translation of a formula*)
and fm pos (Const("op &", _) $ p $ q) =
- buildin_expr("AND", [fm pos p, fm pos q])
+ Buildin("AND", [fm pos p, fm pos q])
| fm pos (Const("op |", _) $ p $ q) =
- buildin_expr("OR", [fm pos p, fm pos q])
+ Buildin("OR", [fm pos p, fm pos q])
| fm pos (Const("op -->", _) $ p $ q) =
- buildin_expr("=>", [fm (not pos) p, fm pos q])
+ Buildin("=>", [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
+ 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_expr("=", [fm pos p, fm pos q])
+ Buildin("=", [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])])
+ 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_expr("=", [tx, ty])
+ Buildin("=", [tx, ty])
else if is_intnat T then
- buildin_expr("AND",
- [buildin_expr("<", [tx, suc ty]),
- buildin_expr("<", [ty, suc tx])])
+ 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_expr("<", [tm x, tm y])
+ Buildin("<", [tm x, tm y])
else if is_intnat T then
- buildin_expr("<=", [suc (tm x), tm y])
+ 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_expr("<=", [tm x, tm y])
+ Buildin("<=", [tm x, tm y])
else if is_intnat T then
- buildin_expr("<", [tm x, suc (tm y)])
+ Buildin("<", [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])
+ 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*)
@@ -239,89 +239,14 @@
end;
- (*Generalize an Isabelle formula, replacing by Vars
- 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("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;
-
- (*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)
+ (*The oracle proves the given formula t, if possible*)
+ fun oracle (sign, OracleExn t) =
+ let val dummy = if !trace then writeln ("Subgoal abstracted to\n" ^
+ Sign.string_of_term sign t)
else ()
in
- if valid (expr_of false absP) then absP
- else raise OracleExn P
+ if valid (expr_of false t) then t
+ else raise OracleExn t
end;
end;