# HG changeset patch # User wenzelm # Date 1121362098 -7200 # Node ID 45a3dc4688bc1b85cebfa7af328afde818bb9bfe # Parent 2e7d7ec7a268d4bf049758c9a83cf41b116f9f55 improved oracle setup; diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/Integ/Presburger.thy --- a/src/HOL/Integ/Presburger.thy Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/Integ/Presburger.thy Thu Jul 14 19:28:18 2005 +0200 @@ -983,7 +983,7 @@ use "cooper_dec.ML" oracle - presburger_oracle = CooperDec.mk_presburger_oracle + presburger_oracle ("term") = CooperDec.presburger_oracle use "cooper_proof.ML" use "qelim.ML" diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/Integ/presburger.ML --- a/src/HOL/Integ/presburger.ML Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/Integ/presburger.ML Thu Jul 14 19:28:18 2005 +0200 @@ -28,12 +28,6 @@ (*-----------------------------------------------------------------*) -(* Invoking the oracle *) - -fun pres_oracle sg t = - invoke_oracle (theory "Presburger") "presburger_oracle" - (sg, CooperDec.COOPER_ORACLE t) ; - val presburger_ss = simpset_of (theory "Presburger"); fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = @@ -279,7 +273,7 @@ let val pth = (* If quick_and_dirty then run without proof generation as oracle*) if !quick_and_dirty - then pres_oracle sg (Pattern.eta_long [] t1) + then presburger_oracle sg (Pattern.eta_long [] t1) (* assume (cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/Presburger.thy Thu Jul 14 19:28:18 2005 +0200 @@ -983,7 +983,7 @@ use "cooper_dec.ML" oracle - presburger_oracle = CooperDec.mk_presburger_oracle + presburger_oracle ("term") = CooperDec.presburger_oracle use "cooper_proof.ML" use "qelim.ML" diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/Tools/Presburger/presburger.ML --- a/src/HOL/Tools/Presburger/presburger.ML Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/Tools/Presburger/presburger.ML Thu Jul 14 19:28:18 2005 +0200 @@ -28,12 +28,6 @@ (*-----------------------------------------------------------------*) -(* Invoking the oracle *) - -fun pres_oracle sg t = - invoke_oracle (theory "Presburger") "presburger_oracle" - (sg, CooperDec.COOPER_ORACLE t) ; - val presburger_ss = simpset_of (theory "Presburger"); fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = @@ -279,7 +273,7 @@ let val pth = (* If quick_and_dirty then run without proof generation as oracle*) if !quick_and_dirty - then pres_oracle sg (Pattern.eta_long [] t1) + then presburger_oracle sg (Pattern.eta_long [] t1) (* assume (cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(t1,CooperDec.integer_qelim (Pattern.eta_long [] t1))))) diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/ex/SVC_Oracle.ML --- a/src/HOL/ex/SVC_Oracle.ML Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/ex/SVC_Oracle.ML Thu Jul 14 19:28:18 2005 +0200 @@ -5,7 +5,7 @@ Installing the oracle for SVC (Stanford Validity Checker) -The following code merely CALLS the oracle; +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 @@ -26,21 +26,21 @@ val nPar = length params val vname = ref "V_a" val pairs = ref ([] : (term*term) list) - fun insert t = - let val T = fastype_of t + fun insert t = + let val T = fastype_of t val v = Unify.combound (Var ((!vname,0), Us--->T), - 0, nPar) - in vname := Symbol.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) + 0, nPar) + in vname := Symbol.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 @@ -66,11 +66,11 @@ | 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*) + 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) @@ -92,20 +92,13 @@ (*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; +fun svc_tac i st = + let + val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i) + val th = svc_oracle (Thm.theory_of_thm st) abs_goal + in compose_tac (false, th, 0) i end + handle TERM _ => no_tac; (*check if user has SVC installed*) diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/ex/SVC_Oracle.thy --- a/src/HOL/ex/SVC_Oracle.thy Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/ex/SVC_Oracle.thy Thu Jul 14 19:28:18 2005 +0200 @@ -8,15 +8,18 @@ Based upon the work of Søren T. Heilmann *) -theory SVC_Oracle imports Main (** + Real??**) -uses "svc_funcs.ML" begin +theory SVC_Oracle +imports Main +uses "svc_funcs.ML" +begin consts - (*reserved for the oracle*) iff_keep :: "[bool, bool] => bool" iff_unfold :: "[bool, bool] => bool" +hide const iff_keep iff_unfold + oracle - svc_oracle = Svc.oracle + svc_oracle ("term") = Svc.oracle end diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/ex/svc_funcs.ML --- 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;