src/HOL/SVC_Oracle.ML
author wenzelm
Tue, 17 Aug 1999 22:11:05 +0200
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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
     1
(*  Title:      HOL/SVC_Oracle.ML
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     5
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     6
Installing the oracle for SVC (Stanford Validity Checker)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     7
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     8
Based upon the work of Søren T. Heilmann
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
     9
*)
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    10
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    11
(*Present the entire subgoal to the oracle, assumptions and all, but possibly
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    12
  abstracted.  Use via compose_tac, which performs no lifting but will
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    13
  instantiate variables.*)
7237
2919daadba91 turned SVC_Oracle into a new-style 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 new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    15
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    16
fun svc_tac i st = 
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    17
  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    18
      val th = invoke_oracle svc_thy "svc_oracle"
7162
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    19
	             (#sign (rep_thm st), Svc.OracleExn prem)
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    20
   in 
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    21
      compose_tac (false, th, 0) i st
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    22
   end 
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    23
   handle Svc.OracleExn _ => Seq.empty
8737390d1d0a biconditionals and the natural numbers
paulson
parents: 7144
diff changeset
    24
	| Subscript       => Seq.empty;
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    25
7237
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    26
end;
2919daadba91 turned SVC_Oracle into a new-style theory in order to get automatic
wenzelm
parents: 7187
diff changeset
    27
7144
0feee8201d67 the SVC oracle theory
paulson
parents:
diff changeset
    28
7187
676027b1d770 svc_enabled is now declared as a function
paulson
parents: 7162
diff changeset
    29
(*True if SVC appears to exist*)
676027b1d770 svc_enabled is now declared as a function
paulson
parents: 7162
diff changeset
    30
fun svc_enabled() = getenv "SVC_HOME" <> "";