# HG changeset patch # User wenzelm # Date 1012947488 -3600 # Node ID f362c0323d92e89c541cb58f74074b40f974ac2c # Parent cdf338ef5fadd7002d1ef438ce75db5f20e079e2 moved SVC stuff to ex; diff -r cdf338ef5fad -r f362c0323d92 src/HOL/IsaMakefile --- 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 diff -r cdf338ef5fad -r f362c0323d92 src/HOL/PreList.thy --- 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] diff -r cdf338ef5fad -r f362c0323d92 src/HOL/SVC_Oracle.ML --- 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 (); diff -r cdf338ef5fad -r f362c0323d92 src/HOL/SVC_Oracle.thy --- 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 diff -r cdf338ef5fad -r f362c0323d92 src/HOL/Tools/svc_funcs.ML --- 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 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; diff -r cdf338ef5fad -r f362c0323d92 src/HOL/ex/ROOT.ML --- 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"; diff -r cdf338ef5fad -r f362c0323d92 src/HOL/ex/SVC_Oracle.ML --- /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 (); diff -r cdf338ef5fad -r f362c0323d92 src/HOL/ex/SVC_Oracle.thy --- /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 diff -r cdf338ef5fad -r f362c0323d92 src/HOL/ex/svc_funcs.ML --- /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 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;