--- a/src/HOL/IsaMakefile Tue Feb 05 15:51:28 2002 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 05 23:18:08 2002 +0100
@@ -92,15 +92,13 @@
Option.ML Option.thy Power.ML Power.thy PreList.thy \
Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
- SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
- SetInterval.thy Sum_Type.ML Sum_Type.thy \
+ Set.ML Set.thy SetInterval.ML SetInterval.thy Sum_Type.ML Sum_Type.thy \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
Tools/datatype_rep_proofs.ML \
Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \
Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
- Tools/record_package.ML Tools/split_rule.ML \
- Tools/svc_funcs.ML Tools/typedef_package.ML \
+ Tools/record_package.ML Tools/split_rule.ML Tools/typedef_package.ML \
Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
@@ -553,10 +551,10 @@
ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
ex/NatSum.thy ex/PER.thy ex/Primrec.thy ex/Puzzle.ML ex/Puzzle.thy \
ex/Qsort.ML ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
- ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/Tarski.ML \
- ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML ex/mesontest2.ML \
- ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_test.ML ex/svc_test.thy \
- ex/document/root.bib ex/document/root.tex
+ ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
+ ex/Tarski.ML ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
+ ex/mesontest2.ML ex/mesontest2.thy ex/set.ML ex/set.thy ex/svc_funcs.ML \
+ ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
@$(ISATOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/PreList.thy Tue Feb 05 15:51:28 2002 +0100
+++ b/src/HOL/PreList.thy Tue Feb 05 23:18:08 2002 +0100
@@ -9,7 +9,7 @@
theory PreList =
Option + Wellfounded_Relations + NatSimprocs + Recdef + Record +
- Relation_Power + SVC_Oracle:
+ Relation_Power:
(*belongs to theory Divides*)
declare dvdI [intro?] dvdE [elim?] dvd_trans [trans]
--- a/src/HOL/SVC_Oracle.ML Tue Feb 05 15:51:28 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(* Title: HOL/SVC_Oracle.ML
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1999 University of Cambridge
-
-Installing the oracle for SVC (Stanford Validity Checker)
-
-The following code merely CALLS the oracle;
- the soundness-critical functions are at HOL/Tools/svc_funcs.ML
-
-Based upon the work of Søren T. Heilmann
-*)
-
-
-(*Generalize an Isabelle formula, replacing by Vars
- all subterms not intelligible to SVC.*)
-fun svc_abstract t =
- let
- (*The oracle's result is given to the subgoal using compose_tac because
- its premises are matched against the assumptions rather than used
- to make subgoals. Therefore , abstraction must copy the parameters
- precisely and make them available to all generated Vars.*)
- 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 Pattern.aeconv (!pairs, t) of
- Some v => v
- | None => insert t)
- (*abstraction of a numeric literal*)
- fun lit (t as Const("0", _)) = t
- | lit (t as Const("1", _)) = t
- | lit (t as Const("Numeral.number_of", _) $ w) = t
- | lit t = replace 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 t = lit 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 = lit 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 = lit 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,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("op <", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = 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;
-
-
-(*Present the entire subgoal to the oracle, assumptions and all, but possibly
- abstracted. Use via compose_tac, which performs no lifting but will
- instantiate variables.*)
-local val svc_thy = the_context () in
-
-fun svc_tac i st =
- let val prem = BasisLibrary.List.nth (prems_of st, i-1)
- val (absPrem, _) = svc_abstract prem
- val th = invoke_oracle svc_thy "svc_oracle"
- (#sign (rep_thm st), Svc.OracleExn absPrem)
- in
- compose_tac (false, th, 0) i st
- end
- handle Svc.OracleExn _ => Seq.empty
- | Subscript => Seq.empty;
-
-end;
-
-
-(*check if user has SVC installed*)
-fun svc_enabled () = getenv "SVC_HOME" <> "";
-fun if_svc_enabled f x = if svc_enabled () then f x else ();
--- a/src/HOL/SVC_Oracle.thy Tue Feb 05 15:51:28 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: HOL/SVC_Oracle.thy
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1999 University of Cambridge
-
-Installing the oracle for SVC (Stanford Validity Checker)
-
-Based upon the work of Søren T. Heilmann
-*)
-
-theory SVC_Oracle = NatBin (** + Real??**)
-files "Tools/svc_funcs.ML":
-
-consts
- (*reserved for the oracle*)
- iff_keep :: "[bool, bool] => bool"
- iff_unfold :: "[bool, bool] => bool"
-
-oracle
- svc_oracle = Svc.oracle
-
-end
--- a/src/HOL/Tools/svc_funcs.ML Tue Feb 05 15:51:28 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,260 +0,0 @@
-(* Title: HOL/Tools/svc_funcs.ML
- ID: $Id$
- 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 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 ue (Buildin(s, l)) =
- "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
- | ue (Interp(s, l)) =
- "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
- | ue (UnInterp(s, l)) =
- "(" ^ s ^ (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.sysify_path svc_output_file ^
- " " ^ File.sysify_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
-
- (*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;
-
- (*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,_) = raise OracleExn 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
- (*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,[])
- (*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 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 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 (!nat_vars, body_e)
- 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;
-
-end;
--- a/src/HOL/ex/ROOT.ML Tue Feb 05 15:51:28 2002 +0100
+++ b/src/HOL/ex/ROOT.ML Tue Feb 05 23:18:08 2002 +0100
@@ -35,4 +35,5 @@
time_use_thy "MT";
time_use_thy "Tarski";
+time_use_thy "SVC_Oracle";
if_svc_enabled time_use_thy "svc_test";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/SVC_Oracle.ML Tue Feb 05 23:18:08 2002 +0100
@@ -0,0 +1,113 @@
+(* Title: HOL/SVC_Oracle.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1999 University of Cambridge
+
+Installing the oracle for SVC (Stanford Validity Checker)
+
+The following code merely CALLS the oracle;
+ the soundness-critical functions are at HOL/Tools/svc_funcs.ML
+
+Based upon the work of Søren T. Heilmann
+*)
+
+
+(*Generalize an Isabelle formula, replacing by Vars
+ all subterms not intelligible to SVC.*)
+fun svc_abstract t =
+ let
+ (*The oracle's result is given to the subgoal using compose_tac because
+ its premises are matched against the assumptions rather than used
+ to make subgoals. Therefore , abstraction must copy the parameters
+ precisely and make them available to all generated Vars.*)
+ 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 Pattern.aeconv (!pairs, t) of
+ Some v => v
+ | None => insert t)
+ (*abstraction of a numeric literal*)
+ fun lit (t as Const("0", _)) = t
+ | lit (t as Const("1", _)) = t
+ | lit (t as Const("Numeral.number_of", _) $ w) = t
+ | lit t = replace 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 t = lit 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 = lit 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 = lit 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,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const("op <", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = 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;
+
+
+(*Present the entire subgoal to the oracle, assumptions and all, but possibly
+ abstracted. Use via compose_tac, which performs no lifting but will
+ instantiate variables.*)
+local val svc_thy = the_context () in
+
+fun svc_tac i st =
+ let val prem = BasisLibrary.List.nth (prems_of st, i-1)
+ val (absPrem, _) = svc_abstract prem
+ val th = invoke_oracle svc_thy "svc_oracle"
+ (#sign (rep_thm st), Svc.OracleExn absPrem)
+ in
+ compose_tac (false, th, 0) i st
+ end
+ handle Svc.OracleExn _ => Seq.empty
+ | Subscript => Seq.empty;
+
+end;
+
+
+(*check if user has SVC installed*)
+fun svc_enabled () = getenv "SVC_HOME" <> "";
+fun if_svc_enabled f x = if svc_enabled () then f x else ();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/SVC_Oracle.thy Tue Feb 05 23:18:08 2002 +0100
@@ -0,0 +1,22 @@
+(* Title: HOL/ex/SVC_Oracle.thy
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1999 University of Cambridge
+
+Installing the oracle for SVC (Stanford Validity Checker)
+
+Based upon the work of Søren T. Heilmann
+*)
+
+theory SVC_Oracle = Main (** + Real??**)
+files "svc_funcs.ML":
+
+consts
+ (*reserved for the oracle*)
+ iff_keep :: "[bool, bool] => bool"
+ iff_unfold :: "[bool, bool] => bool"
+
+oracle
+ svc_oracle = Svc.oracle
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/svc_funcs.ML Tue Feb 05 23:18:08 2002 +0100
@@ -0,0 +1,260 @@
+(* Title: HOL/Tools/svc_funcs.ML
+ ID: $Id$
+ 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 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 ue (Buildin(s, l)) =
+ "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+ | ue (Interp(s, l)) =
+ "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
+ | ue (UnInterp(s, l)) =
+ "(" ^ s ^ (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.sysify_path svc_output_file ^
+ " " ^ File.sysify_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
+
+ (*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;
+
+ (*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,_) = raise OracleExn 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
+ (*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,[])
+ (*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 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 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 (!nat_vars, body_e)
+ 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;
+
+end;