src/HOL/SVC_Oracle.ML
author wenzelm
Tue Aug 17 22:11:05 1999 +0200 (1999-08-17)
changeset 7237 2919daadba91
parent 7187 676027b1d770
child 7284 29105299799c
permissions -rw-r--r--
turned SVC_Oracle into a new-style theory in order to get automatic
handling of its additional dependency on Tools/svc_funcs.ML;
wenzelm@7237
     1
(*  Title:      HOL/SVC_Oracle.ML
paulson@7144
     2
    ID:         $Id$
paulson@7144
     3
    Author:     Lawrence C Paulson
paulson@7144
     4
    Copyright   1999  University of Cambridge
paulson@7144
     5
paulson@7144
     6
Installing the oracle for SVC (Stanford Validity Checker)
paulson@7144
     7
paulson@7144
     8
Based upon the work of Søren T. Heilmann
paulson@7144
     9
*)
paulson@7144
    10
paulson@7144
    11
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
paulson@7144
    12
  abstracted.  Use via compose_tac, which performs no lifting but will
paulson@7144
    13
  instantiate variables.*)
wenzelm@7237
    14
local val svc_thy = the_context () in
wenzelm@7237
    15
paulson@7162
    16
fun svc_tac i st = 
wenzelm@7237
    17
  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
wenzelm@7237
    18
      val th = invoke_oracle svc_thy "svc_oracle"
paulson@7162
    19
	             (#sign (rep_thm st), Svc.OracleExn prem)
paulson@7162
    20
   in 
paulson@7162
    21
      compose_tac (false, th, 0) i st
paulson@7162
    22
   end 
paulson@7162
    23
   handle Svc.OracleExn _ => Seq.empty
paulson@7162
    24
	| Subscript       => Seq.empty;
paulson@7144
    25
wenzelm@7237
    26
end;
wenzelm@7237
    27
paulson@7144
    28
paulson@7187
    29
(*True if SVC appears to exist*)
paulson@7187
    30
fun svc_enabled() = getenv "SVC_HOME" <> "";