7144

1 
(* Title: HOL/SVC_Oracle


2 
ID: $Id$


3 
Author: Lawrence C Paulson


4 
Copyright 1999 University of Cambridge


5 


6 
Installing the oracle for SVC (Stanford Validity Checker)


7 


8 
Based upon the work of Søren T. Heilmann


9 
*)


10 


11 
(*Present the entire subgoal to the oracle, assumptions and all, but possibly


12 
abstracted. Use via compose_tac, which performs no lifting but will


13 
instantiate variables.*)


14 
val svc_tac = SUBGOAL


15 
(fn (prem,i) =>


16 
let val (svc_prem, insts) = Svc.abstract prem


17 
val th = invoke_oracle thy "svc_oracle"


18 
(sign_of thy, Svc.OracleExn svc_prem)


19 


20 
in compose_tac (false, th, 0) i


21 
end handle Svc.OracleExn _ => no_tac);


22 


23 
