author  wenzelm 
Tue, 17 Aug 1999 22:11:05 +0200  
changeset 7237  2919daadba91 
parent 7187  676027b1d770 
child 7284  29105299799c 
permissions  rwrr 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

1 
(* Title: HOL/SVC_Oracle.ML 
7144  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.*) 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

14 
local val svc_thy = the_context () in 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

15 

7162  16 
fun svc_tac i st = 
7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

17 
let val prem = BasisLibrary.List.nth (prems_of st, i1) 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

18 
val th = invoke_oracle svc_thy "svc_oracle" 
7162  19 
(#sign (rep_thm st), Svc.OracleExn prem) 
20 
in 

21 
compose_tac (false, th, 0) i st 

22 
end 

23 
handle Svc.OracleExn _ => Seq.empty 

24 
 Subscript => Seq.empty; 

7144  25 

7237
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

26 
end; 
2919daadba91
turned SVC_Oracle into a newstyle theory in order to get automatic
wenzelm
parents:
7187
diff
changeset

27 

7144  28 

7187  29 
(*True if SVC appears to exist*) 
30 
fun svc_enabled() = getenv "SVC_HOME" <> ""; 