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.*)

7162

14 
fun svc_tac i st =


15 
let val prem = List.nth (prems_of st, i1)


16 
val th = invoke_oracle thy "svc_oracle"


17 
(#sign (rep_thm st), Svc.OracleExn prem)


18 
in


19 
compose_tac (false, th, 0) i st


20 
end


21 
handle Svc.OracleExn _ => Seq.empty


22 
 Subscript => Seq.empty;

7144

23 


24 
